Skip to main content
1 of 2
Emil Jeřábek
  • 47.8k
  • 4
  • 151
  • 209

$\let\eq\leftrightarrow\def\p#1{\langle#1\rangle}$Fix a Gödel numbering of formulas such that a subformula of $\phi$ has a smaller number than $\phi$. Let a truth predicate up to $n$ be a set $T$ of tuples $\p{\phi,\vec a}$, where $\phi$ is a formula of PA, and $\vec a$ an assignment to its free variables, which satisfies the usual Tarski definition for formulas $\phi\le n$:

  • If $\phi\le n$ is of the form $t=s$ for some terms $t$ and $s$, then $\forall\vec a\,(\p{\phi,\vec a}\in T\eq t(\vec a)=s(\vec a))$. (So you need an evaluation function for terms here. I leave this to the reader.)

  • If $\phi\le n$ has the form $\psi\land\chi$, then $\forall\vec a\,(\p{\phi,\vec a}\in T\eq\p{\psi,\vec a}\in T\land\p{\chi,\vec a}\in T)$, and similarly for $\lor$, $\to$, $\neg$.

  • If $\phi\le n$ has the form $\exists x_i\,\psi$, then $\forall\vec a\,(\p{\phi,\vec a}\in T\eq\exists b\,\p{\psi,\vec a[i\mapsto b]}\in T)$, where $\vec a[i\mapsto b]$ is the sequence that differs from $\vec a$ such that the $i$th element is $b$, and similarly for $\forall x_i\,\psi$.

These conditions can be written as a $\Delta^1_0$ formula $\def\trp{\mathrm{TrPred}}\trp(T,n)$.

$\def\aca{\mathrm{ACA}_0}\aca$ proves $\exists T\,\trp(T,n)\to\exists T\,\trp(T,n+1)$: if $\trp(T,n)$, and, say, $n+1$ is the Gödel number of $\phi=\exists x_i\,\psi$, then $\trp(T',n+1)$, where $$T'=\{\p{x,\vec y}\in T:x\le n\}\cup\{\p{n+1,\vec a}:\exists b\,\p{\psi,\vec a[i\mapsto b]}\in T\}.$$

Thus, $\aca+\Sigma^1_1$-induction proves $\forall n\,\exists T\,\trp(T,n)$.

Now, given a PA-proof $\phi_0,\dots,\phi_s$, let $n$ be larger than the Gödel numbers of all $\phi_i$, and let $T$ satisfy $\trp(T,n)$. Then prove by induction on $i$ that $\forall\vec a\,\p{\phi_i,\vec a}\in T$. But if $\phi_s$ is a simple contradiction such as $0\ne0$, the definition of $\trp$ implies $\p{\psi_s,\varnothing}\notin T$. This is a contradiction. Thus, $\aca+\Sigma^1_1$-induction proves the consistency of PA.

You can easily upgrade this to a bona fide satisfaction predicate $\models$ for all formulas: you can prove by induction that any two truth predicates up to $n$ agree an all formulas $\phi\le n$, and then you can define $$\mathbb N\models\phi[\vec a]\iff\exists T,n\,(n\ge\phi\land\trp(T,n)\land\p{\phi,\vec a}\in T),$$ which is due to uniqueness of the truth predicates equivalent to $$\forall T,n\,(n\ge\phi\land\trp(T,n)\to\p{\phi,\vec a}\in T),$$ and satisfies the Tarski definition for all formulas, provably in $\aca+\Sigma^1_1$-induction. (If you want $\models$ to exist as a set, use $\Delta^1_1$-comprehension on top of this.)

Emil Jeřábek
  • 47.8k
  • 4
  • 151
  • 209