Truth and Feasible Reducibility

TL;DR

This paper proves that three canonical truth theories based on Peano arithmetic are feasibly reducible to PA, meaning proofs in these theories can be efficiently translated into PA proofs, showing no significant speed-up.

Contribution

It establishes that these truth theories are polynomial-time reducible to PA, contrasting with the behavior over finitely axiomatizable base theories.

Findings

Feasibly reducible to PA with polynomial time translation

No significant speed-up over PA for these truth theories

Contrasts with finitely axiomatizable base theories

Abstract

Let $\mathcal{T}$ be any of the three canonical truth theories $\textsf{CT}^-$ (Compositional truth without extra induction), $\textsf{FS}^-$ (Friedman--Sheard truth without extra induction), and $\textsf{KF}^-$ (Kripke--Feferman truth without extra induction), where the base theory of $\mathcal{T}$ is $\textsf{PA}$ (Peano arithmetic). We show that $\mathcal{T}$ is \textit{feasibly reducible to} $\textsf{PA}$, i.e., there is a polynomial time computable function $f$ such that for any proof $\pi $ of an arithmetical sentence $\phi $ in $\mathcal{T}$, $f(\pi )$ is a proof of $\phi $ in $\textsf{PA}$. In particular, $\mathcal{T}$ has at most polynomial speed-up over $\textsf{PA}$, in sharp contrast to the situation for $\mathcal{T}[\textsf{B}]$ for \textit{finitely axiomatizable} base theories $\textsf{B}$.

Equations

$$m=\sum _{i=0}^n{2}^i(w_i+1).$$

$${┌1+((1+1)+0)┐}^{\circ }=3,$$

$$\underline{n}=\underline{{\epsilon }_0}+\underline{2}\times (\underline{{\epsilon }_1}+\underline{2}\times (\dots {\epsilon }_{k-1}+\underline{2}\times \underline{{\epsilon }_k})\dots )$$

$$\mathcal{M}\models R[\alpha]\textnormal{ iff }\mathcal{M}\bigl{(}\langle R,\alpha(v_{1}),\ldots,\alpha(v_{c})\rangle\bigr{)}.$$

$$\mathcal{M}\models \varphi (a_1,\dots ,a_c)$$

$$\mathcal{M}⪯\mathcal{N}.$$

$$\mathcal{M}{⪯}_{\mathcal{L}}\mathcal{N}.$$

$$\parallel\phi\parallel_{\mathcal{T}}=\left\{\begin{array}[]{l}\textnormal{ the length of the shortest proof of $\phi$, if $\mathcal{T}\vdash\phi$};\\ \infty\textnormal{ otherwise.}\end{array}\right.$$

$$\mathcal{T}{⊢}^n\varphi .$$

$${\mathcal{T}}_2{⊢}^n\varphi \Rightarrow {\mathcal{T}}_1{⊢}^{f(n)}\varphi .$$

$$n\text{ is a proof of }\varphi \text{ in }{\mathcal{T}}_2\Rightarrow f(n)\text{ is a proof of }\varphi \text{ in }{\mathcal{T}}_1.$$

$$\parallel {\varphi }_n{\parallel }_{{\mathcal{T}}_1}>f(\parallel {\varphi }_n{\parallel }_{{\mathcal{T}}_2}).$$

$$R(n_0,\dots ,n_k)\text{ iff }\parallel \varphi (\underline{n_0},\dots ,\underline{n_k}){\parallel }_{\mathcal{T}}\le p(|n_0|,\dots ,|n_k|).$$

$${\text{Proof}}_{\mathcal{T}}(x,y):=\text{"x is a proof of y from the axioms of T"}$$

$$\mathbb{N}\models {\text{Proof}}_{\mathcal{T}}(m,n),$$

$${\text{Pr}}_{\mathcal{T}}(y):=\exists x{\text{Proof}}_{\mathcal{T}}(x,y)$$

$${\text{Con}}_{\mathcal{T}}:=\neg {\text{Pr}}_{\mathcal{T}}(\underline{\exists x(x\ne x)}).$$

$${\text{Proof}}_{\mathcal{T}}^{\varphi }(x,y)$$

$$(\varphi (\underline{n})\to {\text{Proof}}_{\mathcal{T}}^{\varphi }(\underline{n},\underline{n})),$$

$$\forall x\left(\varphi (x)\to \psi (x)\right)\to \forall y\forall z\left({\text{Proof}}_{\mathcal{T}}^{\varphi }(y,z)\to {\text{Proof}}_{\mathcal{T}}^{\psi }(y,z)\right).$$

$${\text{Pr}}_{\mathcal{T}}^{\varphi }(y):=\exists x{\text{Proof}}_{\mathcal{T}}^{\varphi }(x,y)$$

$${\text{Con}}_{\mathcal{T}}^{\varphi }:=\neg {\text{Pr}}_{\mathcal{T}}^{\varphi }(\underline{\exists x(x\ne x)}).$$

$$\parallel {\text{Con}}_{\mathcal{T}}(f(\underline{n})){\parallel }_{\mathcal{T}}>f(n{)}^{\delta }.$$

$$\parallel {\text{Con}}_{\text{I}{\Sigma }_1}(2_{\underline{n}}){\parallel }_{\text{I}{\Sigma }_1}$$

$$\parallel {\text{Con}}_{\text{PA}}(2_{\underline{n}}){\parallel }_{\text{PA}}$$

$$\forall x,y,t\exists z\left(N(t)\to \forall s<t\left((x{)}_s=(z{)}_s\wedge (z{)}_t=y\right)\right)$$

$$\forall \alpha \in \text{Asn}(\varphi )\left({\text{Sat}}_n(\underline{\varphi },\alpha )\equiv \varphi (\alpha )\right)$$

$$\forall \alpha \in \text{Asn}(\varphi )\left({\text{Sat}}_n(\underline{\varphi },\alpha )\equiv \varphi (\alpha )\right).$$

$$\forall\phi\in\textnormal{{Sent}}_{\mathcal{L}_{\textnormal{{PA}}}}\ \ \textnormal{{dp}}(\phi)\leq k\rightarrow\bigl{(}\textnormal{{Tr}}_{n}(\phi)\equiv\textnormal{{Tr}}_{k}(\phi)\bigr{)}.$$

$$\forall \alpha \in \text{Asn}(\varphi ,\mathcal{M})\Phi (┌R(s_0,\dots ,s_{n-1})┐,\alpha )\equiv \mathcal{M}\models R(s_0,\dots ,s_{n-1})[\alpha ]$$

$$\forall v\in\textnormal{{Var}}\forall\phi(v)\in\textnormal{{Form}}_{\mathcal{L}^{\prime}}\forall\alpha\in\textnormal{{Asn}}(\phi,\mathcal{M})\ \ \Phi(\exists v\phi,\alpha)\equiv\exists\beta\sim_{v}\alpha\ \ \bigl{(}\beta\in\textnormal{{Asn}}(\phi,\mathcal{M})\wedge\Phi(\phi,\beta)\bigr{)}.$$

Full text

1. 1 Introduction

2. 2 Setting the stage: arithmetical machinery

3. 2.1 Arithmetized syntax

4. 2.2 Arithmetized model theory

5. 2.3 Lengths of proofs

6. 2.4 Feasible truth predicates

7. 2.5 Polynomial simulations and feasible reductions for theories extending PA.

8. 2.6 Feasible interpretability and speed-up

9. 3 Dramatis personæ: typed and untyped theories of truth

10. 3.1 $\textnormal{{CT}}^{-}$

11. 3.2 $\textnormal{{KF}}^{-}$ and $\textnormal{{FS}}^{-}$

12. 3.3 Conservativity of truth theories

13. 3.3.1 Conservativity of $\textnormal{{CT}}^{-}$

14. 3.3.2 Conservativity of $\textnormal{{KF}}^{-}$

15. 3.3.3 Conservativity of $\textnormal{{FS}}^{-}$

16. 4 The main act: feasible reductions of truth theories

17. 4.1 Feasible reduction of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ to PA

18. 4.2 Feasible reduction of $\textnormal{{KF}}^{-}[\textnormal{{PA}}]$ to PA

19. 4.3 Feasible reduction of $\textnormal{{FS}}^{-}$ to PA

20. 4.4 Feasible interpretability of truth theories

21. 5 Open Questions

22. 6 Appendix

23. 6.1 Feasible reflexivity

24. 6.2 Congruence lemma

25. 6.3 FACT

26. 6.4 A glossary of technical notions

1 Introduction

One of the celebrated results in the area of axiomatic theories of truth is the Krajewski-Kotlarski-Lachlan (KKL) theorem [13] that asserts that every countable recursively saturated model of PA (Peano arithmetic) is expandable to a model of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ (compositional truth over PA with no extra induction111This theory is referred to as $\textnormal{{CT}}\!\upharpoonright$ in [10], $\textnormal{{CT}}^{-}$ in [2], and $\textnormal{{PA}}^{\mathsf{FT}}$ in [5].). The KKL theorem is an overtly model-theoretic result, but it is well-known that it is equivalent to the conservativity of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ over PA.222This equivalence follows from two key facts: (1) every countable consistent theory has a countable recursively saturated model, and (2) countable recursively saturated models are resplendent, both of which can be verified in the subsystem $\textnormal{{ACA}}_{0}$ of second order arithmetic. Recent proofs of the KKL theorem given by Enayat and Visser [5] (using model-theoretic techniques) and Leigh [15] (using proof-theoretic machinery) show that $\textnormal{{CT}}^{-}[\textnormal{{B}}]$ is conservative over B for every "base theory" B (i.e., a theory B that supports a modicum of coding machinery for handling elementary syntax). Leigh’s proof makes it clear that if B is a base theory with a computable set of axioms, then $\textnormal{{CT}}^{-}[\textnormal{{B}}]$ is proof-theoretically reducible to B, and in particular, there is a primitive recursive function $f$ such that for any proof $\pi$ of a sentence $\phi$ in $\textnormal{{CT}}^{-}[\textnormal{{B}}]$, where $\phi$ is a sentence in the language of B, $f(\pi)$ is a proof of $\phi$ in B. Indeed, Leigh’s "reducing function" $f$ is readily seen to be a provably total function of the fragment of $\mathsf{PRA}$ (Primitive Recursive Arithmetic) commonly known as $\textnormal{{I}}\Delta_{0}+\mathsf{Supexp.}$333$\mathsf{Supexp}$ asserts the totality of the superexponential function $\mathsf{Supexp}(n,x)$, with $\mathsf{Supexp}(0,x)=x$ and $\mathsf{Supexp}(n+1,x)=2^{\mathsf{Supexp}(n,x)}.$ Leigh [15] refers to this function as hyper-exponentiaton.

The main result of this paper shows that $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ is feasibly reducible to PA, i.e., there is a polynomial-time computable function $f$ such that for any proof $\pi$ of an arithmetical sentence $\phi$ in $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$, $f(\pi)$ is a proof of $\phi$ in $\mathsf{PA}$. The feasible reducibility of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ to PA readily implies that $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ does not exhibit significant speed-up over PA, i.e., there is a polynomial function $p(x)$ such that for any arithmetical sentence $\phi$, if $\phi$ is provable in $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ by a proof of length $n$ (in some standard proof system444 The choice of the ”standard proof system” is immaterial since it is well-known that any two such systems polynomially simulate each other [18].), then $\phi$ is provable in $\mathrm{PA}$ by a proof of length $p(n)$. This solves a problem posed by Enayat in 2012 [4].

The absence of significant speed up of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ over PA implied by the feasible reducibility of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ to PA exhibits a dramatic difference between $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ and $\textnormal{{CT}}^{-}[\textnormal{{B}}]$ for finitely axiomatized base theories B, since as shown by Fischer [7], $\textnormal{{CT}}^{-}[\textnormal{{B}}]$ has superexponential speed-up over B for finitely axiomatized base theories B, and therefore, $\textnormal{{CT}}^{-}[\textnormal{{B}}]$ is not feasibly reducible to B for finitely axiomatized base theories B. It is also known that $\textnormal{{CT}}^{-}[\textnormal{{PA}}]+\mathsf{Int}$ (where $\mathsf{Int}$ is the axiom of internal induction) is conservative over PA ([13], [15]) but not feasibly reducible to PA since it has superexponential speed-up over PA [7].

Our proof of the feasible reduction of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ to PA includes the verification that PA proves the formal consistency of every finite subtheory of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$, thereby establishing that $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ is a reflexive theory. This result follows from Leigh’s work [15]; and was also established by Enayat and Visser (unpublished) with help of the "low basis theorem" of computability theory to arithmetize their model-theoretic proof of conservativity of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ over PA. The proof presented here, however, is based on a simpler arithmetization of the Enayat–Visser construction and does not appeal to the low basis theorem; the syntactic analysis of this arithmetization forms one of the main ingredients of the proof of our main result.

We also employ the machinery developed for the proof of our main result to analyse two other prominent theories of truth, namely $\textnormal{{FS}}^{-}[\textnormal{{PA}}]$ (Friedman–Sheard theory of truth over PA, with no extra induction), and $\textnormal{{KF}}^{-}[\textnormal{{PA}}]$ (Kripke–Feferman theory of truth over PA with no extra induction). More specifically, we show that $\textnormal{{FS}}^{-}[\textnormal{{PA}}]$ and $\textnormal{{KF}}^{-}[\textnormal{{PA}}]$ are both reflexive and feasibly reducible to $\mathrm{PA}$. These results, in turn, show that both $\textnormal{{FS}}^{-}[\textnormal{{PA}}]$ and $\textnormal{{KF}}^{-}[\textnormal{{PA}}]$ are interpretable in $\mathsf{PA}$ and have at most polynomial speed-up over $\mathsf{PA}$.

A word about the organization of the paper is in order. Section 2 deals with arithmetical preliminaries and technical machinery that will be employed for establishing our principal results. Section 3 presents basic definitions and facts about the truth theories $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$, $\textnormal{{KF}}^{-}[\textnormal{{PA}}]$, and $\textnormal{{FS}}^{-}[\textnormal{{PA}}]$, including their conservativity over PA. The main results of the paper are contained in Section 4, which contains the proofs of feasible reduction of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$, $\textnormal{{KF}}^{-}[\textnormal{{PA}}]$, and $\textnormal{{FS}}^{-}[\textnormal{{PA}}]$ to PA; these proofs should be viewed as refined arithmetizations of the conservativity proofs presented in Section 3.3. The last subsection of Section 4, on the other hand, spells out the interpretability-theoretic ramifications of our work. Section 5 collects some open questions; and the Appendix (Section 6) consists of routine-but-technical proofs of certain results employed in the body of the paper.

2 Setting the stage: arithmetical machinery

This section discusses basic notions and fundamental machinery that can be generally described as refined arithmetization of certain parts of proof theory and model theory that play a key role in the statements and proofs of our main results in Section 4. Note, however that the material in Subsection 2.6 will be only employed in Subsection 4.4.

2.1 Arithmetized syntax

In this paper, PA denotes the theory using $\{0,S,+,\times\}$ as non-logical function symbols, whose axioms consist of the axioms of Robinson’s Arithmetic Q together with the usual induction scheme for the whole language $\mathcal{L}_{\textnormal{{PA}}}$ of PA. Its intended model are natural numbers $\mathbb{N}$ with addition, multiplication and successor functions. We will also denote $\mathbb{N}$ by $\omega$, typically when treating it as set of indices for some construction. Sometimes in this paper, we will be referring to $\mathbb{N}$ or $\omega$ when working in PA. Then these symbols simply refer to the whole universe. This should not lead to any confusion.

Crucially for our purposes, PA is capable of representing syntax. This means that in PA, one can employ recursion to define notions such as "term," "formula" or "proof in PA" similarly to how these notions are defined in Zermelo–Fränkel set theory. This is a standard topic, covered, e.g., in [11] or [9].

Every sequence $(w_{0},\ldots,w_{n})\in\{0,1\}^{<\omega}$ is represented by a number

[TABLE]

Each formula is represented as a $0,1$-string and then coded as a number. If $s$ is a binary string, then $|s|$ denotes its length.

Throughout the paper we will use certain formulae to represent various syntactic and technical notions. For the convenience of our reader, we gather here all the notation which might be possibly confusing.

Definition 1** (Arithmetized syntax).**

$\textnormal{{len}}(s)=x$ asserts: "$s$ is a sequence and its length is equal to $x$." 2. 2.

$\textnormal{{Term}}_{\mathcal{L}}(x)$ asserts: "$x$ is a term of a language $\mathcal{L}$." For instance, $\textnormal{{Term}}_{\mathcal{L}_{\textnormal{{PA}}}}(x)$ asserts that $x$ is a (code of an) arithmetical term. 3. 3.

$\textnormal{{ClTerm}}_{\mathcal{L}}(x)$ asserts: "$x$ is a closed term of a language $\mathcal{L}$," i.e. a term without free variables. 4. 4.

$\textnormal{{TermSeq}}_{\mathcal{L}}(x)$ asserts: "$x$ is a sequence of terms of the language $\mathcal{L}$." 5. 5.

$\textnormal{{ClTermSeq}}_{\mathcal{L}}(x)$ asserts: "$x$ is a sequence of closed terms of the language $\mathcal{L}$." 6. 6.

${x}^{\circ}=y$ asserts: "$\textnormal{{ClTerm}}_{\mathcal{L}}(x)$ and $y$ is the value of the term $x$." For instance,

[TABLE]

holds provably in PA ($\ulcorner t\urcorner$ stands for the number coding the term $t$). 7. 7.

$\textnormal{{Var}}(x)$ asserts: "$x$ is a variable." For instance, $\textnormal{{Var}}(17)$ means that $17$ is a code of a variable in the coded language. Since without loss of generality we can assume that all first-order languages have the same set of variables, we omit the reference to a specific language in the subscript. 8. 8.

$\textnormal{{Form}}_{\mathcal{L}}(x)$ asserts: "$x$ is a formula of the language $\mathcal{L}$." 9. 9.

$\textnormal{{FV}}(x,y)$ asserts: "$y$ is a free variable of $x$," where $x$ is either a term or a formula. 10. 10.

$\textnormal{{Form}}^{\leq 1}_{\mathcal{L}}(x)$ asserts: "$x$ is a formula of the language $\mathcal{L}$ with at most one free variable", and $\textnormal{{Form}}^{1}_{\mathcal{L}}(x)$ asserts: "$x$ is a formula of the language $\mathcal{L}$ with exactly one free variable." 11. 11.

$\textnormal{{Sent}}_{\mathcal{L}}(x)$ asserts: "$x$ is a sentence of the language $\mathcal{L}$." 12. 12.

$\textnormal{{FVSeq}}(x,y)$ asserts: "$y$ is a (coded) sequence whose elements are (some) free variables of $x$," where $x$ is either a term or a formula. 13. 13.

$\alpha$ is an assignment for a formula or a term $\phi$ if $\alpha$ is a function whose domain includes the free variables of $\phi$. The formula $\textnormal{{Asn}}(x,y)$ asserts: "$y$ is an assignment for $x$," where $x$ is a term or a formula. We will often denote it with $y\in\textnormal{{Asn}}(x)$. If $s$ is a coded set or sequence, we will write $y\in\textnormal{{Asn}}(s)$ to denote that $y$ is an assignment for all elements of $s$. We will sometimes also write $\textnormal{{Asn}}(x_{1},\ldots,x_{n},\alpha)$ or $\alpha\in\textnormal{{Asn}}(x_{1},\ldots,x_{n})$ meaning $\alpha\in\textnormal{{Asn}}(s)$, where $s=\langle x_{1},\ldots,x_{n}\rangle$ 14. 14.

$\beta\sim_{v}\alpha$ asserts: "$\alpha$ and $\beta$ are assignments, $v$ is a variable, and $\alpha(w)=\beta(w)$ for all variables $w$, possibly except for $v$ which belongs to the domain of $\beta$ (and not necessarily to the domain of $\alpha$)."

The reader could expect to see in this list certain other predicates such as Proof or Con. Since we will need some more precise information about these formulae and their length, they will be only introduced in Subsection 2.3.

Next we introduce numerals. For our purposes the numeral $\underline{x}$ for a number $x$ will not be a code of $S\ldots S0$ iterated $x$ times, since this is not an efficient notation when it comes to writing short formulae and proofs. Our numerals will be handled via binary expansions.

Definition 2** (Numerals).**

For any natural number $n$, $\underline{n}$ denotes the binary expansion of $n$ written as a term of $\mathcal{T}$. More precisely: let $n=\sum_{i\leq k}\varepsilon_{i}2^{i}$, where $\varepsilon_{i}\in\{0,1\}$. We define:

[TABLE]

where $\underline{0}=0$, $\underline{1}=S(0)$ and $\underline{2}=\underline{1}+\underline{1}$. Thus it takes $O(\log n)$ symbols to represent $n$.

Let us introduce one more definition:

Definition 3** (Substitutions).**

Let $\phi(v_{1},\ldots,v_{n})$ be a formula with $n$ free variables shown and let $\alpha$ be an assingment for $\phi$. By $\phi[\alpha]$ we denote the formula in which the numeral (in the sense of Definition 2) denoting $\alpha(v_{i})$ is substituted for the variable $v_{i}$. 2. 2.

Similarly, if $t\in\textnormal{{Term}}_{\mathcal{L}}$ and $\alpha\in\textnormal{{Asn}}(t)$, then by $t[\alpha]$ we mean the closed term obtained by substituting the numeral $\alpha(v)$ for each free variable $v$ in $t$. 3. 3.

If $t\in\textnormal{{Term}}_{\mathcal{L}}$ and $\alpha\in\textnormal{{Asn}}(t)$, then by $t^{\alpha}$ we mean ${t[\alpha]}^{\circ}.$ Notice that if $v$ is a variable and $\alpha\in\textnormal{{Asn}}(v)$, then $v^{\alpha}=\alpha(v)$ provably in PA. 4. 4.

If $x\in\textnormal{{Form}}_{\mathcal{L}}$ for some language $\mathcal{L}$, $v\in\textnormal{{Var}}$ and $t\in\textnormal{{Term}}_{\mathcal{L}}$, then $x[t/v]=y$ is an arithmetical formula which asserts "$y$ is the effect of substituting in the formula $x$ the term $t$ for every occurrence of the variable $v$."

We adopt a few conventions as to how we will be dealing with formalized syntactic notions.

Convention 4**.**

If $\phi$ is a standard formula or a standard term, we will sometimes denote the corresponding code by $\ulcorner\phi\urcorner$ to prevent ambiguity, but most of the time we skip the corners to lighten the notation. 2. 2.

We can clearly code a formula $\phi$ as a binary string. Then by $|\phi|$ we mean the length of this string. Note that $\ulcorner\phi\urcorner$ is of size exponential in $|\phi|$ and $\underline{\ulcorner\phi\urcorner}$ is of size linear in $|\phi|$. We deal with proofs in $\mathcal{T}$ in a similar fashion. 3. 3.

Since we will sometimes skip the corners denoting formulae, $\underline{\ulcorner\phi\urcorner}$ is most of the time denoted by $\underline{\phi}$ for a standard formula $\phi$. 4. 4.

We will sometimes use the formulae defining syntactic notions as if they were denoting sets. For example, we will sometimes write "$x\in\textnormal{{Form}}_{\mathcal{L}_{\textnormal{{PA}}}}$" rather than "$\textnormal{{Form}}_{\mathcal{L}_{\textnormal{{PA}}}}(x)$." 5. 5.

We will use provably functional formulae such as $\underline{x}$, ${x}^{\circ}$, or $x[t/v]$ as if they were terms. 6. 6.

For better readability we will sometimes skip formulae denoting syntactic operations and write the effect of the operations instead. Thus, for example, we will write $T(\neg\phi)$ to denote "There exists $\psi$ which is the negation of the sentence $\phi$ and $T(\psi)$."

2.2 Arithmetized model theory

Peano arithmetic is capable of accommodating a substantial part of the model theory of countable structures. We will make constant use of this fact throughout the whole paper. This subsection briefly introduces the reader to this topic. The rough convention is as follows: a theory is a definable set of sentences. If $\phi$ is a formula which defines a set of (codes of) sentences, then we call that formula a theory.

Models come in two kinds. By a full model $\mathcal{M}$ we mean the elementary diagram of that model (or, actually, a formula defining the elementary diagram). It is given as a complete Henkinized theory. By a model $\mathcal{M}$, we mean a formula defining its domain and some relations on that domain (this does not mean that we only deal with models of relational languages, but rather, we construe the denotations of function and constant symbols as relations).

Definition 5**.**

A formula $\phi$ defines a theory in a language $\mathcal{L}$ if for all $x$, \phi(x)\rightarrow\bigl{(}x\in\textnormal{{Sent}}_{\mathcal{L}}\bigr{)} holds. By a full model of a theory $\mathcal{T}$, we mean a theory $\mathcal{T}^{\prime}\supseteq\mathcal{T}$ in a language $\mathcal{L}^{\prime}$ expanding $\mathcal{L}$ with some constants (possibly trivially) such that:

• •

$\mathcal{T}^{\prime}$ is complete and consistent, so for any $\phi$, $\phi\in\mathcal{T}^{\prime}$ if and only if $\neg\phi\notin\mathcal{T}^{\prime}$.

• •

$\mathcal{T}^{\prime}$ has all existential statements witnessed by constants which means that if $\exists x\phi(x)\in\mathcal{T}^{\prime}$, then for some constant $c$, $\phi(c)\in\mathcal{T}^{\prime}$.

By a model of a language $\mathcal{L}$ (or simply an $\mathcal{L}$-structure), we mean a formula $\mathcal{M}$ which defines a set of (coded) sequences such that if $\mathcal{M}(s)$, then:

• •

$s(0)$ is either a symbol of the language $\mathcal{L}$ or some fixed element $d$ which is not a symbol of $\mathcal{L}$.

• •

If $s(0)$ is a relation symbol of $\mathcal{L}$, then the length of $s$ is the arity of $s(0)$ plus one.

• •

If $s(0)$ is a function symbol of $\mathcal{L}$, then the length of $s$ is the arity of $s(0)$ plus two. We treat constants as functions of arity zero.

• •

If $s(0)$ is the fixed element $d$, then $s$ has length two.

• •

If $a=s(n)$ for some $n>0$, then $\mathcal{M}(\langle d,a\rangle)$ holds. ($a$ is in the domain of a model.)

In the above, a model is essentially defined as a particular kind of tuple: (definition of the domain, definition of the first relation, definition of the second relation $\ldots$). However, since we allow models with infinite signatures, we define it in the above compact way rather than an actual tuple of formulae. However, if a model is defined with a standard number of definable relations, we can easily construct a definition in the format specified above. The second warning is as follows: although officially in this paper a full model is the same as the elementary diagram of that model, in practice, we will refer to models in the usual way, since it is clear how to transfer statements about models to statements about their elementary diagrams and vice versa.

Definition 6**.**

If $\mathcal{M}$ is a full model, we write $x\in M$ to say that $x$ is a constant in the language of a full model $\mathcal{M}$. (This means that $x$ is an element of $\mathcal{M}$, since we implicitly assume that all full models are built on Henkin constants.) If $\mathcal{M}$ is a model, the expressions $x\in M$, means that $\mathcal{M}(d,x)$ holds. 2. 2.

If $\mathcal{M}$ is a (full) model over a language $\mathcal{L}$, and $\phi\in\textnormal{{Form}}_{\mathcal{L}}$, we say that $\alpha$ is an $\mathcal{M}$-assignment or an $\mathcal{M}$-valuation for a formula $\phi$ if $\alpha$ is a (coded) finite function, whose domain contains $\textnormal{{FV}}(\phi)$, $\alpha\in\textnormal{{Asn}}(\phi)$, and for every $x$, $\alpha(x)\in M$. We denote this by $\alpha\in\textnormal{{Asn}}(\phi,\mathcal{M})$. 3. 3.

If $\mathcal{M}$ is a full model over a language $\mathcal{L}$, $\phi\in\textnormal{{Form}}_{\mathcal{L}}$, and $\alpha$ is an $\mathcal{M}$-assignment, then the relation $\mathcal{M}\models\phi[\alpha]$ is defined simply as $\phi(\alpha(x_{1}),\ldots,\alpha(x_{c}))\in\mathcal{M}$. 4. 4.

If $\mathcal{M}$ is a model over a language $\mathcal{L}$, $\phi\in\textnormal{{Form}}_{\mathcal{L}}$, and $\alpha$ is an $\mathcal{M}$-assignment, then the relation $\mathcal{M}\models\phi[\alpha]$ is defined only for $\phi$ of standard complexity via the usual compositional conditions with quantifiers restricted to the domain of $\mathcal{M}$ and satisfaction for base relations $R\in\mathcal{L}$ (of arity $c$) defined as follows:

[TABLE]

We define satisfaction for equalities of terms in an analogous fashion. 5. 5.

If $\mathcal{M}$ is a full model, we will write $\textsf{ElDiag}(\mathcal{M})$ (elementary diagram of $\mathcal{M}$) instead of $\mathcal{M}$ when we want to stress that we are thinking of a theory rather than of a structure. 6. 6.

If $\mathcal{M}$ is a (full) model over a language $\mathcal{L}$, $a_{1},\ldots,a_{c}\in M$ and $\phi(v_{1},\ldots,v_{c})$ is a formula with the displayed free variables, we will write

[TABLE]

meaning there there exists an $\mathcal{M}$-valuation $\alpha$ for $\phi$ such that $\alpha(v_{i})=a_{i}$ for all $i<c$ and $\mathcal{M}\models\phi[\alpha].$ 7. 7.

If $\mathcal{M}$ is a (full) model over a language $\mathcal{L}$ and $\phi(v_{1},\ldots,v_{c})\in\textnormal{{Form}}_{\mathcal{L}}$ with all free variables displayed, then by $\phi(\mathcal{M})$ we mean the set of (tuples of) elements defined by the formula $\phi$ in $\mathcal{M}$. In other words, it is the set of tuples $(a_{1},\ldots,a_{c})$ of the elements of $\mathcal{M}$ such that $\mathcal{M}\models\phi[\alpha]$ for some (equivalently, any) $\alpha\in\textnormal{{Asn}}(\phi)$ such that $\alpha(v_{i})=a_{i},i\leq c$.

Note that we haven’t yet defined what it means that a model satisfies a theory. This is not an omission. Since for general (not full) models, satisfaction is defined only for standard sentences, we only define satisfaction for standard formulae. This is actually a scheme: for each formula we define what it means that a model satisfies this formula. More precisely: for each $n\in\mathbb{N}$, we define what it means that a model satisfies a formula of depth $n$.

On the other hand, in our paper, non-full models will play a crucial role and in some specific circumstances we are going to say that a model satisfies a theory. This will be defined in some specific cases of our interest later in Definition 29.

Let us define some more notions which will be particularly important in further parts of our paper.

Definition 7**.**

Let $\mathcal{M},\mathcal{N}$ be full models of theories in the same language. We say that $\mathcal{N}$ is an elementary extension of $\mathcal{M}$ if $\mathcal{M}$ is contained in $\mathcal{N}$.

Recall that officially, a full model is the same as the elementary diagram of that model, so elementary submodels in our sense correspond to elementary submodels in the usual sense. In what follows, we will sometimes conflate an elementary submodel with an image of the elementary embedding. This should be understood in the obvious way: a formula $\phi(x,y)$ defines an elementary embedding between models $\mathcal{M}$ and $\mathcal{N}$ if it is a injection on elements of the models $\mathcal{M},\mathcal{N}$ (i.e., it is a relation on constants such that $\phi(a,b_{1}),\phi(a,b_{2})$ together imply $(b_{1}=b_{2})\in\mathcal{N}$ and $\phi(a_{1},b),\phi(a_{2},b)$ together imply that $(a_{1}=a_{2})\in\mathcal{M}$) and the image is an elementary submodel of $\mathcal{M}$ (i.e, the restriction of $\mathcal{N}$ to the language with constants representing the image of $\mathcal{M}$ is a full model).

We will denote both being an elementary submodel and being an image of an elementary embedding with

[TABLE]

Sometimes we only require that the elementarity relation only holds for formulae in a language $\mathcal{L}$ such that $\mathcal{M},\mathcal{N}$ are full models over a language containing $\mathcal{L}$. We then write:

[TABLE]

Crucially, in this paper we will be looking at the situation where $\mathcal{M}$ is a full model, $\mathcal{N}$ is a (non-full) model over a bigger language and $\mathcal{N}$ is an $\mathcal{L}$-elementary extension of $\mathcal{M}$. This is a slightly subtler notion which will be made precise in Definition 30.

Definition 8**.**

Let $\mathcal{M},\mathcal{N}$ be models or full models in languages $\mathcal{L}_{\mathcal{M}}$, $\mathcal{L}_{\mathcal{N}}$ respectively. We say that $\mathcal{N}$ is an expansion of $\mathcal{M}$ if the following conditions are satisfied:

• •

$\mathcal{L}_{\mathcal{M}}\subseteq\mathcal{L}_{\mathcal{N}}$.

• •

For every element $a\in N$ there is an element $b\in M$ such that $\mathcal{N}\models x=y[\alpha]$, where $\alpha(x)=a$, $\alpha(y)=b$. (That is, the domain does not change. We write it in this slightly convoluted manner, since we want the definition to work both for models and full models).

• •

For every atomic formula $\phi\in\mathcal{L}_{\mathcal{M}}$ and $\mathcal{M}$-assignment $\alpha$ for $\phi$, $\mathcal{M}\models\phi[\alpha]$ if and only if $\mathcal{N}\models\phi[\alpha]$.

We can say that PA is capable of handling basic model theory, since it is able to capture the link between models and consistent theories. In the context of our definitions, this means that in PA every consistent theory can be extended to a complete consistent theory with Henkin constants.

Theorem 9** (Arithmetized Completeness Theorem).**

For every $n\in\mathbb{N}$, PA proves that if $\mathcal{T}$ is a consistent $\Delta_{n}$-theory, then it has a $\Delta_{n+1}$-full model.

By $\Delta_{n}$-theory, we mean a set of sentences defined both with a $\Sigma_{n}$-formula and a $\Pi_{n}$-formula. $\Delta_{n+1}$-full model is defined in an analogous way. The above theorem is standard, cf. Section 13.2 of Kaye’s book [11]. Throughout the paper, we will be using the following handy conventions concerning models:

Convention 10**.**

When there is no risk of confusion, we will use the same symbol for a predicate symbol and for its denotation in a given (full) model. 2. 2.

We will sometimes denote (full) models as tuples, like $(\mathcal{M},T)$. This will simply mean that $(\mathcal{M},T)$ is an expansion of $\mathcal{M}$ with a predicate $T$.

2.3 Lengths of proofs

This section summarizes the basic definitions and tools that we will need in connection with analysing lengths of proofs; much of this material is taken from Pudlák’s survey article [18].

Definition 11**.**

Recall that $|\phi|$ denotes the length of binary code of $\phi$ and $\underline{\ulcorner\phi\urcorner}$ is its Gödel number (which we denote as $\underline{\phi}$ by our Convention 4).

Let $\phi$ be an $\mathcal{L}_{\mathcal{T}}$-formula.

[TABLE] 2. 2.

If $\parallel\phi\parallel_{\mathcal{T}}\leq n$, we write also

[TABLE]

We treat theories simply as sets of sentences, not necessarily closed under deductions. This is because changing the axiomatization of a theory might result in facilitating proofs.

Definition 12** (Simulations, Speed-up, Reducibility).**

Let $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ be two theories and $\mathcal{F}$ a family of functions $f:\mathbb{N}\rightarrow\mathbb{N}$. We shall say that $\mathcal{T}_{1}$ $\mathcal{F}$-simulates $\mathcal{T}_{2}$ iff there exists a function $f\in\mathcal{F}$ such that for every sentence $\phi\in\mathcal{L}_{\mathcal{T}_{1}}\cap\mathcal{L}_{\mathcal{T}_{2}}$ that is provable in both $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$, and for every $n\in\mathbb{N}$, we have:

[TABLE]

We say that $\mathcal{T}_{2}$ is $\mathcal{F}$-reducible to $\mathcal{T}_{1}$ if there exists a function $f\in\mathcal{F}$ such that for every $n\in\mathbb{N}$ we have:

[TABLE]

We say that $\mathcal{T}_{2}$ has a super-$\mathcal{F}$ speed-up over $\mathcal{T}_{1}$ if $\mathcal{T}_{1}$ does not $\mathcal{F}$-simulate $\mathcal{T}_{2}$.

Typical examples in the literature of speed-up (simulability) phenomena concern the cases where $\mathcal{F}$ is the family of either polynomial or elementary functions, which respectively correspond to super-polynomial speed-up (or polynomial simulation) and super-exponential (or super-elementary) speed-up.

Remark 13**.**

The main focus of our paper is the relation of $\mathcal{F}$-reducibility, where $\mathcal{F}$ is the family of all P-time computable functions. Recall that $f$ is a P-time computable function if it is a total function such that for each $n$ (the binary code of) $f(n)$ can be computed by a deterministic Turing machine which takes as input (the binary code of) $n$ (see [9] for the precise formulation) and which runs in polynomial time. We call this relation feasible reducibility.

The proofs of the following observations are routine:

Observation 14**.**

Let $\mathcal{F}$ be any family of functions from $\mathbb{N}$ to $\mathbb{N}$.

If $\mathcal{T}_{2}$ is $\mathcal{F}$-reducible to $\mathcal{T}_{1}$, then $\mathcal{T}_{1}$ $\mathcal{F}$-simulates $\mathcal{T}_{2}$. Moreover if $\mathcal{T}_{2}$ is feasibly reducible to $\mathcal{T}_{1}$, then $\mathcal{T}_{1}$ polynomially simulates $\mathcal{T}_{2}$. 2. 2.

If $\mathcal{F}$ is countable, then $\mathcal{T}_{2}$ has a super $\cal{F}$ speed-up over $\mathcal{T}_{1}$ if there exists an infinite sequence of formulae $\phi_{0},\phi_{1},\ldots,$ provable in both $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ such that for every function $f\in\mathcal{F}$ there exists $n\in\mathbb{N}$ such that

[TABLE]

The most prominent role in the investigations in the lengths of proofs is played by consistency statements. We shall now discuss arithmetized provability. Recall that $|n|$ denotes the length of the binary expansion of $n$.

Definition 15** (Pudlák, [17]).**

Let $\mathcal{T}$ be a theory, $\phi(x_{0},\ldots,x_{n})$ be a formula and $R\subseteq\mathbb{N}^{k+1}$ be a relation. We say that $\phi$ polynomially numerates $R$ in $\mathcal{T}$ if there exists a polynomial $p(x_{0},\ldots,x_{k})$ such that for all natural numbers $n_{0},\ldots,n_{k}$

[TABLE]

Theorem 16** (Pudlák, [17] Theorem 3.2).**

For any consistent theory $\mathcal{T}\supseteq\textnormal{{Q}}$ with an NP-time set of axioms555An NP-time set or relation is one whose characteristic function can be computed by a non-deterministic Turing machine that runs in polynomial time. and any $R\subseteq\mathbb{N}^{k}$ the following are equivalent:

$R$* is an NP-time relation;* 2. 2.

$R$* is polynomially numerable in Q;* 3. 3.

$R$* is polynomially numerable in $\mathcal{T}$.*

Since on hand in our paper, we want slightly stronger results concerning feasible reducibility between theories rather than mere facts about speed-up, and on the other, we work with relatively strong theories anyway, we will use a modification of Pudlák’s result, (which actually is simpler than the original theorem).

Definition 17**.**

Let $\mathcal{T}$ be a theory, $\phi(x_{0},\ldots,x_{n})$ be a formula and $R\subseteq\mathbb{N}^{k+1}$ be a relation. We say that $\phi$ uniformly polynomially numerates $R$ in $\mathcal{T}$ if there exists a P-time computable function $f$ such that for all natural numbers $n_{0},\ldots,n_{k}$, $R(n_{0},\ldots,n_{k})$ holds iff $f(n_{0},\ldots,n_{k})$ is a proof of $\phi(\underline{n_{0}},\ldots,\underline{n_{k}})$ in $\mathcal{T}$.

In what follows, we need only the following simple fact which may be proved by a natural formalisation of Turing Machines in $\textnormal{{I}}\Delta_{0}+\textnormal{{Exp}}$. It is significantly simpler than Pudlák’s result, since we do not need to consider cuts or use cut-shortening techniques.

Theorem 18**.**

For any consistent theory $\mathcal{T}\supseteq\textnormal{{I}}\Delta_{0}+\textnormal{{Exp}}$ with a set of axioms computable in polynomial time, and any $R\subseteq\mathbb{N}^{k}$ the following are equivalent:

$R$* is a P-time relation;* 2. 2.

$R$* is uniformly polynomially numerable in $\textnormal{{I}}\Delta_{0}+\textnormal{{Exp}}$;* 3. 3.

$R$* is uniformly polynomially numerable in $\mathcal{T}$.*

Corollary 19**.**

Let $\mathcal{T}$ be a theory with a P-time set of axioms. Then there exists a formalization of the relation

[TABLE]

and a polynomially computable function $f(n)$ such that

[TABLE]

implies that $f(n,m)$ is a proof of $\textnormal{{Proof}}_{\mathcal{T}}(\underline{m},\underline{n})$ in $\textnormal{{I}}\Delta_{0}+\textnormal{{Exp}}$.

Moreover, we define formulae Con and Pr in the usual manner as follows:

[TABLE]

and

[TABLE]

If not stated otherwise, throughout this paper $\mathcal{T}$, and $\mathcal{T}_{i}$ for $i\in\mathbb{N}$ range over P-time axiomatizable theories.

Remark 20** (Relativized provability predicates).**

The content of this remark will be needed only in Section 4.4. The formalization of the provability predicate from Corollary 19 is of the form: "There exists an accepting computation of the Turing machine which recognizes $\mathcal{T}$ proofs". Let $\phi(x)$ be any arithmetical formula. By writing

[TABLE]

we mean the relativized version of the above predicate, i.e., the one in which the relevant Turing machine is supplied with an oracle given by $\phi$ and recognizes the theorems of $\mathcal{T}+\phi$ (whatever $\phi$ means). We can treat $\mathcal{T}+\phi$ as a new arithmetized theory, but then in typical cases it won’t be $\Delta_{1}$. This is why we decide to distinguish between the roles played by the lower and the upper indices in $\textnormal{{Proof}}_{\mathcal{T}}^{\phi}(x,y)$: the former will be reserved for theories satisfying the thesis of Corollary 19 and the latter for arbitrary formulae, playing the roles of oracles. Obviously the relativized version of Corollary 19 need not be true, but we will only demand that the following two conditions hold:

There exists a P-time computable function $f$ such that for all $n$ and all $\phi(x)$, $f(n,\ulcorner\phi\urcorner,\ulcorner\mathcal{T}\urcorner)$ is a PA proof of

[TABLE]

where $\mathcal{T}$ denotes the chosen arithmetical definition of $\mathcal{T}$. 2. 2.

Likewise, there exists a P-time computable function $g$ such that $g(\ulcorner\phi\urcorner,\ulcorner\psi\urcorner,\ulcorner\mathcal{T}\urcorner)$ is a PA proof of the sentence

[TABLE]

This requires that $\textnormal{{Proof}}_{\mathcal{T}}^{\phi}(y,z)$ be constructed uniformly in $\phi$, which can certainly be assured.

In particular, $\textnormal{{Proof}}_{\mathcal{T}}^{\phi}(x,y)$ is of length polynomial in the lengths of $\phi$ and the chosen definition of $\mathcal{T}$. As usual

[TABLE]

and

[TABLE]

The following theorem gives a canonical example of a family of sentences whose proofs grow super-exponentially. Let $\textnormal{{Pr}}_{\mathcal{T}}(\underline{m},\underline{n})$ denote the canonical sentence expressing "there is a proof of sentence $n$ from the axioms of $\mathcal{T}$ of length at most $m$." Then $\textnormal{{Con}}_{\mathcal{T}}(\underline{m}):=\neg\textnormal{{Pr}}_{\mathcal{T}}(\underline{m},0=1)$.

Theorem 21** (Pudlák,[18], Theorem 7.2.2).**

Let $\mathcal{T}$ be a sufficiently strong theory. Let $f$ be an increasing computable function, provably total in $\mathcal{T}$, whose graph has a polynomial numeration in $\mathcal{T}$. Then there exists a $\delta>0$ such that

[TABLE]

In particular, for $f(n):=2_{n}$, where $2_{0}:=1$, and $2_{n+1}:=2^{2_{n}}$, there is some some $\delta>0$ such that:

[TABLE]

2.4 Feasible truth predicates

Now we turn to arithmetized partial truth predicates, which we want to apply to arbitrary sentences of fixed complexity, defined here in a way that is different from the usual one (i.e., $\Sigma_{n}$, $\Pi_{n}$). The measure of complexity will be given by the depth of formulae, as defined below.

Definition 22**.**

The depth of a formula is the length of the longest path in its syntactic tree (which is allowed to contain arbitrary terms as leaves). $\textnormal{{dp}}(\phi,n)$ denotes an arithmetical formula representing the relation "The depth of a formula $\phi$ is at most $n$." We will also write it as $\textnormal{{dp}}(\phi)\leq n$.

For example $0=0\wedge\forall x\neg(SSS(x)=0)$ has depth $3$.

To state some results in greater generality we will use Pudlák’s notion of sequential theories (since there seems to be more than one good definition of sequentiality, we include Pudlák’s definition):

Definition 23** (Pudlák, [17]).**

A theory $\mathcal{T}$ is sequential, if

Robinson’s arithmetic Q is interpretable in $\mathcal{T}$ relativized to some formula $N(x)$ of $\mathcal{L}_{\mathcal{T}}$ and 2. 2.

there exists a formula $(x)_{t}$ (of two variables $x$, $t$) that defines in $\mathcal{T}$ a total function (in both variables) and such that $\mathcal{T}$ proves

[TABLE]

Now the promised "feasible" partial truth predicates:

Theorem 24** (Pudlák, [18], Theorem 3.3.1).**

Let $\mathcal{T}$ be a sequential theory. There is a family of formulae $\textnormal{{Sat}}_{n}(x,y)\in\mathcal{L}_{\mathcal{T}}$ and a polynomial $q(x)$ such that for every $n$ there exists a $\mathcal{T}$-proof of compositional Tarski’s conditions for $\textnormal{{Sat}}_{n}(x,y)$ such that the size of that proof is less than $q(n)$. Moreover for every $\phi(x_{1},\ldots,x_{k})$ of length less than $n$, the shortest $\mathcal{T}$ proof of

[TABLE]

is less than $q(n)$.

Moreover, by inspection of Pudlák’s proof one quickly sees that in fact finding the above mentioned proofs of polynomial length is feasible. This means that the above theorem can be slightly strengthened as in the theorem below.

Theorem 25**.**

Let $\mathcal{T}$ be a sequential theory. There is a family of formulae $\textnormal{{Sat}}_{n}(x,y)\in\mathcal{L}_{\mathcal{T}}$ and P-time computable functions $f(x)$, $g(x,y)$ such that for every $n$, $f(n)$ is a $\mathcal{T}$ proof of compositional Tarski’s conditions for $\textnormal{{Sat}}_{n}(x,y)$. Moreover for every $\phi(x_{1},\ldots,x_{k})$ of length less than $n$, $g(\ulcorner\phi\urcorner,n)$ is a $\mathcal{T}$-proof of

[TABLE]

In what follows, $\textnormal{{Tr}}_{n}(x)$ abbreviates $\textnormal{{Sat}}_{n}(x,\varnothing)$.

Observation 26**.**

There exists a P-time computable function $f$ such that for every $k\leq n$, $f(n,k)$ is a proof in PA of

[TABLE]

The proof uses induction (in PA) on the complexity of $\phi$ and provable Tarski biconditionals for $\textnormal{{Tr}}_{l}$ predicates.

In further parts of the paper, we will also need the relativized version of the Theorem 25 (we state it only for PA). If $\mathcal{M}$ is a $\Delta_{k}$-model (not necessarily a full one) for a language $\mathcal{L}^{\prime}$ with finitely many fresh non-arithmetical relational symbols, then by $\mathcal{M}$-relativized Tarski’s conditions for a formula $\Phi(x,y)$ we mean the usual statement that $\Phi(x,y)$ satisfies Tarski’s compositional truth conditions in which the condition for atomic formulae is:

[TABLE]

for an arbitrary relation $R$ in $\mathcal{L}^{\prime}$, and the condition for the existential quantifier is given by

[TABLE]

Corollary 27**.**

Let $\mathcal{M}$ be any $\Delta_{k}$-model. There is a family of formulae $\textnormal{{Sat}}^{\mathcal{M}}_{n}(x,y)\in\textnormal{{Form}}_{\mathcal{L}}$ and P-time computable functions $f(x,y)$, $g(x,y,z)$ such that for every $n$, $f(\ulcorner\mathcal{M}\urcorner,n)$ is a PA-proof of the $\mathcal{M}$-relativized compositional Tarski’s conditions for $\textnormal{{Sat}}^{\mathcal{M}}_{n}(x,y)$. Moreover for every $\phi(x_{1},\ldots,x_{k})$ of length less than $n$, $g(\ulcorner\mathcal{M}\urcorner,\ulcorner\phi\urcorner,n)$ is a PA-proof of

[TABLE]

The family $\textnormal{{Sat}}_{n}^{\mathcal{M}}(x,y)$ can be defined essentially by relativizing $\textnormal{{Sat}}_{n}(x,y)$ predicates from Theorem 24. Since the definition of $\mathcal{M}$ does not depend on $n$, the length of $\textnormal{{Sat}}_{n}^{\mathcal{M}}(x,y)$ will be polynomial in $n$.

As above, we will write $\textnormal{{Tr}}_{n}^{\mathcal{M}}$ to denote satisfaction under the empty valuation. Occasionally, we will use the handy notational convention described below.

Convention 28**.**

If $\phi(v_{1},\ldots,v_{n})\in\textnormal{{Form}}$ is a formula with standardly many many variables, we will be writing $\textnormal{{Sat}}_{k}(\phi,a_{1},\ldots,a_{n})$ to denote

[TABLE]

where $\alpha\in\textnormal{{Asn}}(\phi)$ is some valuation which assigns $a_{1},\ldots a_{n}$ to the variables $(v_{1},\ldots,v_{n})$.

Let us end this subsection with a definition of satisfaction of theories for a larger class of models.

Definition 29**.**

Let $n\in\mathbb{N}$. Let $\mathcal{M}\models\textnormal{{B}}$ be a model over a language $\mathcal{L}$ and let $(\mathcal{M},T)$ be its expansion to an $\mathcal{L}^{\prime}$-structure. Suppose that $\mathcal{T}$ is a theory over the language $\mathcal{L}^{\prime}$ such that $\mathcal{T}\setminus\textnormal{{B}}$ consists only of sentences of depth $\leq n$. We say that

[TABLE]

if $(\mathcal{M},T)\models\textnormal{{Tr}}_{n}(\phi)$ for all $\phi\in\mathcal{T}\setminus\textnormal{{Sent}}_{\mathcal{L}}$.

The above definition is actually a scheme. We define separately for all standard $n$ what it means for an expanded structure to satisfy a theory whose axioms have depth bounded by $n$. Note that whenever $(\mathcal{M},T)$ is an expansion of a full model $\mathcal{M}\models\textnormal{{B}}$ and $\mathcal{T}$ extends B with finitely many standard sentences $\phi_{1},\ldots,\phi_{n}$, the condition $(\mathcal{M},T)\models\mathcal{T}$ means simply that $(\mathcal{M},T)\models\phi_{i}$ for $i\leq n$. Let us introduce one more definition in the similar spirit.

Definition 30**.**

Let $\mathcal{M},\mathcal{N}\models\textnormal{{B}}$, where B is a theory over language $\mathcal{L}$. Let $\mathcal{T}$ be a theory over language $\mathcal{L}^{\prime}$ such that $\mathcal{T}\setminus\textnormal{{B}}$ consists only of sentences of depth $\leq n$. Suppose that $(\mathcal{N},T)\models\mathcal{T}$ is an expansion of $\mathcal{N}$. We say that $(\mathcal{N},T)$ is an $\mathcal{L}$-elementary extension of $\mathcal{M}$ if $\mathcal{N}$ is an elementary extension of $\mathcal{M}$. We denote it with

[TABLE]

2.5 Polynomial simulations and feasible reductions for theories extending PA.

Let us fix $\mathcal{T}_{2}\supseteq\mathcal{T}_{1}\supseteq\textnormal{{PA}}$ such that $\mathcal{T}_{2}$ conservatively extends $\mathcal{T}_{1}$. It turns out that in order to verify that $\mathcal{T}_{2}$ is feasibly reducible to $\mathcal{T}_{1}$ it is sufficient to demonstrate that the formalized conservativity statements for finite fragments of $\mathcal{T}_{2}$ over finite fragments of $\mathcal{T}_{1}$ are feasibly provable in $\mathcal{T}_{1}$. The theorem below makes this precise.666We are grateful to Fedor Pakhomov who pointed out to us that this is the most direct way of proving our main results. Our previous proofs employed the conceptually more transparent—but technically more demanding—framework of feasible interpretations, as explained in Subsection 4.4. Before stating the theorem, we need a definition.

Definition 31**.**

Let $\mathcal{T}$ be a theory. By $\mathcal{T}\upharpoonright_{n}$ we mean the set of axioms of $\mathcal{T}$ of length at most $n$. Abusing notation, we treat $\mathcal{T}\upharpoonright_{\underline{n}}$ as the canonical formula representing $\mathcal{T}\upharpoonright_{n}$ in $\textnormal{{I}}\Delta_{0}+\textnormal{{Exp}}$.

Theorem 32**.**

Let $\mathcal{T}$ be a theory extending PA with an NP-set of axioms. If there is a polynomial $p(n)$ such that for every $n\in\mathbb{N}$,

[TABLE]

then PA polynomially simulates $\mathcal{T}$. Moreover, if $\mathcal{T}$ admits a P-time computable set of axioms and there exists a P-time computable function $f$ and a polynomial $p(n)$ such that for all $n$, $f(n)$ is a PA-proof of

[TABLE]

then $\mathcal{T}$ is feasibly reducible to PA.

Recall that $\textnormal{{dp}}(\phi)$ is the height of the syntactic tree of $\phi$ and that we use this symbol for the arithmetic formula representing this function. The proof of Theorem 32 will be facilitated by the following lemma which shows that PA is feasibly strongly reflexive.

Lemma 33**.**

There exists a P-time computable function $f$ such that for every $n,k\in\mathbb{N}$, $f(n,k)$ is a PA proof of:

[TABLE]

Proof of Lemma 33.

The proof follows the usual pattern, but we have to check that each transformation at work is feasible. Here we provide the general outline; the details are verified carefully in Subsection 6.1 of the Appendix. Assume first that $n\leq k$. Working in PA, we first prove cut-elimination for First Order Logic (this is a single sentence independent of $n$). Then we show that every axiom of PA of length $\leq n$ is true. For finitely many axioms of Robinson’s Q, this is done independently of $n$. For induction axioms of length at most $n$ we use Proposition 80, and for logical axioms we use Proposition 79. Next we apply cut-elimination over First Order Logic to show that for a sentence $\phi$ of depth $\leq k$ if $\textnormal{{Pr}}_{\textnormal{{PA}}\upharpoonright_{n}}(\phi),$ then there is a cut-free proof of a sequent

[TABLE]

where $\Gamma$ contains only axioms of $\textnormal{{PA}}\upharpoonright_{\underline{n}}$. By the subformula property, in such a proof every formula is of depth bounded by $k$. Then, using induction on the number of proof lines in a proof using only formulae of depth at most $k$, we show that if

[TABLE]

is provable, then we have:

[TABLE]

where $\alpha\in\textnormal{{Asn}}(\Gamma\cup\Delta)$ abbreviates $\forall x\in\Gamma\cup\Delta\ \ \alpha\in\textnormal{{Asn}}(x)$, as in Definition 1. Since we already know that all $\textnormal{{PA}}\upharpoonright_{n}$ axioms are true, we conclude that $\phi$ is true.

If $k\leq n$, then it is sufficient to carry out the above proof substituting $n$ for $k$ everywhere and use Observation 26. Note that all the transformations above are uniform in $n,k$, hence in particular they give rise to a function $f$ as in the thesis of the lemma. ∎

Proof of Theorem 32.

Assume $\mathcal{T}\vdash^{n}\phi$ and $\phi\in\mathcal{L}_{\textnormal{{PA}}}$. Then in fact $\mathcal{T}\upharpoonright_{n}\vdash\phi$ and $\phi$ is of depth at most $n$. Let $k$ code this proof. Then, by the properties of the provability predicate we have:

[TABLE]

Hence also $\textnormal{{PA}}\vdash\textnormal{{Pr}}_{\mathcal{T}\upharpoonright_{\underline{n}}}(\phi)$. By the formalized conservativity we have that $\textnormal{{PA}}\vdash\textnormal{{Pr}}_{\textnormal{{PA}}\upharpoonright_{\underline{p(n)}}}(\phi)$; by Lemma 33, we have $\textnormal{{PA}}\vdash\textnormal{{Tr}}_{p(n)}(\phi)$; and by feasibly provable $T$-biconditionals (Theorem 24) we obtain $\textnormal{{PA}}\vdash\phi$. All the intermediate steps are polynomial in $n$.

Also, if $\mathcal{T}$ has a P-time computable axiomatization, by Corollary 19 there exists a P-time computable function $h$ such that given a proof $k\in\mathcal{T}$ of a formula $\phi$, $h(k)$ is the proof of the sentence

[TABLE]

Given a function $f$ as in our assumptions and the function $f^{\prime}$ as in Lemma 33 one easily defines the appropriate feasible reduction by concatenating the proofs given by $f$, $f^{\prime}$ and $h$ as in the proof for polynomial simulation. ∎

Corollary 34**.**

Suppose that there exists a polynomial $p(n)$ and there is a $k\in\mathbb{N}$ such that for every $n\in\mathbb{N}$, $\textnormal{{PA}}\vdash^{p(n)}\theta_{n}$, where $\theta_{n}$ expresses "Every $\Delta_{2}$-full model of $\textnormal{{PA}}\upharpoonright_{\underline{p(n)}}$ has an $\mathcal{L}_{\textnormal{{PA}}}$-elementary extension to a full $\Delta_{k}$-model of $\mathcal{T}\upharpoonright_{\underline{n}}$." Then PA polynomially simulates $\mathcal{T}$. Moreover, if $\mathcal{T}$ is P-time, and there exists a P-time function $f$ such that for all $n\in\mathbb{N}$, $f(n)$ is a PA-proof of $\theta_{n}$, then $\mathcal{T}$ is feasibly reducible to PA.

Let us make one remark before we proceed to the proof of Corollary 34. Recall from Subsection 2.2 that in the current paper we treat full models as specific arithmetically definable sets of sentences. Note that although we cannot quantify over models in general, we can do this for models of fixed quantifier complexity using arithmetical satisfaction predicates.

Proof of Corollary 34.

Fix $k$ and polynomial $p$. We shall prove the assumptions of Theorem 32. Fix $n$. Start the proof by showing $\theta_{n}$ using a subproof of length $p(n)$. Then fix $\phi$ of depth $\leq n$ and assume:

[TABLE]

It immediately follows that $\textnormal{{PA}}\upharpoonright_{\underline{p(n)}}+\neg\phi$ is consistent. We check that this is a $\Delta_{1}$-theory (this verification is polynomial in the definition of $\textnormal{{PA}}\upharpoonright_{\underline{p(n)}}+\neg\phi$, hence polynomial in $n$). We prove the Arithmetized Completeness Theorem 9 for $\Delta_{1}$-theories; this is independent of $n$ and gives us a $\Delta_{2}$-full model of $\textnormal{{PA}}\upharpoonright_{\underline{p(n)}}+\neg\phi$. Now, by $\theta_{n}$, this model has an elementary extension to a full model of $\mathcal{T}\upharpoonright_{\underline{n}}$. By elementarity $\mathcal{T}\upharpoonright_{\underline{n}}+\neg\phi$ is consistent, which ends the feasible proof of the conservativity claim.

The proof of moreover part of the theorem is fully analogous: we apply it to the respective part of Theorem 32. ∎

Corollary 35**.**

Suppose there is a polynomial $p(n)$ and there is a $k\in\mathbb{N}$ such that for every $n\in\mathbb{N}$, $\textnormal{{PA}}\vdash^{p(n)}\theta_{n}$, where $\theta_{n}$ expresses "Every $\Delta_{2}$-full model of $\textnormal{{PA}}\upharpoonright_{p(n)}$ has an $\mathcal{L}_{\textnormal{{PA}}}$-elementary extension to a $\Delta_{k}$-model of $\mathcal{T}\upharpoonright_{n}$." Then PA polynomially simulates $\mathcal{T}$. Moreover, if $\mathcal{T}$ is P-time and there exists a P-time computable function $f$ such that for all $n$, $f(n)$ is a PA-proof of $\theta_{n}$, then $\mathcal{T}$ is feasibly reducible to PA.

Note that above $\mathcal{L}_{\textnormal{{PA}}}$-elementary extensions are understood in the sense of Definition 30.

Proof.

We show that the above assumption implies the assumption of the previous corollary. Fix $\mathcal{T}$. Take $p(n)$ and $k$ as in the assumptions. Work in PA. Fix an arbitrary $\Delta_{2}$-full model $\mathcal{M}$ of $\textnormal{{PA}}\upharpoonright_{\underline{p(n)}}$. Then there exists a $\Delta_{k}$-model $\mathcal{N}\models\mathcal{T}\upharpoonright_{n}$ which is an elementary extension of $\mathcal{M}$. We argue that the $\Delta_{2}$-theory

[TABLE]

is consistent. This will finish the proof, since by Arithmetized Completeness Theorem we will get a $\Delta_{3}$-full model of this theory (the length of this subproof is polynomial in $n$ as the proof of ACT is independent of $n$).

Take an arbitrary proof $\pi$ of a sentence $\phi$ in $\Phi$ and prove cut-elimination for first order logic (the length of this proof is independent of $n$) and conclude that there exists a proof $\pi^{\prime}$ of $\phi$ in $\Phi$ with the subformula property. It follows that every formula in this proof is either an arithmetical formula or is a subformula of an additional axiom of $\mathcal{T}\upharpoonright_{\underline{n}}$. In particular non-arithmetical formulae which occur in this proof are of depth bounded by $n$. Define:

[TABLE]

where $\textnormal{{Sat}}^{\mathcal{N}}_{n}(x,y)$ is a feasible relativized truth predicate from Corollary 27. By induction on the length of $\pi^{\prime}$ show that if $\Gamma\longrightarrow\Delta$ occurs in $\pi^{\prime}$, then for every $\alpha$

[TABLE]

It follows that $\pi^{\prime}$ cannot be a proof of the empty sequent, hence $\Phi$ is consistent. ∎

The following is the ultimate corollary that best fits the proofs of our main results:

Corollary 36**.**

Suppose that $\mathcal{T}$ is a finite extension of PA of the form $\textnormal{{PA}}+\phi$, $k\in\mathbb{N}$ and the following sentence is provable in PA:

"If B is any finite fragment of PA, then every $\Delta_{2}$-full model of B has an $\mathcal{L}_{\textnormal{{PA}}}$ elementary extension to a $\Delta_{k}$-model of $\textnormal{{B}}+\phi$."

Then $\mathcal{T}$ is feasibly reducible to PA.

Proof.

The assumptions of Corollary 36 clearly implies that the assumptions of Corollary 35, as the verification that B is a $\Delta_{1}$-finite fragment of PA can be done quickly and uniformly in $n$. ∎

We will end this subsection with two simple observations which may be obtained by inspection of the proof of Theorem 32 and the proof of subsequent corollaries. They provide some slightly different sufficient condition for feasible reducibility. Observation 38 will be useful in Subsection 4.3.

Observation 37**.**

Suppose that $\mathcal{T}$ is a theory with a P-time set of axioms which is PA-provably feasibly strongly reflexive, i.e., there exists a P-time computable function $h$ such that for each $n,k\in\mathbb{N}$, $h(n,k)$ is a PA proof of the sentence

[TABLE]

Then $\mathcal{T}$ is feasibly reducible to PA.

Observation 38**.**

Suppose that $\mathcal{T}$ satisfies assumptions of Corollary 35 (with the "moreover" part) or Corollary 36. Then $\mathcal{T}$ is PA-provably feasibly strongly reflexive.

Proof.

By (very direct) inspection of proofs of Corollaries 35 and 36, we see that if $\mathcal{T}$ satisfies assumptions of any of these statements, then there exists a P-time computable function $f$ and a polynomial $p(n)$ such that for each $n\in\mathbb{N}$, $f(n)$ is a PA-proof of

[TABLE]

It follows that $\mathcal{T}$ is PA-provably feasibly strongly reflexive. Indeed , fix the above mentioned function $f$, polynomial $p$ and $g$ witnessing the feasible reflexivity of PA. We define $h(n,k)$. Compute first $f(n)$, then compute $g(p(n),k)$, i.e. the proof of

[TABLE]

Then after performing some fixed number of logical transformations obtain the proof of * ‣ 37. ∎

2.6 Feasible interpretability and speed-up

This section presents sufficient conditions for feasible interpretability, a notion that will be only used in Subsection 4.4. All the basic notions relied to relative interpretability can be found in [9], Chapter III. We begin with an observation of Albert Visser, presented in [7].777The formulation of the cited theorem is, however, is not quite right since it is claimed that it holds without any restrictions on $\mathcal{T}_{2}$, which is incorrect, e.g., let $s\textnormal{{PA}}:=\textnormal{{PA}}+\left\{\textnormal{{Con}}_{\textnormal{{PA}}}(2_{\underline{n}})\ \ |\ \ n\in\mathbb{N}\right\}$. Then the identity interpretation witnesses relative interpretability of $s\textnormal{{PA}}$ in PA, but the former theory has super-exponential speed-up over the latter. However, with the proviso that $\mathcal{T}_{2}$ is fintiely axiomatizable the proof goes through. Also the proof of our Proposition 42 can be easily adapted to this case.

Theorem 39**.**

Suppose that $\mathcal{T}_{2}\supseteq\mathcal{T}_{1}$, where both $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ are formulated in the language of PA and $\mathcal{T}_{2}$ is finitely axiomatizable and relatively interpretable in $\mathcal{T}_{1}$. Then $\mathcal{T}_{1}$ polynomially simulates $\mathcal{T}_{2}$ with respect to $\Pi_{1}$-sentences.

The crucial insight in the proof of the above theorem is that relative interpretations are always $\Pi_{1}$-correct if the interpreting theory is an extension of PA in the same language, i.e., for every $\Pi_{1}$-sentence $\phi$ of $\mathcal{L}_{\mathcal{T}_{1}}$ we have:

[TABLE]

where $I$ is the chosen relative interpretation of $\mathcal{T}_{2}$ in $\mathcal{T}_{1}$.

The next definition is formulated so as to allow us to lift the $\Pi_{1}$-correctness in Theorem 39 to wider-and-wider class of sentences so as to establish polynomial simulations of non-finitely axiomatizable theories.

Definition 40**.**

Let $\mathcal{T}_{1}$, $\mathcal{T}_{2}$ be two theories each of which has an NP-set of axioms.

An interpretation $I:\mathcal{T}_{2}\rightarrow\mathcal{T}_{1}$ is $n$-correct if for an arbitrary sentence $\phi$ of depth $n$ we have:

[TABLE] 2. 2.

An interpretation $I:\mathcal{T}_{2}\rightarrow\mathcal{T}_{1}$ is *feasible888Feasible interpretations are thoroughly investigated in Verbrugge’s doctoral thesis [20]. In particular, as shown in Theorem 6.4.2 of [20], there is a sentence $\theta$ such that $\textnormal{{PA}}+\theta$ is interpretable in PA, and yet there is no feasible interpretation of $\textnormal{{PA}}+\theta$ in PA. * if there is a polynomial $p(n)$ such that for all arbitrary sentences $\phi$ and all $n\in\mathbb{N}$ we have:

[TABLE] 3. 3.

A family of interpretations $\{I_{n}\}_{n\in\mathbb{N}}:\mathcal{T}_{2}\rightarrow\mathcal{T}_{1}$ is polynomially correct if for each $n$, $I_{n}$ is $n$-correct and there exists a polynomial $p(n,k)$ such that the following two conditions hold:

1. (a)

$p(n,k)$ witnesses that $I_{k}$ is a feasible interpretation, i.e., for every $k,n\in\mathbb{N}$, and for every sentence $\phi$ of $\mathcal{L}_{\mathcal{T}_{2}}$,

[TABLE]

. 2. (b)

For every $k\in\mathbb{N}$ and every sentence $\phi$ of length at most $k$,

[TABLE] 4. 4.

A family of interpretations $\{I_{n}\}_{n\in\mathbb{N}}:\mathcal{T}_{2}\rightarrow\mathcal{T}_{1}$ is uniformly polynomially correct if for each $n$, $I_{n}$ is $n$-correct and there exist P-time computable functions $f$, $g$ such that the following two conditions hold:

1. (a)

For every $k\in\mathbb{N}$, and every $\mathcal{T}_{2}$-proof $\pi$ of $\phi\in\mathcal{L}_{\mathcal{T}_{2}}$ $f(k,\pi)$ is a $\mathcal{T}_{1}$-proof of $\phi^{I_{k}}$. 2. (b)

For every $k\in\mathbb{N}$, and every sentence $\phi$ of length at most $k$, $g(k,\ulcorner\phi\urcorner)$ is a $\mathcal{T}_{1}$-proof of

[TABLE]

Remark 41**.**

In the context of theories with no additional rules of reasoning, condition (a) in the definition of polynomial correctness (point 3.) can equivalently be replaced with the following one

1. (a)’.

For every $k$,

[TABLE]

for every axiom $\phi$ of $\mathcal{T}_{2}$ (including the logical axioms for $\mathcal{L}_{\mathcal{T}_{2}}$) of length at most $n$.

(Analogously for the uniform version.) However, we prefer (a) over (a)’ as it can be used in the context of theories such as $\textnormal{{FS}}^{-}$ which is closed under two additional rules of reasoning: NEC and CONEC.

The proposition below follows simply by unravelling the relevant definitions:

Proposition 42**.**

If there exists a polynomially correct family of interpretations $\{I_{n}\}_{n\in\mathbb{N}}:\mathcal{T}_{2}\rightarrow\mathcal{T}_{1}$, then $\mathcal{T}_{1}$ polynomially simulates $\mathcal{T}_{2}$. Moreover, if $\{I_{n}\}_{n\in\mathbb{N}}$ is a uniformly polynomially correct family of interpretations, then $\mathcal{T}_{2}$ is feasibly reducible to $\mathcal{T}_{1}$.

Proof.

Fix a polynomially correct family of interpretations $\{I_{n}\}_{n\in\mathbb{N}}$ and let $p(n,k)$ be a polynomial witnessing this. Suppose that $\mathcal{T}_{2}\vdash^{n}\phi$ for some $\phi\in\mathcal{L}_{\mathcal{T}_{2}}\cap\mathcal{L}_{\mathcal{T}_{1}}$. Then

• •

$\phi$ is of length at most $n$,

• •

every axiom of $\mathcal{T}_{2}$ which occurs in the proof is of length at most $n$, and

Hence, by Definition 40, $\mathcal{T}_{1}\vdash^{p(n,n)}\phi^{I_{n}}$. Since $I_{n}$ is $n$-correct, we have that

[TABLE]

The moreover part is fully analogous. ∎

Remark 43**.**

By the inspection of the proof one quickly realizes that in fact the requirements for the family $\{I_{n}\}_{n\in\mathbb{N}}$ can be relaxed even further. We do not have to demand that each $I_{n}$ interprets the whole theory $\mathcal{T}_{2}$, instead we can make the weaker demand that there is a polynomial $p(n)$ such that for every $n$ we have:

[TABLE]

where $\mathcal{T}\upharpoonright_{n}$ denotes the set of axioms of $\mathcal{T}$ of length at most $n$.

3 Dramatis personæ: typed and untyped theories of truth

In this section B denotes a "base theory" for a theory of truth, i.e., a theory with a modicum of arithmetic capable of handling syntax. For example any theory extending $\textnormal{{I}}\Delta_{0}+\textnormal{{Exp}}$ will do. $T$ denotes a fresh unary predicate that is not in the language of B. $\mathcal{L}_{\textnormal{{B}}}$ denotes the language of B and $\mathcal{L}_{T}$ denotes the language of B enriched with the predicate $T$. For simplicity assume that the signature of $\mathcal{L}_{\textnormal{{B}}}$ extends the arithmetical signature with finitely many relational symbols.

In this paper, we will be dealing with theories of truth conservative over their base theories. We say that a theory $\mathcal{T}$ in the language $\mathcal{L}_{\mathcal{T}}$ is conservative over $\textnormal{{B}}\subseteq\mathcal{T}$ if for every sentence $\phi\in\mathcal{L}_{\textnormal{{B}}}$ we have:

[TABLE]

In our case, this means that adding the truth predicate and some axioms governing its behaviour does not allow us to prove new arithmetical sentences.

Below, we discuss some prominent examples of truth theories. A standard reference to the subject is Halbach’s book [10].

3.1 $\textnormal{{CT}}^{-}$

Definition 44**.**

$\textnormal{{CT}}^{-}[\textnormal{{B}}]$ is the theory extending a theory B with the following sentences:

1. $\textnormal{{CT}}1$

$\forall s,t\in\textnormal{{ClTerm}}_{\mathcal{L}_{\textnormal{{B}}}}\ \ T(s=t)\equiv{s}^{\circ}={t}^{\circ}$. 2. $\textnormal{{CT}}2$

$\forall s_{1},\ldots,s_{n}\in\textnormal{{ClTerm}}_{\mathcal{L}_{\textnormal{{B}}}}\ TR(s_{1},\ldots,s_{n})\equiv R({s_{1}}^{\circ},\ldots,{s_{n}}^{\circ})$, for every relational symbol of $\mathcal{L}_{\mathcal{T}}$. 3. $\textnormal{{CT}}3$

$\forall\phi,\psi\in\textnormal{{Sent}}_{\mathcal{L}_{\textnormal{{B}}}}\ \ T(\phi\vee\psi)\equiv T\phi\vee T\psi$. 4. $\textnormal{{CT}}4$

$\forall\phi\in\textnormal{{Sent}}_{\mathcal{L}_{\textnormal{{B}}}}\ \ T(\neg\phi)\equiv\neg T\phi$. 5. $\textnormal{{CT}}5$

$\forall\phi\in{\textnormal{{Form}}}^{\leq 1}_{\mathcal{L}_{\textnormal{{B}}}}\forall v\in\textnormal{{Var}}\ \ T(\exists v\phi)\equiv\exists xT\phi(\underline{x})$. 6. $\textnormal{{CT}}6$

\forall\phi(\bar{x})\in\textnormal{{Form}}_{\mathcal{L}_{\textnormal{{B}}}}\forall\bar{s},\bar{t}\in\textnormal{{ClTermSeq}}_{\mathcal{L}_{\textnormal{{B}}}}\ \ \bigl{(}\bar{{s}^{\circ}}=\bar{{t}^{\circ}}\rightarrow T\phi[\bar{s}/\bar{x}]\equiv T\phi[\bar{t}/\bar{x}]\bigr{)}

The last condition is sometimes called * generalized regularity*, or generalized term-extensionality. It should resemble the well known extensionality rule from deductive calculi for first-order logic, i.e.

[TABLE]

We include it since without it the quantifier axiom for $\textnormal{{CT}}^{-}$ behaves in an unnatural way.999It behaves decently already after adding the ungeneralized version of CT6 for single terms. For example, for $\textnormal{{B}}=\textnormal{{PA}}$ we have:

[TABLE]

Obviously one can simply interchange the quantifier axiom with the following one:

[TABLE]

But then, without regularity, the following implication:

[TABLE]

becomes unprovable. With the Regularity both quantifier axioms are easily seen to be equivalent.

The above version of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ was claimed to be conservative over PA in [21]. However, no proof of this fact was provided and only a hint that it requires a slight modification of the Enayat and Visser construction (see [5]). This modification, however, adds a layer of technical difficulty, so in the current version we prove feasible conservativity of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ in full detail. A detailed proof of conservativity of this theory is provided also in [12].

3.2 $\textnormal{{KF}}^{-}$ and $\textnormal{{FS}}^{-}$

The idea behind the untyped notion of truth is that the truth predicate can be meaningfully applied also to sentences containing it, to the effect that we could e.g., judge

[TABLE]

to be true. In this setting the following additional axiom seems desirable:

[TABLE]

where "TRP" abbreviates "TRansParency". Obviously if one wants to have a compositional theory of self-applicable truth, one cannot simply take (TRP) the axioms $\textnormal{{CT}}1$ through $\textnormal{{CT}}6$ and let the quantifiers range over all formulae of $\mathcal{L}_{T}$, since the resulting theory would be inconsistent by Tarski’s Theorem. The next two theories which we shall investigate exhibit two different directions in which one can look for a natural theory of untyped truth. In the first one the axiom $\textnormal{{CT}}3$ is rejected and somewhat compensated. In the second one the transparency axiom is missing.

Definition 45**.**

$\textnormal{{KF}}^{-}[\textnormal{{B}}]$ is the $\mathcal{L}_{T}$-theory extending B with the following axioms:

• $\textnormal{{KF}}1$

$\forall s,t\in\textnormal{{ClTerm}}_{\mathcal{L}_{\textnormal{{B}}}}\ \ T(s=t)\equiv{s}^{\circ}={t}^{\circ}$.

• $\textnormal{{KF}}2$

$\forall s,t\in\textnormal{{ClTerm}}_{\mathcal{L}_{\textnormal{{B}}}}\ \ T(s\neq t)\equiv{s}^{\circ}\neq{t}^{\circ}$.

• $\textnormal{{KF}}3$

$\forall s_{1},\ldots,s_{n}\in\textnormal{{ClTerm}}_{\mathcal{L}_{\textnormal{{B}}}}\ TR(s_{1},\ldots,s_{n})\equiv R({s_{1}}^{\circ},\ldots,{s_{n}}^{\circ})$, for every relational symbol of $\mathcal{L}_{\textnormal{{B}}}$.

• $\textnormal{{KF}}4$

$\forall s_{1},\ldots,s_{n}\in\textnormal{{ClTerm}}_{\mathcal{L}_{\textnormal{{B}}}}\ T\neg R(s_{1},\ldots,s_{n})\equiv\neg R({s_{1}}^{\circ},\ldots,{s_{n}}^{\circ})$, for every relational symbol of $\mathcal{L}_{\textnormal{{B}}}$.

• $\textnormal{{KF}}5$

$\forall\phi\in\textnormal{{Sent}}_{\mathcal{L}_{T}}\ \ T(\neg\neg\phi)\equiv T\phi.$

• $\textnormal{{KF}}6$

$\forall\phi,\psi\in\textnormal{{Sent}}_{\mathcal{L}_{T}}\ \ T(\phi\vee\psi)\equiv T\phi\vee T\psi.$

• $\textnormal{{KF}}7$

$\forall\phi,\psi\in\textnormal{{Sent}}_{\mathcal{L}_{T}}\ \ T(\neg(\phi\vee\psi))\equiv T\neg\phi\wedge T\neg\psi.$

• $\textnormal{{KF}}8$

$\forall y\in\textnormal{{Var}}\forall\phi\in\textnormal{{Form}}^{\leq 1}_{\mathcal{L}_{T}}\ \ T(\exists y\phi(y))\equiv\exists xT\phi(\underline{x}).$

• $\textnormal{{KF}}9$

$\forall y\in\textnormal{{Var}}\forall\phi\in\textnormal{{Form}}^{\leq 1}_{\mathcal{L}_{T}}\ \ T(\neg\exists y\phi(y))\equiv\forall xT\neg\phi(\underline{x}).$

• $\textnormal{{KF}}10$

\forall\bar{s},\bar{t}\in\textnormal{{ClTermSeq}}_{\mathcal{L}_{\textnormal{{B}}}}\forall\phi(\bar{x})\in\textnormal{{Form}}_{\mathcal{L}_{T}}\ \ \Big{(}{\bar{s}}^{\circ}={\bar{t}}^{\circ}\rightarrow T\phi(\bar{s})\equiv T\phi(\bar{t})\Big{)}.

• $\textnormal{{KF}}11$

$\forall\phi\in\textnormal{{Sent}}_{\mathcal{L}_{T}}\forall t\in\textnormal{{Term}}_{\mathcal{L}_{\textnormal{{B}}}}\ \ {t}^{\circ}=\phi\rightarrow TT(t)\equiv T\phi$.

• $\textnormal{{KF}}12$

$\forall\phi\in\textnormal{{Sent}}_{\mathcal{L}_{T}}\forall t\in\textnormal{{Term}}_{\mathcal{L}_{\textnormal{{B}}}}\ \ {t}^{\circ}=\phi\rightarrow T\neg T(t)\equiv T\neg\phi$.

KF, a theory obtained by augmenting $\textnormal{{KF}}^{-}[\textnormal{{PA}}]$ with full induction scheme for formulae with the truth predicate, was introduced by Feferman in [6] as an axiomatisation of a theory of truth proposed by Kripke in [14]. $\textnormal{{KF}}^{-}$ represents an attempt to define a reasonably behaved self-applicable truth predicate guided by the following intuition: we try to mark the sentences which are definitely true. We start with the set of true equations on arithmetical sets. Then we proceed in stages, e.g. whenever $\phi$ and $\psi$ are definitely true, we mark $\phi\wedge\psi$ as definitely true. Whenever $\phi$ is definitely true, we mark $T(\phi)$ as definitely true. Whenever $\neg\phi(\underline{x})$ is definitely true for all $x$, we mark $\neg\exists\phi(\underline{x})$ as definitely true. Thus in the process we only enlarge the set of true sentences until it reaches a fixed point. $\textnormal{{KF}}^{-}$ axiomatises properties of fixed points obtained in such a way.

The desirable feature of $\textnormal{{KF}}^{-}[\textnormal{{B}}]$ is that it satisfies the TRP axiom. However, the idempotence of the truth predicate fails rather spectacularily in a different place. It turns out that adding both derivation rules

[TABLE]

to $\textnormal{{KF}}^{-}[\textnormal{{B}}]$ at the same time yields this theory inconsistent (see [10], Lemma 15.20. The Lemma is stated for the full KF, but the induction axioms are not used in the proof). Moreover, the rule (NEC) is inconsistent with the following axiom of consistency which says that no sentence is both true and false:

[TABLE]

Dually, the rule (CONEC) is inconsistent with the axiom of completeness which states that every sentence is either true or false.

The other standard candidate for a well-behaved theory of self-referential truth is Friedman–Sheard’s theory FS.

Definition 46**.**

$\textnormal{{FS}}^{-}[\textnormal{{B}}]$ is the extension of B in the language extending $\mathcal{T}$ with the following axioms:

1. $\textnormal{{FS}}1$

\forall s,t\in\textnormal{{ClTerm}}_{\mathcal{L}_{\textnormal{{B}}}}\ \ T(s=t)\equiv\bigl{(}{s}^{\circ}={t}^{\circ}\bigr{)}. 2. $\textnormal{{FS}}2$

$\forall s_{1},\ldots,s_{n}\in\textnormal{{ClTerm}}_{\mathcal{L}_{\textnormal{{B}}}}\ TR(s_{1},\ldots,s_{n})\equiv R({s_{1}}^{\circ},\ldots,{s_{n}}^{\circ})$, for every relational symbol of $\mathcal{L}_{\textnormal{{B}}}$. 3. $\textnormal{{FS}}3$

$\forall\phi\in\textnormal{{Sent}}_{\mathcal{L}_{T}}\ \ T(\neg\phi)\equiv\neg T(\phi)$. 4. $\textnormal{{FS}}4$

$\forall\phi,\psi\in\textnormal{{Sent}}_{\mathcal{L}_{T}}\ \ T(\phi\vee\psi)\equiv T(\phi)\vee T(\psi)$. 5. $\textnormal{{FS}}5$

$\forall v\in\textnormal{{Var}}\forall\phi\in\textnormal{{Form}}^{\leq 1}_{\mathcal{L}_{T}}\ \ T(\exists v\phi)\equiv\exists xT\phi(\underline{x})$. 6. $\textnormal{{FS}}6$

\forall\bar{s},\bar{t}\in\textnormal{{ClTermSeq}}_{\mathcal{L}_{\textnormal{{B}}}}\forall\phi(\bar{x})\in\textnormal{{Form}}_{\mathcal{L}_{T}}\ \ \Big{(}{\bar{s}}^{\circ}={\bar{t}}^{\circ}\rightarrow T\phi(\bar{s})\equiv T\phi(\bar{t})\Big{)}.

which additionally is closed under the rules (NEC) and (CONEC).

Note that in none of the above theories we extend the induction scheme to the full $\mathcal{L}_{T}$. As usual we write simply $\textnormal{{FS}}^{-}$ to abbreviate $\textnormal{{FS}}^{-}[\textnormal{{PA}}]$.

A set of axioms, which is deductively equivalent to the above was first introduced in [8]. The above list of axioms is taken from [10] with a minor variation: we supplemented the normal axiomatization with $\textnormal{{FS}}6$ for reasons analogous to the ones for $\textnormal{{CT}}^{-}$.

At first sight, $\textnormal{{FS}}^{-}[\textnormal{{B}}]$ seems to be much more natural than $\textnormal{{KF}}^{-}[\textnormal{{B}}]$. The presence of NEC and CONEC rules compensates in a way the lack of the transparency axiom making the theory symmetric: for every $\phi\in\mathcal{L}_{T}$ it holds that

[TABLE]

This heavily contrasts with the case of $\textnormal{{KF}}^{-}[\textnormal{{B}}]$. However this symmetric feature turns out to be very pricey, as the well-known McGee’s theorem shows:

Theorem 47** (McGee, [16]).**

$\textnormal{{FS}}^{-}[\textnormal{{B}}]$* is $\omega$-inconsistent.*

Moreover, the fully inductive versions of both theories differ dramatically in strength, when evaluated over PA: $\textnormal{{KF}}[\textnormal{{PA}}]$ can define $\varepsilon_{0}$ levels of the ramified truth hierarchy (i.e. $\textnormal{{RT}}_{<\alpha}$ for every $\alpha<\varepsilon_{0}$. See [10] for details), while the strength of $\textnormal{{FS}}[\textnormal{{PA}}]$ is exhausted by $\omega$-many such levels. We sketch the proof of the latter fact in Subsection 3.3.3 and give a strengthening of it in Subsection 4.3.

Both $\textnormal{{KF}}^{-}[\textnormal{{B}}]$ and $\textnormal{{FS}}^{-}[\textnormal{{B}}]$ are conservative extensions of B.

Theorem 48** (Cantini, [1]).**

$\textnormal{{KF}}^{-}[\textnormal{{B}}]$* is a conservative extension of B.*

The above theorem has been proved by Cantini for PA, but his proof works essentially in the same way for all base theories B with a modicum of arithmetic. Conservativity of $\textnormal{{FS}}^{-}$ follows from the work of Halbach. He showed that FS with full induction is reducible to the system $\textnormal{{RT}}_{<\omega}$ with full induction and a stratified family of compositional truth predicates. His proof, however, does not rely on induction in the considered theories or on the specific choice of the base theory. Therefore, essentially the same argument shows that $\textnormal{{FS}}^{-}[\textnormal{{B}}]$ is reducible to $\textnormal{{RT}}^{-}_{<\omega}[\textnormal{{B}}]$ for a wide choice of base theories B. Conservativity of $\textnormal{{RT}}^{-}_{<\omega}[\textnormal{{B}}]$ can in turn be shown by using known proofs of conservativity for $\textnormal{{CT}}^{-}$, so, in a sense, it was "in the air".101010However, we know of no published proof of this result. We will provide more details (including the definition of $\textnormal{{RT}}^{-}_{<\omega}$) in Subsection 3.3.3.

Theorem 49** (Essentially due to Halbach).**

$\textnormal{{FS}}^{-}[\textnormal{{B}}]$* is a conservative extension of B.*

We shall sketch both proofs in the next Subsection 3.3.

3.3 Conservativity of truth theories

The main goal of this paper is to establish that certain truth theories over PA are feasibly reducible to PA. This involves certain elaborate technical arguments in each case. However, what these proofs have in common is that they all rely on the results from Subsection 2.5 since they follow the same general pattern: Suppose that $\mathcal{T}$ is a theory of truth over PA that is conservative over PA. Moreover, assume that the conservativity proof in fact can be formalized in PA and that it is uniform in the sense that the proof works equally well for PA and its large enough finitely axiomatized fragments B that containing $\textnormal{{I}}\Delta_{0}+\textnormal{{Exp}}$. Then $\mathcal{T}$ can be shown to be feasibly reducible to PA. Let us recall the precise formulation of this fact (it was formulated as Corollary 36):

Suppose that $\mathcal{T}$ is a finite extension of PA of the form $\textnormal{{PA}}+\phi$, $k\in\mathbb{N}$, and the following sentence is provable in PA:

"If B is any finite fragment of PA, then every $\Delta_{2}$-full model of B has an elementary extension to a $\Delta_{k}$-model of $\textnormal{{B}}+\phi$."

Then $\mathcal{T}$ is feasibly reducible to PA.

The proofs of our feasible reducibility results will in each case consist in an appropriate arithmetization in PA of a known conservativity proof of $\mathcal{T}$ over fragments of PA. Therefore, we are forced to pay close attention to the specific features of the arithmetical implementation of the conservativity proofs, which is bound to obscure the main idea of the proof of feasible reduction. Therefore, to provide some help to the reader, we present outlines of the relevant conservativity proofs in this section.

3.3.1 Conservativity of $\textnormal{{CT}}^{-}$

In this section, we sketch the proof of the following conservativity result:

Theorem 50**.**

Fix any fragment B of PA extending $\textnormal{{I}}\Delta_{0}+\textnormal{{Exp}}$. Then $\textnormal{{CT}}^{-}[\textnormal{{B}}]$ is conservative over B.

Sketch of a proof.

We will base our proof on the argument given by Enayat and Visser in [5]. Fix any model $\mathcal{M}$ of B. We will construct $(\mathcal{M}^{\prime},T)\models\textnormal{{CT}}^{-}[\textnormal{{B}}]$ where $\mathcal{M}\preceq\mathcal{M}^{\prime}$ by first constructing a chain of models

[TABLE]

such that $\mathcal{M}_{0}=\mathcal{M}$, $\mathcal{M}_{i}\preceq\mathcal{M}_{i+1}$ and the subsets $S_{i}$ are partially defined satisfaction predicates. Each $S_{i+1}$ satisfies compositional conditions for all valuations from $\mathcal{M}_{i+1}$ but only for formulae from $\mathcal{M}_{i}$. This condition is axiomatized as a scheme. For example, we require for any arithmetical formulae $\phi,\psi\in\mathcal{M}_{i}$ separately that:

[TABLE]

and for any formula $\phi$

[TABLE]

Thus we require that $S_{i+1}$ behaves compositionally for formulae which belong to $\mathcal{M}_{i}$, including nonstandard ones. Additionally, we require that $S_{i+1}$ agrees with $S_{i}$ on formulae from $\mathcal{M}_{i-1}$ and arbitrary valuations. Note that if $\phi\in M_{i}$, then a direct subformula of $\phi$ also belongs to $M_{i}$. In other words: the predicate gets fixed on the formulae on which it is guaranteed to behave compositionally.

We write the compositional conditions for $S_{n+1}$ in a pointwise manner (formula by formula), so in order to check that such an extension exists, by compactness, we only have to check that for each finite subset of formulae from $\mathcal{M}_{i}$, we can find a predicate $S_{i+1}$ which satisfies compositional conditions for these formulae. This turns out to be possible with a fairly straightforward recursion.

Finally, we take the sum of models $(\mathcal{M}_{i},S_{i})$. In order to check that the resulting sum satisfies compositional axioms (for formulae and assignments), we take an arbitrary formula $\phi$, its direct subformulae, and some fixed valuation $\alpha$ for $\phi$. We check that it satisfied compositional conditions in the model $(\mathcal{M}_{i+1},S_{i+1})$, such that $\phi$ and was present already in $\mathcal{M}_{i}$, and that the compositional conditions were preserved along the construction.

Finally, we turn the model $(\mathcal{M}^{\prime},S)$ with a satisfaction class (i.e., a set of pairs $(\phi,\alpha)$ such that $\phi$ is an arithmetical formula and $\alpha\in\textnormal{{Asn}}(\phi)$) obtained as a sum of a chain into a model with a truth class. We define $T\subsetneq M^{\prime}$ as follows

[TABLE]

This concludes the sketch of the proof. A detailed argument will be presented in Subsection 4.1. ∎

The proof as written above does not overtly formalise in PA. The problem is as follows: when we speak in PA of full models $(\mathcal{M}_{i},S_{i})$, we really speak of formulae defining elementary diagrams of $(\mathcal{M}_{i},S_{i})$. The defining formulae for the full models can in general be more and more complex as we iterate the construction, and there might be no formally correct way of defining the sum of the obtained chain of models. Actually, we cannot even define the whole chain, but only its standard initial fragments.

There are a couple of ways to circumvent this issue. The route undertaken in this paper is the simplest we know of: we do not speak directly of models, but rather, through appropriate first order theories. More specifically, we will show that for any natural number $x$, the theory $\mathcal{T}_{x}$ (formulated in an extension of the language of B with finitely many new predicate symbols), saying:

"There exists a chain $(\mathcal{M}_{0},S_{0})\subseteq(\mathcal{M}_{1},S_{1})\subseteq\ldots\subseteq(\mathcal{M}_{x},S_{x})$ of models satisfying the conditions from the Enayat–Visser construction."

is consistent. This will be done by formalising the inductive step in the construction by Enayat and Visser, i.e., by showing that for all numbers $x$, if $\mathcal{T}_{x}$ is consistent, then $\mathcal{T}_{x+1}$ is consistent as well. The consistency of $\mathcal{T}_{x}$ is a $\Pi_{1}$-statement, so PA will be able to verify that for any $x$ the theory $\mathcal{T}_{x}$ is consistent. This in turn will be enough to show that the theory saying:

"There is a chain of models: $(\mathcal{M}_{0},S_{0})\subseteq(\mathcal{M}_{1},S_{1})\subseteq\ldots$ of infnite length which satisfy conditions from Enayat–Visser construction."

is consistent, hence has a model. From this model we will be able to define the whole chain in a uniform way and, consequently, its sum, which will give us a model of $\textnormal{{CT}}^{-}[\textnormal{{B}}]$ (not a full model though). The details involve a number of intricate and technical considerations; they are presented in the next section.

3.3.2 Conservativity of $\textnormal{{KF}}^{-}$

In this subsection we will outline the proof of conservativity of $\textnormal{{KF}}^{-}[\textnormal{{B}}]$, where B is a fragment of PA extending $\textnormal{{I}}\Delta_{0}+\textnormal{{Exp}}$. The standard proof of conservativity is motivated by the original construction of Kripke.111111What we present here more resembles a modified constructions which seems to be first formulated by Cantini in [1]. We can define truth predicate semantically as a fixed point of an operator that takes a subset $T_{\alpha}$ of $\mathbb{N}$, thought of as the set of sentences (possibly containing the truth predicate) which can be already identified as true at a given stage of the construction, and replaces it with $T_{\alpha+1}\supseteq T_{\alpha}$ in the following way:

• •

If $\phi$ is a true atomic or negated atomic formula, then $\phi\in T_{\alpha+1}$.

• •

If $\phi\in T_{\alpha}$, then $\phi\in T_{\alpha+1}$.

• •

If $\phi\in T_{\alpha}$, and $\phi={t}^{\circ}$ for a term $t$, then $T(t)\in T_{\alpha+1}$.

• •

If $\neg\phi\in T_{\alpha}$, and $(\neg\phi)={t}^{\circ}$, then $\neg T(t)\in T_{\alpha+1}$.

• •

If $\phi\in T_{\alpha}$, then $\neg\neg\phi\in T_{\alpha+1}$.

• •

If $\phi\in T_{\alpha}$ or $\psi\in T_{\alpha}$, then $\phi\vee\psi\in T_{\alpha+1}$.

• •

If $\neg\phi\in T_{\alpha}$ and $\neg\psi\in T_{\alpha}$, then $\neg(\phi\vee\psi)\in T_{\alpha+1}$.

• •

If $\phi(\underline{x})\in T_{\alpha}$, then $\exists v\phi(v)\in T_{\alpha+1}$.

• •

If $\neg\phi(\underline{x})\in T_{\alpha}$ for all $x$, then $\neg\exists v\phi(v)\in T_{\alpha+1}$.

If $\lambda$ is a limit ordinal, we set $T_{\lambda}=\bigcup_{\alpha<\lambda}T_{\alpha}$. In the above construction, we enlarge the set $T_{\alpha}$ of sentences which are definitely true with a set of sentences which are definitely true if we interpret the truth predicate as the set $T_{\alpha}$. Since at each stage, we only keep enlarging our set, the construction will reach its fixed point. Such fixed points can be easily shown to satisfy the axioms of $\textnormal{{KF}}^{-}[\textnormal{{B}}]$. The outlined argument carries over to an arbitrary model $\mathcal{M}$ of B thus establishing conservativity of $\textnormal{{KF}}^{-}[\textnormal{{B}}]$ over its base theory.

The main problem with the outlined argument is that it does not directly formalize in PA since it relies on the principle: "Every positive operator on subsets of $\mathbb{N}$ reaches a fixpoint." which is clearly not available in PA. However, there is a rather simple fix to this problem.

Start with a *recursively saturated *model $\mathcal{M}\models\textnormal{{B}}$. Notice that for $n\in\omega$, the $n$-th set obtained in the inductive procedure described above, $T_{n}$, is arithmetically definable in $\mathcal{M}$ (let us call the defining formula $\Theta_{n}$). By definability of $T_{n}$ and recursive saturation of $\mathcal{M}$, we can deduce that already $T_{\omega}$ is a truth predicate satisfying axioms of $\textnormal{{KF}}^{-}[\textnormal{{B}}]$. Essentially, this relies on the fact that in recursively saturated models $\phi(\underline{x})\in T_{\omega}$ holds for all $x\in M$ if and only if $\phi(\underline{x})\in T_{k}$ holds for some $k\in\omega$ and all $x\in M$.121212A very similar argument has been presented in [3] in the proof that any recursively saturated model of PA can be expanded to a model of $\textnormal{{PT}}^{-}$ with internal induction for total formulae. It seems that this reasoning appears originally in [1], where Cantini proved conservativity of $\textnormal{{KF}}^{-}$ with internal induction for total formulae over PA.

It turns out that this argument can be repeated in PA for a finitely axiomatized fragment B of PA extending $\textnormal{{I}}\Delta_{0}+\textnormal{{Exp}}$. Namely, we first take a full model $\mathcal{M}$ of B, then we take its recursively saturated elementary extension, a full model $\mathcal{M}^{\prime}$ and we define the predicate $T$ in $\mathcal{M}^{\prime}$ as the sum of all sets defined with certain formulae $\Theta_{c}$ defining the analogues of the sets $T_{c}$ from the above construction. The details will be given in Subsection 4.2

3.3.3 Conservativity of $\textnormal{{FS}}^{-}$

The proof of conservativity of $\textnormal{{FS}}^{-}$ over PA is analogous to the one showing the upper bounds on the proof-theoretical strength of its fully inductive version, $\textnormal{{FS}}[\textnormal{{PA}}]$. As an intermediate step we pass through a theory of iterated compositional truth predicate of length $\omega$, $\textnormal{{RT}}_{<\omega}^{-}$.

Definition 51**.**

$\textnormal{{RT}}_{<n+1}^{-}[\textnormal{{B}}]$ is the extension of B in the language $\mathcal{L}_{<n+1}$ extending $\mathcal{L}_{\textnormal{{PA}}}$ with $n+1$ new predicate symbols $\{T_{0},\ldots,T_{n}\}$ (we stipulate that $\mathcal{L}_{<0}=\mathcal{L}_{\textnormal{{PA}}}$ and $\textnormal{{RT}}^{-}_{<0}=\textnormal{{PA}}$) satisfying the following axioms for all $k<n+1$:

1. $\textnormal{{RT}}1$

$\forall s,t\in\textnormal{{ClTerm}}_{\mathcal{L}_{\textnormal{{PA}}}}\ \ T_{k}(s=t)\equiv{s}^{\circ}={t}^{\circ}$. 2. $\textnormal{{RT}}2$

$\forall\phi\in\textnormal{{Sent}}_{\mathcal{L}_{<k}}\ \ T_{k}(\neg\phi)\equiv\neg T_{k}(\phi)$. 3. $\textnormal{{RT}}3$

$\forall\phi,\psi\in\textnormal{{Sent}}_{\mathcal{L}_{<k}}\ \ T_{k}(\phi\vee\psi)\equiv T_{k}(\phi)\vee T_{k}(\psi)$. 4. $\textnormal{{RT}}4$

$\forall\phi(x)\in\textnormal{{Form}}^{\leq 1}_{\mathcal{L}_{<k}}\forall v\in\textnormal{{Var}}\ \ T_{k}(\exists v\phi)\equiv\exists x\ \ T_{k}(\phi(\underline{x}))$. 5. $\textnormal{{RT}}5$

\forall\bar{s},\bar{t}\in\textnormal{{ClTermSeq}}_{\mathcal{L}_{\textnormal{{PA}}}}\forall\phi(x)\in\textnormal{{Form}}^{\leq 1}_{\mathcal{L}_{<k}}\ \ \bigl{(}{\bar{s}}^{\circ}={\bar{t}}^{\circ}\rightarrow T_{k}(\phi(\bar{s}))\equiv T_{k}(\phi(\bar{t}))\bigr{)}. 6. $\textnormal{{RT}}6$

\bigwedge_{i<k}\forall s\in\textnormal{{ClTerm}}_{\mathcal{L}_{\textnormal{{PA}}}}\ \bigl{(}{s}^{\circ}\in\textnormal{{Sent}}_{\mathcal{L}_{<i}}\rightarrow T_{k}(T_{i}(s))\equiv T_{i}({s}^{\circ})\bigr{)}. 7. $\textnormal{{RT}}7$

\forall i<k\forall s\in\textnormal{{ClTerm}}_{\mathcal{L}_{\textnormal{{PA}}}}\ \ \bigl{(}{s}^{\circ}\in\textnormal{{Sent}}_{\mathcal{L}_{<i}}\rightarrow T_{k}(T_{i}(s))\equiv T_{k}({s}^{\circ})\bigr{)}

Define $\textnormal{{RT}}_{<\omega}^{-}[\textnormal{{PA}}]:=\bigcup_{n\in\omega}\textnormal{{RT}}_{<n}^{-}[\textnormal{{PA}}]$

Remark 52**.**

We assume that the initially chosen coding is extended in such a way that the length of $T_{n}$ is logarithmic in $n$ (in fact, polynomial will do, so this logarythmic bound is not that important).

As in the case of $\textnormal{{FS}}^{-}$, $\textnormal{{RT}}^{-}_{<n}$ and $\textnormal{{RT}}^{-}_{<\omega}$ abbreviate $\textnormal{{RT}}^{-}_{<n}[\textnormal{{PA}}]$ and $\textnormal{{RT}}^{-}_{<\omega}[\textnormal{{PA}}]$ respectively. Note that similarly to all the rest of theories studied in this paper, in $\textnormal{{RT}}_{<\omega}^{-}$ we do not extend the scheme of induction to formulae with the truth predicate.

Now let B be our base theory. We shall now reduce the problem of conservativity of $\textnormal{{FS}}^{-}[\textnormal{{B}}]$ over B to the analogous problem for $\textnormal{{RT}}^{-}_{<\omega}$. Let us recall that an interpretation ∗ is an $\omega$-interpretation, if for every arithmetical sentence $\phi$ we have

[TABLE]

In order to perform the above mentioned reduction it suffices to show that every "finite piece" of $\textnormal{{FS}}^{-}$ can be $\omega$-interpreted in $\textnormal{{RT}}^{-}_{<\omega}$. In this context "an $n$-piece" means "a sentence which can be deduced from B and axioms $\textnormal{{FS}}1$–$\textnormal{{FS}}6$ (note that in this context $\textnormal{{FS}}2$ is missing) using at most $n$ applications of NEC and CONEC rules." We shall denote it with $\textnormal{{FS}}^{-}_{n}[\textnormal{{B}}]$. Thus $\phi$ is in $\textnormal{{FS}}^{-}_{1}[\textnormal{{B}}]$ if it can be deduced using one application of the NEC rule or one application of the CONEC rule. (But not both. Our definition differs from the original one given by Halbach.) Now the following holds:

Lemma 53** (Essentially Halbach, [10], Theorem 14.31).**

For each $n$, $\textnormal{{FS}}^{-}_{n}[\textnormal{{B}}]$ is $\omega$-interpretable in $\textnormal{{RT}}_{<2n+1}^{-}[\textnormal{{B}}]$.

Proof.

Define a family $\{g_{n}\}_{n\in\mathbb{N}}$ of primitive recursive functions as follows

[TABLE]

Where $T_{n}(g_{n}(t))$ abbreviates

[TABLE]

and $g_{n}(x)=y$ is a natural $\Delta_{0}$-formula which represents $g_{n}$ in $\textnormal{{I}}\Delta_{0}+\textnormal{{Exp}}$. We shall check that for every $n$, $g_{n+1}$ is an $\omega$-interpretation of $\textnormal{{FS}}^{-}_{n}[\textnormal{{B}}]$ in $\textnormal{{RT}}^{-}_{<2n+1}[\textnormal{{B}}]$. It is evident that each $g_{n}$ acts as identity on arithmetical sentences. Moreover, for every $\phi\in\mathcal{L}_{T}$ and each $n$, $g_{n}(\phi)$ is a sentence of $\mathcal{L}_{<n}$ (that is, it contains truth predicates with indices at most $n-1$) and this fact is provable in B. Hence if $\phi$ is any axiom from $\textnormal{{FS}}1$ through $\textnormal{{FS}}6$ and $0<k\leq n$, then

[TABLE]

Now, following the lines of Halbach’s argument, we fix $n$ and, by induction on $i$ up to $n$, we show that for every $i\leq n$ and every $j\in\{i+1,\ldots,2n+1-i\}$131313That this range of $j$ shrinks in the induction process is needed to deal with CONEC. we have:

[TABLE]

Note that ($*$ ‣ 3.3.3) witnesses that the above holds for $i=0$. Now inductively assume that the above holds for an $0<i<n$ and fix $j\in\{i+2,\ldots,2n+1-(i+1)\}$.

Fix a proof $\pi$ of $\psi$ in $\textnormal{{FS}}^{-}_{i+1}[\textnormal{{B}}]$. Arguing by induction assume that the last rule used in $\pi$ is either NEC or CONEC. In both cases we will use the fact that for all $k\leq l<m$, and every $\phi\in\mathcal{L}_{<k}$, $\textnormal{{RT}}^{-}_{<m}[\textnormal{{B}}]$ proves

[TABLE]

If $\psi$ is obtained by NEC, then $\psi=T(\theta)$ and by our induction assumption we know that $\textnormal{{RT}}^{-}_{<2n+1}[\textnormal{{B}}]\vdash g_{j-1}(\theta)$. Since $g_{j-1}(\theta)\in\textnormal{{Sent}}_{<j-1}$, by ($**$ ‣ 3.3.3) we obtain $\textnormal{{RT}}^{-}_{<2n+1}[\textnormal{{B}}]\vdash T_{j-1}(g_{j-1}(\theta))$. The last sentence is by definition equal to $g_{j}(T(\theta))$, hence this case is done.

If $\psi$ is obtained by CONEC, then we argue dually using $g_{j+1}$ applied to $T(\psi)$. ∎

In the rest of this section we sketch the proof of conservativity of $\textnormal{{RT}}^{-}_{<\omega}[\textnormal{{B}}]$ over B based on Enayat-Visser construction. For starters, let us note that it suffices to construct, for an arbitrary model $\mathcal{M}\models\textnormal{{B}}$ a chain of models $(\mathcal{M}_{i})_{i\in\omega}$ such that

$\mathcal{M}_{0}=\mathcal{M}$; 2. 2.

$\mathcal{M}_{i}\models\textnormal{{RT}}^{-}_{<i}$; 3. 3.

$\mathcal{M}_{i}\preceq_{\mathcal{L}_{<i}}\mathcal{M}_{i+1}$.

Then $\bigcup_{i\in\mathbb{N}}\mathcal{M}_{i}$ will be an elementary extension of $\mathcal{M}$ satisfying $\textnormal{{RT}}^{-}_{<\omega}[\textnormal{{B}}]$. To get $\mathcal{M}_{i+1}$ we basically start the Enayat-Visser construction (as sketched in Subsection 3.3.1) on $\mathcal{M}_{i}$ for the base language $\mathcal{L}_{<i}$. More precisely, we build an $\omega$-chain of models $(\mathcal{M}_{i}^{j},S_{j})_{j\in\mathbb{N}}$ such that

$\mathcal{M}^{0}_{i}=\mathcal{M}_{i}$ and $S_{0}=\varnothing$; 2. 2.

$\mathcal{M}^{j}_{i}\preceq_{\mathcal{L}_{<i}}\mathcal{M}^{j+1}_{i}$; 3. 3.

$S_{j}\subseteq S_{j+1}$ 4. 4.

$S_{j+1}$ is a satisfaction class for $\textnormal{{Form}}_{\mathcal{L}_{<i}}(\mathcal{M}^{j}_{i})$ with respect to all valuations from $\mathcal{M}^{j+1}_{i}$

Satisfying the above requirements would suffice to guarantee that in the limit model axioms $\textnormal{{RT}}1$ through $\textnormal{{RT}}6$ will hold. However, to account for $\textnormal{{RT}}7$ we have to improve our satisfaction classes $S_{j}$ slightly. This can be done by requiring that $S_{j+1}$ makes true all the statements $\phi$ such that

[TABLE]

for $l\leq i$ and $\phi\in\textnormal{{Sent}}_{\mathcal{L}_{<l}}^{\mathcal{M}^{j}_{i}}$ (i.e., $\langle\phi,\alpha\rangle\in S_{j+1}$ for such any $\phi$ and for every assignment $\alpha\in\mathcal{M}^{j+1}_{i}$). This, in turn, requires only a tiny modification of the original Enayat–Visser proof. Details will be presented in Section 4.3.

4 The main act: feasible reductions of truth theories

This section contains the principal results of this paper. The first three subsections are devoted, respectively, to feasible reductions of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$, $\textnormal{{KF}}^{-}[\textnormal{{PA}}]$, and $\textnormal{{FS}}^{-}[\textnormal{{PA}}]$ to PA. The last section, on the other hand, presents an interpretability-theoretic perspective of our work.

4.1 Feasible reduction of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ to PA

This section is devoted to the proof of the following result:

Theorem 54**.**

$\textnormal{{CT}}^{-}[\textnormal{{PA}}]$* is feasibly reducible to PA.*

An immediate corollary of Theorem 54 is that $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ does not have super-polynomial speed-up over PA. The proof of a special case of this corollary for $\Pi_{1}$-sentences of arithmetic was presented by Fischer [7], based on an outline suggested by Visser, but as pointed out in a footnote in Subsection 2.6 the presented proof lacks an important detail.

Our proof of Theorem 54 will be based on the verification of the veracity of the assumption of Corollary 36 for $k=4$ and $\mathcal{T}=\textnormal{{CT}}^{-}[\textnormal{{PA}}]$. In fact, we shall do slightly better: let us say that a theory B is good if it is formulated in a language $\mathcal{L}_{\textnormal{{B}}}$ that extends $\mathcal{L}_{\textnormal{{PA}}}$ with new finitely many relation symbols (so all terms are arithmetical) and B extends $\textnormal{{I}}\Sigma_{1}$. We shall show that for every $l\in\mathbb{N}$ the following single sentence is provable in PA:

"If B is any $\Delta_{1}$-good theory, then every $\Delta_{l}$-full model of B has an elementary extension to a $\Delta_{l+2}$-model of $\textnormal{{CT}}^{-}[\textnormal{{B}}]$."

In the above, $l$ is to be thought as independent of the size of the proof that our reduction takes as an argument. In the case of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ we will need the above theorem only for $l=2$. The more uniform version will be needed to handle the $\textnormal{{FS}}^{-}[\textnormal{{PA}}]$ case.

Our proof consists in formalizing the $\omega$-chain Enayat–Visser construction inside PA, according to the sketch given in Subsection 3.3. As in the conservativity proof of Enayat and Visser, we shall make a detour through partial satisfaction classes. Let us introduce one more definition that will play an intermediate role in the proof below.

Convention 55**.**

If $P$ is an arbitrary unary predicate and $\phi(x)$ an arbitrary formula with one free variable, then we write $\phi\upharpoonright_{P}$ for the formula $\phi(x)\wedge P(x)$.

Definition 56** ($\textnormal{{CS}}^{-}\upharpoonright_{P}$).**

Let B be a theory in a finite language $\mathcal{L}_{\textnormal{{B}}}$ extending $\textnormal{{I}}\Sigma_{1}$ and $P$ be a fresh unary predicate. $\textnormal{{CS}}^{-}\upharpoonright_{P}[\textnormal{{B}}]$ is the theory of $P$-restricted, extensional satisfaction class for $\mathcal{L}_{\textnormal{{B}}}$ formulated in the language $\mathcal{L}_{S}=\mathcal{L}_{\textnormal{{B}}}\cup\{S\}\cup\{P\}$ and extending B with the following axioms:

\forall x,y\bigl{(}S(x,y)\rightarrow x\in\textnormal{{Form}}_{\mathcal{L}_{\textnormal{{B}}}}\upharpoonright_{P}\wedge y\in\textnormal{{Asn}}(x)\bigr{)}. 2. 2.

\forall s_{0}\ldots\forall s_{n}\in\textnormal{{Term}}_{\mathcal{L}_{\textnormal{{B}}}}\upharpoonright_{P}\forall\alpha\in\textnormal{{Asn}}(s_{0},\ldots,s_{n})\bigl{(}S(R(s_{0},\ldots,s_{n}),\alpha)\equiv R(s_{0}^{\alpha},\ldots,s_{n}^{\alpha})\bigr{)}. 3. 3.

\forall\phi,\psi\in\textnormal{{Form}}_{\mathcal{L}_{\textnormal{{B}}}}\upharpoonright_{P}\forall\alpha\in\textnormal{{Asn}}(\phi,\psi)\ \ \bigl{(}S(\phi\vee\psi,\alpha)\equiv S(\phi,\alpha)\vee S(\psi,\alpha)\bigr{)}. 4. 4.

\forall\phi\in\textnormal{{Form}}_{\mathcal{L}_{\textnormal{{B}}}}\upharpoonright_{P}\forall\alpha\in\textnormal{{Asn}}(\phi)\ \ \bigl{(}S(\neg\phi,\alpha)\equiv\neg S(\phi,\alpha)\bigr{)}. 5. 5.

\forall\phi\in\textnormal{{Form}}_{\mathcal{L}_{\textnormal{{B}}}}\upharpoonright_{P}\forall v\in\textnormal{{Var}}\upharpoonright_{P}\forall\alpha\in\textnormal{{Asn}}(\exists v\phi)\ \ \bigl{(}S(\exists v\phi,\alpha)\equiv\exists\ \ \beta\sim_{v}\alpha,\beta\in\textnormal{{Asn}}(\phi)\ \ S(\phi,\beta)\bigr{)}.

and the axiom of generalized regularity:

[TABLE]

If $\mathcal{M}\models\textnormal{{B}}$ and $P\subseteq M$, $S\subseteq M^{2}$ is such that $(\mathcal{M},S,P)\models\textnormal{{CS}}^{-}\upharpoonright_{P}[\textnormal{{B}}]$, then $S$ is called a $P$-restricted extensional satisfaction class for $\mathcal{L}_{\textnormal{{B}}}$ on $\mathcal{M}$. If $S$ is "$x=x$"-restricted, it is called full. Note that the above notion makes sense even if $(\mathcal{M},S,P)$ is not a full model since $\textnormal{{CS}}^{-}\upharpoonright_{P}[\textnormal{{B}}]$ is a finite extension of B (recall Definition 29).

Note that in the definition above we do not restrict the range of assignments (denoted by variable $\alpha$ in the above definition). In effect, we do not assume that the assignments come from the restricted set. This is crucial to our purposes.

Convention 57**.**

Below we always assume that $P$ is either empty or defines in $\mathcal{M}$ a universe of an elementary submodel of $\mathcal{M}$. This certainly can be sustained along the inductive condition from the proof below. Under this assumption, $P$ is closed under the direct subformula relation, which we denote with $\triangleleft$. More precisely

[TABLE]

The distinctive feature of Enayat-Visser technique of building truth classes is that one creates a well-behaved satisfaction class via a union of chain argument. Let us now state the proposition which will provide us with a proof of the induction step in this construction.

Lemma 58** (Arithmetized Enayat-Visser construction).**

Let $\mathcal{L}_{\textnormal{{B}}}$ be a finite language extending $\mathcal{L}_{\textnormal{{PA}}}$. The sentence expressing the following implication is provable in PA for every $l\in\mathbb{N}$:

If $(\mathcal{M},S,P)$ is a $\Delta_{l}$-full model for $\mathcal{L}_{\textnormal{{B}}}$ such that:

$\mathcal{M}\models\textnormal{{I}}\Sigma_{1}$; 2. 2.

$S$* is a $P$-restricted satisfaction class for $\mathcal{L}_{\textnormal{{B}}}$;*

then there exists a $\Delta_{l+1}$-full model $\mathcal{N}$ for $\mathcal{L}_{\textnormal{{B}}}$ and an $\Delta_{l+1}$-set $S^{\prime}\subseteq N^{2}$ such that:

$\mathcal{M}\preceq\mathcal{N}$; 2. 2.

$S^{\prime}$* is an $M$-restricted satisfaction class for $\mathcal{L}_{\textnormal{{B}}}$ (we add a predicate for the universe of $\mathcal{M}$ to the language);* 3. 3.

$S\subseteq S^{\prime}$.

Remark 59**.**

We call the reader’s attention to the asymetry in the above lemma: we start with a full model $(\mathcal{M},S,P)$ but finish with a full model $\mathcal{N}$ and two its subsets $S^{\prime}$, $M$. This will be compensated for in our inductive construction.

Proof.

We work in PA. Let $(\mathcal{M},S,P)$ be as in the antecedent of the implication. We follow the lines of the standard Enayat-Visser proof from [5], but we perform it inside PA. Moreover we have the additional technical complication caused by adding the regularity axiom to $\textnormal{{CT}}^{-}[\textnormal{{B}}]$. Let us define the language $\mathcal{L}_{\textnormal{{EV}}}$:

[TABLE]

Now let us define the Enayat-Visser theory for $(\mathcal{M},P,S)$ as the sum of the following sets:

[TABLE]

We argue that this theory is consistent. Then, by ACT (Theorem 9) there will be a $\Delta_{l+1}$-model $\mathcal{N}$ of this theory. Then putting:

[TABLE]

we easily check that the triple $(\mathcal{N},S^{\prime},M)$ satisfies the claim.

To prove the consistency, we will argue by the compactness theorem. Let $F$ be a finite (in the sense of PA) fragment of this theory. For each predicate $U_{\phi}$ which occurs in $F$ we will find a formula $\theta_{\phi}(x)\in\mathcal{L}_{\textnormal{{B}}}$ such that

[TABLE]

where $F[\theta_{\phi}/U_{\phi}]_{U_{\phi}\in F}$ denotes the theory resulting from $F$ by replacing each occurrence $U_{\phi}$ with the corresponding formula $\theta_{\phi}$. Note that the above makes perfect sense, since $(\mathcal{M},S,P)$ is a full model. This clearly guarantees that $F$ is consistent. Moreover from now on we do not need to bother with the sentences from $\textsf{ElDiag}(\mathcal{M})$, since they obviously hold in $\mathcal{M}$.

As in the original Enayat-Visser proof we construe $\theta_{\phi}$’s by induction on the appropriately defined rank. Note that we have more work to do here than in the proofs given by Enayat and Visser [5] (since in their set-up, the language of arithmetic is purely relational), and by Cieśliński [2] (since in his set-up $\textnormal{{CT}}^{-}$ does not include our generalized regularity axiom $\textnormal{{CT}}6$). Let $c$ be the set of formulae $\phi$ such that the predicate $U_{\phi}$ occurs in a formula in $F$. Let $b$ be an arbitrary coded set of formulae of $\mathcal{L}_{\textnormal{{B}}}$. We put $\textsf{ rank}^{b}(\phi)\geq x$ iff there exists a sequence $y$ such that the following three conditions hold (in the last condition $\triangleleft$ denotes the relation of being an immediate subformula):

$\textnormal{{len}}(y)=x+1$ and $(y)_{x}=\{\phi\}$. 2. 2.

For all $i<x+1$ $(y)_{i}\subseteq b$. 3. 3.

For all $i<x$ for all $\theta$, $\theta\in(y)_{i+1}$ iff for all $\psi$ such that $\mathcal{M}\models\psi\triangleleft\theta$, $\psi\in(y)_{i}$.

We say that $\textsf{ rank}^{b}(\phi)=x$ if $x$ is the greatest $x$ such that $\textsf{ rank}^{b}(\phi)\geq x$. This definition makes sense, since if $\textsf{ rank}^{b}(\phi)\geq x$, then $x\leq|b|$ where $|c|$ denotes the cardinality of $c$.

Example 60**.**

If $b=\{0=0,0=0\vee 1=1\}$, then the $\textsf{ rank}^{b}(0=0\vee 1=1)=0$, since $1=1\notin b$.

The intuition behind the above definition is that $\textsf{ rank}^{c}(\phi)$ is the complexity of $\phi$ where formulae whose some immediate subformula does not belong to $c$ are treated as atoms. The idea is that for any such formula the satisfaction set $U_{\phi}$ can be defined almost arbitrarily and then $U_{\psi}$’s for formulae of higher rank can be defined in terms of previously defined satisfaction sets.

Observe that if we follow the above described recursive procedure, then all the compositional axioms (i.e., counterparts of axioms for atomic formulae, disjunction, negation and quantifier) from $F$ will be satisfied. However, we have one immediate problem: it can happen that (an instance of) the axiom of regularity for $\phi$ and $\psi$ is in $F$, but $\phi$ and $\psi$ get different ranks. In such a situation the standard procedure does not seem to guarantee that $\theta_{\phi}$ and $\theta_{\psi}$ (i.e. formulae which interpret $U_{\phi}$ and $U_{\psi}$ in $(\mathcal{M},S,P)$) will satisfy the regularity axiom. To simplify the notation let us define $\phi\approx_{F}\psi$ if the following is in $F$:

[TABLE]

Note that it can happen only if the following holds in $\mathcal{M}$ (this follows by definition of the Enayat–Visser theory):

[TABLE]

A solution to our puzzle is to complete $c$, obtaining $\widehat{c}$, to assure that we have for all $\phi$, $\psi$

[TABLE]

It is convenient to extend $\approx_{F}$ a little bit to make it an equivalence relation. We say that $\xi$ is the term trivialization of $\phi$, and write $\xi=\widehat{\phi}$ if the following four conditions hold:

For every occurrence $t$ of a term in $\xi$, if all occurrences of variables in $t$ are free, then $t$ is a free occurrence of a variable. 2. 2.

No variable occurs in $\xi$ as both bounded and free, and no variable occurs as free more than once. 3. 3.

For some $\rho$, a function with domain $\textnormal{{FV}}(\theta)$ and values in $\textnormal{{Term}}_{\mathcal{L}_{\textnormal{{B}}}}$, the equality $\xi[\rho]=\phi$ holds. (Recall that $\xi[\rho]$ denotes the result of a formal substitution of terms for free variables of $\xi$ and that $\textnormal{{Term}}_{\mathcal{L}_{\textnormal{{B}}}}$ contains also terms with free variables.) 4. 4.

The indices of free variables of $\xi$ are chosen in a canonical way (for example according to the tree-ordering of the syntactical tree of $\xi$. This is only needed to guarantee uniqueness).

The idea behind $\widehat{\phi}$ is that if for some term substitution $\rho$ and some formula $\psi$ we have

[TABLE]

then, $\widehat{\phi}=\widehat{\psi}$ and there are unique term substitutions $\gamma_{1}$, $\gamma_{2}$ such that:

[TABLE]

We write $\phi\approx^{\mathcal{M}}\psi$ if $\mathcal{M}\models\widehat{\phi}=\widehat{\psi}$.141414The idea of using such term trivializations was directly inspired by Graham Leigh’s [15]. Obviously $\approx^{\mathcal{M}}$ is an equivalence relation. Moreover, $\approx^{\mathcal{M}}$ is a congruence with respect to the direct subformula relation $\triangleleft$, i.e. the following lemma holds. For its proof consult the appendix.

Lemma 61** (Congruence lemma).**

For all $\phi$, $\phi^{\prime}$, $\psi^{\prime}$ it holds that

[TABLE]

By induction it follows that the congruence lemma holds for $\triangleleft_{a}$ in place of $\triangleleft$, where $\triangleleft_{a}$ denotes the $a$-step transitive closure of $\triangleleft$ (by stipulation $\triangleleft_{0}$ is the relation of equality).

Finally, observe that for every $\phi$, $U_{\widehat{\phi}}$ and $U_{\phi}$ are mutually interdefinable. Indeed, fix $\phi$ and $\gamma:\textnormal{{FV}}(\widehat{\phi})\rightarrow\textnormal{{Term}}_{\mathcal{L}_{\textnormal{{B}}}}$ such that $\widehat{\phi}[\gamma]=\phi$. Then, having $U_{\widehat{\phi}}$, we define $U_{\phi}$ with the condition:

[TABLE]

Similarly, having $U_{\phi}$ we define $U_{\widehat{\phi}}$ with the condition:

[TABLE]

Now, define $\widehat{c}$ to be the completion of $c$ if for all $\psi$, $\psi\in\widehat{c}$ if and only if there exists $i,j\leq m$ and $\psi^{\prime},\phi,\phi^{\prime}\in c$ such that the following pair of conditions hold:

$\mathcal{M}\models\psi\triangleleft_{i}\psi^{\prime}\wedge\phi\triangleleft_{j}\phi^{\prime}$ 2. 2.

$\phi\approx^{\mathcal{M}}\psi$.

[TABLE]

Let us observe that with the current definition of $\widehat{c}$ it holds that for all $\phi,\psi\in c$

[TABLE]

Indeed, suppose this is not the case. Then, assumming without loss of generality that

[TABLE]

there exists $\phi^{\prime}\in\widehat{c}$ such that $\phi^{\prime}\triangleleft_{i+1}\phi$ but no formula from $\widehat{c}$ is the $i+1$-st direct subformula of $\psi$. By the congruence lemma (and induction) there exists $\psi^{\prime}$ such that $\psi^{\prime}\triangleleft_{i+1}\psi$ and $\psi^{\prime}\approx^{\mathcal{M}}\phi^{\prime}$. Since $\phi^{\prime}\in\widehat{c}$, then there are $\theta,\theta^{\prime},\phi^{\prime\prime}\in c$ such that for some $j,k\leq m$ $\theta\triangleleft_{j}\theta^{\prime}$ and $\phi^{\prime}\triangleleft_{k}\phi^{\prime\prime}$ and $\phi^{\prime}\approx^{\mathcal{M}}\theta$ (possibly $\phi^{\prime\prime}=\phi=\theta^{\prime}$ and $\theta=\phi^{\prime}$—when $\phi^{\prime}\in c$). Since $\approx^{\mathcal{M}}$ is an equivalence relation, then $\psi^{\prime}\approx^{\mathcal{M}}\theta$. Now, by the definition of $\widehat{c}$ we obtain that $\psi^{\prime}\in\widehat{c}$, a contradiction.

For every $x$, let $F\upharpoonright_{x}$ denote the fragment of $F$ consisting of axioms for $U_{\phi}$ predicates for $\phi$ of $\textsf{ rank}^{\widehat{c}}$ at most $x$ and recall that if $\{\theta_{\phi}\}$ is a family of formulae with one free variable indexed with $\phi$ such that $U_{\phi}\in F\upharpoonright_{x}$, then

[TABLE]

denotes the theory resulting from $F\upharpoonright_{x}$ by replacing every occurrence of $U_{\phi}$ with the formula $\theta_{\phi}$. Let $\zeta(x)$ be the formula asserting the following implication:

"There exists the unique family of $\mathcal{L}_{\textnormal{{B}}}\cup\{S\}$-formulae $\{\theta_{\phi}\}_{\textsf{ rank}^{\widehat{c}}(\phi)\leq x}$ indexed with formulae of $\textsf{ rank}^{\widehat{c}}\leq x$ such that:

For every $\phi$, if $\textsf{ rank}^{\widehat{c}}(\phi)=0$, then:

1. (a)

if $\mathcal{M}\models\exists t_{1},\ldots,t_{a}\in\textnormal{{Term}}_{\mathcal{L}_{\textnormal{{B}}}}\phi=R(t_{0},\ldots,t_{a})$, then $\theta_{\phi}(x)=R(t_{0}^{x},\ldots,t_{a}^{x})$, and 2. (b)

if $\phi$ is from $P$, then $\theta_{\phi}(x)=S(\phi,x)$, and 3. (c)

if for some $\psi\in P$, $\phi\approx^{\mathcal{M}}\psi$, then $U_{\phi}$ is defined from $U_{\psi}$ using ($U_{\widehat{\phi}}\rightarrow U_{\phi}$) and ($U_{\phi}\rightarrow U_{\widehat{\phi}}$); 4. (d)

otherwise put $\theta_{\phi}(x)=(x\neq x)$. 2. 2.

$(\mathcal{M},S,P)\models F\upharpoonright_{x}[\theta_{\phi}/U_{\phi}]_{\textsf{ rank}^{\widehat{c}}(\phi)\leq x}$."

Now, we prove $\forall x\zeta(x)$ by induction. This concludes the proof of Lemma 58.∎

Let us now complete the proof of Theorem 54. We shall show how, working inside PA, given an arbitrary good $\Delta_{1}$-theory B, we can elementarily extend an arbitrary $\Delta_{l}$-full model of B to a $\Delta_{l+2}$-model of $\textnormal{{CT}}^{-}[\textnormal{{B}}]$. To this end, working in PA, fix a good theory B, $l\in\mathbb{N}$ and a $\Delta_{l}$-full model $\mathcal{M}$ of B. Next, still working in PA we shall construct an unbounded $\Delta_{l+1}$-chain of $\Delta_{l+1}$-full models

[TABLE]

such that:

• R1

$\mathcal{M}\preceq\mathcal{M}_{0}$,

and for each $y$ we have:

1. R2

$\mathcal{M}_{y}\preceq\mathcal{M}_{y+1}$, 2. R3

$S_{0}=\varnothing$ and $S_{y+1}$ is an $M_{y}$-restricted satisfaction class for $\mathcal{L}_{\textnormal{{B}}}$ and 3. R4

$S_{y}\subseteq S_{y+1}$.

In particular each triple $(\mathcal{M}_{x},S_{x},M_{x-1})$ will have a fixed $\Delta_{l+1}$-complexity. Let us assume that such a chain has been constructed and $\mathcal{M}_{x}(y)$ and $S_{x}(y)$ are formulae defining the sequences of respective $\mathcal{L}_{\textnormal{{B}}}$-full models and restricted satisfaction classes. For example it holds that $\mathcal{M}_{x}(y)$ iff $y$ is the definition of the $x$-th full model (recall that officially full models are identified with their elementary diagrams). Then (in PA) we define the limit model with the formulae:

[TABLE]

where $\textnormal{{Sat}}_{l+1}(x,y)$ denotes the canonical satisfaction predicate for $\Sigma_{l+1}$-formulae.151515Recall that by Convention 28, $\textnormal{{Sat}}_{l+1}(y,z)$ means $\textnormal{{Sat}}_{l+1}(y,\zeta)$, where $\zeta$ is a valuation which assigns $z$ to the only variable of $y$. Note that $\mathcal{M}_{\infty}$ is really a full $\mathcal{L}_{\textnormal{{B}}}$-model, since the chain is elementary with respect to $\mathcal{L}_{\textnormal{{B}}}$-formulae and each $\mathcal{M}_{x}$ is a full model for $\mathcal{L}_{\textnormal{{B}}}$.

The rest of the argument follows along the lines of Enayat–Visser proof: we check that $S_{\infty}$ is a full satisfaction class on $\mathcal{M}_{\infty}$, hence $(\mathcal{M}_{\infty},S_{\infty})$ is a $\Delta_{l+2}$-model of $\textnormal{{CT}}^{-}$.

Let us now construct the promised chain of models: reasoning in PA, we first define a sequence of increasing theories $\left\langle\mathcal{T}_{m}:m\in\mathbb{N}\right\rangle.$ Intuitively speaking, for each $m$, $\mathcal{T}_{m}$ describes a structure $\mathcal{K}_{m}=\left\langle(\mathcal{M}_{i},S_{i}):i\leq m\right\rangle$ and the family $\{(\mathcal{M}_{i},S_{i},M_{i-1})\}_{i\leq m}$ satisfies conditions R1 –R4 for boundedly many numbers. In other words, $\{(\mathcal{M}_{i},S_{i},M_{i-1})\}_{i\leq m}$ is the initial segment of our desired chain consisting of first $m+1$ models.

We now give a precise description of $\mathcal{T}_{m}$. The non-logical symbols of $\mathcal{T}_{m}$ consist of $\mathcal{L}_{\textnormal{{B}}}$, together with constant symbols for every element of $M$, unary predicate symbols $\{\textnormal{M}_{i}:i\leq m\}$, and binary predicate symbols $\{\textnormal{S}_{i}:i\leq m\}.$ Let $\mathcal{L}_{m}$ denote this language.

Convention 62**.**

If $\phi$ is any formula (in the sense of PA), and $\textnormal{M}(x)$ is any of $\textnormal{M}_{i}$’s then we write $\phi^{\textnormal{M}}$ to denote the relativisation of $\phi$ to M. This means that we syntactically replace all quantifiers $\exists x\alpha(x)$ with $\exists x\left(\textnormal{M}(x)\wedge\alpha(x)\right)$, all quantifiers $\forall x\alpha(x)$ with $\forall x\left(\textnormal{M}(x)\rightarrow\alpha(x)\right)$ and adding to $\phi$ a conjunct $\bigwedge_{x_{i}\in\textnormal{{FV}}(\phi)}\textnormal{M}(x_{i})$.

The official translations of R1 through R4 above are as follows:

• •

Condition R1 is translated as $\left\{\phi^{\textnormal{M}_{0}}\ \ |\ \ \phi\in\textsf{ElDiag}(\mathcal{M})\right\}$.

• •

Condition R2 is translated as

[TABLE]

• •

Condition R4 is expressed by the following finite set of sentences:

$\left\{\forall x\forall\alpha(\left(\textnormal{S}_{i}(x,\alpha)\rightarrow\textnormal{S}_{i+1}(x,\alpha)\right):i<m\right\}.$

• •

Condition R3 is expressed by the conjunction of the universal closures of the following finitely many axioms $1$i-$6$i, $0\leq i\leq m$, which directly correspond to the ones from Definition 56 (we stipulate that $\phi^{\mathcal{M}_{-1}}(x)$ is always the formula $x\neq x$) :

• 1i

S_{i}(x,y)\rightarrow\bigl{(}\textnormal{{Form}}_{\mathcal{L}_{\textnormal{{B}}}}^{\textnormal{M}_{i-1}}(x)\wedge\textnormal{{Asn}}^{\textnormal{M}_{i}}(x,y)\bigr{)}.

• 2i

\left(\textnormal{{TermSeq}}_{\mathcal{L}_{\textnormal{{B}}}}^{\textnormal{M}_{i-1}}(\bar{s})\wedge\left(x=R(\bar{s})\right)^{\textnormal{M}_{i-1}}\wedge\textnormal{{Asn}}^{\textnormal{M}_{i}}(x,\alpha)\right)\rightarrow\bigl{(}S_{i}(x,\alpha)\equiv(R(\bar{s}^{\alpha}))^{\textnormal{M}_{i}}\bigr{)}.

• 3i

$\left(\textnormal{{Form}}_{\mathcal{L}_{\textnormal{{B}}}}^{\textnormal{M}_{i-1}}(x)\wedge(x=\neg y)^{\textnormal{M}_{i-1}}\wedge\textnormal{{Asn}}^{\textnormal{M}_{i}}(x,\alpha)\right)\rightarrow\left(S_{i}(x,\alpha)\equiv\lnot S_{i}(y,\alpha)\right).$

• 4i

$\left(\textnormal{{Form}}_{\mathcal{L}_{\textnormal{{B}}}}^{\textnormal{M}_{i-1}}(x)\wedge\left(x=y_{1}\vee y_{2}\right)^{\textnormal{M}_{i-1}}\wedge\textnormal{{Asn}}^{\textnormal{M}_{i}}(x,\alpha)\right)\rightarrow$

\textnormal{S}_{i}(x,\alpha)\equiv\bigl{(}\textnormal{S}_{i}\left(y_{1},\alpha\right)\vee\textnormal{S}_{i}\left(y_{2},\alpha\right)\bigr{)}.

• 5i

\left(\textnormal{{Form}}_{\mathcal{L}_{\textnormal{{B}}}}^{\textnormal{M}_{i-1}}(x)\wedge\bigl{(}\exists v\ \ (\textnormal{{Var}}(v)\wedge x=\exists v\ y)\bigr{)}^{\textnormal{M}_{i}}\wedge\textnormal{{Asn}}^{\textnormal{M}_{i}}(x,\alpha)\right)\rightarrow

$\textnormal{S}_{i}(x,\alpha)\equiv\exists\alpha^{\prime}\left((\alpha^{\prime}\sim_{v}\alpha)^{\textnormal{M}_{i}}\wedge\textnormal{S}_{i}(y,\alpha^{\prime})\right).$

• 6i

$\left(\textnormal{{Form}}_{\mathcal{L}_{\textnormal{{B}}}}^{\textnormal{M}_{i-1}}(x)\wedge\textnormal{{VarSeq}}^{\textnormal{M}_{i-1}}(\bar{v})\wedge\textnormal{{TermSeq}}^{\textnormal{M}_{i-1}}_{\mathcal{L}_{\textnormal{{B}}}}(\bar{s})\wedge\textnormal{{TermSeq}}^{\textnormal{M}_{i-1}}_{\mathcal{L}_{\textnormal{{B}}}}(\bar{t})\wedge\textnormal{{Asn}}^{\textnormal{M}_{i}}(x,\bar{s},\bar{t},\alpha)\right)\rightarrow$

$\left(\left((y_{1}=x[\bar{s}/\bar{v}])^{\textnormal{M}_{i}}\wedge(y_{2}=x[\bar{t}/\bar{v}])^{\textnormal{M}_{i}}\wedge\left(\bar{s}^{\alpha}=\bar{t}^{\alpha}\right)^{\textnormal{M}_{i}}\right)\rightarrow\right.$

\left.\bigl{(}S_{i}(y_{1},\alpha)\equiv S_{i}(y_{2},\alpha)\bigr{)}\right).

We can now use induction on $m$ to show that $\forall m\ \textnormal{{Con}}(\mathcal{T}_{m})$:

Base case

Recall that $\mathcal{M}$ is a fixed $\Delta_{l}$-full model of B. Let $S_{0}=\varnothing.$ Then since $S_{0}$ is definable in $\mathcal{M}$, the elementary diagram of $\mathcal{K}_{0}:=(\mathcal{M},S_{0})$ is also definable. This makes it clear that $\textnormal{{Con}}(\mathcal{T}_{0})$ holds.

Inductive step

Fix $m$ and suppose that $\textnormal{{Con}}(\mathcal{T}_{m})$ holds. Then by Theorem 9, there is a full model $\mathcal{K}_{m}$ of $\mathcal{T}_{m}$ satisfying R1 through R4 above whose elementary diagram is $\Delta_{1+l}$-definable.

Let $\mathcal{L}_{\mathcal{T}_{m}}$ be the language of ${\mathcal{T}_{m}}$, and let $\mathcal{K}_{m}^{-}$ be the reduct of the structure $\mathcal{K}_{m}$ to the language $\{\textnormal{M}_{m},\textnormal{S}_{m},\textnormal{M}_{m-1},+,\cdot\}$ in which the universe of discourse is the $\mathcal{K}_{m}$-interpretation of $\textnormal{M}_{m}.$ For example, since $\mathcal{L}_{\mathcal{T}_{1}}=\{\textnormal{M}_{1},\textnormal{M}_{0},+,\cdot,\textnormal{S}_{0},\textnormal{S}_{1}\}$, a model $\mathcal{K}_{1}$ of $\mathcal{T}_{1}$ will be a structure of the form $(K_{1},M_{1},M_{0},\oplus,\odot,S_{0},S_{1})$, where $M_{i}=\mathrm{M}_{i}^{\mathcal{K}}$, $S_{i}=\mathrm{S}_{i}^{\mathcal{K}}$, and $K_{1}$ is the domain of discourse of $\mathcal{K}_{1}.$ In this case, $\mathcal{K}_{1}^{-}=(M_{1},\oplus,\odot,S_{1}).$ So in general $\mathcal{K}_{m}^{-}$ is of the form $(M_{m},\oplus,\odot,S_{m}).$161616Recall the conventions from Subsection 2.2. Although officially full models are elementary diagrams, we refer to them as though they were usual structures, as it is routine to translate statements about complete Henkinized theories into statements about structures. Observe that $\mathcal{K}_{m}^{-}$ is a full model. Typically, its domain is smaller than the domain of $\mathcal{K}_{m}$.

Also let $\mathcal{M}_{m}$ be the reduct of $\mathcal{K}^{-}_{m}$ to $\mathcal{L}_{\textnormal{{B}}}$. Let us observe that taking reducts does not raise the complexity of (the definition of) models, so $\mathcal{K}_{m}^{-}$ and $\mathcal{M}_{m}$ are still $\Delta_{l+1}$-full models. To this model apply Lemma 58 for $\mathcal{M}=\mathcal{M}_{m}$, $S=S_{m}$ and $P=M_{m-1}$. We are given $\mathcal{N}$, a $\Delta_{l+2}$-full model for $\mathcal{L}_{\textnormal{{B}}}$, and a $\Delta_{l+2}$-set $S^{\prime}$ such that $S^{\prime}$ is an $M_{m}$-restricted satisfaction class and $\mathcal{M}_{m}\preceq\mathcal{N}$. Now we "glue" this model to the end of the chain given by $\mathcal{K}_{m}$. More precisely, we define a model $\mathcal{K}_{m+1}$ for $\mathcal{L}_{m+1}$ in the following way. The universe of $\mathcal{K}_{m+1}$ is the sum of the universes of $\mathcal{K}_{m}$ and $\mathcal{N}$ (without loss of generality, renaming the elements of $N\setminus M_{m}$ if necessary, we assume that $K_{m}\cap N=M_{m}$). $\textnormal{M}_{m+1}$ is interpreted as $N$, $\textnormal{S}_{m+1}$ as $S^{\prime}$ and $+$ and $\cdot$ are interpreted on elements from N as they were in $\mathcal{N}$. For $0\leq i\leq m$ $\textnormal{M}_{i}$ and $\textnormal{S}_{i}$ are interpreted as in $\mathcal{K}_{m}$. Thus we have obtained a structure which contains an elementary chain of models of B, with $\mathcal{N}$ being the top one and possibly some extra elements in the domain of $K_{m}\setminus N$.

Also note that for a structure defined in this manner we do not have an elementary diagram at our disposal, hence an argument is needed to show that $\textnormal{{Con}}(\mathcal{T}_{m+1})$ holds. We argue as in the proof of Corollary 35. Note that if $\pi$ is an alleged proof of contradiction from the axioms of $\mathcal{T}_{m+1}$ which has a subformula property, then only the following types of sentences can occur in it:

• A

formulae of the form $\phi^{\textnormal{M}_{0}}$ for $\phi\in\mathcal{L}_{\textnormal{{B}}}$;

• B

subformulae of sentences of the form

[TABLE]

for $\phi(x_{0},\ldots,x_{1})\in\textnormal{{Form}}_{\mathcal{L}_{\mathrm{B}}}$, $i<m+1$.

• C

subformulae of sentences from (formalization) of condition R4;

• D

subformulae of sentences from 1i - 6i, i$\leq m+1$.

The complexity of formulae from C and D is bounded by a standard number. This is not the case of formulae from A or B. However, to decide every such sentence we can use $\textsf{ElDiag}(\mathcal{K}_{m})$ and $\textsf{ElDiag}(\mathcal{N})$ and this is clearly sufficient (all formulae from B are in the universal closure of boolean closure of formulae of type $\phi^{\textnormal{M}_{i}}$ for $i\leq m+1$). All in all, we can define a $\Sigma_{n}$-truth predicate for $\mathcal{K}_{m+1}$, for sufficiently large $n$, which would work for all formulae from the proof $\pi$. It follows that $\pi$ cannot be a proof of contradiction. This ends the inductive step and we can conclude that $\forall m\ \textnormal{{Con}}(\mathcal{T}_{m})$ holds.

We shall now define the promised chain of models as a full model of the limit of $\mathcal{T}_{m}$’s. Define:

[TABLE]

Here $\mathbb{N}$ is treated internally, it simply denotes the universe. $T_{\infty}$ is a consistent theory of complexity $\Delta_{l}$ (it is computable in $\textsf{ElDiag}(\mathcal{M}))$. It follows that it has a $\Delta_{l+1}$-full model $\mathcal{K}_{\infty}$. This model gives rise to the $\Delta_{l+1}$-chain of $\Delta_{l+1}$-full models $(\mathcal{M}_{x},M_{x-1},S_{x})_{x\in\mathbb{N}}$, which can be defined as follows:

[TABLE]

The construction guarantees that under such a definition, the chain $(\mathcal{M}_{x},S_{x},M_{x-1})$ satisfies the requirements R1 through R4. This finally concludes the proof of feasible reduction of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$ to PA.∎

4.2 Feasible reduction of $\textnormal{{KF}}^{-}[\textnormal{{PA}}]$ to PA

In this subsection we will establish:

Theorem 63**.**

$\textnormal{{KF}}^{-}[\textnormal{{PA}}]$* is feasibly reducible to PA.*

Our proof of the above theorem will demonstrate that the assumption of Corollary 36 holds with the choice of $\mathcal{T}=\textnormal{{KF}}^{-}[\textnormal{{PA}}]$ and $k=4$, i.e., we will prove:

Lemma 64**.**

PA* proves that for any finite fragment P of PA, every full $\Delta_{2}$-model of B has an elementary extension to a $\Delta_{4}$-model of $\textnormal{{KF}}^{-}[\textnormal{{B}}]$.*

Before proving Lemma 64, we will first show that PA can formalize the proof of the existence of recursively saturated models.

Lemma 65**.**

For any $k\in\mathbb{N}$, PA proves that any $\Delta_{k}$-full model $\mathcal{M}$ of a finite fragment B of PA, there exists a $\Delta_{k+1}$-full model $\mathcal{M}^{\prime}$ such that PA proves:

[TABLE]

Let us first make sense of the above claim. Recall that by a full model $\mathcal{M}$ over a language $\mathcal{L}$, we mean an elementary diagram of that model, that is, a complete consistent Henkinized theory.

We say that a model is recursively saturated if for every Turing machine with code $e$, and every finite sequence of elements of $\mathcal{M}$, $a_{1},\ldots,a_{b}\in M$, if for every finite sequence $\phi_{1}(x,\bar{y}),\ldots,\phi_{c}(x,\bar{y})$ of formulae whose Gödel numbers are accepted by the machine with index $e$, there exists an $a\in M$ such that

[TABLE]

then there exists $d\in M$ such that for every $\phi\in\mathcal{L}$ which is accepted by the machine with the code $e$,

[TABLE]

The above definition is well-known. We cite it here to ensure the reader that it really can be spelled out in PA and that the claim of recursive saturation of $\mathcal{M}$ can be effectively produced in polynomial time given the definition of $\mathcal{M}$.

Let us note that the lemma itself is also well known. Its formulation and proof can be found in [19], Lemma IX.4.2. We demonstrate it here for the convenience of the reader.

Proof of Lemma 65.

We reason in PA. Let $\mathcal{L}_{\textnormal{{PA}}}^{*}$ be the arithmetical language with constants $c_{i,j},i,j\in\mathbb{N}$ added. Let $(\phi_{i}^{*})$ be any polynomial time enumeration of all sentences of the language $\mathcal{L}_{\textnormal{{PA}}}^{*}$. Let $\mathcal{M}\models\textnormal{{B}}$ be a full model and let $\textsf{ElDiag}(\mathcal{M})^{*}$ be the theory whose axioms are elementary diagram of $\mathcal{M}$ (which, according to our official definition from Subsection 2.2 is the model $\mathcal{M}$ itself), all Henkin sentences (in the language with the new constants), and all sentences of the following shape:

[TABLE]

where $N\in\mathbb{N}$, and all the constants of $\mathcal{L}_{\textnormal{{PA}}}^{*}\setminus\mathcal{L}_{\textnormal{{PA}}}$ occurring in the formulae $\phi_{1}^{*},\ldots,\phi_{k}^{*}$ are of the form $c_{j,l}$ for $j<i$, and the machine with the code $e$ accepts sentences $\phi_{1}^{*},\ldots,\phi_{k}^{*}$ in less than $N$ steps. By Theorem 9 (ACT) the theory $\textsf{ElDiag}(\mathcal{M})^{*}$ has a $\Delta_{k+1}$-full model $\mathcal{M}^{\prime}$. This ends the proof of the claim * ‣ 65 in PA. ∎

Now, we proceed to the proof of Lemma 64 which will end the proof of Theorem 63.

Proof.

We work in PA. Let $\mathcal{N}$ be any $\Delta_{2}$-model of B. By Lemma 65, there exists a $\Delta_{3}$-full recursively saturated model $\mathcal{M}$ of B.

In our proof, we use a construction resembling the one given originally by Kripke in [14]. As we have already noted in Subsection 3.3.2, a very similar argument appeared before in [1] and [3]. By induction, we define a sequence of arithmetical formulae $\Gamma_{c},c\in M$. That is, a sequence of elements $\Gamma_{c}\in M$ such that $\mathcal{M}\models\Gamma_{c}\in\textnormal{{Form}}^{\leq 1}_{\mathcal{L}_{\textnormal{{PA}}}}$. Let $\Gamma_{0}(x)$ be a definition of the atomic diagram of $\mathcal{M}$. More precisely, let

[TABLE]

Having defined the formula $\Gamma_{n}$, we set $\Gamma_{n+1}(\phi)$ (which we also denote by $\phi\in\Gamma_{n+1}$) if and only if one of the following conditions is satisfied:

• •

$\bigvee_{j\leq n}\ \phi\in\Gamma_{j}.$

• •

$\exists t\in\textnormal{{ClTerm}}_{\mathcal{L}_{\textnormal{{B}}}}\ \phi=Tt\wedge{t}^{\circ}\in\Gamma_{n}$.

• •

$\exists t\in\textnormal{{ClTerm}}_{\mathcal{L}_{\textnormal{{B}}}}\ \phi=\neg Tt\wedge(\neg{t}^{\circ})\in\Gamma_{n}$.

• •

$\exists\psi\in\textnormal{{Sent}}_{\mathcal{L}_{T}}\ \phi=(\neg\neg\psi)\wedge\psi\in\Gamma_{n}$.

• •

$\exists\psi,\eta\in\textnormal{{Sent}}_{\mathcal{L}_{T}}\ \phi=(\psi\vee\eta)\wedge(\psi\in\Gamma_{n}\vee\eta\in\Gamma_{n})$.

• •

$\exists\psi,\eta\in\textnormal{{Sent}}_{\mathcal{L}_{T}}\ \phi=\neg(\psi\vee\eta)\wedge(\neg\psi\in\Gamma_{n}\wedge\neg\eta\in\Gamma_{n}).$

• •

$\exists v\in\textnormal{{Var}}\ \psi\in\textnormal{{Form}}^{\leq 1}_{\mathcal{L}_{T}}\ \phi=\exists v\psi(v)\wedge\exists x\ \ \psi(\underline{x})\in\Gamma_{n}$.

• •

$\exists v\in\textnormal{{Var}}\ \psi\in\textnormal{{Form}}^{\leq 1}_{\mathcal{L}_{T}}\ \phi=\neg\exists v\psi\wedge\forall x\ \ (\neg\phi(\underline{x}))\in\Gamma_{n}$.

Now, let $T$ be the subset of the domain of $M$ defined as the sum $\bigcup_{i\in\mathbb{N}}\Gamma_{i}(\mathcal{M})$. In other words,

[TABLE]

Consider the expanded model $(\mathcal{M},T).$ Since the definition of $(\mathcal{M},T)$ is $\Sigma_{1}$ in the complexity of $\mathcal{M}$, the complexity of the resulting model is $\Delta_{4}$. We would like to ensure that $(\mathcal{M},T)$ is a model $\textnormal{{KF}}^{-}[\textnormal{{B}}]$. The model $(\mathcal{M},T)$ satisfies B, since $\mathcal{M}$ does, so it is enough to check that $(\mathcal{M},T)$ satisfies truth-theoretic axioms $\textnormal{{KF}}1$–$\textnormal{{KF}}10$.

This is obvious for $\textnormal{{KF}}1,\textnormal{{KF}}2$. Let us check the claim for $\textnormal{{KF}}4$. Suppose that $(\mathcal{M},T)\models T(\phi\vee\psi)$. Since $(\mathcal{M},T)\models T(\phi\vee\psi)$, there exists $i$ such that

[TABLE]

Then by definition of $\Gamma_{i}$, either $\mathcal{M}\models\phi\in\Gamma_{i-1}$ (and, consequently, $T(\phi)$ holds) or $\mathcal{M}\models\psi\in\Gamma_{i-1}$ (and then $T(\psi)$ holds). Conversely, if $(\mathcal{M},T)\models T\phi$ or $(\mathcal{M},T)\models T\psi$, then for some $i$, $\mathcal{M}\models\phi\in\Gamma_{i}$ or $\mathcal{M}\models\psi\in\Gamma_{i}$. But then $\phi\vee\psi\in\Gamma_{i+1}$ and, consequently, $(\mathcal{M},T)\models T(\phi\vee\psi)$. This guarantees that $(\mathcal{M},T)\models\textnormal{{KF}}4$. The proofs for axioms $\textnormal{{KF}}3,\textnormal{{KF}}5$ are similar, as are the proofs for axioms $\textnormal{{KF}}9,\textnormal{{KF}}10$. Let us focus on axiom $\textnormal{{KF}}7$.

Suppose that $(\mathcal{M},T)\models T\neg\exists v\ \psi$. Then there exists $i$ such that $\mathcal{M}\models\neg\exists v\ \psi\in\Gamma_{i}$. This implies that for all $x$, $\mathcal{M}\models\neg\psi(\underline{x})\in\Gamma_{i-1}$. Therefore, for all $x\in M$, $(\mathcal{M},T)\models\neg\psi(\underline{x})$ holds.

Conversely, suppose that for all $x\in M$, $(\mathcal{M},T)\models T\neg\psi(\underline{x})$. In other words, for every $x\in M$, there exists $i$ such that $\mathcal{M}\models\neg\psi(\underline{x})\in\Gamma_{i}$. We claim that there exists $k$ such that for all $x$, $\mathcal{M}\models\neg\psi(\underline{x})\in\Gamma_{k}$. Suppose otherwise. Then for every $k$, the following set of arithmetical formulae is realised in $\mathcal{M}$ by some $x$:

[TABLE]

Therefore, by recursive saturation, there exists an $a\in M^{\prime}$ such that for every $k$,

[TABLE]

contrary to the assumption. This implies that there exists $k\in M$ such that $\mathcal{M}\models\neg\psi(\underline{x})\in\Gamma_{k}$ for every $x\in M^{\prime}$, and therefore $\mathcal{M}\models\neg\exists x\psi(x)\in\Gamma_{k+1}$. We conclude that $(\mathcal{M},T)\models\textnormal{{KF}}7$ holds. The case of axiom $\textnormal{{KF}}6$ is straightforward.

In order to prove that $\textnormal{{KF}}8$ holds, we check by induction on $n$ (in PA) that this axiom is satisfied by formulae in $\Gamma_{n}$. The conclusion follows immediately. This concludes the proof of the lemma. ∎

4.3 Feasible reduction of $\textnormal{{FS}}^{-}$ to PA

In this section we strengthen the conservativity proof from Subsection 3.3.3 by establishing the following result:

Theorem 66**.**

$\textnormal{{FS}}^{-}$* is feasibly reducible to PA.*

The key step in our construction is to feasibly reduce the theory of $\omega$-many truth predicates, $\textnormal{{RT}}_{<\omega}^{-}$, defined in Subsection 3.3.3, to PA. This is achieved in the following lemma.

Lemma 67**.**

$\textnormal{{RT}}^{-}_{<\omega}$* is feasibly reducible to PA.*

Proof.

We shall prove that the assumptions of Corollary 34 hold for $\mathcal{T}=\textnormal{{RT}}_{<\omega}^{-}$. Fix $n$ and an arbitrary finite fragment B of PA, w.l.o.g. $\textnormal{{B}}\supseteq I\Sigma_{1}$ and assume that $\mathcal{M}\models\textnormal{{B}}$ is a $\Delta_{2}$-full model. We shall build a $\Delta_{4}$-model of $\textnormal{{RT}}^{-}_{<\omega}[\textnormal{{B}}]$, which clearly suffices (note that now we are talking about $\omega$ internally). The aim is to formalize in PA the conservativity proof from Subsection 3.3.3. In order to do this we shall build a chain of uniformly definable $\Delta_{3}$-full models $(\mathcal{M}_{n})_{n\in\mathbb{N}}$ such that $\mathcal{M}\preceq_{\mathcal{L}_{\textnormal{{PA}}}}\mathcal{M}_{0}$ and for each $n$

$\mathcal{M}_{n}$ is a full $\Delta_{3}$-model of $\textnormal{{RT}}^{-}_{<n+1}[\textnormal{{B}}]$, and 2. 2.

$\mathcal{M}_{k}\preceq_{\mathcal{L}_{<k+1}}\mathcal{M}_{n}$ for each $k<n$.

Clearly the limit model will be a model of $\textnormal{{RT}}^{-}_{\omega}$ (even a full one—this follows by elementarity). To define the respective chain we shall implement the argument from Section 4.1: the chain $\mathcal{M}_{0},\ldots,\mathcal{M}_{k}$ will be described by a $\Delta_{2}$-theory $\mathcal{T}_{k}$ formulated in the language $\mathcal{L}_{\mathcal{T}_{k}}$ whose non-logical symbols are:

symbols of $\mathcal{L}_{\textnormal{{B}}}$; 2. 2.

unary predicates: $M_{0},\ldots,M_{k}$; 3. 3.

unary predicates: $T_{0},\ldots,T_{k}$.

Similarly to the proof for $\textnormal{{CT}}^{-}[\textnormal{{B}}]$ in Subsection 4.1, the axioms of $\mathcal{T}_{k}$ can be divided into three groups:

$\mathcal{M}_{0}$ is an elementary supmodel of $\mathcal{M}$. Formally this is expressed as an infinite set of axioms: $\left\{\phi^{\textnormal{M}_{0}}\ \ |\ \ \phi\in\textsf{ElDiag}(\mathcal{M})\right\}$. 2. 2.

$(\mathcal{M}_{i})_{i\leq k}$ forms an elementary chain of submodels. More precisely: for each $i$, $\mathcal{M}_{i}$ is an $\mathcal{L}_{<i+1}$ elementary submodel of $\mathcal{M}_{i+1}$. Formally this is expressed analogously to the condition (R2) from the proof for $\textnormal{{CT}}^{-}$. 3. 3.

For every $i\leq k$, $\mathcal{M}_{i}$ is a model of $\textnormal{{RT}}^{-}_{<i+1}$. This is expressed by formally relativizing the axioms of $\textnormal{{RT}}^{-}_{<i+1}$ to $M_{i}$.

Now, by induction on $n$ we show that $\forall n\textnormal{{Con}}(\mathcal{T}_{n})$. We follow the lines of the sketch of the conservativity proof given in Subsection 3.3.3. For $n=0$ we simply use the proof from Section 4.1 to build an elementary supmodel of $\mathcal{M}$ satisfying $\textnormal{{CT}}^{-}[\textnormal{{B}}]$. For the induction step, note that, using the same reasoning as we did in Section 4.1 to verify $\textnormal{{Con}}(\mathcal{T}_{k+1})$, it is enough to build a model for $\textnormal{{RT}}^{-}_{<k+1}$ which would be a full model for $\mathcal{L}_{<k}$ but will possibly leave some sentences with $T_{k}$ undefined. As in the conservativity proof for $\textnormal{{RT}}^{-}_{<\omega}$ we use the fact that $\textnormal{{RT}}^{-}_{<k+1}$ is deductively equivalent to the theory I$\mathcal{T}$ below 171717”$I$” abbreviates ”Induction” as this theory is used in the induction step of our construction.:

[TABLE]

From $\textnormal{{Con}}(\mathcal{T}_{k})$ we obtain a model $\mathcal{K}$ of $\textnormal{{RT}}^{-}_{<k}$. We build an extension satisfying I$\mathcal{T}$ in $\omega$ many steps via the union of chain argument. The following is the analogue of Lemma 58 in our situation:

Lemma 68** (Arithmetized Enayat–Visser construction+).**

The sentence expressing the following implication is provable in PA for every $l\in\mathbb{N}$:

If $(\mathcal{M},S,P)$ is a $\Delta_{l}$-full model for $\mathcal{L}_{<k}\cup\{S\}\cup\{P\}$ such that:

$\mathcal{M}\models\textnormal{{I}}\Sigma_{1}$; 2. 2.

$S$* is a $P$-restricted satisfaction class for $\mathcal{L}_{<k}$;*

then there exists a $\Delta_{l+1}$-full model $\mathcal{N}$ and a $\Delta_{l+1}$-set $S^{\prime}\subseteq N^{2}$ such that the following conditions hold:

$\mathcal{M}\preceq\mathcal{N}$; 2. 2.

$S^{\prime}$* is an $M$-restricted satisfaction class for $\mathcal{L}_{<k}$ (we add a predicate for the universe of $\mathcal{M}$ to the language);* 3. 3.

$S\subseteq S^{\prime}$; 4. 4.

*for every $\phi\in\textnormal{{Form}}_{<k-1}(\mathcal{M})$, $(\mathcal{N},S^{\prime},M)\models T_{k-1}(\phi)\rightarrow\forall\alpha S^{\prime}\left(\phi,\alpha\right)$. *

Sketch of the proof.

We indicate how to modify the proof Lemma 58. Firstly, we add the following sentences to the definition of Enayat-Visser theory of $(\mathcal{M},S,P)$:

[TABLE]

Now we work with a finite fragment $F$ of the Enayat and Visser theory. The next step which requires a modification, is the definition of $\textsf{ rank}^{b}$ for a coded set of sentences $b$. According to the previous definition, formula $\phi$ was of $\textsf{ rank}^{b}$ zero if and only if either $\phi$ was atomic or some immediate subformula of $\phi$ was outside $b$. Now we will treat as formulae of $\textsf{ rank}^{b}$ zero all formulae from $\textnormal{{Form}}_{\mathcal{L}_{<k-1}}(\mathcal{M})$ as well. For such formulae $\phi$ we have an obvious candidate for the definition of $\theta_{\phi}(x)$ (i.e. the formula defining the extension for $U_{\phi}(x)$ in $\mathcal{M}$). We define:

[TABLE]

Note that $T_{k-1}$ satisfies generalized regularity, so it is sufficient to verify the truth of $\phi$ on numerals naming values of $\alpha$. The definition of $\textsf{ rank}^{b}\geq x$ is now as follows: there exists a sequence $y$ such that

$\textnormal{{len}}(y)=x+1$ and $(y)_{x}=\{\phi\}$. 2. 2.

For all $i<x+1$ $(y)_{i}\subseteq b$. 3. 3.

For all $i<x$ for all $\theta$, $\theta\in(y)_{i+1}$ iff $\theta\in\textnormal{{Form}}_{\mathcal{L}_{<k}}\setminus\textnormal{{Form}}_{\mathcal{L}_{<k-1}}$ and for all $\psi$ such that $\mathcal{M}\models\psi\triangleleft\theta$, $\psi\in(y)_{i}$.181818Note that if $\phi\in\textnormal{{Form}}_{\mathcal{L}_{<k-1}}$, this condition implies that $y$ has length $1$.

The definitions of $\textsf{ rank}^{b}=x$ and $\widehat{b}$ (for an arbitrary $b$) are analogous to the ones from the original lemma. The last step which requires a modification is the definition of the formula $\zeta(x)$. Below, as in the proof for $\textnormal{{CT}}^{-}$, $c$ is the set of formulae $\phi$ such that $U_{\phi}$ occurs in $F$. We define $\zeta(x)$ to be the formula expressing:

"There exists the unique family of $\mathcal{L}_{<k}\cup\{S\}$-formulae $\{\theta_{\phi}\}_{\textsf{ rank}^{\widehat{c}}(\phi)\leq x}$ indexed with formulae of $\textsf{ rank}^{\widehat{c}}\leq x$ such that:

For every $\phi$, if $\textsf{ rank}^{\widehat{c}}(\phi)=0$, then:

1. (a)

if $\mathcal{M}\models\exists t_{1},\ldots,t_{a}\in\textnormal{{Term}}_{\mathcal{L}_{\textnormal{{B}}}}\phi=R(t_{0},\ldots,t_{a})$ for a relation symbol $R\in\mathcal{L}_{\textnormal{{B}}}$, then $\theta_{\phi}(\alpha)=R(t_{0}^{\alpha},\ldots,t_{a}^{\alpha})$, and 2. (b)

if $\mathcal{M}\models\exists t\in\textnormal{{Term}}_{\mathcal{L}_{\textnormal{{B}}}}(\phi=T_{k-1}(t))$, then $\theta_{\phi}(\alpha)=T_{k-1}(t^{\alpha})$, and 3. (c)

if $\phi\in\textnormal{{Form}}_{\mathcal{L}_{<k-1}}(\mathcal{M})$, then $\theta_{\phi}(x):=T_{k-1}(\phi[x])$, and 4. (d)

if $\phi$ is from $P$, then $\theta_{\phi}(x)=S(\phi,x)$, and 5. (e)

if for some $\psi\in P$, $\phi\approx^{\mathcal{M}}\psi$, then $U_{\phi}$ is defined from $U_{\psi}$ using ($U_{\widehat{\phi}}\rightarrow U_{\phi}$) and ($U_{\phi}\rightarrow U_{\widehat{\phi}}$); 6. (f)

otherwise $\theta_{\phi}(x)=(x\neq x)$. 2. 2.

$(\mathcal{M},S,P)\models F\upharpoonright_{x}[\theta_{\phi}/U_{\phi}]_{\textsf{ rank}^{\widehat{c}}(\phi)\leq x}$."

Note that conditions (c) - (e) are the same as in the original definition. THe rest of the proof is as previously. ∎

Once we can prove $\forall n\textnormal{{Con}}(\mathcal{T}_{n})$, the construction of the chain $(\mathcal{M}_{n})_{n\in\omega}$ and its sum is precisely the same as in Section 4.1. ∎

Now we want to finish the proof of Theorem 66. We have just shown that $\textnormal{{RT}}^{-}_{<\omega}[\textnormal{{PA}}]$ satisfies the assumptions of Corollary 35 (with the "moreover" part). By Observation 38, it follows that $\textnormal{{RT}}^{-}_{<\omega}[\textnormal{{PA}}]$ is PA-provably feasibly strongly reflexive, i.e., there exists a P-time computable function $f$ such that for all $n,k\in\mathbb{N}$, $f(n,k)$ is a PA proof of the sentence

[TABLE]

Note that there exists a P-time computable function $g$ such that for any $n$, $g(n)$ is a PA proof of the sentence

[TABLE]

The above is in fact an easy consequence of the proof of Halbach’s reduction of $\textnormal{{FS}}^{-}$ to $\textnormal{{RT}}^{-}_{<\omega}$ from Lemma 53.

Finally let us observe that the relation $R(k,n,m)$ defined:

"$k$ is a $\textnormal{{FS}}_{n}^{-}$ proof of $m$"

is P-time, so, it is uniformly polynomially binumerable in $\textnormal{{I}}\Delta_{0}+\textnormal{{Exp}}$. This gives us a function $h$ such that for every proof $\pi$ of a sentence $\phi$, $h(\ulcorner\pi\urcorner,n)$ is a PA proof of $\textnormal{{Pr}}_{\textnormal{{FS}}^{-}_{n}}(\underline{\phi})$. Our desired reduction can now be defined as follows: given an $\textnormal{{FS}}^{-}$ proof $\pi$ of a sentence $\phi$ compute $n$ and $k$ such that there are exactly $n$ applications of NEC and CONEC in $\pi$ and $\phi$ is of depth $k$. Using $h$ find the proof of $\textnormal{{Pr}}_{\textnormal{{FS}}^{-}_{n}}(\underline{\phi})$. Compute $g(n)$, i.e. the proof of ($\textnormal{HR}_{n}$). Compute $f(n,k)$, i.e. the proof of ($\textnormal{REF}_{n}$). Apply finitely many logical operations, to conclude $\textnormal{{Tr}}_{k}(\underline{\phi})$. Finally apply Theorem 25 to compute the proof of

[TABLE]

Concatenation of the above proofs yields a PA proof of $\phi$. ∎

4.4 Feasible interpretability of truth theories

In Section 2.5 we gave a terse proof of Theorem 32; that proof did not directly link the notions of feasible reducibility with feasible interpretability, which is how we originally conceived of—and arrived at—our main results. Since interpretations, especially of the feasible variety, are of foundational and philosophical interest in connection with axiomatic theories of truth, we now explain the interpretability-theoretic perspective of our work by establishing the following result:

Theorem 69** (Feasible interpretability of truth theories).**

Let $\mathcal{T}$ be any of the truth theories $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$, $\textnormal{{KF}}^{-}[\textnormal{{PA}}]$, and $\textnormal{{FS}}^{-}[\textnormal{{PA}}]$. Then there exists a uniformly polynomially correct family

$\{I_{n}\}_{n\in\mathbb{N}}:\mathcal{T}\rightarrow\textnormal{{PA}}$**

of interpretations (in the sense of Definition 40).

Note that, by Proposition 42, the existence of a uniformly polynomially correct family of interpretations guarantees feasible reducibility. The proof of Theorem 69 can be readily read-off the second proof of Theorem 32 which we give in this section. We shall demonstrate that the assumptions of Theorem 32 imply the existence of a uniformly polynomially correct family of interpretations. This will make it clear that Theorem 69 holds since we have already already verified in Subsections 4.1, 4.2, and 4.3 that the assumptions of Theorem 32 are met when $\mathcal{T}$ is any of the truth theories $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$, $\textnormal{{KF}}^{-}[\textnormal{{PA}}]$, and $\textnormal{{FS}}^{-}[\textnormal{{PA}}]$. The second proof of Theorem 32 is based on a feasible version of the Arithmetized Completeness Theorem, which we now turn to. In Lemma 70 below an $n$-set should be understood as a set that is definable by a formula of depth $n$ ("definable" in the sense of the feasible $\textnormal{{Sat}}_{n}$ predicates).

Lemma 70** (Feasible Arithmetized Completeness Theorem, FACT).**

There exists a polynomial $p(n)$ and a P-time computable function $f$ such that for every $n$, $f(n)$ is a PA proof of the sentence expressing:

"If an $n$-theory $\mathcal{T}$ in a language $\mathcal{L}$ is consistent then it has a $p(n)$-model."

Moreover there exists a P-time computable function $f$ such that for any $l,k$, $f(l,k)$ is a PA proof of the sentence expressing:

"If $\mathcal{M}$ is an $l$-model of a $k$-theory $\mathcal{T}$, then $\mathcal{T}$ is consistent."

Remark 71** (Uniformity of FACT).**

As a corollary to the proof of the above lemma we will obtain the following proposition:

Proposition 72**.**

Suppose that $\phi(x,\bar{y})$ is an $\mathcal{L}_{\textnormal{{PA}}}$-formula such that

[TABLE]

($\bar{y}$ are the parameters). Then there exists a formula $\phi^{\prime}(x,\bar{y})$ such that $\textnormal{{PA}}\vdash$

[TABLE]

Moreover, there exists a P-time computable function $f$, such that $f(\ulcorner\phi\urcorner)$ is a proof of $\textnormal{{ACT}}_{\phi}$.

Proof of Lemma 70.

See the Appendix. ∎

Let us also mention that in addition to FACT we have also the Feasible Compactness Theorem (the proof of which is rather obvious, as we deal here with consistency in the syntactical sense)

Lemma 73** (Arithmetized Compactness Theorem).**

There exists a P-time computable function $f$ such that for every $n\in\mathbb{N}$, $f(n)$ is a PA proof of the sentence

"An $n$-theory $\mathcal{T}$ is consistent if and only if each bounded fragment of $\mathcal{T}$ is consistent."

We are now ready to present the second proof of Theorem 32. We include the statement here for the benefit of the reader.

Theorem 74** (Theorem 32 redux).**

Let $\mathcal{T}$ be a theory extending PA with an NP-set of axioms. If there is a polynomial $p(n)$ such that for every $n\in\mathbb{N}$,

[TABLE]

Then PA polynomially simulates $\mathcal{T}$. Moreover, if $\mathcal{T}$ admits a P-time computable set of axioms and there exists a P-time computable function $f$ such that for all $n\in\mathbb{N}$, $f(n)$ is a PA proof of

[TABLE]

then $\mathcal{T}$ is feasibly reducible to PA.

Second proof of Theorem 32, Sketch.

We will construct a uniformly polynomially correct family of interpretations $\{I_{n}\}_{n\in\mathbb{N}}:\mathcal{T}\rightarrow\textnormal{{PA}}$. Let us define the theory $\Phi_{n}$:

[TABLE]

where $\textnormal{{Con}}_{\mathcal{T}_{\upharpoonright_{y}}}^{\textnormal{{Tr}}_{n}}$ says that there is no proof of contradiction using as axioms sentences in $\mathcal{T}\upharpoonright_{y}$ or true sentences of depth $n$ (see Remark 20 for an explanation). Observe that the length of (the formula defining) $\Phi_{n}$ is polynomial in $n$ and its shape depends uniformly on $n$. Then for every $n$, $\textnormal{{PA}}\vdash\textnormal{{Con}}_{\Phi_{n}}$ and the proof is uniform in $n$, so in fact there exists a polynomial $p_{1}(n)$ such that for every $n$,

[TABLE]

(for the precise argument see [9], Theorem 2.37). By FACT we know that there exists a formula $\mathcal{M}_{\Phi_{n}}$ and a polynomial $p_{2}(n)$ such that

[TABLE]

Now $I_{n}$ is defined as a relativization to $\mathcal{M}_{\Phi_{n}}$ i.e. a function defined on formulae of the language of $\mathcal{T}$ which preserves boolean operations such that for every relational symbol $R$ and all terms $s_{1},\ldots,s_{n}$

[TABLE]

(recall that full models are coded as elementary diagrams) and for every existential formula $\exists x\phi$,

[TABLE]

We check by contraposition that $I_{n}$ is $n$-correct. Work in PA. Assume $\neg\phi$, where $\phi$ is of length at most $n$. We will derive $\phi^{I_{n}}$. Surely, $\neg\phi$ is of depth at most $n+1$. Let $q(n)$ be as in Theorem 24. Then, by provable Tarski biconditionals, with a proof of length $q(n)$ we conclude

[TABLE]

We show that this implies $\Phi_{n}(\neg\phi)$. By our main assumption ($*$ ‣ 74) and Lemma 33 we obtain a polynomial $p_{3}(n)$ such that

[TABLE]

which directly implies that $\neg\phi$ belongs to $\Phi_{n}$. Consequently

[TABLE]

and the proof of it has length $O(p_{1}(n)+p_{2}(n)+q(n)+p_{3}(n,n))$. Now using at most $|\phi|$ many steps involving formulae of length polynomial in $n$ we obtain

[TABLE]

What is left to show is that for some polynomial $p(n,k)$ and each $k\in\mathbb{N}$,

[TABLE]

for every sentence $\psi$ in $\mathcal{T}\upharpoonright_{n}$. We use polynomial binumerability of $\mathcal{T}\upharpoonright_{n}$ to guarantee that there is a polynomial $p_{4}$ such that for all $n$ and $\psi\in\mathcal{T}\upharpoonright_{n}$,

[TABLE]

Now, as previously, we have

[TABLE]

Hence, adding a few more steps, we also have

[TABLE]

Then, as previously we check that $\psi^{I_{k}}$ is satisfied.

The "moreover" part holds, since if $\mathcal{T}$ is P-time computable, then we can feasibly find a PA proof witnessing that

[TABLE]

The rest of steps are fully analogous. ∎

5 Open Questions

The proofs of our main results in Section 4 suggest that the answers to the following questions are both in the positive; we pose them here as questions since definitive positive answers to them requires a number of technical verifications that are yet to be carried out.

Question A. Is the conservativity of $\textnormal{{CT}}^{-}[\textnormal{{PA}}]$, $\textnormal{{KF}}^{-}[\textnormal{{PA}}]$, and $\textnormal{{FS}}^{-}[\textnormal{{PA}}]$ over PA provable in Buss’s system $\mathsf{S}_{2}^{1}?$

Question B. Suppose B is a sequential theory that is inductive; i.e., the scheme of induction over the natural numbers of B is provable in B. Are $\textnormal{{CT}}^{-}[\textnormal{{B}}]$, $\textnormal{{KF}}^{-}[\textnormal{{B}}]$, and $\textnormal{{FS}}^{-}[\textnormal{{B}}]$ feasibly reducible to B?

6 Appendix

The bulk of the work in the following paper is inherently technical, especially since we are dealing with nuanced arithmetizations and sizes of proofs, and therefore the arguments need to be checked in a very careful manner. In order to minimally distract the reader from the main flow of the argument, we decided to relegate some of the checking to this Appendix.

6.1 Feasible reflexivity

In Section 2.5, we proved Theorem 32 which is the technical core of our paper and which provides us with a uniform way of obtaining polynomial simulations and feasible reductions. We presented two proofs of that theorem. The first of them used the following Lemma (originally Lemma 33):

Lemma 75**.**

There exists a P-time computable function $f$ such that for all $n,k\in\mathbb{N}$ $f(n,k)$ is a PA proof of the:

[TABLE]

It states that we can uniformly find PA proofs of the uniform reflection for bounded fragments of PA. In the proof, we assumed that the statement holds for the axioms in these fragments, and that arithmetical satisfaction predicates enjoy certain regularity properties. Below, we formulate these results in a precise manner and prove them.

Definition 76**.**

If $\alpha$ is a valuation and $v$ is in the domain of $\alpha$, then by $\alpha[v\mapsto x]$ we mean a valuation $\alpha^{\prime}$ which is the same as $\alpha$ except for the variable $v$ whose value is $x$. 2. 2.

If $y$ is a formula, then $\textnormal{{Ind}}(y,v)$ denotes the instantiation of the induction scheme (with parameters) with formula $y$ w.r.t. $v$, i.e. the following formula

[TABLE]

For the sake of simplicity we assume that PA is axiomatized by induction scheme with free variables treated as parameters. This is in order to avoid taking universal closures of axioms. Let us observe that, living inside PA, we know that every object can be named by a closed term. The Proposition below says that for every formula $\phi$ being satisfied by a sequence $y$ is equivalent to the truth of the sentence $\phi[y]$.191919For the notation $\phi[y]$, recall Definition 3.

Convention 77**.**

For the sake of simplicity let us agree that saying that for every $n$ the family $\{\phi_{n}\}_{n\in\mathbb{N}}$ is uniformly feasible in $n$ means that there exists a P-time computable function $f$ such that for each $n$, $f(n)$ is PA proof of $\phi_{n}$.

Proposition 78**.**

The following regularity properties for $\textnormal{{Sat}}_{n}$ predicates are uniformly feasible in $n$:

$\left[\left(\textnormal{{dp}}(y)=n\wedge\alpha^{\prime}=\alpha[v\mapsto S(\alpha(v))]\right)\rightarrow\textnormal{{Sat}}_{n}(y,\alpha^{\prime})\equiv\textnormal{{Sat}}_{n}(y[S(v)/v],\alpha)\right]$. 2. 2.

$\left[\left(\textnormal{{dp}}(y)=n\wedge\alpha^{\prime}=\alpha[v\mapsto z]\right)\rightarrow\textnormal{{Sat}}_{n}(y,\alpha^{\prime})\equiv\textnormal{{Sat}}_{n}(y[\underline{z}/v],\alpha)\right]$.

Proposition 79** (Essentially Pudlák, [17]).**

The following formulae are uniformly feasible in $n$:

$\textnormal{{dp}}(x)=n\wedge"x\textnormal{ is a logical axiom }"\wedge\alpha\in\textnormal{{Asn}}(x)\rightarrow\textnormal{{Sat}}_{n}(x,\alpha)$** 2. 2.

$\textnormal{{dp}}(y)=n\wedge"y\textnormal{ is of the form }x\rightarrow z"\wedge\alpha\in\textnormal{{Asn}}(y)\wedge\textnormal{{Sat}}_{n}(y,\alpha)\wedge\textnormal{{Sat}}_{n}(x,\alpha)\rightarrow\textnormal{{Sat}}_{n}(z,\alpha)$**

Now we prove that for every $n$ the truth of all PA axioms of induction of depth $n$ can be feasibly established in PA.

Proposition 80**.**

The following sentences are uniformly feasible in $n$:

[TABLE]

Proof of Proposition 80.

For the purposes of this proof, we say that $y$ is small if $\textnormal{{dp}}(\textnormal{{Ind}}(y,v))\leq n$. Let $\phi_{1}(y,v,\alpha)$ abbreviate the following formula:

"$y$ is a small formula such that $v$ is a free variable of $y$ and $\alpha$ is an assignment for $y$"

Moreover let $\phi_{2}(y,v,\alpha,x)$ abbreviate

$\exists\alpha^{\prime}\ \ \left(\alpha^{\prime}=\alpha[v\mapsto x]\wedge\textnormal{{Sat}}_{n}(y,\alpha^{\prime})\right)$,

Let $\phi(x,v,y,\alpha)=\phi_{1}(y,v,\alpha)\wedge\phi_{2}(y,v,\alpha,x)$. The idea is that $\alpha$ encodes a sequence of parameters used in the induction and $x$ is the varying value assigned to the variable $v$ while proving $\forall vy$ via induction. We work in PA. We start with $\textnormal{{Ind}}(\phi(x,v,y,\alpha),x)$ which is an axiom of length polynomial in $n$ (since $\phi(x,v,y,\alpha)$ is). Using a few transformations (their number is independent of $n$) we obtain

[TABLE]

Let us look at $\textnormal{{Ind}}(\phi_{2}(y,v,\alpha,x),x)$. Observe that by Proposition 78

$\phi_{2}(y,v,\alpha,0)$ is equivalent to $\textnormal{{Sat}}_{n}(y[\underline{0}/v],\alpha)$ and 2. 2.

$\phi_{2}(y,v,\alpha,S(x))$ is equivalent to $\textnormal{{Sat}}_{n}(y[S(v)/v],\alpha)$.

Hence $\textnormal{{Ind}}(\phi_{2}(y,v,\alpha,x),x)$ implies

[TABLE]

Now by compositional axioms for $\textnormal{{Sat}}_{n}$ the above is equivalent to

[TABLE]

∎

6.2 Congruence lemma

We sketch the proof of the following lemma from Section 4.1.

Lemma 81** (Congruence lemma).**

For all $\phi$, $\phi^{\prime}$, $\psi^{\prime}$ it holds that

[TABLE]

Sketch of the proof.

We prove the lemma by induction on the complexity of $\phi$ (carried out in $\mathcal{M}$ which we assumed to satisfy $\textnormal{{I}}\Sigma_{1}$). The only non-trivial step is the one for $\exists$. Assume $\phi^{\prime}=\exists v\phi$. Then $\psi^{\prime}=\exists v\psi$. Take $\widehat{\phi^{\prime}}(=\widehat{\psi^{\prime}})$, which, by definition, is of the form $\exists v\eta$. In $\eta$ replace all the occurrences of maximal terms in $\eta$ (i.e. the ones which do not occur within a term) which contain only free variables (in $\eta$) with fresh variables, without using the same variable twice. Then rename the free variables of the resulting formula according to the procedure adopted in condition $4.$ of the definition of the term trivialization. In this way we obtain the term trivialization of both $\psi$ and $\phi$. ∎

6.3 FACT

In Subsection 4.4, an alternative proof has been provided of Theorem 32 which says that if PA proves reflection over fragments of another theory $\mathcal{T}$, then $\mathcal{T}$ is feasibly reducible to PA. The second proof of that theorem used the fact that arithmetized completeness theorem can proved with a proof of size polynomial in the size of the formula defining $\mathcal{T}$. This was stated as Lemma 70. In this subsection, we prove this result.

Lemma 82** (Feasible Arithmetized Completeness Theorem, FACT).**

There exists a polynomial $p(n)$ and a P-time computable function $f$ such that for every $n$, $f(n)$ is a PA proof of the sentence

"If an $n$-theory $\mathcal{T}$ in a language $\mathcal{L}$ is consistent then it has a $p(n)$ full model"

Moreover, there exists a P-time computable function $f$ such that for any $l,k$, $f(l,k)$ is a PA proof of the sentence

"If $\mathcal{M}$ is a $l$-full model of a $k$-theory $\mathcal{T}$, then $\mathcal{T}$ is consistent."

Proof.

To prove the second part we show by induction on the lengths of proofs that any $l$-full model (which, recall, is the same as a complete consistent Henkinized theory) is closed under reasoning in first order logic. This argument is carried out uniformly with the only difference that we use different feasible satisfaction predicates depending on the complexity of the model.

To prove the first part we follow the "leftmost branch" strategy. The proof is routine but we present it to be on the safe side. Assume that an $\mathcal{L}$-theory $\theta(x)$ of depth $n$ is consistent. (Note that $\theta(x)$ and $\mathcal{L}$ might contain arbitrary parameters.) Note that we need not care about the rise in $\Sigma_{k}$-complexity of the formula defining a model for $\theta(x)$ as long as the construction of the relevant formula is uniformly feasible in $n$. Let $\textnormal{{Form}}^{H}_{\mathcal{L}}$ be the set of formulae of $\mathcal{L}$ enriched with Henkin constants (we denote the Henkin constant for the formula $\phi$ with $c_{\phi}$ and assume that the function $\phi\mapsto c_{\phi}$ is $\Delta_{1}$).

Step $1.$: finding a complete, consistent Henkin extension Let $\theta^{\prime}(x)$ be defined as

[TABLE]

Here $\theta^{\prime}(x)$ is of depth polynomial in $n$ (we may assume that the length, hence also the depth, of the formula defining $\mathcal{L}$ is polynomial in $n$) and of length polynomial in the length of $\theta$. We check that $\textnormal{{Con}}_{\theta^{\prime}(x)}$ holds: each proof of $\exists x(x\neq x)$ from the axioms of $\theta^{\prime}(x)$ can be transformed into $\theta(x)$ proof of

[TABLE]

Then we check that the above is equivalent to

[TABLE]

which contradicts the consistency of $\theta$. Note that the above argument is uniform in $\theta$.

Let $\sigma(x)=y$ be any enumeration of $\textnormal{{Form}}_{\mathcal{L}}^{H}$. For any binary sequence $\tau$ of length $y$ let $\textsf{enum}(\sigma,\tau,y)$ be the theory:

[TABLE]

$\textsf{enum}(\sigma,\tau,y)$ enumerates first $y$ elements of $\sigma$, adding negation at the front of the $i$-th element if $\tau(i)=1$. Let $\theta^{H}(x)$ be the sentence saying:

"There exist the unique $y,\tau$ such that

$\tau\textnormal{ is a binary sequence of length }y$ and 2. 2.

$\forall i<y\left(\tau(i)=0\iff\textnormal{{Con}}_{\theta^{\prime}+\textsf{enum}(\sigma,\tau,i)+\sigma(i)}\right)$ and 3. 3.

$\left(\textnormal{{Con}}_{\theta^{\prime}+\textsf{enum}(\sigma,\tau,y)+\sigma(y)}\wedge x=\sigma(y)\right)\vee\left(\neg\textnormal{{Con}}_{\theta^{\prime}+\textsf{enum}(\sigma,\tau,y)+\sigma(y)}\wedge x=\neg\sigma(y)\right).$"

Once again $\theta^{H}(x)$ is of length polynomial in the length of $\theta$ and this polynomial does not depend on the initial choice of $\theta$. We show that $\theta^{H}$ is a complete and consistent theory with Henkin sentences (which, according to our definitions is the same as a full model). The whole argument was carried out uniformly in $\theta$ and can be produced by a P-time function $f$.

∎

6.4 A glossary of technical notions

This paper contains a fairly large number of technical definitions; here we enclose a glossary of such terms in order to assist the reader.

• •

$x\in\textnormal{{Asn}}(y)$ means that $x$ is an assignment for a formula or a term $y$ (or for a set of terms or formulae $y$), i.e. $x$ is a function whose domain includes the free variables of $y$ (or whose domain includes free variables of all elements of $y$). See Definition 1 and Convention 4.

• •

$x\in\textnormal{{ClTerm}}_{\mathcal{L}}$ means that $x$ is a closed term of a language $\mathcal{L}$, see Definition 1 and Convention 4.

• •

$x\in\textnormal{{ClTermSeq}}_{\mathcal{L}}$ means that $x$ is a sequence of closed terms of a language $\mathcal{L}$, see Definition 1 and Convention 4.

• •

$\textnormal{{Con}}_{\mathcal{T}}$ is an arithmetized consistency statement for $\mathcal{T}$. See Corollary 19.

• •

$\textnormal{{CT}}^{-}$ is the compositional theory of truth over PA, see Definition 44.

• •

$\textnormal{{CT}}^{-}[\textnormal{{B}}]$ is the compositional theory of truth over a theory B extending $\textnormal{{I}}\Delta_{0}+\textnormal{{Exp}}$, see Definition 44.

• •

$\textnormal{{dp}}(\phi)$ is the syntactic depth of a formula $\phi$, see Definition 22.

• •

$\textsf{ElDiag}(\mathcal{M})$ (elementary diagram of $\mathcal{M}$) is the same as a full model $\mathcal{M}$, this notation is used when $\mathcal{M}$ is viewed as a complete Henkinized theory, rather than a structure.

• •

$x\in\textnormal{{Form}}_{\mathcal{L}}$ means that $x$ is a formula of the language $\mathcal{L}$, see Definition 1 and Convention 4.

• •

$x\in\textnormal{{Form}}^{\leq 1}_{\mathcal{L}}$ means that $x$ is a formula of the language $\mathcal{L}$ with at most one free variable, see Definition 1 and Convention 4.

• •

$x\in\textnormal{{Form}}^{1}_{\mathcal{L}}(x)$ means that $x$ is a formula of the language $\mathcal{L}$ with exactly one free variable, see Definition 1 and Convention 4.

• •

$\textnormal{{FS}}^{-}$ is the Friedman–Sheard self-referential theory of truth over PA without induction, see Definition 46.

• •

$\textnormal{{FS}}^{-}[\textnormal{{B}}]$ is the Friedman–Sheard self-referential theory of truth over a theory B extending $\textnormal{{I}}\Delta_{0}+\textnormal{{Exp}}$ without induction, see Definition 46.

• •

$x\in\textnormal{{FV}}(y)$ means that $x$ is a free variable of $y$, see Definition 1 and Convention 4.

• •

$x\in\textnormal{{FVSeq}}(y)$ means that $y$ is a coded sequence whose elements are (some) free variables of $x$, see Definition 1 and Convention 4.

• •

$\textnormal{{KF}}^{-}$ is the Kripke–Feferman self-referential theory of truth over PA without induction, see Definition 45.

• •

$\textnormal{{KF}}^{-}[\textnormal{{B}}]$ is the Kripke–Feferman self-referential theory of truth over a theory B extending $\textnormal{{I}}\Delta_{0}+\textnormal{{Exp}}$ without induction, see Definition 45.

• •

$\textnormal{{len}}(s)$ is the length of a sequence $s$, see Definition 1 and Convention 4.

• •

$n$-model (full model) is a (full) model defined with a formula of depth $n$.

• •

$\textnormal{{Pr}}_{\mathcal{T}}(y)$ means that there exists a proof of $y$ in the theory $\mathcal{T}$. See Corollary 19.

• •

$\textnormal{{Proof}}_{\mathcal{T}}(m,n)$ means that $m$ is a proof of $n$ from the theory $\mathcal{T}$. See Corollary 19.

• •

$x\in\textnormal{{Sent}}_{\mathcal{L}}$ means that $x$ is a sentence of the language $\mathcal{L}$, see Definition 1 and Convention 4.

• •

$x\in\textnormal{{Term}}_{\mathcal{L}}$ means that $x$ is a term of the language $\mathcal{L}$, see Definition 1 and Convention 4.

• •

$x\in\textnormal{{TermSeq}}_{\mathcal{L}}$ means that $x$ is a sequence of terms of the language $\mathcal{L}$, see Definition 1 and Convention 4.

• •

$n$-theory is a theory defined with a formula of depth $n$.

• •

$\textnormal{{Var}}(x)$ means that $x$ is (an arithmetized) variable, see 1.

• •

$\beta\sim_{v}\alpha$ means $\alpha$ and $\beta$ are functions, $v$ is a variable and $\alpha(w)=\beta(w)$ for all variables $w$, possibly except for $v$ which also possibly belongs only to the domain of $\beta$, see Definition 1.

• •

$\phi[\alpha]$ is a formula $\phi$ with the numeral $\underline{\alpha(v)}$ substitued for every every occurrence of $v$ for every free variable $v$ of $\phi$, see Definition 3.

• •

$\phi[s/v]$ denotes the formula $\phi$ with the term $s$ substituted for the variable $v$, see Definition 3.

• •

$\parallel\phi\parallel_{\mathcal{T}}$ is the length of the shortest proof of $\phi$ in $\mathcal{T}$, see Definition 11.

• •

$\phi\triangleleft\psi$ means that $\phi$ is an immediate subformula of $\psi$, see the proof of Lemma 58.

• •

$\widehat{\phi}$ is the term trivialization of $\phi$, see remarks preceding Lemma 61.

• •

$\mathcal{M}\preceq_{\mathcal{L}}\mathcal{N}$ means that $\mathcal{M}^{\prime}\preceq\mathcal{N}^{\prime}$, where $\mathcal{M}^{\prime},\mathcal{N}^{\prime}$ are reducts of $\mathcal{M},\mathcal{N}$ to the language $\mathcal{L}$, see Definition 30 or 7 and the subsequent remarks.

• •

$t^{\alpha}$ is the value of term $t$ in which every free variable $v$ has been evaluated to $\alpha(v)$, see Definition 3.

• •

$\mathcal{T}\vdash^{n}\phi$ means that the length of the shortest proof of $\phi$ in $\mathcal{T}$ is not greater than $n$, see Definition 11.

• •

$\mathcal{T}\upharpoonright_{n}$ for a theory $\mathcal{T}$ means the set of axioms of $\mathcal{T}$ of length at most $n$, see Definition 31.

• •

$\underline{x}$ is a numeral denoting $x$, see Definition 2 and Convention 4.

• •

${x}^{\circ}=y$ means that $y$ is the value of the term $x$, see Definition 1 and Convention 4.