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$
    – user104955
    Commented Apr 22, 2015 at 20:28

1 Answer 1


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
    Commented Apr 23, 2015 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$
    – user104955
    Commented Apr 23, 2015 at 8:36
  • $\begingroup$ Why is there a diagonal sentence in ZF? $\endgroup$
    – Jihad
    Commented Apr 23, 2015 at 16:26
  • $\begingroup$ en.wikipedia.org/wiki/Diagonal_lemma $\endgroup$
    – user104955
    Commented Apr 23, 2015 at 16:59
  • $\begingroup$ It seems too hard. This problem assume proof without diagonal lemma. $\endgroup$
    – Jihad
    Commented Apr 23, 2015 at 20:16

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .