# Hilbert–Bernays provability conditions

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?

• Presumably, you need to start with a diagonal sentence. Perhaps: $A\leftrightarrow (\Box A \to \bot)$. – 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$

Thus:

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

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