Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The higher dimensional propositional calculus

Antonio Bucciarelli, Pierre-Louis Curien, Antonio Ledda, Francesco Paoli, Antonino Salibra

TL;DR

The paper develops a comprehensive sequent calculus for the $n$-dimensional propositional logic $n ext{CL}$, introducing $n ext{LK}$ with a single $n$-ary connective $q$, constants $e_i$, and dimension-indexed turnstiles $ hd_i$. It proves soundness and completeness by two routes: a semantic Lindenbaum-$n ext{BA}$ approach and a syntactic inversion-based approach that yields cut admissibility. The work also establishes an equivalence between $n ext{LK}$ and $n ext{CL}$ and relates the finite-dimensional classical case to standard PC through explicit translations, while providing foundational multideal/ultramultideal tools for the completeness proofs. Overall, it offers a robust framework for higher-dimensional logics, with potential implications for finite-valued reasoning, algebraic semantics, and proof theory. The results provide both semantic grounding and syntactic control (including cut-admissible proofs) for reasoning in $n$-valued settings, enabling precise encodings and translations to and from classical and multivalued logics.

Abstract

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.

The higher dimensional propositional calculus

TL;DR

The paper develops a comprehensive sequent calculus for the -dimensional propositional logic , introducing with a single -ary connective , constants , and dimension-indexed turnstiles . It proves soundness and completeness by two routes: a semantic Lindenbaum- approach and a syntactic inversion-based approach that yields cut admissibility. The work also establishes an equivalence between and and relates the finite-dimensional classical case to standard PC through explicit translations, while providing foundational multideal/ultramultideal tools for the completeness proofs. Overall, it offers a robust framework for higher-dimensional logics, with potential implications for finite-valued reasoning, algebraic semantics, and proof theory. The results provide both semantic grounding and syntactic control (including cut-admissible proofs) for reasoning in -valued settings, enabling precise encodings and translations to and from classical and multivalued logics.

Abstract

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.
Paper Structure (17 sections, 36 theorems, 31 equations, 3 figures)

This paper contains 17 sections, 36 theorems, 31 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Church algebras of finite dimension
  4. Boolean algebras of finite dimension
  5. Multideals and ultramultideals
  6. The $n$-dimensional Propositional Calculus
  7. Syntax of $n\mathrm{LK}$
  8. The classical case: syntax
  9. A closer look at the syntax of $n\mathrm{LK}$
  10. Semantics of $n\mathrm{LK}$
  11. Completeness
  12. The Lindenbaum algebra $L_n$
  13. Completeness of $n\mathrm{LK}$
  14. The classical case: semantics
  15. Equivalence of $n\mathrm{CL}$ and $n\mathrm{LK}$
  16. ...and 2 more sections

Key Result

Theorem 2.4

If $\mathbf{A}$ is an $n\mathrm{CH}$ of type $\tau$ and $c\in A$, then the following conditions are equivalent:

Figures (3)

  • Figure 1: The system $n\mathrm{LK}$. Indices $i,j,k$ range over the set $\hat{n}=\{1,\ldots,n\}$ of dimensions, $\pi,\rho\in S_n$ and $X\in V$. $\Gamma,\Delta$ are finite multisets of formulas, represented as lists.
  • Figure 2: The Propositional Calculus.
  • Figure 3: The translations $2\mathrm{LK}$${\leftrightarrow}$$\mathrm{PC}$.

Theorems & Definitions (83)

  • Definition 2.1
  • Example 2.2
  • Definition 2.3
  • Theorem 2.4
  • Proposition 2.5
  • Definition 2.6
  • Example 2.7
  • Example 2.8
  • Theorem 2.9
  • Corollary 2.10
  • ...and 73 more