1 Introduction↩︎

In an ideal world, semantic and proof-theoretic methods go hand in hand: after all, the first-order completeness theorem tells us that r.e. first-order theories can be characterized one way or the other. Yet, in practice the methods come apart. When working semantically one often focuses on intended models rather than arbitrary models of the language. If we then consider the theories of these intended models, we typically end up with a non r.e. set of sentences, that is, the set of sentences will not be axiomatizable. A prominent example of this mismatch between semantics and proof-theory arises in theories of truth. If one attempts to characterize the truth predicate semantically, one typically defines the (an) interpretation and the resulting truth theory is thus non-axiomatizable.

Nonetheless, axiomatic theories have been proposed as axiomatizations of certain semantic truth theories; for instance, the axiomatic truth theory \(\mathrm{KF}\) from [1] has been proposed as an axiomatization of the Strong Kleene version of Kripke’s theory of truth [2]. The question then arises: according to which criteria can \(\mathrm{KF}\) be considered as an axiomatization of Kripke’s theory of truth? And, more generally, when can an axiomatic truth theory be considered to axiomatize a non r.e. semantic truth theory? This question was addressed by [3], who propose a number of criteria to this effect. Arguably, amongst these criteria, \(\mathbb{N}\)-categoricity stands out as particularly compelling: an axiomatic theory \(\Sigma\) is an \(\mathbb{N}\)-categorical axiomatization of a semantic theory \(\mathrm{Th}_\mathfrak{M}\), where \(\mathfrak{M}\) is a class of interpretations of the truth predicate defined over the standard model \(\mathbb{N}\), iff \[\begin{align} \label{eq:ncat}(\mathcal{N},S)\vDash\Sigma&\text{ iff }S\in\mathfrak{M}. \end{align}\tag{1}\] Indeed, the theory \(\mathrm{KF}\) is an \(\mathbb{N}\)-categorical axiomatization of Kripke’s theory of truth, that is, a set \(S\subseteq\omega\) is an interpretation of the truth predicate of \(\mathrm{KF}\) over the standard model iff \(S\) is a fixed point of the Strong Kleene jump \(\mathrm{SK}\): \[\begin{align} (\mathcal{N},S)\vDash\mathrm{KF}\text{ iff }\mathrm{SK}(S)=S. \end{align}\] Whilst it might have its limitations, the criterion of \(\mathbb{N}\)-categoricity is surely part of answering the question of whether a given axiomatic truth theory counts as an axiomatization of a given semantic truth theory.¹

It may then come as a surprise that there are semantic truth theories that are not amenable to an \(\mathbb{N}\)-categorical axiomatization, i.e., to which the criterion of \(\mathbb{N}\)-categoricity is inapplicable. Indeed both the revision theory of truth (see, e.g., [4]) but also Kripke’s theory of truth in its supervaluational variant are examples of such theories.² The reason is that the definition of the respective class of (intended) models is too complicated in the recursion-theoretic sense: satisfaction (the left side of the biconditional 1 ) can be defined by a \(\Delta^1_1\)-formula of the language of second-order arithmetic. By contrast, the definition of the respective class of models (the right side of the biconditional) requires a \(\Pi^1_1\)-formula in the case of the supervaluation scheme – and even more complicated formulae in the case of the revision theory or Field’s theory. This observation entails that well-known theories intended to axiomatize supervaluational truth, notably the theory \(\mathrm{VF}\) from [6], are not \(\mathbb{N}\)-categorical axiomatizations of the supervaluational version of Kripke’s truth theory.

The lack of an \(\mathbb{N}\)-categorical axiomatization of the supervaluational version of Kripke’s truth theory was one of the key aspects that motivated [7]. In essence, he proposed the following:

The SSK-thesis: there is a fixed-point semantics that captures the essential aspects of the supervaluational schema whilst limiting its recursion-theoretic complexity, hence resulting in an \(\mathbb{N}\)-categorical axiomatization.

Indeed, [7] puts forward such a semantics, supervaluation-style truth, based on a satisfaction scheme that he calls \(\mathrm{SSK}\) – for ‘supervaluational Strong Kleene’. Moreover, Stern proposes an axiomatic truth theory, which he labels \(\mathrm{IT}\), and which he alleges to be an \(\mathbb{N}\)-categorical axiomatization of Kripke’s truth theory based on the scheme \(\mathrm{SSK}\).

Of course, the SSK thesis is somewhat vague, since we haven’t specified what the ‘essential aspects’ of the supervaluational schema are. This can be clarified as follows. The starting point of Stern’s analysis was the observation that the supervaluation schemata \[\begin{align} (\mathbb{N},S)\vDash_{s}\varphi&\text{ iff }\forall S'\supseteq S(\Phi(S')\Rightarrow (\mathbb{N},S')\vDash\varphi), \end{align}\] where \(\Phi\) is an \(\mathcal{L}_\mathrm{Tr}\)-definable condition with parameters, can be understood as collecting classical consequences of the set of sentences Strong Kleene grounded in \(S\) over the standard model: \[\exists G(S\vDash_\mathrm{sk}G\,\&\,\forall S'\supseteq S(\Phi(S')\,\&\,(\mathbb{N},S')\vDash G\Rightarrow (\mathbb{N},S')\vDash\varphi).\footnotemark\] The correspondence between the two characterization holds as long as \(\Phi\) forces a precisification \(S'\) to be consistent with the starting hypothesis \(S\), that is, as long as \(\Phi(S')\) entails that \(\{\varphi\,|\,\neg\varphi\in S\}\cap S'=\emptyset\).³ In particular, the supervaluation schemata \(\mathrm{VB,VC,MC}\) discussed below can be viewed as collecting classical second-order consequences of the set of Strong Kleene truths over the hypothesis \(S\).

Stern observed that, instead of taking classical consequences of \(G\) relative to a specific class of truth models over the standard model, one can simply consider the classical first-order consequences of the Strong Kleene-grounded sentences. This constitutes the SSK satisfaction scheme, and gives rise to what Stern called supervaluation-style semantics. This approach would lead to a significant reduction of the recursion-theoretic complexity and would even give rise to an arithmetically definable jump (or so he argued). Specifically, [7] claimed that the fixed points of the \(\mathrm{SSK}\)-scheme are the fixed points of a first-order arithmetical operator \(\Theta\) (cf. Definition 1), and that the \(\mathrm{SSK}\) schema has an \(\mathbb{N}\)-categorical axiomatization in the form of the theory \(\mathrm{IT}\). In addition, under these assumptions, he showed that the \(\mathrm{SSK}\)-scheme has the same minimal fixed point as the supervaluation scheme.

This reconstruction gives us a precise way of understanding the SSK thesis: the preservation of ‘essential aspects’ of the supervaluational scheme amounts to recovering all first-order penumbral truths of classical logic and arithmetic, something that one would hope to retain when moving from second-order to first-order formulations of the supervaluational schema.

Unfortunately, as we show in this paper, the SSK thesis hasn’t been successfully realized by [7] since some of Stern’s reasoning was flawed. Specifically:

• the fixed points of the operator associated with the \(\mathrm{SSK}\)-schema and \(\Theta\) constitute two distinct classes of fixed points;

• the fixed points of the \(\mathrm{SSK}\)-schema are in general not closed under the \(\omega\)-rule;

• as a consequence, the minimal fixed point of the \(\mathrm{SSK}\)-schema and the supervaluation scheme differ;

• the theory \(\mathrm{IT}\) is not \(\mathbb{N}\)-categorical with respect to \(\mathrm{SSK}\)-fixed points.

However, not all is lost and, as we show, the SSK-thesis can be vindicated, albeit in a less uniform way than argued in [7]. In fact, since the fixed points of the \(\mathrm{SSK}\) schema and \(\Theta\) come apart, we end up with different semantic constructions – each of them recovering penumbral truths of classical logic and arithmetic – that enjoy \(\mathbb{N}\)-categorical axiomatizations in virtue of their lower recursion-theoretic complexity.⁴ The choice forced upon us is essentially as follows. We can stick to the well-motivated \(\mathrm{SSK}\) schema but lose the desirable closure under \(\omega\)-logic. As a consequence, the universal quantifier will not commute with the truth predicate in \(\mathbb{N}\)-categorical axiomatizations of the \(\mathrm{SSK}\) schema. Alternatively, we can adopt a more ‘standard’ arithmetical jump with familiar closure conditions. However, the arithmetical jump will, in contrast to the \(\mathrm{SSK}\) schema and its associated operator, “merely” collect consequences of a given truth set/hypothesis rather than submitting the hypothesis to semantic scrutiny. This undermines the philosophical and semantic motivation underlying supervaluational-style semantics and leads to some undesirable formal features (e.g. failure of what will be called ‘classical soundness’).

In the paper we will study the classes of models given by fixed points of \(\mathrm{SSK}\), \(\Theta\), and \(\Theta^*\) – a variant of \(\Theta\) equipped with additional closure properties. We will also provide \(\mathbb{N}\)-categorical axiomatizations for each of them – as we have seen, a highly desirable feature. After describing some preliminaries in Section 2 and Section 3, we isolate some gaps and problems in the previous attempt to realize the SSK thesis by [7] in Section 4. These include \(\mathrm{SSK}\)’s failure to be closed under \(\omega\)-logic. Section 5 provides two \(\mathbb{N}\)-categorical axiomatizations of \(\mathrm{SSK}\), that we will dub \(\mathrm{PK}\) and \(\mathrm{PK}^+\). We then move to the study of \(\Theta\) and its variation \(\Theta^*\): Section 6 presents \(\mathbb{N}\)-categorical axiomatizations for (the fixed points of) each operator, and establishes lower-bounds for their proof-theoretic strength. Section 7 draws connections between supervaluation-style fixed-point semantics and the standard supervaluational approaches: although the minimal fixed points of \(\mathrm{VB}\) (a class of supervaluational fixed points that imposes a weak consistency condition), \(\Theta\) and \(\Theta^*\) coincide, this is not true for all fixed points. In fact, every \(\mathrm{VB}\) fixed point is a \(\Theta^*\), and hence a \(\Theta\) fixed point, but the converse provably fails. We conclude by assessing the results presented in the paper along some key dimensions.

2 Preliminaries and notation↩︎

2.1 Language, Theories, Coding↩︎

Our notation follows, for the most part, the conventions in [9]. We will be working with languages whose logical symbols are \(\neg, \vee, \wedge, \forall, \exists\). We also write \(\varphi \rightarrow \psi\) as an abbreviation for \(\neg \varphi \vee \psi\). As a default practice, our base language \(\mathcal{L}_\mathbb{N}\) is a definitional extension of the language of Peano Arithmetic (\(\mathrm{PA}\)) with finitely many function symbols for primitive recursive functions. We assume a standard formalization of the syntax of first-order languages as it is for instance carried out in [10]. The expression \(\Bar{n}\) stands for the numeral of the number \(n\) (although we omit the bar for specific numbers). We write \(\# \varphi\) for the code or Gödel number of \(\varphi\), and \(\ulcorner \varphi\urcorner\) for the numeral of that code. \(\mathcal{L}_\mathbb{N}\) is assumed to contain a finite set of function symbols that will stand for certain primitive recursive operations. In particular, we want to include function symbols for some primitive recursive syntactic operations on expressions of the language under consideration; for that, we use the traditional subdot notation. For example, \(\oalign{\neg\cr\hfil.\hfil}\) is the function symbol for the primitive recursive operation that, when inputted the code of a formula, yields the code of its negation. The same applies to \(\oalign{\vee\cr\hfil.\hfil}, \oalign{\forall\cr\hfil.\hfil}, \oalign{\wedge\cr\hfil.\hfil}, \oalign{\exists\cr\hfil.\hfil}\). We assume a function symbol for the substitution function, and write \(x (t/v)\) for the result of formally substituting \(v\) with \(t\) in \(x\); \(\ulcorner \varphi(\dot{x})\urcorner\) abbreviates \(\ulcorner \varphi (v)\urcorner (\mathrm{num}(x)/\ulcorner v\urcorner)\), for \(x\) a term variable (and provided \(\varphi\) only has one free variable) and \(\mathrm{num}(x)\) the function symbol corresponding to the operation of sending a number to its numeral. Furthermore, we avail ourselves to the notation \(t^\circ\) for the result of applying to a term \(t\) the evaluation function (which outputs the value of the inputted term). Note that \(\cdot^\circ\) is an abbreviation for a formula, and not a term of the language. The development of syntax just mentioned can be comfortably carried out in Peano arithmetic \((\mathrm{PA})\), which will be our background theory of syntax.

For the formulation of the theories of truth, we will (mostly) be concerned with the extension of \(\mathcal{L}_\mathbb{N}\) with a (unary) truth predicate \(\mathrm{Tr}\). \(\mathrm{PAT}\) is then the theory formulated in the language \(\mathcal{L}_\mathrm{Tr}\) consisting of the axioms of \(\mathrm{PA}\) with induction extended to the whole language. We will then write \(\mathrm{Var}_{\mathcal{L}_\mathrm{Tr}}(x)\) for the formula representing the set of (codes of) variables, \(\mathrm{CT}_{\mathcal{L}_\mathrm{Tr}}(x)\) for the formula representing the set of (codes of) closed terms of \({\mathcal{L}_\mathrm{Tr}}\), \(\mathrm{For}_{\mathcal{L}_\mathrm{Tr}}(x)\) (\(\mathrm{For}_{\mathcal{L}_\mathrm{Tr}}(x,y_0,...,y_n)\)), for the formula representing the set of all formulae (formulae with \(y_0,...y_n\) free) of \({\mathcal{L}_\mathrm{Tr}}\), and \(\mathrm{Sent}_{\mathcal{L}_\mathrm{Tr}}(x)\), for the formula representing the set of all sentences of \({\mathcal{L}_\mathrm{Tr}}\). We also use \(\mathrm{Var}_{\mathcal{L}_\mathrm{Tr}}\), \(\mathrm{CT}_{\mathcal{L}_\mathrm{Tr}}\), \(\mathrm{For}_{\mathcal{L}_\mathrm{Tr}}\), and \(\mathrm{Sent}_{\mathcal{L}_\mathrm{Tr}}\) to stand for the sets corresponding to these formulae. We will occasionally omit reference to \({\mathcal{L}_\mathrm{Tr}}\) when this is clear from the context. We often quantify over variables \(s,t\) to refer to codes of closed terms, so that \(\forall t\,\varphi(t)\) is short for \(\forall x (\mathrm{CT}_{\mathcal{L}_\mathrm{Tr}}(x)\rightarrow\varphi(x))\).

We assume an appropriate ordinal notation system OT up to \(\Gamma_0\), and the ordinal less-than relation \(<\) on \(\Gamma_0\) (for more detailes, see, e.g., [11]). For simplicity, we identify each ordinal number with its notation. We use \(0\) as the ordinal number, the ordinal sum \(\alpha + \beta\), and the Veblen function \(\varphi_{\alpha}\beta\). Given a language \(\mathcal{L}\), an ordinal number \(\alpha < \Gamma_0\), and an \(\mathcal{L}\)-formula \(A\), transfinite induction for \(A\) up to \(\alpha\) is defined as the formula: \[\mathrm{TI}(\alpha, A):= \forall \beta (\forall \gamma < \beta A(\gamma) \to A(\beta)) \to \forall \beta < \alpha A(\beta).\] In line with the latter, the schema \(\mathrm{TI}_{\mathcal{L}}(<\alpha)\) is defined to be the set \(\{ \mathrm{TI}(\beta, A) \;|\;\beta < \alpha \;\& \;A \in \mathcal{L} \}\). Finally, if \(S\) is a theory, its proof-theoretic ordinal (denoted \(\vert S\vert\)) is the ordinal \(\alpha\) such that \(\mathrm{PA}+\mathrm{TI}_{\mathcal{L}_\mathbb{N}}(<\alpha)\) and \(S\) prove the same \(\mathcal{L}_\mathbb{N}\)-statements (and verifiably so within \(\mathrm{PA}\)). If \(T\), \(S\) are theories, we write \(\vert T\vert \geqq \vert S\vert\) to indicate that the proof-theoretic ordinal of \(T\) is equal or greater than the proof-theoretic ordinal of \(S\). Similarly, \(\vert T\vert \equiv \vert S\vert\) is defined as \(\vert T\vert \geqq \vert S\vert\) and \(\vert S\vert \geqq \vert T\vert\).

2.2 Supervaluations↩︎

In his seminal [2], Kripke proposes to determine the extension of the truth predicate via a fixed-point construction. Famously, this construction is carried out in Strong Kleene (SK) logic. However, SK fails to capture many penumbral truths, that is, truths that hold merely in virtue of the logical relations occurring between sentences of a language. An example of such a sentence is \(\lambda\vee\neg \lambda\), for \(\lambda\) the Liar sentence. As a remedy, Kripke in his paper also suggests to run the construction with some form of supervaluational logic. This will be our departure point. For \(X\subseteq \mathrm{Sent}_{\mathcal{L}_\mathrm{Tr}}\), we define \[\begin{align} \mathrm{CON}(X)&:=\neg \exists \varphi(\{\#\varphi,\#\neg\varphi\}\subseteq X);\\ \mathrm{MXC}(X)&:= \neg \exists \psi(\{\#\psi,\#\neg\psi\}\subseteq X\land (\forall \varphi(\#\varphi\notin X \rightarrow\#\neg \varphi\in X))). \end{align}\] \(\mathrm{MXC}(X)\) expresses that \(X\) is a maximally consistent set of \(\mathcal{L}_\mathrm{Tr}\)-sentences.

For a satisfaction relation \(e\), we will write \(X \vDash_{e} A\) to abbreviate \((\mathbb{N},X, X^-)\vDash_{{e}} A\), where \(X\subseteq \mathrm{Sent}_{\mathcal{L}_\mathrm{Tr}}\) is the relevant interpretation of the truth predicate and \(X^-\) is defined as \(\{\#\varphi\;|\;\#\neg\varphi\in X\}\cup \{n\in\omega\;|\;\mathbb{N}\vDash \neg \mathrm{Sent}_{\mathcal{L}_\mathrm{Tr}}(\bar n)\}\). Similarly, for the classical satisfaction relation (\(\vDash\)), \(X\vDash A\) just stands for \((\mathbb{N}, X)\vDash A\). In the literature, one often distinguishes the following supervaluational satisfaction relations: \[\begin{align} \tag{2}X\vDash_\mathrm{sv} \varphi & \text{ iff }\forall X' (X'\supseteq X \Rightarrow X' \vDash \varphi)\\ \tag{3} X\vDash_\mathrm{vb} \varphi &\text{ iff } \forall X' (X'\supseteq X \, \&\, X' \cap X^- =\varnothing \Rightarrow X' \vDash \varphi)\\ X\vDash_\mathrm{vc} \varphi &\text{ iff } \forall X' (X'\supseteq X\, \&\, \mathrm{CON}(X') \Rightarrow X' \vDash \varphi)\\ \tag{4} X\vDash_\mathrm{mc} \varphi &\text{ iff } \forall X' (X'\supseteq X\, \&\, \mathrm{MCX}(X') \Rightarrow X' \vDash \varphi) \end{align}\] To avoid triviality, and following the truth-theoretic literature on supervaluationism, we are mainly interested in consistent set of sentences. For \(\mathrm{CON}(X)\) and \(j\in \{\mathrm{sv, vb, vc, mc}\}\), we let: \[J(X):=\{\#\varphi\;|\;\, X\vDash_j \varphi\}\]

\(J(\cdot)\), for \(J\in \{\mathrm{SV, VB, VC, MC}\}\), is the J-supervaluational jump. It can be checked that, for arbitrary \(X\subseteq \mathrm{Sent}_{\mathcal{L}_\mathrm{Tr}}\), the jump is monotone. It then follows by the theory of positive inductive definitions (see e.g. [12], [13]) that \(J(\cdot)\) has a fixed point, and in particular a minimal one obtained by iterating the operator over the empty set.

It is worth noting that, to establish the existence of non-trivial fixed points, we need a further property to guarantee that at every stage of the inductive definition we can find an admissible precisification. Otherwise triviality ensues. One property that guarantees the existence of non-trivial fixed points is to require the admissibility condition to be compact on the set of consistent interpretations: let \(X:=\{S\,|\,\mathrm{CON}(S)\}\) , \(\Phi^S:=\{S'\,|\,S\subseteq S'\,\&\,\Phi(S')\}\) and for \(Y\subseteq X\) set \(\Phi(Y):=\{\Phi^S\,|\,S\in Y\}\). Then \(\Phi\) is compact on \(X\) iff for all \(Y\subseteq X\): \[\text{if }\Phi^{S_1}\cap\ldots\cap\Phi^{S_n}\neq\emptyset\text{ for all }S_1,\ldots S_n\in Y\text{ and all }n\in\omega,\text{ then }\bigcap\Phi(Y)\neq\emptyset.\] The admissibility condition associated with the schemes \(\mathrm{SV, VB, VC, MC}\) are compact in that sense.

3 Supervaluation-style truth↩︎

While Kripke’s fixed-point semantics over supervaluational logics succeeds in recovering all penumbral truths, the theory is not free from objections. As argued in [7] supervaluational truth fails to be compositional and, because of its recursion-theoretic complexity, is not \(\mathbb{N}\)-categorically axiomatizable. Accordingly, Stern develops a new theory of truth, which he calls supervaluational-style truth, aimed at addressing some of these shortcomings.

As we have seen, to address such worries Stern notes that supervaluation satisfaction involves recognizable Strong-Kleene and classical components. Stern studies a monotone evaluation schema isolating these two elements of supervaluational satisfaction: \[\label{eq:sskst} X\vDash_\mathrm{ssk}\varphi \text{ iff } \exists \psi(X\vDash_\mathrm{sk}\psi \text{ and } \mathrm{PAT}\vdash \psi\rightarrow \varphi)\tag{5}\] In the definition of \(\vDash_\mathrm{ssk}\), \(\vDash_\mathrm{sk}\) is the familiar definition of satisfaction in Strong Kleene logic for \(\mathcal{L}_\mathrm{Tr}\). For \(X\subseteq \omega\) consistent, the Strong-Kleene supervaluational jump is then: \[\mathrm{SSK}(X):=\{\#\varphi\;|\;\, X\vDash_\mathrm{ssk}\varphi\}.\] The jump is monotone, and therefore will have fixed points, including a minimal one.

To study the Strong-Kleene supervaluational jump, Stern also introduces a related jump based on a positive inductive definition in \(\mathcal{L}_\mathbb{N}\) (with parameters).

Stern provides arguments to show that (i) the fixed points of \(\mathrm{SSK}\) and \(\Theta\) coincide and, making crucial use of (i), that (ii) there is an \(\mathbb{N}\)-categorical (in the sense of [3]) axiomatization of those fixed points. To achieve (ii), Stern introduces the following theory.

As it turns out the argument in support of (i) was flawed and, as a consequence, neither (i) nor (ii) can be achieved.

4 Supervaluational-style truth: some problems↩︎

Stern tried to establish that the fixed points of SSK and \(\Theta\) coincide, i.e., that \(S=\Theta(S) \Leftrightarrow S=\mathrm{SSK}(S)\). However, the proof relied on the mistaken assumption that \(\Theta(S)\subseteq \mathrm{SSK}(S)\) for any consistent set of formulas \(S\) (see [7]). This fails for the following reason. We say that a set \(X\subseteq \omega\) is sound with respect to some operator \(\mathcal{J}:\mathcal{P}(\omega)\longrightarrow \mathcal{P}(\omega)\) when \(X\subseteq \mathcal{J}(X)\). Then, the above failure is to be located in the fact that any set of formulas is sound with respect to \(\Theta\), and this does not happen for \(\mathrm{SSK}\)—not even when the set of formulas is consistent.

Proposition 3 immediately entails that iterations of \(\Theta\) over any \(X\subseteq \omega\) reach a fixed point. These fixed points may turn out to be rather ill-behaved – even if we focus on the non-trivial, consistent fixed points:

The proposition entails the key property of classical soundness (cf. Def. 7) does not obtain for all \(\Theta\) fixed-points. Classical soundness will play a prominent role in what follows.

Proposition 3 fails for SSK. By taking, for instance, \(S=\{\#\tau_0\vee\tau_1\}\), where \(\tau_0\) and \(\tau_1\) are truth-tellers, one can immediately see that \(S\nsubseteq \mathrm{SSK}(S)\). However, although none of the problems above apply to \(\mathrm{SSK}\) fixed points, the latter are not very attractive either, as they are not closed under \(\omega\)-logic, a basic feature of SK fixed points.

The issues above also imply that Stern’s theory \(\mathrm{IT}\) is not an \(\mathbb{N}\)-categorical axiomatization of the fixed points of either SSK or \(\Theta\). In particular:

Although, by [Tout] and [Tnegdel] of Proposition 6, \(\Theta\) cannot be categorically axiomatized by \(\mathrm{IT}\), some fixed points of \(\Theta\) are still models for \(\mathrm{IT}\). In particular, all fixed points that are classically sound, \(\mathrm{Tr}\)-downwards closed, and \(\neg \mathrm{Tr}\)-downwards closed, will be models of \(\mathrm{IT}\) (cf. Proposition 20). Since these notions will play a prominent role in what follows, we provide precise definitions for them.

Proposition 4 showed that some \(\Theta\) fixed points are not \(\mathrm{Tr}\)-downwards closed, and hence not classically sound, and some are not \(\neg\mathrm{Tr}\)-downwards closed. This being said, some \(\Theta\) fixed points meet all the conditions: they are classically sound, \(\mathrm{Tr}\)- and \(\neg\mathrm{Tr}\)-downwards closed. One such fixed point is the minimal fixed point.

5 The \(\mathbb{N}\)-categoricity of SSK↩︎

One major difficulty in achieving an \(\mathbb{N}\)-categorical axiomatization for \(\mathrm{SSK}\)-fixed points is the inexpressibility, in first-order logic, of the notion of (Strong Kleene) satisfaction built in its definition. The satisfaction relation is hyperarithmetical, and hence inexpressible in \(\mathcal{L}_\mathrm{Tr}\). This does not exclude, however, that there may be ways of capturing enough of Strong-Kleene satisfaction to obtain an extensionally correct characterization of \(\mathrm{SSK}\)-fixed points. In this section we provide one such axiomatization.

By the diagonal lemma, \(\mathrm{PAT}\) proves that there is a formula \(\pi(x)\) such that: \[\begin{align} \pi(x)\leftrightarrow& \mathrm{True}_0(x)\vee\\ & \exists t( x=\oalign{\mathrm{Tr}\cr\hfil.\hfil}t\land \mathrm{Tr}t^\circ)\,\vee\\ & \exists t( x=\oalign{\neg\cr\hfil.\hfil}\oalign{\mathrm{Tr}\cr\hfil.\hfil}t\land (\mathrm{Tr}\oalign{\neg \cr\hfil.\hfil}t^\circ\vee \neg \mathrm{Sent}_{\mathcal{L}_\mathrm{Tr}}(t^\circ))\,\vee\\ &\exists y (x=\oalign{\neg\cr\hfil.\hfil}\oalign{\neg \cr\hfil.\hfil}y \land \mathrm{Tr}\ulcorner \pi(\dot{y})\urcorner)\,\vee\\ &\exists y,z(x=(y\oalign{\land \cr\hfil.\hfil}z)\land \mathrm{Tr}\ulcorner \pi(\dot{y})\urcorner)\land \mathrm{Tr}\ulcorner \pi(\dot{z})\urcorner)\\ &\exists y,z(x=\oalign{\neg\cr\hfil.\hfil}(y\oalign{\land \cr\hfil.\hfil}z)\land \mathrm{Tr}\ulcorner \pi(\oalign{\neg\cr\hfil.\hfil}\dot{y})\urcorner)\land \mathrm{Tr}\ulcorner \pi(\oalign{\neg\cr\hfil.\hfil}\dot{z})\urcorner)\\ &\exists y (x=\oalign{\forall \cr\hfil.\hfil}v y \land \forall t\,\mathrm{Tr}\ulcorner \pi(\dot{y}(t/v)\urcorner)\,\vee\\ &\exists y (x=\oalign{\neg \cr\hfil.\hfil}\oalign{\forall \cr\hfil.\hfil}v y \land \forall t\,\mathrm{Tr}\ulcorner \pi(\oalign{\neg\cr\hfil.\hfil}\dot{y}(t/v)\urcorner). \end{align}\]

Thus, the formula \(\pi(x)\) performs a standard iteration for truth ascriptions, but exploits the diagonal lemma to yield Strong Kleene compositionality in the case of logically complex formulae – in much the same way that the well-known definition of \(\mathrm{KF}\) over the theory \(\mathrm{PUTB}\) does (see, e.g., [9]).

The following result shows that, in a certain class of models, \(\pi(x)\) captures Strong-Kleene satisfaction:

For future use, we recall that, for \(\mathrm{Tr}\)-positive formulae, Strong-Kleene satisfaction and classical satisfaction coincide.

As the following lemma shows, the theory \(\mathrm{PK}\) has similar compositional properties as the theory \(\mathrm{IT}\) with the exception that the truth predicate does not commute with the universal quantifier.

Now, we establish the \(\mathbb{N}\)-categoricity results for \(\mathrm{SSK}\) fixed points:

We first prove (almost) one direction as a lemma:

In a sense, \(\mathrm{PK}\) amounts to the bare minimum required to establish its \(\mathbb{N}\)-categoricity with respect to \(\mathrm{SSK}\). We can extend the theory with principles that are independently justified and sound with respect to the intended semantics, and yet retain \(\mathbb{N}\)-categoricity. Principles that appear particularly natural are, on the one hand, a less artificial restriction of the naive \(\mathrm{Tr}\)-schema allowing disquotation for all \(\mathrm{Tr}\)-positive sentences; on the other, since the \(\mathrm{SSK}\)-fixed points over \(\mathbb{N}\) are classically sound, it is plausible to reflect this in the axiomatization by adding the schema \(\mathrm{Tr}\text{-}\mathrm{Out}\) to it.

\(\mathrm{PK}^+\) is also \(\mathbb{N}\)-categorical with respect to \(\mathrm{SSK}\). The argument above carries over with minor modifications: Lemma 4 still holds if one requires satisfiability of \(\mathrm{PUTB}\) instead of just \(\mathrm{TB}\pi\). This is enough, in the proof of Theorem 3, to show that fixed points of \(\mathrm{SSK}\) indeed satisfy \(\mathrm{PUTB}\).

Since \(\mathrm{PK}^+\) includes \(\mathrm{PUTB}\), it is proof-theoretically at least as strong as \(\mathrm{KF}\) or ramified truth up to \(\varepsilon_0\). \(\mathrm{IT}\) (see Def. 2) is clearly an upper bound for \(\mathrm{PK}^+\), but it’s evidently not sharp as the former has the same proof-theoretic strength of the theory of inductive definitions \(\mathrm{ID}_1\) [7]. It is an open question whether \(\mathrm{PK}^+\) has precisely the strength of \(\mathrm{PUTB}\). In addition, a full proof-theoretic analysis of \(\mathrm{PK}\) is lacking.

6 The \(\mathbb{N}\)-categorical axiomatization of \(\Theta\), \(\Theta^*\), and variations↩︎

6.1 \(\mathbb{N}\)-categorical axioms for \(\Theta\)↩︎

By Proposition 6, \(\mathrm{IT}\) isn’t \(\mathbb{N}\)-categorical with respect to the \(\Theta\) fixed points, but are there other axiomatic theories which are \(\mathbb{N}\)-categorical with respect to those fixed points? In this subsection, we answer that question in the affirmative.

Thus, the major differences between \(\mathrm{IT}^-\) and \(\mathrm{IT}\) are simply the exclusion of T-Out and of the right-to-left directions of axioms IT6 and IT7. Note that Axiom IT9 is provable from axioms IT1, IT2 and IT8.

We shall prove:

6.2 \(\Theta^*\) and \(\mathbb{N}\)-categorical axioms for it↩︎

Fixed points of \(\Theta\) are not very attractive though. The reason is that they are not necessarily Kripke-sets in the sense that \(\#\varphi\in X \Leftrightarrow \#\mathrm{Tr}\ulcorner \varphi\urcorner \in X\) and \(\#\neg\varphi\in X \Leftrightarrow \#\neg \mathrm{Tr}\ulcorner \varphi\urcorner \in X\). In particular, as we showed in Proposition 4, some fixed points will contain codes of sentences of the form \(\mathrm{Tr}\ulcorner \varphi\urcorner\), while not containing the code of \(\varphi\) – and similarly for \(\neg \mathrm{Tr}\ulcorner \varphi\urcorner\) and \(\neg\varphi\). This phenomenon is reflected in the absence of the right-to-left directions of \(\mathrm{IT}^-6\) and \(\mathrm{IT}^-7\) in \(\mathrm{IT}^-\). However, by tweaking the formula \(\xi(x,X)\) slightly, we can obtain a class of fixed points that are (\(\mathbb{N}\)-categorically) axiomatized by a theory which restores the missing components of the original \(\mathrm{IT6}\) and \(\mathrm{IT7}\):

We then define: \[\Theta^*(S):= \{ n\in\omega \;|\;\mathbb{N}\vDash \exists y (\xi^*(y,X) \wedge \mathrm{Pr}_{\mathrm{PAT}}(y\oalign{\rightarrow\cr\hfil.\hfil}x))[n,S]\}\] Note that, for any set \(S\), \(S\) is sound with respect to \(\Theta^*\) – just like with \(\Theta\). However, it follows immediately from the definition of \(\Theta^*\) that \(\Theta^*\) fixed points are Kripke sets:

It is now easy to see what theory characterizes \(\Theta^*\) fixed points \(\mathbb{N}\)-categorically:

\(\Theta^*\) does not impose any requirement on what the truth predicate looks like internally. In a way analogous to that of the different supervaluation schemes, however, we can also require that, internally, the truth predicate be consistent, or consistent and complete. This is done by defining new operators:

In light of our \(\mathbb{N}\)-categoricity result for \(\Theta^*\), the following is easily established:

6.3 Relationships between fixed points of \(\Theta\) and \(\Theta^*\)↩︎

We start by providing a general result about \(\Theta\) and \(\Theta^*\), which reveals that their constructions preserve classical soundness and, in the case of \(\Theta\), also \(\mathrm{Tr}\)- and \(\neg\mathrm{Tr}\)-downwards closure:

In the constructions above, we say that \(X\) is the starting set of the construction.

Next, we show that fixed points of \(\Theta^*\) are also fixed points of \(\Theta\). This is immediate by inspecting the definitions of \(\Theta\) and \(\Theta^*\):

By Proposition 4, there are fixed points of \(\Theta\) that are not \(\mathrm{Tr}\)- and \(\neg \mathrm{Tr}\)-downwards closed. However, \(\mathrm{Tr}\) and \(\neg \mathrm{Tr}\)-downwards closure are still not sufficient to yield the \(\mathbb{N}\)-categoricity of \(\mathrm{IT}\). There could still be complex sentences, such as \(\tau_0\vee \tau_1\), within \(\Theta^*\) fixed points, without their constituent sentences being there—which would violate \(\mathrm{Tr}\)-Out. However, if classical soundness is added as a condition on the fixed points, we obtain a more restricted class of fixed points that \(\mathrm{IT}\) can \(\mathbb{N}\)-categorically axiomatize.

6.4 Proof-Theory↩︎

\(\mathrm{IT}^*\) also enjoys considerable proof-theoretic strength. In particular, we can show that it is at least as proof-theoretically strong as the theory \(\mathrm{KF}\). The proof-theoretic strength will be obtained by defining ramified truth predicates, so we refer the reader to [9] for a definition of the relevant languages and systems. Instead of using \(\mathrm{IT}^*\), however, we will provide a more general result by using \(\mathrm{IT}^-\); since the latter is a subtheory of \(\mathrm{IT}^*\), the claim will follow immediately.

Just like in the case of \(\mathrm{PK}\), \(\mathrm{IT}^*, \mathrm{IT}^-\) are sub-theories of \(\mathrm{IT}\). However, a sharp proof-theoretic analysis of \(\mathrm{IT}^*, \mathrm{IT}^-\) is not yet available.

By contrast, the proof-theoretic analysis of \(\mathrm{IT}^*+\mathrm{Tr}\text{-Out}\) follows the one for \(\mathrm{IT}\) from [7]: the lower bound is provided by the provability of Bar-Induction in (a fragment of) \(\mathrm{IT}^*+\mathrm{Tr}\text{-Out}\), which is known to be sufficient to derive the arithmetical theorems of \(\mathrm{ID}_1\); for the upper bound argument, the strategy is to formalize in the theory \(\mathrm{KPU}\) the stages of the construction of the minimal fixed point of \(\Theta\), and establish the equivalence between membership in the fixed point and provability in the infinitary system defined in Proposition 8. Since, provably in \(\mathrm{KPU}\), \(\mathrm{I}_{\Theta}=\mathrm{I}_{\Theta^*}\), we can use such a provability predicate as an adequate interpretation for the truth predicate of \(\mathrm{IT}^*+\mathrm{Tr}\text{-}\mathrm{Out}\). That is:

7 Relations with standard supervaluationist fixed points↩︎

In this section we establish some connections between supervaluation-style fixed-point semantics and the standard supervaluational approaches. The aim is to draw a precise picture of the prospects and limitations of supervaluation-style semantics and its connection to standard supervaluational semantics.

Recall the schema \(\mathrm{VB}\) introduced in Section 2.2. It is easy to see that the minimal fixed points of \(\Theta\), \(\Theta^*\) and \(\mathrm{VB}\) coincide:

By contrast, it can be shown that the minimal fixed point is a proper subset of the least \(\mathrm{VB}\) fixed point—and, as a consequence, of the least fixed points of \(\Theta\) and \(\Theta^*\):

It is clear that some fixed points of \(\Theta\) are not VB fixed points. For instance, some fixed points of \(\Theta\) fail to be transparent for the truth predicate (Proposition 4). It is also clear that some \(\Theta^*\) fixed points are not VB fixed points: all fixed-point models of VB satisfy T-Out, but not all \(\Theta^*\) fixed points do.⁶ What if we restrict our attention to \(\Theta^*\) fixed-point models of T-Out, i.e., that are classically sound? In Proposition 20, we showed that those models are precisely the ones that satisfy \(\mathrm{IT}\). It then follows that the class of classically sound fixed points of \(\Theta^*\) cannot coincide with the class of supervaluational, VB fixed points. Otherwise, VB would have an \(\mathbb{N}\)-categorical axiomatization (namely, \(\mathrm{IT}\)), which we know isn’t the case by the complexity considerations described in the introduction.

There is more we can say about fixed points of VB and of \(\Theta^*\). First, that the class of VB fixed points is a subclass of the \(\Theta^*\) fixed points:

In fact, we can show that any least fixed point generated by a \(\mathrm{VB}\)-sound set corresponds to the least fixed point of \(\Theta\) generated from that set. To prove that, we need two observations.

Let us now examine in greater depth the connection between the class of classically sound \(\Theta^*\) fixed points and the \(\mathrm{VB}\) fixed points. First, let us denote: \[\mathcal{Z}:=\{ S \;|\;S=\Theta^*(S) \; \& \; S \; \text{is classically sound}\}\] We will consider this class of fixed points and refer to them in the usual terms. In particular, we say that some fixed point \(S\) is \(\mathcal{Z}\)-maximal iff there is no \(S'\in \mathcal{Z}\) s.t. \(S\subsetneq S'\). By adapting a result from [7] to the present setting, we can show that the \(\mathcal{Z}\)-maximal fixed points and the \(\mathrm{VB}\) maximal fixed points are not the same.

Notice that for the familiar operators considered in this paper, the existence of the maximal intrinsic fixed point follows from the existence of the relevant minimal fixed points, as these minimal fixed points are themselves intrinsic.

In fact, we can provide specific examples of simple fixed points that are in \(\mathcal{Z}\) but are not \(\mathrm{VB}\) fixed points. The following is a variation of an example we have used repeatedly:

The situation is very similar when we consider the operator \(\Theta_\mathrm{c}\) and the supervaluationist scheme VC. We omit the proofs of the following results, which are just reproductions of all proofs we have carried out for VB:

In the case of MC and \(\Theta^*_\mathrm{mc}\), it must be noted that the scheme MC is not itself classically sound. Therefore, we can forget about that aspect when establishing their relations. Thus, the connection is even more direct than the case of \(\Theta^*\) and \(\Theta^*_\mathrm{c}\), although the proofs do not change much:

Yet something makes the case of \(\Theta^*_\mathrm{mc}\) particularly different: the example given in Lemma 11 does not apply here. The reason is simple: when one considers maximally consistent extensions of a set \(Y\) containing \(\#(\neg\tau_1\vee\neg\tau_2)\), the maximal consistency requirement implies that at least one of the disjuncts (\(\#\neg\tau_1\) or \(\#\neg\tau_2\)) must be in the extension as well.

This being said, here are a few more things we can uncover about where MC and \(\Theta^*_\mathrm{mc}\) come apart. As we did before with \(\Theta^*\) and \(\Theta^*_\mathrm{c}\), we display a concrete counterexample of a fixed point of \(\Theta^*_\mathrm{mc}\) which is not a fixed point of MC.

8 Conclusion↩︎

In the introductory Section 1, we have claimed that the SSK thesis can be vindicated, albeit in a less uniform manner than was envisaged by [7]. In the light of the results just presented, we now explain in more detail what the vindication and the non-uniformity consists in, and sketch their philosophical import.

We can say that the SSK thesis has been vindicated on the following grounds. First, all the operators we have considered – \(\mathrm{SSK}\), \(\Theta\), and \(\Theta^*\) – give rise to a fixed-point semantics that accounts for all first-order penumbral truths of classical logic and arithmetic. That is, they preserve what in Section 1 we dubbed the essential aspects of supervaluational truth. Second, the fixed points in question have a considerably lower recursion-theoretic complexity, and are therefore amenable to \(\mathbb{N}\)-categorical axiomatizations, as we have shown. Moreover, the \(\mathrm{SSK}\)-fixed points are true to the semantic motivation supporting the supervaluation schemes we discussed in Section 1: the \(\mathrm{SSK}\)-scheme collects the first-order logical consequences of Strong Kleene truths. In contrast, the \(\Theta\)- and \(\Theta^*\)-fixed points merely collect consequences of a given hypothesis. Yet, the flipside is that attractive \(\Theta\) (\(\Theta^*\))-fixed points are fixed points of supervaluational truth, as they actually collect consequences in \(\omega\)-logic. \(\mathrm{SSK}\)-fixed points are not closed under \(\omega\)-logic and will thus typically fall short of supervaluational truth, that is, \(\mathrm{SSK}\)-fixed points are usually not supervaluational fixed points.⁷

We see that each of these incarnations of supervaluational-style truth has its own strengths and weaknesses. We now analyze them in turn along key dimensions:

Principles of Truth.↩︎

Although the fixed-point models of \(\mathrm{SSK}\), \(\Theta\), and \(\Theta^*\) have all \(\mathbb{N}\)-categorical axiomatizations, this does not entail that all such axiom systems are equally natural.

The principles of truth for \(\mathrm{IT}^-\), \(\mathrm{IT}^*\) and \(\mathrm{IT}^*+\mathrm{Tr}\text{-}\mathrm{Out}\) preserve the desirable features of the the theory \(\mathrm{IT}\) discussed in [7]. In particular. they are arguably as compositional as supervaluational-style truth can be. In fact, following Stern’s characterization of \(\mathrm{IT}\) in [7], they have the advantage that, when full compositionality fails, we can locate where it does and the extent of this failure by means of a first-order formula – \(\xi(x,X)\) for \(\mathrm{IT}^-\), \(\xi^*(x,X)\) for \(\mathrm{IT}^*\) and \(\mathrm{IT}^*+\mathrm{Tr}\text{-}\mathrm{Out}\). But even between these theories important differences arise. As we have seen, the lack of a right-to-left direction in axioms \(\mathrm{IT}^-6\) and \(\mathrm{IT}^-7\), which is remedied in \(\mathrm{IT}^*\) and \(\mathrm{IT}^*+\mathrm{Tr}\text{-}\mathrm{Out}\), makes the latter more natural than \(\mathrm{IT}^-\): unlike \(\mathrm{IT}^-\), \(\mathrm{IT}^*\) and \(\mathrm{IT}^*+\mathrm{Tr}\text{-}\mathrm{Out}\) allow for full truth disquotation inside the truth predicate. In addition, \(\mathrm{IT}^*+\mathrm{Tr}\text{-}\mathrm{Out}\) stands out for its proof-theoretic strength, which matches the one of \(\mathrm{IT}\). They amount to the strongest, \(\mathbb{N}\)-categorical axiomatic theories of truth available.

The truth predicate of the \(\mathrm{IT}\)-theories commutes with the universal quantifier, in contrast to the truth predicate of the theories of \(\mathrm{PK}\) and \(\mathrm{PK}^+\), as the \(\Theta\)-fixed points, unlike the \(\mathrm{SSK}\)-fixed points, are closed under the \(\omega\)-rule. While there are good reasons why the \(\mathrm{SSK}\)-fixed points are not closed under \(\omega\)-logic, it means that the theories \(\mathrm{PK}\) and \(\mathrm{PK}^+\) cannot give a satisfactory semantic explanation for the truth of universally quantified sentences. Putting universally quantified sentences aside, \(\mathrm{PK}\) and \(\mathrm{PK}^+\) preserve the desirable features of theories of supervaluation-style truth as highlighted by Lemma 3:

• they allow for full disquotation inside the truth predicate;

• they allow for double negation introduction/elimination inside the truth predicate

• they commute with conjunction;

• they locate the failure of compositionality by means of the formula \(\theta(x)\) (for disjunctions, existential sentences and universal sentences).

Moreover, from the semantic perspective \(\mathrm{PK}\) and \(\mathrm{PK}^+\) are more successful in limiting the failure of compositionality since \(\mathrm{Tr}\ulcorner \neg\tau_1\vee\neg\tau_2\urcorner\) will be true in the models of \(\mathrm{PK}\) and \(\mathrm{PK}^+\) only if either \(\mathrm{Tr}\ulcorner \neg\tau_1\urcorner\) or \(\mathrm{Tr}\ulcorner \neg\tau_2\urcorner\) (cf. Lemma 11) is true in the model.

However, the theory \(\mathrm{PK}\) assumes an, arguably, fairly ad hoc axiom, \(\mathrm{TB}\pi\), which seems difficult to motivate. The axiom is required to guarantee that we can express \(S\vDash_\mathrm{sk}\varphi\) over the standard model. Introducing \(\mathrm{TB}\pi\) enables us to define this notion by a positive inductive definition (relative to the standard model). Without this axiom we would not be able to show the \(\mathbb{N}\)-categoricity of \(\mathrm{PK}\) and the theory would not behave in the intended way. \(\mathrm{PK}^+\) remedies this by allowing disquotation for all \(\mathrm{Tr}\)-positive sentences. Arguably, this is a more natural restriction to the naive \(\mathrm{Tr}\)-schema, as it is justified by the role played by negation (or equivalent logical tools) in the Liar paradox. In addition, \(\mathrm{PK}^+\) features the axiom schema of \(\mathrm{Tr}\)-Out, which naturally follows from the classical soundness of \(\mathrm{SSK}\)-fixed points.

Semantic Rationale.↩︎

We have already mentioned that the \(\mathrm{SSK}\) fixed-point semantics comes equipped with semantico-philosophical rationale. For one, the fixed-point semantics is associated with a semantic evaluation scheme, the \(\mathrm{SSK}\)-scheme, which, arguably, captures directly the core idea of ‘first-orderizing’ the ‘second-order’ supervaluation schema. For another, but for related reasons, the \(\mathrm{SSK}\)-fixed points are submitted to semantic scrutiny: every sentence in a given \(\mathrm{SSK}\)-fixed point \(S\) must be true in the model \((\mathbb{N},S)\) according to the \(\mathrm{SSK}\)-scheme, that is, \(\mathrm{SSK}\)-fixed points are semantically self-supporting. Since the \(\mathrm{SSK}\)-scheme is classically sound this also implies that the members of \(S\) are classically true in the model \((\mathbb{N},S)\).

Neither holds for the fixed-point semantics associated with the operations \(\Theta\) or \(\Theta^*\): there is no motivated semantic evaluation scheme associated with these fixed-point semantics, nor are the fixed points subjected to any form of semantic scrutiny. The latter shows in the fact that \(\Theta\) and \(\Theta^*\) are sound for any given hypothesis \(S\in\mathcal{P}(\mathrm{Sent})\), that is, starting from any set of sentences \(S\) we can inductively define a fixed point \(\mathrm{I}_S\supseteq S\) of \(\Theta\) and \(\Theta^*\) respectively. This means that the sentences in the starting hypothesis are accepted as true without scrutiny independently of their semantic status. Unsurprisingly then, not all fixed points of \(\Theta\) and \(\Theta^*\) are classically sound – and, even if they are classically sound, they may contain, e.g., disjunctions that are neither supported by the Strong Kleene scheme nor \(\mathrm{PAT}\)-truths (see the example of Lemma 11 discussed above). So, generally speaking, the \(\Theta\) and \(\Theta^*\) fixed points lack semantic justification. Rather, these fixed points can be conceived of as the set of theorems derivable within the proof system outlined in Proposition 8 with \(S\) as additional axioms. Ultimately, this means that, from a semantic perspective, the fixed points of \(\Theta\) and \(\Theta^*\) will be well supported and motivated if(f) the initial hypothesis is. However, motivating a particular hypothesis is external to the fixed-point semantics of \(\Theta\) and \(\Theta^*\). Yet, if such a motivation for an initial hypothesis \(S\) is given, e.g., that it is supervaluationally self-supporting, then this motivation is indeed fully transferred to the fixed point \(\mathrm{I}_S\) constructed over \(S\): \(\mathrm{I}_S\) will be a supervaluational fixed point. Indeed, as we showed in Proposition 24, all supervaluational fixed points can be constructed using \(\Theta\) and \(\Theta^*\) in such a way.

Two ways of first-orderizing↩︎

Summing up, the \(\mathrm{SSK}\)- and \(\Theta\)-operators can be considered as two different ways of ‘first-orderizing’ the supervaluation scheme. The \(\mathrm{SSK}\)-operator and scheme provide us with a first-order formulation of the semantic idea underlying the supervaluation scheme. In contrast to the supervaluation scheme, it only collects the first-order penumbral truths and falls short of collecting second-order penumbral truths. This also explains why the \(\mathrm{SSK}\)-fixed points are not closed under the \(\omega\)-rule. The \(\mathrm{SSK}\)-scheme embraces the idea of the supervaluation scheme but implements it in an independent way that leads to a distinct (and disjoint) class of supervaluation-style fixed points and a novel supervaluation-style theory.

In contrast, the various \(\Theta\)-operators ‘first-orderize’ the supervaluational fixed-point construction, as these operators are defined via a first-order arithmetical formula. We can then use the first-order construction to extract axiomatic truth theories that are as close as possible to a proof-theoretic characterization of supervaluational truth (cf. Proposition 20). Yet, in contrast to the \(\mathrm{SSK}\)-scheme, there is no semantics in the ordinary sense associated with these operators, and the fixed-point construction does not lend any semantic justification to the sentences in the fixed points. The fixed points of the various \(\Theta\)-operators are somewhat ‘hit-and-miss’, depending on the choice of the initial hypothesis. The moral of our discussion then is that we can first-orderize supervaluational truth either by giving a first-order formulation of the underlying semantic idea or by first-orderizing the fixed-point construction. However, these are two different projects that, unfortunately, cannot be performed in an integrated and uniform manner.

9 Open problems↩︎

After our investigation, there remain some open problems that may be addressed in future research. Some of them concern the proof-theoretic strength of many of the theories that we have introduced here.

By definition, we know that \(\mathrm{PK}^+\) has at least the proof-theoretic strength of \(\mathrm{PUTB}\), but it is still open whether this lower-bound is precise. By contrast, both the lower- and the upper-bound of \(\mathrm{PK}\) are still undetermined.

Proposition 21 established a lower-bound for both \(\mathrm{IT}^-\) and \(\mathrm{IT}^*\), namely the strength of \(\mathrm{RT}_{<\varepsilon_0}\). As with \(\mathrm{PK}^+\), it remains unknown whether this bound is exact; while the strength of \(\mathrm{IT}\) represents an upper-bound, it is clearly not sharp.

A further question is related to \(\mathrm{SSK}\)-fixed points. We have shown how some said fixed points are not closed under \(\omega\)-logic, e.g., the least \(\mathrm{SSK}\) fixed point. But we lack a general proof to the effect that no \(\mathrm{SSK}\) fixed point is closed under \(\omega\)-logic:

If, unlike we conjecture, the answer to the first question is in the affirmative, it would still be open whether any such fixed point coincides with a supervaluational fixed point:

Acknowledgements↩︎

Pablo Dopico’s work was supported by a LAHP (London Arts and Humanities Partnership) studentship. Carlo Nicolai’s research was supported by the Arts and Humanities Research Council (UK), grants AH/V015516/1 and AH/Z506515/1. Both Pablo Dopico and Carlo Nicolai acknowledge support from the European Union’s Horizon research and innovation programme within the project PLEXUS (Grant agreement No 101086295).

References↩︎

---

1. \(\mathbb{N}\)-categoricity is mainly cogent in the context of classical theories of truth where sentences \(\varphi\) are in general not equivalent to \(\mathrm{Tr}\ulcorner \varphi\urcorner\). When such an equivalence is in place – e.g. in the context of axiomatizations of Kripke’s fixed-point semantics in a Strong Kleene setting –, \(\mathbb{N}\)-categoricity may be trivially obtained.↩︎

2. The impossibility to \(\mathbb{N}\)-categorically axiomatize the revision theory of truth then permeates other truth theories based on revision rules, most notably Field’s [5].↩︎

3. The correspondence will thus not hold for the trivial admissibility condition \(\Phi\) with \(\Phi(S'):\leftrightarrow S'=S'\) and thus fails for the scheme \(\mathrm{sv}\) discussed below.↩︎

4. We recall that, because of the higher recursion-theoretic complexity of supervaluational fixed-point semantics, \(\mathbb{N}\)-categorical axiomatizations will not be available for the latter. In some sense it is impossible to equip supervaluational fixed-point semantics with a fitting proof theory. This shows, for example, in the fact that the models of \(\mathrm{VF}\) are not just the supervaluational fixed points but, in addition, fixed points of \(\Theta\) or even the set of stable truth of the Herzberger sequence over the empty set [8]. It thus seems difficult to associate \(\mathrm{VF}\) with supervaluational fixed points in some strong sense.↩︎

5. We note that for consistent sets of sentences \(S\) we have that \[\text{if }S\vDash_\mathrm{sk}\varphi,\text{ then }S\vDash\varphi,\] for all sentences \(\varphi\).↩︎

6. Again, just take the fixed point that obtains by applying \(\Theta^*\) to \(\{\#\tau_1\vee\tau_2\}\).↩︎

7. We do not know whether there are \(\mathrm{SSK}\)-fixed points that are also supervaluational fixed points, and whether there is a nice class of such fixed points. We conjecture that this is not the case.↩︎