Some Locally Tabular Logics with Contraction and Mingle

Anderson and Belnap’s implicational system $\bb {RMO}_\rightarrow$ can be extended conservatively by the usual axioms for fusion and for the Ackermann truth constant t. The resulting system $\bb{RMO}$* is algebraized by the quasivariety IP of all idempotent commutative residuated po-monoids. Thus, the axiomatic extensions of $\bb {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 \approx (x\rightarrow t)\rightarrow x$. It follows that if an axiomatic extension of $\bb {RMO}$* has $((p\rightarrow t)\rightarrow p)\rightarrow p$ among its theorems then it is locally tabular. In particular, such an extension is strongly decidable, provided that it is finitely axiomatized.