Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

share|cite|improve this question
up vote 2 down vote accepted

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.

share|cite|improve this answer
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.