Conservativeness of PAV

This post continues on the theme of the argument against deflationism, concerning the conservativness of truth theories. I want to discuss the role of induction.

It turns out that this is a very complicated issue, and people have slipped up a bit over it. But there are some points that aren't too complicated, and one concerns the result of extending $\mathsf{PA}$ with new vocabulary, and therefore new induction instances, but without new axioms for the new vocabulary. If there are no new axioms, then the result is conservative.

Suppose we let $L$ be the usual first-order language of arithmetic (non-logical vocabulary is $\{0,^{\prime},+,\times\}$) and let

$V := \{P_1, \dots\}$

be some new vocabulary. Each $P_i$ is a predicate symbol (say, of arity $k_i$). Let $L_V$ be the extended language. Let $\mathsf{PA}$ be the usual system of Peano arithmetic in $L$, with the induction scheme,

$\phi^x_0 \wedge \forall x(\phi \to \phi^x_{x^{\prime}}) \to \forall x \phi$

(here $\phi$ is a formula (possibly with parameters), and $\phi^x_t$ is the result of substituting the term $t$ for all free occurrences of $x$, relabelling bound variables inside $\phi$ if necessary to avoid collisions).

Definition: $\mathsf{PAV}$ is the result of extending $\mathsf{PA}$ with all instances of induction for the extended language $L_V$.

Theorem: $\mathsf{PAV}$ conservatively extends $\mathsf{PA}$.

Proof. The "proof idea" is to give a translation that maps every proof (derivation) in the "bigger" theory into a proof in the "smaller" theory. We define a translation

$^{\circ}: L_V \to L$

as follows. For any $L$ symbol, including variables and terms, the translation is the identity mapping. For compounds, we assume $^{\circ}$ just commutes. For a $n$-ary predicate symbol $P \in V$, we translate an atomic formula $P(t_1, \dots, t_n)$ as follows:

$(P(t_1, \dots, t_n))^{\circ} := (P)^{\circ}(t_1, \dots, t_n)$.

where $(P)^{\circ}(x_1, \dots, x_n)$ is any $L$-formula. This translation is crazy, of course. But we have no axioms constraining the symbol $P$, so we can translate it any way we like. (If we did have such axioms, say $Ax_{P}$, we would need to try and translate $Ax_{P}$ as a theorem of $\mathsf{PA}$.)

The formula $(P(t_1, \dots, t_n))^{\circ}$ is then an $L$-formula. This means that, for any $\phi \in L_V$, $(\phi)^{\circ}$ is equivalent to some $L$-forrnula, say $\theta$. Now consider the induction axiom for any $\phi \in L_V$:

$\phi^x_0 \wedge \forall x(\phi \to \phi^x_{x^{\prime}}) \to \forall x \phi$

Its translation under $^{\circ}: L_V \to L$ is equivalent (because $^{\circ}$ commutes with connectives and quantifiers) to

$\theta^x_0 \wedge \forall x(\theta \to \theta^x_{x^{\prime}}) \to \forall x \theta$

And this is an induction axiom in $L$. Hence, it is an axiom of $\mathsf{PA}$.
Finally, suppose that

$\mathsf{PAV} \vdash \psi$, 

where $\psi \in L$. Then applying the translation $^{\circ}$ to all the formulas in the derivation of $\psi$ converts the derivation into a derivation of $\psi$ in $\mathsf{PA}$ (in $L$), as each induction instance is translated to an induction instance in $L$ (which is an axiom of $\mathsf{PA}$) and the translation preserves $\vdash$ too. So,

$\mathsf{PA} \vdash \psi$.

QED.

This may be applied to the case where the new vocabulary is a predicate $T(x)$, perhaps to be thought of as a truth predicate, but we do not include any new axioms for $T(x)$ itself. Halbach 2011 calls the corresponding theory $\mathsf{PAT}$. So, $\mathsf{PAT}$ conservatively extends $\mathsf{PA}$.