Relative consistency : "T proves F" VS "arithemic proves that T proves F" This is related to my previous question. The thing was to show : 
$ZF \vdash \neg Con(ZF + AF) \longrightarrow \neg Con(ZF)$
If $ZF + AF$ is inconsistant then there is a finite number of $ZF + AF$ axioms, $\psi_1,\dots,\psi_n$ such as $\psi_1 \wedge \dots \wedge \psi_n \longrightarrow \phi \wedge \neg \phi$
We know that we have a model $WF$ such as for all $ZF+AF$ axioms, $F$, we can write 
$ZF \vdash F^{WF}$
So $ZF \vdash \psi_1^{WF} \wedge \dots \wedge \psi_n^{WF}$
So $ZF \vdash \phi^{WF} \wedge \neg \phi^{WF}$
So $ZF \vdash \neg Con(ZF)$
My problem is that I wonder if somehow, we didn't do something weaker than $ZF \vdash \neg Con(ZF + AF) \longrightarrow \neg Con(ZF)$.
Indeed, if $ZF \vdash \phi \wedge \neg \phi$ then $ZF \vdash \neg Con(ZF)$ (in fact even $Peano \vdash \neg Con(ZF)$). 
But why $ZF \vdash \neg Con(ZF+AF)$ would imply that $ZF+AF \vdash \phi \wedge \neg \phi$ ?
Couldn't the demonstration be non standard ?
Thanks in advance to anyone who has some clue...
 A: I am not sure I understand the question. The way you phrase it is a bit confusing. Nevertheless this is the answer to what I think that you are asking:
It can be proved that if we have a recursively enumerable set of natural numbers $X$ then there exists a formula $\phi$ of the language of Peano arithmetic such that: 
$$PA\vdash\phi(\bar{m}) \iff m\in X$$
This is essentially what is used to prove the first incompleteness theorem since the set of the consequences of PA is recursively enumerable (here I used $\bar{m}$ to denote the element $m$ in the language of PA). 
Of course we can prove something similar in a theory stronger than PA like ZF or ZF+AF (or any other theory that extends PA as long as it's axiomatic). For such a theory (let's call it $T$) since its consequences are recursively enumerable we have that: 
$$T\vdash\phi\iff T\vdash Pr(\ulcorner\phi\urcorner)$$
If we can prove something in ZF we can of course prove it in ZF+AF. Since the consistency is a statement about the provability of a contradiction it is immediate that the contradiction is provable.
What this says essentially is that we cannot prove the existence of a proof of a contradiction without being able to prove the contradiction. Or we can say that a non-standard demonstration is not demonstratable.
P.S.: If I misinterpreted the question please let me know what it is you are looking for.
