SOME LOCALLY TABULAR LOGICS WITH CONTRACTION AND MINGLE

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 RMO* is algebraized by the quasivariety IP of all idempotent commutative residuated po-monoids. Thus, the axiomatic extensions of RMO* are 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 identity 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 approximate to (x -> t) -> x. It follows that if an axiomatic extension of RMO* has ((p -> t) -> p) -> p among its theorems then it is locally tabular. In particular, such an extension is strongly decidable, provided that it is finitely axiomatized.