Let "provability formula" ${\rm Prf}(x, y)$ written in the manner that provability operator $\square A$ defined as $\exists x\ {\rm Prf}(x, \overline A)$ satisfying Hilbert–Bernays axioms:

  1. If ZF $\vdash A$ then ZF $\vdash \square A$.

  2. ZF $\vdash \square A \to \square \square A$.

  3. ZF $\vdash (\square A \land \square (A \to B) \to \square B)$.

From here I have to prove Goedel's Theorem, i.e. ZF $\vdash (\square \neg \square \perp \to \square \perp)$. Here $\perp$ is some contradiction, for example $(\Phi \land \neg \Phi)$.

Usually implications can be derived using deduction lemma. But here I'm little bit confused. Or maybe I understand "prove" incorrectly, i.e. it is not derivation?

  • $\begingroup$ Presumably, you need to start with a diagonal sentence. Perhaps: $A\leftrightarrow (\Box A \to \bot)$. $\endgroup$ – GME Apr 22 '15 at 20:28

Assume that $T$ satisfies the Hilbert-Bernays conditions and that:

$T\vdash A \leftrightarrow (\Box A \to \bot)$

for some sentence $A$. Call this the diagonal sentence.

By the first and third conditions it follows that:

$T\vdash\Box A \to \Box(\Box A \to \bot)$

and thus by another application of the third condition:

$T\vdash\Box A \to (\Box\Box A \to \Box \bot)$

By the second condition we then get:

$T\vdash\Box A \to (\Box A \to \Box\bot)$

and thus:

$T\vdash\Box A \to \Box \bot$

Contraposition, the first and third condition then yield:

$T\vdash\Box\neg\Box\bot \to \Box\neg \Box A$

If we can show that $T\vdash\Box\neg\Box A \to \Box A$, then we'd be done. But the diagonal sentence can also be written:

$T\vdash A\leftrightarrow \neg\Box A$


$T\vdash\neg \Box A \to A$

We can then apply the first and third conditions again to get $T\vdash\Box\neg\Box A \to \Box A$ as required.

  • $\begingroup$ I'm sorry, but for me it is unclear how you applying first and then third conditions. As I understood, from $A \to B$ you can always derive $\square A \ \to \square B$. Can you show this please? $\endgroup$ – Jihad Apr 23 '15 at 7:43
  • $\begingroup$ Sure. So if $T\vdash A \to B$, then $T\vdash \Box(A \to B)$ by the first condition. Condition 3 can be re-written as $T\vdash \Box(A \to B) \to (\Box A \to \Box B)$. So it follows that $T\vdash \Box A \to \Box B$. $\endgroup$ – GME Apr 23 '15 at 8:36
  • $\begingroup$ Why is there a diagonal sentence in ZF? $\endgroup$ – Jihad Apr 23 '15 at 16:26
  • $\begingroup$ en.wikipedia.org/wiki/Diagonal_lemma $\endgroup$ – GME Apr 23 '15 at 16:59
  • $\begingroup$ It seems too hard. This problem assume proof without diagonal lemma. $\endgroup$ – Jihad Apr 23 '15 at 20:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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