Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Sequent calculi for first-order ST

Francesco Paoli, Adam Přenosil

Abstract

Strict-Tolerant Logic (ST) underpins naive theories of truth and vagueness (respectively including a fully disquotational truth predicate and an unrestricted tolerance principle) without jettisoning any classically valid laws. The classical sequent calculus without Cut is sometimes advocated as an appropriate proof-theoretic presentation of ST. Unfortunately, there is only a partial correspondence between its derivability relation and the relation of local metainferential ST-validity - these relations coincide only upon the addition of elimination rules and only within the propositional fragment of the calculus, due to the non-invertibility of the quantifier rules. In this paper, we present two calculi for first-order ST with an eye to recapturing this correspondence in full. The first calculus is close in spirit to the Epsilon calculus. The other calculus includes rules for the discharge of sequent-assumptions; moreover, it is normalisable and admits interpolation.

Sequent calculi for first-order ST

Abstract

Strict-Tolerant Logic (ST) underpins naive theories of truth and vagueness (respectively including a fully disquotational truth predicate and an unrestricted tolerance principle) without jettisoning any classically valid laws. The classical sequent calculus without Cut is sometimes advocated as an appropriate proof-theoretic presentation of ST. Unfortunately, there is only a partial correspondence between its derivability relation and the relation of local metainferential ST-validity - these relations coincide only upon the addition of elimination rules and only within the propositional fragment of the calculus, due to the non-invertibility of the quantifier rules. In this paper, we present two calculi for first-order ST with an eye to recapturing this correspondence in full. The first calculus is close in spirit to the Epsilon calculus. The other calculus includes rules for the discharge of sequent-assumptions; moreover, it is normalisable and admits interpolation.
Paper Structure (9 sections, 31 theorems, 11 equations, 4 figures)

This paper contains 9 sections, 31 theorems, 11 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Strict-Tolerant Logic: Its Semantics and Proof Theory
  3. The Calculus $\mathcal{ST}^{H}$
  4. Presentation of the calculus
  5. Soundness and completeness
  6. Relationship with the Epsilon calculus
  7. The Calculus $\mathcal{MQST}$
  8. Normalisation and Interpolation for $\mathcal{MQST}$
  9. Conclusions and Open Problems

Key Result

Lemma 1

$\models_{\mathrm{ST}} \Gamma \vartriangleright \Delta$ iff $\models_{\mathrm{CL}} \Gamma \vartriangleright \Delta$.

Figures (4)

  • Figure 1: Rules of $\mathcal{ST}^P$
  • Figure 2: Additional rules for $\mathcal{ST}^{H}$
  • Figure 3: Quantifier rules in $\mathcal{E}$
  • Figure 4: Quantifier rules in $\mathcal{MQST}$

Theorems & Definitions (64)

  • Lemma 1: Cob1; see also Girard
  • Theorem 2: DP
  • Theorem 3: Pynko, see also BarrioPrenosil
  • Definition 4
  • Definition 5
  • Lemma 6
  • Definition 7
  • Theorem 8
  • Lemma 9
  • Definition 10
  • ...and 54 more