Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Finite Hilbert systems for Weak Kleene logics

Vitor Greati, Sérgio Marcelino, Umberto Rivieccio

Abstract

Multiple-conclusion Hilbert-style systems allow us to finitely axiomatize every logic defined by a finite matrix. Having obtained such axiomatizations for Paraconsistent Weak Kleene and Bochvar-Kleene logics, we modify them by replacing the multiple-conclusion rules with carefully selected single-conclusion ones. In this way we manage to introduce the first finite Hilbert-style single-conclusion axiomatizations for these logics.

Finite Hilbert systems for Weak Kleene logics

Abstract

Multiple-conclusion Hilbert-style systems allow us to finitely axiomatize every logic defined by a finite matrix. Having obtained such axiomatizations for Paraconsistent Weak Kleene and Bochvar-Kleene logics, we modify them by replacing the multiple-conclusion rules with carefully selected single-conclusion ones. In this way we manage to introduce the first finite Hilbert-style single-conclusion axiomatizations for these logics.
Paper Structure (6 sections, 23 theorems, 15 equations, 3 figures)

This paper contains 6 sections, 23 theorems, 15 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Language and semantics of $\mathbf{BK}{}$ and $\mathbf{PWK}{}$
  3. Basics of Hilbert-style axiomatizations
  4. Finite H-systems for PWK
  5. Finite H-systems for BK
  6. Concluding remarks

Key Result

Proposition 1

For all $k \in \mathbb{N}$, $\varphi(p_1,\ldots,p_k) \in L_{{\Sigma_{\land\lor\neg}}}(P)$ and $\vec{a} \in B_{\mathtt{u}}^k$, ${\varphi}_{\mathbf{B}_{\mathtt{u}}}(\vec{a}) = {\varphi}_{\mathbf{B}}(\vec{a})$ if $\vec{a} \in \left\{ {\mathtt{f},\mathtt{t}} \right\}^k$ and ${\varphi}_{\mathbf{B}_{\math

Figures (3)

  • Figure 1: 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 $\Gamma \subseteq \Phi$.
  • Figure 2: Proofs in $\mathsf{R}_{\mathbf{CL}}$ bearing witness, respectively, to $\varnothing \rhd_{\mathsf{R}_{\mathbf{CL}}} p \to p$ and $\neg(p\land q) \rhd_{\mathsf{R}_{\mathbf{CL}}} \neg p, \neg q$.
  • Figure 3: A derivation in $\mathsf{R}_{\mathbf{BK}\star}$ showing that $\neg(p\land q) \rhd_{\mathsf{R}_{\mathbf{BK}\star}} \neg p \lor \neg q$.

Theorems & Definitions (53)

  • Proposition 1
  • Theorem 2: bonzio2021plonka
  • Theorem 3: urquhart2001, Theorem 2.3.1
  • Example 1
  • Example 2
  • Theorem 4: marcelino19syn, Theorem 3.5
  • Lemma 5
  • proof
  • Definition 1
  • Theorem 6
  • ...and 43 more