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,

${\varphi }_0^x\wedge \mathrm{\forall }x(\varphi \to {\varphi }_{x^{\prime }}^x)\to \mathrm{\forall }x\varphi$

(here $\varphi$ is a formula (possibly with parameters), and ${\varphi }_t^x$ is the result of substituting the term $t$ for all free occurrences of $x$, relabelling bound variables inside $\varphi$ 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 $A{x}_P$, we would need to try and translate $A{x}_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 $\varphi \in L_V$, $(\varphi {)}^{\circ }$ is equivalent to some $L$-forrnula, say $\theta$. Now consider the induction axiom for any $\varphi \in L_V$:

${\varphi }_0^x\wedge \mathrm{\forall }x(\varphi \to {\varphi }_{x^{\prime }}^x)\to \mathrm{\forall }x\varphi$

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

${\theta }_0^x\wedge \mathrm{\forall }x(\theta \to {\theta }_{x^{\prime }}^x)\to \mathrm{\forall }x\theta$

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

$\mathsf{PAV}⊢\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 $⊢$ too. So,

$\mathsf{PA}⊢\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}$.