Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Generating proof systems for three-valued propositional logics

Vitor Greati, Giuseppe Greco, Sérgio Marcelino, Alessandra Palmigiano, Umberto Rivieccio

TL;DR

This work develops methods to automatically generate finite, analytic proof systems for propositional logics defined by single finite three-valued matrices. It presents two complementary formalisms—3-labelled calculi and Set-Set Hilbert-style calculi—and a two-step procedure (matrix-to-rule translation followed by streamlining) that yields valid, cut-free, and analytic axiomatizations. The chapter demonstrates how to axiomatize prominent three-valued logics (Ł$_3$, K, LP, BK, S3, J3, G3, P3, etc.) and discusses monadic versus non-monadic regimes, including concrete finite Set-Set axiom systems for fragments of BK, Ł$_3$, and Gödel logics. It also establishes correspondences and translations between the two formalisms, highlighting modularity, completeness, and decidability aspects, and identifies open questions for non-monadic matrices and higher expressiveness. The results provide a practical blueprint for automatic proof-system generation in finite three-valued settings, with potential extensions to non-deterministic and partial matrices.

Abstract

In general, providing an axiomatization for an arbitrary logic is a task that may require some ingenuity. In the case of logics defined by a finite logical matrix (three-valued logics being a particularly simple example), the generation of suitable finite axiomatizations can be completely automatized, essentially by expressing the matrix tables via inference rules. In this chapter we illustrate how two formalisms, the 3-labelled calculi of Baaz, Fermüller and Zach and the multiple-conclusion (or Set-Set) Hilbert-style calculi of Shoesmith and Smiley, may be uniformly employed to axiomatize logics defined by a three-valued logical matrix. The generating procedure common to both formalisms can be described as follows: first (i) convert the matrix semantics into rule form (we refer to this step as the generating subprocedure) and then (ii) simplify the set of rules thus obtained, essentially relying on the defining properties of any Tarskian consequence relation (we refer to this step as the streamlining subprocedure). We illustrate through some examples that, if a minimal expressiveness assumption is met (namely, if the matrix defining the logic is monadic), then it is straightforward to define effective translations guaranteeing the equivalence between the 3-labelled and the Set-Set approach.

Generating proof systems for three-valued propositional logics

TL;DR

This work develops methods to automatically generate finite, analytic proof systems for propositional logics defined by single finite three-valued matrices. It presents two complementary formalisms—3-labelled calculi and Set-Set Hilbert-style calculi—and a two-step procedure (matrix-to-rule translation followed by streamlining) that yields valid, cut-free, and analytic axiomatizations. The chapter demonstrates how to axiomatize prominent three-valued logics (Ł, K, LP, BK, S3, J3, G3, P3, etc.) and discusses monadic versus non-monadic regimes, including concrete finite Set-Set axiom systems for fragments of BK, Ł, and Gödel logics. It also establishes correspondences and translations between the two formalisms, highlighting modularity, completeness, and decidability aspects, and identifies open questions for non-monadic matrices and higher expressiveness. The results provide a practical blueprint for automatic proof-system generation in finite three-valued settings, with potential extensions to non-deterministic and partial matrices.

Abstract

In general, providing an axiomatization for an arbitrary logic is a task that may require some ingenuity. In the case of logics defined by a finite logical matrix (three-valued logics being a particularly simple example), the generation of suitable finite axiomatizations can be completely automatized, essentially by expressing the matrix tables via inference rules. In this chapter we illustrate how two formalisms, the 3-labelled calculi of Baaz, Fermüller and Zach and the multiple-conclusion (or Set-Set) Hilbert-style calculi of Shoesmith and Smiley, may be uniformly employed to axiomatize logics defined by a three-valued logical matrix. The generating procedure common to both formalisms can be described as follows: first (i) convert the matrix semantics into rule form (we refer to this step as the generating subprocedure) and then (ii) simplify the set of rules thus obtained, essentially relying on the defining properties of any Tarskian consequence relation (we refer to this step as the streamlining subprocedure). We illustrate through some examples that, if a minimal expressiveness assumption is met (namely, if the matrix defining the logic is monadic), then it is straightforward to define effective translations guaranteeing the equivalence between the 3-labelled and the Set-Set approach.
Paper Structure (27 sections, 20 theorems, 25 equations, 3 figures, 4 tables)

This paper contains 27 sections, 20 theorems, 25 equations, 3 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Prominent three-valued logics
  4. Ł ukasiewicz (Ł$_3$).
  5. Strong Kleene (K).
  6. Logic of Paradox (LP).
  7. Logic of Paradox with implication ($\textbf{LP$^\rightarrow\xspace{}$}{}$).
  8. Paraconsistent Weak Kleene (PK).
  9. Bochvar-Kleene ($\textbf{BK}$).
  10. Sobociński ($\textbf{S3}$)
  11. Da Costa and D'Ottaviano's (J3).
  12. Gödel (G3)
  13. Post ($\textbf{P3}$)
  14. Logics $\textbf{L7}$ and $\textbf{L8}$.
  15. The formalism of 3-labelled calculi
  16. ...and 12 more sections

Key Result

Lemma 4.2

A 3-labelled logical rule of the form holds in $\mathbb{M} := \langle \mathbf{A}, D \rangle$ if, and only if, ${\copyright}_{\mathbf{A}}(\nu_1,\ldots,\nu_k) = \nu$.

Figures (3)

  • Figure 1: Three-valued interpretations for the connectives of the logics listed in Table \ref{['tab:usecases']}.
  • Figure 2: Graphical representation of $\mathsf{R}$--derivations using finitary inference rules, in the form of a leaf node, a discontinued node and an expanded node, respectively.
  • Figure :

Theorems & Definitions (68)

  • Definition 2.1
  • Definition 2.2
  • Definition 4.1
  • Lemma 4.2
  • Theorem 4.3: BaaFerZac98avronzamanssamebook
  • Example 4.4
  • Definition 4.5
  • Proposition 4.6
  • Example 4.7
  • Example 4.8
  • ...and 58 more