# 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...

-

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.

-
hum... Indeed, if what you say if true, my question does not really make sence... I was sure that $T \vdash \phi \leftarrow PA \vdash Pr_T(\ulcorner \phi \urcorner)$ was not true. But now that you explain it, it seems perfectly true to me. Indeed we can always take a standard model for PA and then we can always have a standard proof. This is weird, I read something different 'in Handbook of mathematical logic'. But I probably misunderstood. Thanks a lot anyway. I think I need some rest now :) – Archimondain Mar 23 '11 at 19:38
@Archimondain: What isn't true is $PA\vdash Pr(\phi)\to\phi$. – Apostolos Mar 23 '11 at 19:58
But we should have $PA \vdash Pr_T(\phi) \longrightarrow (\psi_1 \wedge \dots \wedge \psi_n \longrightarrow \phi)$ for some $\psi_1$... $\psi_n$, right ? – Archimondain Mar 24 '11 at 10:59
@Archimondain: $\psi\land\lnot\psi\to\phi$ is a tautology so what you are asking is trivially true. Though I suspect that again you are asking something else. The point is this: Inside the model or the system we cannot decide if there exist non-standard elements. But our metamathematical world is assumed standard. This is why we can prove outside of the system that the proof of the provability of $\phi$ exists exactly when there exists a proof of $\phi$. – Apostolos Mar 24 '11 at 12:13
Lol, of course I was asking for some $\psi_1 \dots \psi_n \in T$, corresponding to axioms used in the finite proof of $\phi$. Indeed you have $(PA \vdash Pr_T(\phi)) \rightarrow (\vdash \psi_1 \wedge \dots \wedge \psi_n \rightarrow \phi)$, but do you have $(PA \vdash Pr_T(\phi) \rightarrow (\psi_1 \wedge \dots \wedge \psi_n \rightarrow \phi))$ ? – Archimondain Mar 24 '11 at 13:00