Arithmetical formalization of "F is sound"

Question

In How subtle is Gödel's theorem? More on Roger Penrose, Martin Davis points out the fact that the statement

F is sound $\implies$ G(F) is true

where F is some recursively axiomizable extension of Q and G(F) is the Gödel sentence of F, is a $\Delta^0_2$ sentence. I am wondering if someone can show me or direct me to a reference where this is explicitly shown. I spent a long time trying to formalize it but I could not come up with a way to express "F is sound" arithmetically.

Answer 1

If you read the fine print here, you’ll see that by “sound”, Davis means $\Pi_1$-sound. There is a arithmetical truth predicate for $\Pi_1$ sentences (in fact, this predicate is $\Pi_1$) so the statement is just “if every $\Pi_1$ sentence in $F$ is true, then $G(F)$ is true.” Where by “is true” we mean “satisfies the truth predicate for $\Pi_1$ sentences”.

As for why it is $\Delta_2$, since the property of being in $F$ is $\Sigma_1$ and truth is $\Pi_1$, “F is sound” is of the form $\forall x(\Sigma_1\to\Pi_1)$ and since $\Sigma_1\to\Pi_1$ is $\Pi_1,$ the whole thing is $\Pi_1.$ Since truth is $\Pi_1,$ “$G(F)$ is true” is $\Pi_1.$ So the whole assertion has the form $\Pi_1\to\Pi_1,$ which is $\Delta_2.$

Answer 2

Indeed, full soundness (which is not what Martin is talking about, per spaceisdarkgreen's answer) is not arithmetically expressible. Precisely:

There is no formula $\varphi$ in the language of arithmetic such that whenever $T$ is a (index for a) recursively enumerable theory in the language of arithmetic, $T$ is sound iff $\varphi(T)$ is true (in the standard model $\mathbb{N}$).

(We need to bring different $T$s into the picture to avoid triviality; e.g. since PA is actually sound, technically the sentence "$2+2=4$" is equivalent to the soundness of PA.)

This is just Tarski's undefinability theorem all over again: letting $e_\psi$ be the canonical index for the r.e. theory $\{\psi\}$ we have that $\psi$ is true iff $\varphi(e_\psi)$ is true, and this gives us a way to define truth in the language of arithmetic.