Some locally tabular logics with contraction and mingle
Ai‐ni Hsieh · Reports on Mathematical Logic · 2010
A b s t r a c t. Anderson and Belnap's implicational system RMO! can be extended conservatively by the usual axioms for fusion and for the Ackermann truth constant t. The resulting system RMOis algebraized by the quasivariety IP of all idem- potent commutative residuated po-monoids. Thus, the axiomatic extensions of RMOare in one-to-one correspondence with the relative subvarieties of IP. An algebra in IP is called semiconic if it decomposes subdirectly (in IP) into algebras where the iden- tity element t is order-comparable with all other elements. The semiconic algebras in IP are locally finite. It is proved here that a relative subvariety of IP consists of semiconic algebras if and only if it satisfies x ≈ (x → t) → x. It follows that if an axiomatic extension of RMOhas ((p → t) → p) → p among its theo- rems then it is locally tabular. In particular, such an extension is strongly decidable, provided that it is finitely axiomatized.