Return
Proof-theoretic analysis of subabelian lattice logic
K
DOI:10.1093/logcom/exag014.png)
Abstract
En 中文
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.
Keywords:
Lattice logic
Abelian group logic
self-extensional paraconsistent logic
monosequent calculus
cut-elimination theorem
Journal
J
IF:
0
Papers:
44
Citations:
0
