The higher dimensional propositional calculus

被引:0
作者
Bucciarelli, A. [1 ,2 ]
Curien, P-L [1 ,2 ]
Ledda, A. [3 ]
Paoli, F.
Salibra, A. [1 ,2 ]
机构
[1] IRIF, CNRS, Paris, France
[2] Univ Paris Cite, Paris, France
[3] Univ Cagliari, Dipartimento Pedag Psicol Filosofia, Cagliari, Italy
关键词
Boolean algebras; Boolean algebras of dimension n; Classical logic of dimension n; sequent calculus; cut elimination;
D O I
10.1093/jigpal/jzae100
中图分类号
O29 [应用数学];
学科分类号
070104 ;
摘要
In recent research, some of the present authors introduced the concept of an $n$-dimensional Boolean algebra and its corresponding propositional logic $n\textrm{CL}$, generalizing the Boolean propositional calculus to $n\geq 2$ perfectly symmetric truth values. This paper presents a sound and complete sequent calculus for $n\textrm{CL}$, named $n\textrm{LK}$. We provide two proofs of completeness: one syntactic and one semantic. The former implies as a corollary that $n\textrm{LK}$ enjoys the cut admissibility property. The latter relies on the generalization to the $n$-ary case of the classical proof based on the Lindenbaum algebra of formulas and Boolean ultrafilters.
引用
收藏
页数:29
相关论文
共 20 条
[1]  
[Anonymous], 2004, LPAR 2004, LNCS
[2]   A CONSTRUCTIVE ANALYSIS OF RM [J].
AVRON, A .
JOURNAL OF SYMBOLIC LOGIC, 1987, 52 (04) :939-951
[3]  
Baaz M., 1999, Automated Reasoning with Analytic Tableaux and Related Methods. International Conference, TABLEAUX'99. Proceedings (Lecture Notes in Artificial Intelligence Vol. 1617), P36
[4]  
Baaz M., 1993, Bulletin of the European Association for Theoretical Computer Science, P192
[5]  
Bucciarelli A., 2024, JANUSZ CZELAKOWSKI L, P377
[6]  
Bucciarelli A., 2019, ART DISCRETE APPL MA, V2, P1, DOI DOI 10.26493/2590-9770.1323.CEB
[7]  
Burris S., 1981, COURSE UNIVERSAL ALG
[8]   Proof theory for locally finite many-valued logics: Semi-projective logics [J].
Ciabattoni, Agata ;
Montagna, Franco .
THEORETICAL COMPUTER SCIENCE, 2013, 480 :26-42
[9]  
Czelakowski J, 2018, OUTST CONTRIB LOGIC, V16, P297, DOI 10.1007/978-3-319-74772-9_12
[10]  
Goranko V., 2020, KNOWLEDGE PROOF DYNA, P173