Proof-theoretic analysis of subabelian lattice logic

Abstract A logic referred to as subabelian lattice logic (SLL) is introduced as a monosequent calculus. This calculus is based on a restricted form of sequent, called a monosequent, which contains either a single formula or the empty set in both the antecedent and the succedent. The conjunction–disjunction fragment of SLL coincides with lattice logic, while the implication–negation fragment of SLL forms a proper subsystem of Abelian group logic. The cut-elimination, decidability and Craig interpolation theorems, as well as the variable sharing and self-extensional properties, are established for SLL. Furthermore, several characteristic properties—such as symmetry elimination, Abelian symmetric implication, Abelian provable contradiction and balanced implication—are established for the implication–negation fragment of SLL. Additionally, an extension of SLL obtained by adding the truth and falsity constants is introduced, and its completeness theorem with respect to a lattice-valued semantics is established.