Saving logic from paradox via nonclassical recapture

Abstract

The Liar paradox arguably shows that a coherent and self-applicable notion of truth is governed by nonclassical logic. It then seems natural to conclude that classical logic is inadequate for defining a truth theory. In this article, we argue that this is not the case. In the spirit of Reinhardt (Math Logic Formal Syst 94:227, 1985; J Philos Logic 15:219–251, 1986), and in analogy with Hilbert’s program for the foundation of classical mathematics, we will articulate an instrumentalist justification for the use classical logic: it will be argued that classical reasoning is a useful but dispensable instrument, which can yield philosophically adequate truth theories.

1 Introduction

Can we reason correctly about truth within a truth theory formulated in classical logic? The Liar paradox seems to suggest a negative answer, by means of an argument along the following lines. The fundamental property of truth is its transparency, in the sense that

$$\begin{aligned} \text {every sentence}\, A \,\text {is equivalent to the statement that} \,A \,\text {is true.} {\quad \quad \quad \mathbf{(T)}} \end{aligned}$$

The existence of liar sentences, claiming their own untruth, reveals a fundamental incompatibility between classical reasoning and the transparency of truth. Hence truth is governed by nonclassical logic.¹ But then, if we want to devise a philosophically adequate theory of self-applicable truth, we ought to adopt a nonclassical logic.

This rather simple argument has an undisputable plausibility. Since classical logic cannot be extended with a transparent truth predicate (pace Ripley 2012), and since (T) has arguably a special status in our web of beliefs about truth,² moving to a nonclassical setting seems only natural. Indeed, especially after (Kripke’s landmark 1975), there has been an extensive use of nonclassical logics within theories of truth and related semantic notions.³ A key motivation for revising classical logic is precisely that, unlike classical theories, nonclassical theories do embody the transparency of truth while dealing adequately with paradoxical sentences.⁴

Notwithstanding the importance of a transparent truth predicate, many theorists consider classical logic to be a property which is just as desirable for a truth theory. Defenders of classical logic have in more than one context pointed out that weakening classical logic comes with too high a cost. In particular, along with Feferman’s famous criticism according to which “nothing like sustained ordinary reasoning” can be carried out in logics such as Strong Kleene (Feferman 1984, p.95) it has been demonstrated that the impact of nonclassical logics goes beyond paradoxes. Nonclassical reasoning affects areas of our theories for which classical logic is unproblematic. In particular, in nonclassical theories it is our mathematical and scientific reasoning that is crippled, too.⁵

It then seems that we are faced with a dilemma: we either adopt a nonclassical logic and give up important parts of mathematical reasoning, or we keep classical logic and give up the prospect of reasoning correctly about truth.⁶

In the attempt to pave a way out of this dilemma, the main goal of the present paper consists in showing that, even if truth is governed by nonclassical logic, we can keep classical logic and reason correctly about truth. Or, to put it more compellingly, to goal is to save logic from paradox (with apologies to Hartry Field⁷). To this end, in the spirit of Reinhardt (1985, 1986), we will articulate an instrumentalist justification for the use classical logic: it will be argued that classical reasoning is a useful but dispensable instrument. Let us here give the gist of the instrumentalism developed in Sect. 3.

Drawing an analogy with some of Hilbert’s idea in his program for the foundation of classical mathematics, we will distinguish between real and ideal truth-theoretic inferences. The former kind of inferences will be taken to be what constitutes the core of a truth theory, while ideal truth-theoretic inferences will be seen as a device to obtain real truth-theoretic inferences. Similarly, we will distinguish between real and ideal truth-theoretic reasoning. The former will be taken to be reliable and intuitive—on a par with finitist methods—while the latter will be conceived of as a mere device to simplify our inferential practice. With these distinctions at hand, we will finally suggest that ideal reasoning should be conservative over real reasoning as far as real truth-theoretic inferences are concerned. In other words, the suggestion is that, while classical logic involves ideal truth-theoretic reasoning, this should be shown to be dispensable for obtaining real truth-theoretic inferences, for which only real truth-theoretic reasoning should be required. Or, to put it more compellingly yet once again, we should be able to recapture⁸ nonclassical reasoning whenever needed. These ideas will be given formal expression, and it will be shown, via a case study, that such an instrumentalism can be successful.

1.1 Plan of article.

The article begins with a preliminary Sect. 2, in which a well-known nonclassical way of reasoning about truth is introduced, namely a naive truth theory formulated over the logic $\texttt{FDE}$. This will be our case study. Additionally, in Sect. 2 we also briefly explain the base syntax theory used to formulate the truth theories studied here. Section 3 contains the main argument, i.e., it presents the instrumentalist interpretation of classical logic, drawing a number of analogies with Hilbert’s instrumentalism in the foundation of mathematics. In Sect. 4, we briefly discuss the debate on the so-called classical recapture strategy, arguing that the present investigation offers a new perspective on that debate. Finally, we conclude in Sect. 5 with a list of open questions and possible extensions of the present study.

2 A nonclassical way of reasoning about truth

As mentioned in the introduction, the key point of this paper is to show that, even though truth is governed by some nonclassical logic, classical logic need not be abandoned. As a case study, we will concentrate on the nonclassical logic First Degree Entailment ($\texttt{FDE}$), also known as Belnap-Dunn Logic.⁹ It will be assumed that $\texttt{FDE}$ is the logic of type-free truth. This will be an underlying assumption. It will neither be argued that there is one true logic governing type-free truth, nor that—should there be one—this is $\texttt{FDE}$.¹⁰

$\texttt{FDE}$ is an interesting and useful logic, particularly well suited for the present purposes. It allows a neat comparison with classical reasoning, and it can be modularly extended to three other well-known stronger systems, i.e., Strong Kleene ($\texttt{SK}$), the Logic of Paradox ($\texttt{LP}$), and Symmetric Strong Kleene ($\texttt{KS}$).¹¹ All these logics have been used to axiomatize fixed-point semantics à la Kripke (1975).¹² Though the inferential principles of $\texttt{FDE}$ are widely known, we will briefly revise them, in order to keep things relatively self-contained. The rules governing the behaviour of conjunction, disjunction, and quantifiers correspond to those of classical logic (for example, a conjunction $A\wedge B$ is derivable iff both conjuncts A and B are derivable). What differentiates $\texttt{FDE}$ from classical logic is the the behaviour of negation. Semantically, $\texttt{FDE}$ rejects the principle of bivalence, according to which every sentence is, exclusively, either true or false. In $\texttt{FDE}$, we cannot exclude that some sentences are both true and false—so called gluts—or neither true not false—so called gaps. Proof-theoretically, this amounts to rejecting the classically valid principles known as Law of Excluded Middle (LEM)—$A\vee \lnot A$ is derivable for any A—and Ex Falso Quodlibet (EFQ)—$A\wedge \lnot A$ implies triviality. To compensate for the absence of LEM and EFQ, $\texttt{FDE}$ has additional rules governing the behaviour of complex sentences whose main connective is negation. In particular, $\lnot \lnot A$ is equivalent to A, and compound formulae behave in accordance with De Morgan dualities, that is: $\lnot (A\vee B)$ and $\lnot (A\wedge B)$ are equivalent to, respectively, $\lnot A\wedge \lnot B$ and $\lnot A\vee \lnot B$; $\lnot \exists x A$ and $\lnot \forall x A$ are equivalent to, respectively, $\forall x\lnot A$ and $\exists x\lnot A$.

These inferential principles can be straightforwardly and completely encoded within a sequent calculus, as shown in Table 1.¹³ A sequent is an expression of the form $\Gamma \Rightarrow \Delta$, where $\Gamma$ and $\Delta$ are finite sets of formulae.¹⁴ Intuitively, left and right rules of sequent calculi correspond to elimination and introduction rules, respectively, of calculi of natural deduction.

Table 1 $\texttt{FDE}$

Over $\texttt{FDE}$, defining a truth theory embodying (T) is rather immediate. Before showing that, however, a small technical detour is needed.

2.1 Syntactic Intermezzo.

In order to formulate a theory of truth, we need an underlying theory of syntax. In particular, we need that every sentence A has a name, which will be denoted by a closed term $\ulcorner {A}\urcorner$ working like quotation marks. This device allows us to express that a certain sentence A is true via the sentence $\textrm{T} \ulcorner {A}\urcorner$. Moreover, we also want to be able to state that some property P(x) is satisfied by all (or some) objects of the intended domain of discourse. For example, if we are talking about natural numbers, we might want to state that (1) and (2) below are equivalent:

• (1) for all x, it is true that $x\ge \texttt{0}$,

• (2) it is true that for all x, $x\ge \texttt{0}$.

While (2) can be formalized by $\textrm{T} \ulcorner {\forall x (x\ge \texttt{0})}\urcorner$, to formalize (1) we need extra resources, as it requires quantification within names.¹⁵ In order to give formal expression to statements such as (1) we require, for every formula A(x) and every term s, our language to contain a (possibly open) term $\ulcorner {A(\dot{s})}\urcorner$, whose free variables are those of the term s.¹⁶ We can then express (1) by $\forall x\,\textrm{T} \ulcorner {\dot{x}\ge \texttt{0}}\urcorner$, where the variable x does occur freely in $\ulcorner {\dot{x}\ge \texttt{0}}\urcorner$ and is bound by $\forall x$.

While details on how to obtain such a syntax theory are not important, for the sake of definiteness, we assume that we are working with the induction-free arithmetical theory Robinson arithmetic Q, where this all can be made rigorous via suitable substitution and numeral functions.¹⁷ In what follows, then, let ${\mathcal {L} _\textrm{T}}$ be the language of first order arithmetic $\mathcal {L}_{\mathbb {N}}$ augmented by a unary truth predicate $\textrm{T}$ and by finitely many symbols for suitable primitive recursive functions formalizing required syntactic notions. End of syntactic intermezzo.

A truth theory over $\texttt{FDE}$ can be defined in two simple steps. The first consists in adding the rules of Table 2.¹⁸ These are negation rules restricted on formulae not containing $\textrm{T}$, which make sure that the theory will behave classically on the $\textrm{T}$-free fragment of the language. Within truth theories, assuming classicality on a base language not containing $\textrm{T}$ is a fairly standard assumption.

Table 2 Restricted negation rules

The second step consists in adding the naive truth-rules shown in Table 3,¹⁹ which immediately entails a transparent truth predicate.

Table 3 Naive truth-rules

Let $\texttt{INT}$, for internal theory,²⁰ be the theory obtained by extending $\texttt{FDE}$ with the rules of Tables 2 and 3.²¹ It is easily observed that every sentence A is equivalent to $\textrm{T} \ulcorner {A}\urcorner$ in $\texttt{INT}$, in the sense that the sequents

$$\begin{aligned} A,&\Gamma \Rightarrow \Delta ,&\textrm{T} \ulcorner {A}\urcorner \\ \lnot A,&\Gamma \Rightarrow \Delta ,&\lnot \textrm{T} \ulcorner {A}\urcorner , \end{aligned}$$

as well as

$$\begin{aligned} \textrm{T} \ulcorner {A}\urcorner ,&\Gamma \Rightarrow \Delta ,&A \\ \lnot \textrm{T} \ulcorner {A}\urcorner ,&\Gamma \Rightarrow \Delta ,&\lnot A, \end{aligned}$$

are derivable for all A.

Also, it can equally easily be observed that $\texttt{INT}$ is pointwise compositional.²² For example, by transparency of $\textrm{T}$ and compositionality of the underlying logic, the following sequents are derivable for any A and B:

$$\begin{aligned}&\textrm{T} \ulcorner {A\wedge B}\urcorner , \Gamma \Rightarrow \Delta , \,\textrm{T} \ulcorner {A}\urcorner , \\&\textrm{T} \ulcorner {A\wedge B}\urcorner , \Gamma \Rightarrow \Delta , \,\textrm{T} \ulcorner {B}\urcorner , \\&\textrm{T} \ulcorner {A}\urcorner , \textrm{T} \ulcorner {B}\urcorner , \Gamma \Rightarrow \Delta , \, \textrm{T} \ulcorner {A\wedge B}\urcorner , \\&\textrm{T} \ulcorner {\forall x A}\urcorner , \Gamma \Rightarrow \Delta ,\, \forall x\textrm{T} \ulcorner {A(\dot{x})}\urcorner , \\&\forall x\textrm{T} \ulcorner {A(\dot{x})}\urcorner , \Gamma \Rightarrow \Delta ,\, \textrm{T} \ulcorner {\forall x A}\urcorner . \end{aligned}$$

And similarly for complex sentences with negation as main connectives. Schematic compositionality of truth extends to negation as well: the sequents

$$\begin{aligned}&\lnot \textrm{T} \ulcorner {A}\urcorner , \Gamma \Rightarrow \Delta , \textrm{T} \ulcorner {\lnot A}\urcorner , \\&\textrm{T} \ulcorner {\lnot A}\urcorner , \Gamma \Rightarrow \Delta , \lnot \textrm{T} \ulcorner {A}\urcorner . \end{aligned}$$

are also derivable in $\texttt{INT}$ for all A.

In sum, the naive theory $\texttt{INT}$ is intuitive, it avoids paradoxes, it explicates the compositional nature of truth in a simple way, and arguably it can be deemed philosophically sound, in the sense that every sequent derivable in it is philosophically acceptable. Moreover, $\texttt{INT}$ has an elegant semantics. One can define a class $\mathcal {C}$ of fixed-point models of the kind of Kripke (1975) and show that, whenever $\Gamma \Rightarrow \Delta$ is derivable in $\texttt{INT}$, then $\Gamma \Rightarrow \Delta$ is satisfied in every fixed-point model $\mathcal {M} \in \mathcal {C}$, in the sense that if every sentence in $\Gamma$ is satisfied in $\mathcal {M}$, then some sentence in $\Delta$ is satisfied in $\mathcal {M}$ too.²³

Table 4 Compositional truth-rules

3 Classical logic, a useful but dispensable instrument

In the previous section, under the assumption that truth is governed by the logic $\texttt{FDE}$, we have seen how to define an adequate truth theory using the nonclassical logic $\texttt{FDE}$ itself, along with naive rules of quotation and disquotation. The goal of the present section is to show how classical logic can be used as a useful but dispensable instrument to obtain an equally adequate theory.

The classical theory of truth will be referred to as $\texttt{EXT}$, for external theory.²⁴ A classical theory of $\texttt{FDE}$-truth cannot be obtained as easily as the theory $\texttt{INT}$ of the previous section. Since the naive rules $(\lnot )\textrm{T}$L/R are inconsistent with classical logic, we need to formulate pointwise compositional rules. These are shown in Table 4.²⁵ The first two rules state that true (false) arithmetical atomic formulae are true (false). The rationale behind the remaining rules is that they should yield a theory in which we can simulate the nonclassical truth-reasoning of $\texttt{INT}$ within the scope of $\textrm{T}$. Indeed, removing the outermost $\textrm{T}$, one gets nothing but the compositional rules of $\texttt{FDE}$ along with the naive truth rules, here formulated as $\textrm{TT}$L/R and $\textrm{T} \lnot \textrm{T}$L/R. This observation could be turned into a more formal statement, showing that every rule of Table 4 is derivable in $\texttt{INT}$.²⁶

Let us now clarify in what sense classical logic can be viewed as a “useful but dispensable instrument”. The main components of the instrumentalism suggested here are best explained by analogy with some views developed by Hilbert in the context of foundational studies of mathematics. The following partly summarizes a few key points in Hilbert’s foundational program.

Hilbert considered finitist methods in mathematics as absolutely reliable and intuitive, and one of his goals was to show that these finitist methods were strong enough to obtain consistency proofs for number theory, analysis and even richer mathematical theories. He introduced a distinction between “real” and “ideal” propositions, maintaining that ideal propositions have no meaning in themselves (Hilbert 1926). This distinction has led many scholars to read Hilbert’s program as an instrumentalist account of mathematics, that is, as a view according to which ideal mathematics is only an instrument. An instrument to preserve classically valid inferences (such as tertium non datur) for infinite totalities, while obtaining real propositions. As observed by Richard Zach, this reading of Hilbert’s program “goes hand in hand with a reading of the proof-theoretic program as a reductionist project” (Zach 2007, p.430). Ideal mathematics should be reduced to real mathematics in the sense that the former should be proven to be conservative over the latter, as far as real propositions are concerned: whenever the ideal theory proves a real proposition P, then P is provable already in real mathematics, by finitary means only. A successful reductionist project would yield a solid justification for the use of ideal mathematics, as it would show that ideal mathematics proves only intuitive, real propositions.

We suggest embarking on a similar program, which can be seen as an extension of the so-called Reinhardt’s program.²⁷ Just as ideal mathematics can be viewed as an instrument for obtaining real mathematical propositions, we suggest to view classical reasoning as an instrument for obtaining real truth-theoretic inferences. Since this idea takes inspiration from Hilbert’s instrumentalism, it will now be elaborated in details by means of three analogies.²⁸

Analogy with finitism. Similarly to how Hilbert considered finitist methods to be reliable and intuitive, we maintain that a fragment of classical reasoning should be considered reliable and intuitive by the advocates of $\texttt{FDE}$ and those of classical logic. The fragment we are referring to is that of $\texttt{EXT}$ not involving the rules $\lnot$L/R on formulae containing $\textrm{T}$. The advocate of $\texttt{FDE}$ should find this claim uncontroversial—let alone the defender of classical reasoning. On the one hand, it has already been observed that, besides $\lnot$L/R, every other principle of classical logic is a defining component of $\texttt{FDE}$. On the other hand, each of the truth rules of $\texttt{EXT}$ are derivable in $\texttt{INT}$, meaning that in $\texttt{INT}$ we can de facto reason using those rules. But then every sequent that is derivable in $\texttt{EXT}$ without use of the rules $\lnot$L/R on formulae containing $\textrm{T}$ is derivable in $\texttt{INT}$ as well.²⁹

Analogy with real VS ideal. Just as Hilbert differentiated between real and ideal propositions, and between real and ideal mathematics, so we suggest that we distinguish between real and ideal truth-theoretic inferences, and between real and ideal truth-theoretic reasoning. The former distinction is already present in the literature in various form, and it has its roots in Reinhardt (1985, 1986). The underlying idea is that, given a truth theory S, one can distinguish between what is derivable in S, and what is derivable in S within the scope of $\textrm{T}$. More precisely, we will distinguish between

• (i) real truth-theoretic inferences, which are defined as inferences of the form

  $$\begin{aligned} \textrm{T} \ulcorner {\Gamma }\urcorner \Rightarrow \textrm{T} \ulcorner {\Delta }\urcorner , \end{aligned}$$

  where for a set of sentences $\Sigma$, $\textrm{T} \ulcorner {\Sigma }\urcorner =\{\textrm{T} \ulcorner {\sigma }\urcorner \mid \sigma \in \Sigma \}$,³⁰

• (ii) ideal truth-theoretic inferences, which are defined as those inferences

  $$\begin{aligned} \Gamma \Rightarrow \Delta \end{aligned}$$

  which are not real truth-theoretic inferences.

As for the distinction between real and ideal truth-theoretic reasoning, it depends upon the previously mentioned analogy with finitism. Real truth-theoretic reasoning is that reasoning that exploits only the reliable and intuitive principles of classical logic, while the rest will be considered ideal truth-theoretic reasoning.³¹ In other words, real truth-theoretic reasoning does not make use of $\lnot$L/R on formulae containing $\textrm{T}$.³²

Analogy with reductionist project. The last aspect combines the first two into a reductionist project. We suggest that ideal truth-theoretic reasoning should be reduced to real truth-theoretic reasoning, in the sense that the former should be conservative over the latter as far as real truth-theoretic inferences are concerned. To appreciate the motivation behind this requirement, suppose that $\mathcal {D}$ is a $\texttt{EXT}$-derivation of a real truth-theoretic inference $\textrm{T} \ulcorner {\Gamma }\urcorner \Rightarrow \textrm{T} \ulcorner {\Delta }\urcorner$, and suppose that $\mathcal {D}$ contains subderivations like $\mathcal {D'}$ below

The derivation $\mathcal {D'}$ makes use of ideal truth-theoretic reasoning, and the step involving $\lnot$L and cut is not “finitistically” (in the above sense) acceptable. So why should we trust in derivations such as $\mathcal {D}$ and take $\textrm{T} \ulcorner {\Gamma }\urcorner \Rightarrow \textrm{T} \ulcorner {\Delta }\urcorner$ to be philosophically acceptable? The reductionist project, then, amounts to requiring that whenever $\textrm{T} \ulcorner {\Gamma }\urcorner \Rightarrow \textrm{T} \ulcorner {\Delta }\urcorner$ is derivable in $\texttt{EXT}$, then the same sequent should be derivable in $\texttt{EXT}$ only via reliable and intuitive methods, hence without use of $\lnot$L/R.³³

A virtue of the program just outlined is that it can be tested formally, as its success or its failure depend on whether the following holds: if $\texttt{EXT} \vdash \textrm{T} \ulcorner {\Gamma }\urcorner \Rightarrow \textrm{T} \ulcorner {\Delta }\urcorner$, then there is a $\texttt{EXT}$-derivation $\mathcal {D}$ of $\textrm{T} \ulcorner {\Gamma }\urcorner \Rightarrow \textrm{T} \ulcorner {\Delta }\urcorner$ such that there is no application of $\lnot$L/R on formulae containing $\textrm{T}$. This is precisely the content of the following

Proposition 3.1

(Main Observation) If $\texttt{EXT} \vdash \textrm{T} \ulcorner {\Gamma }\urcorner \Rightarrow \textrm{T} \ulcorner {\Delta }\urcorner$, then there is a $\texttt{EXT}$-derivation of $\textrm{T} \ulcorner {\Gamma }\urcorner \Rightarrow \textrm{T} \ulcorner {\Delta }\urcorner$ in which every application of $\mathrm {\lnot L}$ and $\mathrm {\lnot R}$, if any, are on formulae not containing $\textrm{T}$.

In order to sketch a proof, let us first recall a well-known fact about theories such as $\texttt{EXT}$:

Lemma 3.2

(Partial Cut Elimination) Given a $\texttt{EXT}$-derivation $\mathcal {D}$ of $\Gamma \Rightarrow \Delta$, one can effectively transform $\mathcal {D}$ into a derivation $\mathcal {D'}$ of the same endsequent, such that the only applications of the rule cut in $\mathcal {D'}$, if any, are on atomic formulae.

Derivations in which cuts are on atomic formulae only are called quasi-normal derivations.

Proof sketch of Proposition 3.1

One can actually prove a stronger claim. Given a formula A in negation normal form,³⁴ call A positive if it only contains positive occurrences of $\textrm{T}$, where an occurrence of $\textrm{T}$ is positive if it falls within an even number of $\lnot$, if any. Call a sequent $\Gamma \Rightarrow \Delta$ positive if it contains only positive formulae (note that $\textrm{T} \ulcorner {\Gamma }\urcorner \Rightarrow \textrm{T} \ulcorner {\Delta }\urcorner$ is a positive sequent). Then, by induction on the height of derivations, one can show that, for any positive sequent $\Gamma \Rightarrow \Delta$, if $\texttt{EXT} \vdash \Gamma \Rightarrow \Delta$, then there is a $\texttt{EXT}$-derivation of $\Gamma \Rightarrow \Delta$ in which every application of $\mathrm {\lnot L}$ and $\mathrm {\lnot R}$, if any, are on formulae not containing $\textrm{T}$. To see this, let $\mathcal {D}$ be a $\texttt{EXT}$-derivation of a positive sequent $\Gamma \Rightarrow \Delta$. Without loss of generality, by Lemma 3.2 we can assume that $\mathcal {D}$ is quasi-normal. By quasi-normality of $\mathcal {D}$, we can exclude that the derivation contains occurrences of formulae $\lnot \textrm{T} \ulcorner {A}\urcorner$, as they would otherwise be subformulae of some formula of the endsequent $\Gamma \Rightarrow \Delta$, which is impossible by positivity of $\Gamma \Rightarrow \Delta$. It then follows that $\mathcal {D'}$ has no subderivations such as

To put it more intuitively: since positive sequents $\Gamma \Rightarrow \Delta$ do not contain occurrences of formulae $\lnot \textrm{T} \ulcorner {A}\urcorner$, and since in normal derivations formulae such as $\lnot \textrm{T} \ulcorner {A}\urcorner$ cannot be deleted via cut (nor be “merged” into a positive formula $\textrm{T} \ulcorner {B}\urcorner$, as $\textrm{T}$ and $\lnot$ do not commute), it follows that to derive a positive sequent we do not need the rules $\lnot$L/R.

Proposition 3.1 shows that the reductionist project can be successful: as far as real truth-theoretic inferences are concerned, ideal truth-theoretic reasoning is conservative over real truth-theoretic reasoning. This means that it is dispensable. We do not need it to obtain real truth-theoretic inferences. Every inference $\textrm{T} \ulcorner {\Gamma }\urcorner \Rightarrow \textrm{T} \ulcorner {\Delta }\urcorner$ derivable in $\texttt{EXT}$ is derivable in $\texttt{EXT}$ without $\lnot$L/R. This, arguably, provides a fairly robust justification for the use of classical logic, as it shows that ideal truth-theoretic reasoning is just a very useful tool. While dispensable, the use of $\lnot$L/R in combination with cut makes our life easier, as these rules simplify and abbreviate derivations. Not using them could increase the length of our derivations super-exponentially.³⁵ However, once we make sure that our instrument is reliable, that it does not yield wrong conclusions, that the real truth-theoretic inferences it yields are philosophically sound, there seems to be no good reason not to make use of it.

4 The costs of nonclassical logics, classical recapture, and nonclassical recapture

As mentioned in the introduction, nonclassical logicians often maintain that nonclassical truth-theories are conceptually superior to classical theories. Nonclassical theories, unlike classical counterparts, deal adequately with paradoxical phenomena and embody the transparency of truth. Defenders of classical logic often respond that weakening classical logic is too high a price to pay. Important parts of the reasoning apparatus available to the classical logician cannot be carried out in nonclassical theories, and it is well-known that nonclassical logics are generally weaker than classical logic (see e.g. Feferman (1984); Halbach (2014); Halbach and Nicolai (2018)). In reply to the charge of deductive weakness, some nonclassical logicians employ the idea of classical recapture. While there are various forms of recapture claims in the literature—see e.g. Field (2008); Beall (2013); Hjortland (2017); Fiore and Rosenblatt (2023)—the underlying idea is that nonclassical theories do not reject classically valid principles across the board. In normal conditions, e.g. when dealing with unproblematic sentences such as “snow is white” or “it is true that $\mathtt {2+2=4}$”, classical reasoning is preserved. It is only in some abnormal circumstances, typically those involving some paradoxical liar-like sentence, that we need a weaker logic. In general, the idea defended by the nonclassical logician is that whenever our domain of discourse consists entirely of unparadoxical sentences, we can reason classically. Hence the name ‘classical recapture’: we can recapture classical reasoning whenever needed.³⁶

Setting aside the issue of whether classical recapture is a viable strategy at all,³⁷ what we would like to emphasise is that in this debate classical and nonclassical logicians both seem to bite a bullet. The former seems to grant that nonclassical logic can give us theories which are conceptually more adequate, but they point out that the incision on classical logic delivers a bigger bullet to bite, namely deductive weakness. The latter seems to concede that classical reasoning is fundamentally correct, even when we reason about truth-theoretic statements not involving paradoxes (such as “is is true that $\mathtt {2+2=4}$”), and the fact that classical reasoning can be restored whenever needed is presented as a virtue of their systems.

The present article offers, we believe, a new perspective on this issue. The instrumentalist justification of classical logic outlined above could also serve as a nonclassical recapture strategy. It offers a defence of classical logic that does not appeal to the deductive weakness of nonclassical logics. Rather, it appeals to the reliability of the instrument. One can concede that classical logic is flawed in semantic contexts, and that a coherent concept of type-free truth is governed by nonclassical logic. Nonetheless, the classical logician can point out that the nonclassical truth-theoretic reasoning can be recaptured within classical theories whenever needed, that is, whenever we are talking about real truth-theoretic inferences.³⁸ Differently put, we can recapture “the correct way of reasoning about truth” ($\texttt{FDE}$, in the present case study³⁹ ) within a system based on classical logic. Not only can we prove the same real truth-theoretic inferences $\textrm{T} \ulcorner {\Gamma }\urcorner \Rightarrow \textrm{T} \ulcorner {\Delta }\urcorner$ but we can reason about them just as we do in a system based on $\texttt{FDE}$. We can reach the same conclusions using the same reliable and intuitive methods.

5 Open questions and possible extensions

There are several ways to extend the present investigation. Let us mention a few of them.

The first possible extension consists in verifying whether similar results hold for other nonclassical logics as well. In particular, one could study what happens with extensions of $\texttt{FDE}$ and with substructural logics. In this respect, note that the nonclassical logics used in the context of truth theories are all a fragment of classical logic. That fragment, from that point of view, can be taken to be the real truth-theoretic reasoning—which is reliable and intuitive. In light of the above, it seems then natural to investigate further whether classical logic can always recapture the relevant part of nonclassical reasoning. That is, given a nonclassical logic L, and given a class $\Phi$ of L-real truth theoretic inferences, one has to verify whether classical logic is conservative over L relative to $\Phi$. The more conservativity results one gets, the stronger the instrumental defence of classical logic becomes.

A second extension concerns the base theories. We have here worked with the induction-free arithmetical base theory Robinson arithmetic Q. But one should check whether the above results are (un)stable over (i) arithmetical theories having some induction schema as a rule of inference⁴⁰ and/or (ii) theories formalizing syntax in alternative ways.

Third, it would be interesting to see whether the same observations can be made for related paradox-breeding concepts that are taken to satisfy some naive schemata, for instance validity, property instantiation, membership.

Fourth, under the assumption that type free truth is governed by $\texttt{FDE}$, it has been argued that the advocates of $\texttt{EXT}$ and $\texttt{INT}$ should agree in considering the $\lnot$L/R-free fragment of classical logic, say $\texttt{CL} ^-$ reliable and intuitive. Digging deeper within the analogy with Hilbert’s instrumentalism, one can investigate whether there is a foundational justification of $\texttt{CL} ^-$. That is, a truth-theoretic view showing that $\texttt{CL} ^-$ is absolutely reliable and intuitive, just like a foundational view in mathematics does for Hilbert’s program.⁴¹

Last but not least, one could try to quantify just how useful classical reasoning is. Let $\textrm{T} \ulcorner {\Gamma }\urcorner \Rightarrow \textrm{T} \ulcorner {\Delta }\urcorner$ be such that $\texttt{EXT} \vdash \textrm{T} \ulcorner {\Gamma }\urcorner \Rightarrow \textrm{T} \ulcorner {\Delta }\urcorner$, and let $\mathcal {D}$ be a $\texttt{EXT}$-derivation of $\textrm{T} \ulcorner {\Gamma }\urcorner \Rightarrow \textrm{T} \ulcorner {\Delta }\urcorner$, possibly using $\lnot$L/R, such that $\mathcal {D}$ is of minimal height (that is, suppose that there is no derivation of $\textrm{T} \ulcorner {\Gamma }\urcorner \Rightarrow \textrm{T} \ulcorner {\Delta }\urcorner$ shorter than $\mathcal {D}$). Proposition 3.1 implies that we can transform $\mathcal {D}$ into a derivation $\mathcal {D'}$ with the same endsequent, such that $\mathcal {D'}$ does not use $\lnot$L/R, except possibly on formulae not containing $\textrm{T}$. Letting $\mathcal {D'}$ be of minimal height as well (that is, suppose that there is no $\lnot$L/R-free derivation of $\textrm{T} \ulcorner {\Gamma }\urcorner \Rightarrow \textrm{T} \ulcorner {\Delta }\urcorner$ shorter than $\mathcal {D'}$), what is the height difference between $\mathcal {D}$ and $\mathcal {D'}$? As already mentioned (see footnote 35), the argument for Proposition 3.1 relies on partial cut elimination, which yields a super-exponential increase of the height of the original derivation. However, whether this upper bound coincides with the lower bound is not obvious. Depending on the outcome, one could establish whether ideal reasoning gives us nonelementary speed-up over real reasoning.