February 16
Mateusz Łełyk,
University of Warsaw
Nonequivalent axiomatizations of ${\rm PA}$ and the Tarski Boundary
We study a family of axioms expressing $$`\text{All axioms of PA are true.' (*)}$$ where PA denotes Peano Arithmetic. More precisely, each such axiom states that all axioms from a chosen axiomatization of PA are true. We start with a very natural theory of truth ${\rm CT}^-({\rm PA})$ which is a finite extension of PA in the language of arithmetic augmented with a fresh predicate T to serve as a truth predicate for the language of arithmetic. Additional axioms of this theory are straightforward translations of inductive Tarski truth conditions. To study various possible ways of expressing (*), we investigate extensions of ${\rm CT}^-({\rm PA})$ with axioms of the form $$\forall x \bigl(\delta(x)\rightarrow T(x)\bigr).$$ In the above (and throughout the whole abstract) $\delta(x)$ is an elementary formula which is proof-theoretically equivalent to the standard axiomatization of PA with the induction scheme, i.e. the equivalence $$\forall x \bigl(\text{Prov}_{\delta}(x)\equiv \text{Prov}_{\rm PA}(x)\bigr).$$ is provable in $I\Sigma_1$. For every such $\delta$, the extension of ${\rm CT}^-({\rm PA})$ with the above axiom will be denoted ${\rm CT}^-[\delta]$.
In particular we shall focus on the arithmetical strength of theories ${\rm CT}^-[\delta]$. The 'line' demarcating extensions of ${\rm CT}^-({\rm PA})$ which are conservative over PA from the nonconservative ones is known in the literature as the Tarski Boundary. For some time, there seemed to be the least (in terms of deductive strength) *natural* extension of ${\rm CT}^-({\rm PA})$ on the nonconservative side of the boundary, whose one axiomatization is given by ${\rm CT}^-({\rm PA})$ and $\Delta_0$ induction for the extended language (the theory is called ${\rm CT}_0$). This theory can equivalently be axiomatized by adding to ${\rm CT}^-({\rm PA})$ the natural formal representation of the statement 'All theorems of ${\rm PA}$ are true.'. We show that the situation between the Tarski Boundary and ${\rm CT}_0$ is much more interesting:
Theorem 1: For every r.e. theory Th in the language of arithmetic the following are equivalent:
1) ${\rm CT}_0\vdash$ Th
2) there exists $\delta$ such that ${\rm CT}^-[\delta]$ and Th have the same arithmetical consequences.
Theorem 1 can be seen as a representation theorem for r.e. theories below ${\rm REF}^{\omega}({\rm PA})$ (all finite iterations of uniform reflection over ${\rm PA}$, which is the set of arithmetical consequences of ${\rm CT}_0$): each such theory can be finitely axiomatized by a theory of the form ${\rm CT}^-[\delta]$, where $\delta$ is proof-theoretically reducible to ${\rm PA}$.
Secondly, we use theories ${\rm CT}^-[\delta]$ to investigate the situation below the Tarski Boundary. We shall prove the following result
Theorem 2: There exists a family $\{\delta_f\}_{f\in\omega^{<\omega}}$ such that for all $f,g\in\omega^{<\omega}$
1) ${\rm CT}^-[\delta_f]$ is conservative over ${\rm PA}$;
2) if $f\subsetneq g$, then ${\rm CT}^-[\delta_g]$ properly extends ${\rm CT}^-[\delta_f]$;
3) if $f\perp g$ then ${\rm CT}^-[\delta_g]\cup CT^-[\delta_f]$ is nonconservative over ${\rm PA}$ (but consistent).