The finitely axiomatizable complete theories of non-associative arrow frames (Q1731561)

The paper studies the non-associative arrow logic NAL. One of the important notions used for studying NAL is a notion of normal forms. Let \(F_k(X)\) denote a set of normal forms of degree \(k\) in variable from \(X\). Then the following holds: There is an algorithm that, given a formula \(\varphi\), a set of propositional variables \(X \supseteq \mathrm{var}(\phi)\) and a finite ordinal \(k\) bigger than or equal to the maximum depth of modal operators nesting in \(\phi\), generates a finite set \(\Sigma \subseteq F_k(X)\) such that \(\vDash \varphi \leftrightarrow \bigvee\Sigma\). A game theory semantic of NAL has been intensively studied. Using it, an alternative proof [\textit{I. Németi}, Proc. Am. Math. Soc. 100, 340--344 (1987; Zbl 0638.03061)] of the following result is presented: NAL has the finite model property and it is decidable. In addition, the descriptions of all finitely axiomatizable, all complete and all consistent theories of NAL are given. A negative answer to a problem concerning the atomicity of the free non-associative relation algebras is given.