Table of Contents
Fetching ...

Adding an Implication to Logics of Perfect Paradefinite Algebras

Vitor Greati, Sérgio Marcelino, João Marcos, Umberto Rivieccio

TL;DR

The paper advances the theory of logics for perfect paradefinite algebras (PP-algebras) by systematically adding an implication. It first proves an impossibility result: no classical-like implication can satisfy both $(\mathsf{A}1)$ and $(\mathsf{A}2)$, motivating a residuated Heyting-style approach. It then constructs the six-element algebra $\mathbf{PP_6^{\Rightarrow_{\mathsf{H}}}}$ and studies the induced logics: Set-Set and Set-Fmla for the variety $\mathbb{V}(\mathbf{PP_6^{\Rightarrow_{\mathsf{H}}}})$ are self-extensional, with a deep analysis of algebraizability, interpolation, and amalgamation. The work shows that the $\leq$ versions are not algebraizable (though equivalential) while the top-assertional versions are fully algebraizable, with Moisil-type symmetric Heyting algebras providing the algebraic semantics; it also provides analytic Hilbert-style axiomatizations and a finite PN-matrix characterization. Finally, it establishes interpolation properties (EIP for $\leq$, CIP and MIP for top) and proves that the PP-implication framework enjoys Maehara amalgamation, highlighting both the expressive power and the limitations of these implicative expansions.

Abstract

Perfect paradefinite algebras are De Morgan algebras expanded with an operation that allows for the full behavior of classical negation to be restored. They form a variety that is term-equivalent to the variety of involutive Stone algebras. Their associated multiple-conclusion (Set-Set) and single-conclusion (Set-Fmla) order-preserving logics are non-algebraizable self-extensional logics of formal inconsistency and undeterminedness determined by a six-valued matrix, studied in depth by Gomes et al. (2022) from both the algebraic and the proof-theoretical perspectives. In the present paper, we continue that study by investigating directions for conservatively expanding these logics with an implication connective (essentially, one that admits the deduction-detachment theorem). We first consider logics given by very simple and manageable non-deterministic semantics whose implication (in isolation) is classical. These, nevertheless, fail to be self-extensional. We then consider the implication realized by the relative pseudo-complement over the six-valued perfect paradefinite algebra. Our strategy is to expand the language of the latter algebra with this connective and study the (self-extensional) Set-Set and Set-Fmla order-preserving and top-assertional logics of the variety induced by the resulting algebra. We provide axiomatizations for such new variety and for such logics, drawing parallels with the class of symmetric Heyting algebras and with Moisil's 'symmetric modal logic'. For the Set-Set logic, in particular, the axiomatization we obtain is analytic. We close by studying interpolation properties for these logics and concluding that the new variety has the Maehara amalgamation property.

Adding an Implication to Logics of Perfect Paradefinite Algebras

TL;DR

The paper advances the theory of logics for perfect paradefinite algebras (PP-algebras) by systematically adding an implication. It first proves an impossibility result: no classical-like implication can satisfy both and , motivating a residuated Heyting-style approach. It then constructs the six-element algebra and studies the induced logics: Set-Set and Set-Fmla for the variety are self-extensional, with a deep analysis of algebraizability, interpolation, and amalgamation. The work shows that the versions are not algebraizable (though equivalential) while the top-assertional versions are fully algebraizable, with Moisil-type symmetric Heyting algebras providing the algebraic semantics; it also provides analytic Hilbert-style axiomatizations and a finite PN-matrix characterization. Finally, it establishes interpolation properties (EIP for , CIP and MIP for top) and proves that the PP-implication framework enjoys Maehara amalgamation, highlighting both the expressive power and the limitations of these implicative expansions.

Abstract

Perfect paradefinite algebras are De Morgan algebras expanded with an operation that allows for the full behavior of classical negation to be restored. They form a variety that is term-equivalent to the variety of involutive Stone algebras. Their associated multiple-conclusion (Set-Set) and single-conclusion (Set-Fmla) order-preserving logics are non-algebraizable self-extensional logics of formal inconsistency and undeterminedness determined by a six-valued matrix, studied in depth by Gomes et al. (2022) from both the algebraic and the proof-theoretical perspectives. In the present paper, we continue that study by investigating directions for conservatively expanding these logics with an implication connective (essentially, one that admits the deduction-detachment theorem). We first consider logics given by very simple and manageable non-deterministic semantics whose implication (in isolation) is classical. These, nevertheless, fail to be self-extensional. We then consider the implication realized by the relative pseudo-complement over the six-valued perfect paradefinite algebra. Our strategy is to expand the language of the latter algebra with this connective and study the (self-extensional) Set-Set and Set-Fmla order-preserving and top-assertional logics of the variety induced by the resulting algebra. We provide axiomatizations for such new variety and for such logics, drawing parallels with the class of symmetric Heyting algebras and with Moisil's 'symmetric modal logic'. For the Set-Set logic, in particular, the axiomatization we obtain is analytic. We close by studying interpolation properties for these logics and concluding that the new variety has the Maehara amalgamation property.
Paper Structure (16 sections, 50 theorems, 75 equations, 2 figures, 2 tables)

This paper contains 16 sections, 50 theorems, 75 equations, 2 figures, 2 tables.

Key Result

Proposition 2.5

$\rhd_{\mathsf{K}}^{\leq}$ is the finitary companion of the logic determined by $\mathcal{M^{{{\uparrow}\lor}}} \,{\coloneqq}\, \{ \langle \mathbf{A}, D \rangle : \mathbf{A} \in \mathsf{K}\text{ and } D \text{ is a prime filter of $\mathbf{A}$}\}$.

Figures (2)

  • Figure 2: Graphical representation of $\mathsf{R}$-derivations, where $\mathsf{R}$ is a $\textsc{Set-Set}{}$ system. The dashed edges and blank circles represent other branches that may exist in the derivation. We usually omit the formulas inherited from the parent node, exhibiting only the ones introduced by the applied rule of inference. Recall that, in both cases, we must have $\Pi \subseteq \Phi$.
  • Figure 3: Proofs in $\mathsf{R}_\mathcal{B}$ witnessing that ${\sim}(p \land q) \;{\lhd\rhd}_{\mathcal{B}}\; {\sim} p \lor {\sim} q$ and $p \lor \bot \; {\lhd\rhd}_{\mathcal{B}} \; p, r$.

Theorems & Definitions (134)

  • Definition 2.1
  • Example 1
  • Definition 2.2
  • Example 2
  • Definition 2.3
  • Example 3
  • Example 4
  • Definition 2.4
  • Proposition 2.5
  • proof
  • ...and 124 more