1
Return

Proof-theoretic analysis of subabelian lattice logic

delete2026-04-01
delete0
PRE
AI
K
Kamide, Norihiro *
DOI:10.1093/logcom/exag014delete
deleteOriginal
deleteOriginal request for help
deleteShare
deleteSave
Abstract

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
JOURNAL OF LOGIC AND COMPUTATION
IF:
0
Papers:
44
Citations:
0

Organization

N
Nagoya City University
Scholars:
5.8K
Papers: 4.6K
Citations: 3.3K
Cited Papers

Cited Papers

Citing Papers

Citing Papers