Against the backdrop of the frequent comparison of theories of truth in the literature on semantic paradoxes with regard to which inferences and metainferences are deemed valid, this paper develops a novel approach to defining a binary predicate for representing the valid inferences and metainferences of a theory within the theory itself under the assumption that the theory is defined with a classical meta-theory. The aim with the approach is to obtain a tool which facilitates the comparison between a theory (...) and its competitors within the theory itself, thereby expressing the disagreement between the theories within the theories. After discussing what we can and should require of an object-linguistic representation of a theory for that purpose, this paper proposes to restrict the representation of valid metainferences to locally valid metainferences, a requirement which turns out to be \-consistent and conservative over classical first-order arithmetic. This approach is then applied to four theories definable on strong Kleene models using a labelled nested sequent calculus. (shrink)

Substructural solutions to the semantic paradoxes have been broadly discussed in recent years. In particular, according to the non-transitive solution, we have to give up the metarule of Cut, whose role is to guarantee that the consequence relation is transitive. This concession—giving up a meta rule—allows us to maintain the entire consequence relation of classical logic. The non-transitive solution has been generalized in recent works into a hierarchy of logics where classicality is maintained at more and more metainferential levels. All (...) the logics in this hierarchy can accommodate a truth predicate, including the logic at the top of the hierarchy—known as CMω—which presumably maintains classicality at all levels. CMω has so far been accounted for exclusively in model-theoretic terms. Therefore, there remains an open question: how do we account for this logic in proof-theoretic terms? Can there be found a proof system that admits each and every classical principle—at all inferential levels—but nevertheless blocks the derivation of the liar? In the present paper, I solve this problem by providing such a proof system and establishing soundness and completeness results. Yet, I also argue that the outcome is philosophically unsatisfactory. In fact, I’m afraid that in light of my results this metainferential solution to the paradoxes can hardly be called a “solution,” let alone a good one. (shrink)

Strict-Tolerant Logic ($$\textrm{ST}$$ ST ) underpins naïve 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 $$\textrm{ST}$$ ST. Unfortunately, there is only a partial correspondence between its derivability relation and the relation of local metainferential $$\textrm{ST}$$ 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 $$\textrm{ST}$$ 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. (shrink)