Sequent calculi for first-order ST

TL;DR

This paper develops two sequent calculi for first-order Strict-Tolerant Logic (ST) aiming to fully align proof-theoretic derivability with ST-validity, addressing limitations of classical calculi in capturing first-order ST.

Contribution

It introduces two novel calculi for first-order ST, one inspired by the Epsilon calculus and another with discharge rules, achieving full correspondence with ST-validity.

Findings

First calculus closely resembles the Epsilon calculus.

Second calculus includes discharge rules and is normalisable.

Both calculi improve proof-theoretic understanding of 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.