provability and theorem

Question

I am studying first order logic and I have a hard time understanding the link between provable formulas and theorem. In the book by Shoenfield, the predicate $ Pr_{T}(a,b)$ of is defined as the set of (a,b) such that there exists formulas $A_{1},A_2,...,A_k$ which are a proof in T and $<Num(A_1),...,Num(A_k)>=b$ and a=$Num(A_k)$. This predicate is recursive and thus representable in the theory N by a formula $B^T$ with x,y distinct variables. Then we define $A^T$ as $\exists y B^T$.

So if I understood well, $T|-A^T_{x}[ \underline{Num(E)}] $ means that there exists a proof of E in T. We also have 3 derivability conditions, one of which interests me here:

if $T|- D $ then $N|-A^T_{x}[ \underline{Num(D)}] $

My issue is that I don't see why this relation is not an equivalence. Because if $T|-A^T_{x}[ \underline{Num(D)}] $ then it means that $D$ is provable in T and thus that it is a theorem.

Can anyone help me with this matter ?

Thanks!

Answer 1

Long comment

The so-called arithmetization of syntax is relative to a theory $T$ with language $L$ [page 123].

The author defines a collection of numerical predicates and relations that mimic the properties of theory $T$: $\text {Term}, \text {Ax}, \text {For}$ and so on.

Specifically, predicate $\text {Pr}_t$ is a binary predicate holding of numbers $a$ and $b$ iff $b$ is the number corresponding to a proof [a derivation in $T$] ending with formula $A$ and $a$ is the number corresponding to $A$, i.e. $a= \ulcorner A \urcorner$.

Then the author defines anew unary predicate: $\text {Thm}_T(a) \leftrightarrow \exists x\text {Pr}_T(a,x)$, that means: there is a proof [in $T$] of formula $A$, i.e. $A$ is a theorem of theory $T$.

Now, to say that a numerical (unary) predicate $P$ is representable in theory $\mathsf N$ means that there is a formula $A_P$ of the theory such that:

if $P(a)$ holds, then $\mathsf N \vdash A_P[k_a/x]$, where $k_a$ is the numeral corresponding to $a$, and

if $P(a)$ does not hold, then $\mathsf N \vdash \lnot A_P[k_a/x]$.

Now we have the condition that $\text {Thm}(a)$ is representable in $\mathsf N$.

This means that:

if $\text {Thm}(\ulcorner \varphi \urcorner)$ holds, i.e. $\mathsf N \vdash \varphi$, then $\mathsf N \vdash A_T[k_a/x]$,

where $a= \ulcorner \varphi \urcorner$.

The condition: if $\mathsf N \vdash \varphi$, then $\mathsf N \vdash A_T[k_a/x]$, is the first derivability condition.

But we have to note that the second clause of representability is: if $P(a)$ does not hold, then $\mathsf N \vdash \lnot A_P[k_a/x]$.

When we apply it to $\text {Thm}$ we have: if $\mathsf N \nvdash \varphi$, then $\mathsf N \vdash \lnot A_T[k_a/x]$ that is stronger than:

if $\mathsf N \nvdash \varphi$, then $\mathsf N \nvdash A_P[k_a/x]$.