Arrow logic and infinite counting (Q1582310)

Arrow logic is a propositional modal logic with three modal operators, dyadic, monadic, and constant, which correspond, respectively, to composition, inverse, and identity of arrows. It is a broadly applicable modal formalism covering various areas from dynamic semantics of natural language to transition systems in computer science. The weakly associative arrow logic, one of the fundamental ones among them, has been proved to be finitely axiomatizable by Maddux and decidable by Nemeti. It is also known by Andreka, Hodkinson and Nemeti that weakly associative relational algebras, which constitute the algebraic counterparts of the logic, have the finite base property. In this paper, the author introduces to the logic various kinds of additional modalities modeling infinite counting features of natural language such as ``much more'', ``of good quantity'', and ``many times'', and proves that the logics thus enriched are also finitely axiomatizable and decidable. The finite axiomatizability results are consequences of (in fact, equivalent to) the finite base property of weakly associative relational algebras. Nevertheless, interestingly enough, it is also shown that their algebras do not enjoy the property.