Weak Representability and Derivability Condition 1

Question

Can someone point out the error in the following reasoning?

Let K be an axiomatizable, consistent extension of Peano Arithmetic. Let P' denote the Gödel number for P.

1. K is axiomatizable, thus Thm(k) is recursively enumerable, thus Thm(K) is weakly representable. This means $$P ∈ Thm(K) ⇔ K ⊢ Prov(P')$$

2. Derivability Condition 1 is $$K ⊢ P ⇒ K ⊢ Prov(P')$$ The converse of this is not necessarily true.

3. By definition $$P ∈ Thm(K) ⇔ K ⊢ P$$

If all three are true, we get a contradiction because (1) and (3) imply the converse of (2), which does not necessarily hold. Can someone explain what is wrong here and why?

Answer 1

Assuming statement 3, statement 2 is just the $\Rightarrow$ version of statement 1, and the converse of statement 2 is just the $\Leftarrow$ version of statement 1. So the issue is that the $\Leftarrow$ version of statement 1 also does not always hold, for the same reason that the converse of statement 2 does not always hold.

This leaves the question of how, if Thm($K$) is weakly representable, there is no contradiction. The answer is that, although Thm($K$) is weakly representable in a wide class of theories, in general the formula used to weakly represent it is not the formula $\text{Prov}(n)$. That formula only represents the set Thm($K$) under the assumption that every $\Sigma^0_1$ sentence provable in $K$ is true, an assumption known as $\Sigma^0_1$-soundness that is not true in general. So, although Thm($K$) is weakly representable, this does not mean that $$ P \in \text{Thm}(K) \Leftrightarrow K \vdash \text{Prov}(P'). $$

Nevertheless, the following theorem does hold:

Representability Theorem. For every consistent recursively axiomatizable theory $K$ in the language of arithmetic, if $K$ includes Robinson Arithmetic $Q$ then every semi-recursive relation is weakly representable in $K$.

In the case where the theory is $\Sigma^0_1$ sound, the proof is essentially just Gödel numbering: we take an algorithm that semi-decides the relation, and we encode the algorithm into a formula of arithmetic.

The proof is more complicated, however, in the general case. One exposition of the full proof is on pp. 382-384 of Hinman, Fundamentals of Mathematical Logic, 2005. The proof method uses Rosser's trick and the diagonalization lemma.

The fact that the formula representing Thm($K$) is not, in general, the formula $\text{Prov}(n)$ is not emphasized in many sources, such as in the Stanford Encyclopedia article on the incompleteness theorems, so it is easy to be confused by this point. Moreover, some sources implicitly assume that they are only dealing with $\Sigma^0_1$-sound or with $\omega$-consistent theories, and sometimes it is hard to tell exactly what assumptions about the theory are being made.