2022/04/01 by Bucciarelli, Antonio, Curien, Pierre-Louis, Ledda, Antonio +2
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2204.00435
In recent research, some of the present authors introduced the concept of an n-dimensional Boolean algebra and its corresponding propositional logic nCL, generalising the Boolean propositional calculus to n>= 2 perfectly symmetric truth values. This paper presents a sound and complete sequent calculus for nCL, named nLK. We provide two proofs of completeness: one syntactic and one semantic. The former implies as a corollary that nLK enjoys the cut admissibility property. The latter relies on the generalisation to the n-ary case of the classical proof based on the Lindenbaum algebra of formulas and Boolean ultrafilters.