Hilbert–Bernays provability conditions

In mathematical logic, the Hilbert–Bernays provability conditions, named after David Hilbert and Paul Bernays, are a set of requirements for formalized provability predicates in formal theories of arithmetic (Smith 2007:224).

These conditions are used in many proofs of Kurt Gödel's second incompleteness theorem. They are also closely related to axioms of provability logic.

The conditions

Let Template:Math be a formal theory of arithmetic with a formalized provability predicate Template:Math, which is expressed as a formula of Template:Math with one free number variable. For each formula Template:Math in the theory, let Template:Math be the Gödel number of Template:Math. The Hilbert–Bernays provability conditions are:

1. If Template:Math proves a sentence Template:Math then Template:Math proves Template:Math.
2. For every sentence Template:Math, Template:Math proves Template:Math
3. Template:Math proves that Template:Math and Template:Math imply Template:Math

Note that Template:Math is predicate of numbers, and it is a provability predicate in the sense that the intended interpretation of Template:Math is that there exists a number that codes for a proof of Template:Math. Formally what is required of Template:Math is the above three conditions.

In the more concise notation of provability logic, letting $T⊢\phi$ denote "$T$ proves $\phi$" and $◻\phi$ denote $\text{Prov}(\mathrm{\#}(\phi ))$:

1. $(T⊢\phi )\to (T⊢◻\phi )$
2. $T⊢(◻\varphi \to ◻◻\varphi )$
3. $T⊢(◻(\phi \to \psi )\to ◻\phi \to ◻\psi )$

Use in proving Gödel's incompleteness theorems

The Hilbert–Bernays provability conditions, combined with the diagonal lemma, allow proving both of Gödel's incompleteness theorems shortly. Indeed the main effort of Godel's proofs lied in showing that these conditions (or equivalent ones) and the diagonal lemma hold for Peano arithmetics; once these are established the proof can be easily formalized.

Using the diagonal lemma, there is a formula $\rho$ such that $T⊩\rho \leftrightarrow \mathrm{\neg }Prov(\mathrm{\#}(\rho ))$.

Proving Godel's first incompleteness theorem

For the first theorem only the first and third conditions are needed.

The condition that Template:Math is ω-consistent is generalized by the condition that if for every formula Template:Math, if Template:Math proves Template:Math, then Template:Math proves Template:Math. Note that this indeed holds for an Template:Math-consistent Template:Math because Template:Math means that there is a number coding for the proof of Template:Math, and if Template:Math is Template:Math-consistent then going through all natural numbers one can actually find such a particular number Template:Math, and then one can use Template:Math to construct an actual proof of Template:Math in Template:Math.

Suppose T could have proven $\rho$. We then would have the following theorems in Template:Math:

1. $T⊩\rho$
2. $T⊩\mathrm{\neg }Prov(\mathrm{\#}(\rho ))$ (by construction of $\rho$ and theorem 1)
3. $T⊩Prov(\mathrm{\#}(\rho ))$ (by condition no. 1 and theorem 1)

Thus Template:Math proves both $Prov(\mathrm{\#}(\rho ))$ and $\mathrm{\neg }Prov(\mathrm{\#}(\rho ))$. But if Template:Math is consistent, this is impossible, and we are forced to conclude that Template:Math does not prove $\rho$.

Now let us suppose Template:Math could have proven $\mathrm{\neg }\rho$. We then would have the following theorems in Template:Math:

1. $T⊩\mathrm{\neg }\rho$
2. $T⊩Prov(\mathrm{\#}(\rho ))$ (by construction of $\rho$ and theorem 1)
3. $T⊩\rho$ (by ω-consistency)

Thus Template:Math proves both $\rho$ and $\mathrm{\neg }\rho$. But if Template:Math is consistent, this is impossible, and we are forced to conclude that Template:Math does not prove $\mathrm{\neg }\rho$.

To conclude, Template:Math can prove neither $\rho$ nor $\mathrm{\neg }\rho$.

Using Rosser's trick

Using Rosser's trick, one needs not assume that Template:Math is Template:Math-consistent. However, one would need to show that the first and third provability conditions holds for Template:Math, Rosser's provability predicate, rather than for the naive provability predicate Prov. This follows from the fact that for every formula Template:Math, Template:Math holds if and only if Template:Math holds.

An additional condition used is that Template:Math proves that Template:Math implies Template:Math. This condition holds for every Template:Math that includes logic and very basic arithmetics (as elaborated in Rosser's trick#The Rosser sentence).

Using Rosser's trick, Template:Math is defined using Rosser's provability predicate, instead of the naive provability predicate. The first part of the proof remains unchanged, except that the provability predicate is replaced with Rosser's provability predicate there, too.

The second part of the proof no longer uses ω-consistency, and is changed to the following:

Suppose Template:Math could have proven $\mathrm{\neg }\rho$. We then would have the following theorems in Template:Math:

1. $T⊩\mathrm{\neg }\rho$
2. $T⊩Pro{v}^R(\mathrm{\#}(\rho ))$ (by construction of $\rho$ and theorem 1)
3. $T⊩\mathrm{\neg }Pro{v}^R(\mathrm{\#}(\mathrm{\neg }\rho ))$ (by theorem 2 and the additional condition following the definition of Rosser's provability predicate)
4. $T⊩Pro{v}^R(\mathrm{\#}(\mathrm{\neg }\rho ))$ (by condition no. 1 and theorem 1)

Thus Template:Math proves both $Pro{v}^R(\mathrm{\#}(\mathrm{\neg }\rho ))$ and $\mathrm{\neg }Pro{v}^R(\mathrm{\#}(\mathrm{\neg }\rho ))$. But if Template:Math is consistent, this is impossible, and we are forced to conclude that Template:Math does not prove $\mathrm{\neg }\rho$.

The second theorem

We assume that Template:Math proves its own consistency, i.e. that:

$T⊩\mathrm{\neg }Prov(\mathrm{\#}(1=0))$.

For every formula Template:Math:

$T⊩\mathrm{\neg }\phi \to (\phi \to (1=0))$ (by negation elimination)

It is possible to show by using condition no. 1 on the latter theorem, followed by repeated use of condition no. 3, that:

$T⊩Prov(\mathrm{\#}(\mathrm{\neg }\phi ))\to (Prov(\mathrm{\#}(\phi ))\to Prov(\mathrm{\#}(1=0)))$

And using Template:Math proving its own consistency it follows that:

$T⊩Prov(\mathrm{\#}(\mathrm{\neg }\phi ))\to \mathrm{\neg }Prov(\mathrm{\#}(\phi ))$

We now use this to show that Template:Math is not consistent:

1. $T⊩Prov(\mathrm{\#}(\mathrm{\neg }Prov(\mathrm{\#}(\rho )))\to \mathrm{\neg }Prov(\mathrm{\#}(Prov(\mathrm{\#}(\rho )))$ (following Template:Math proving its own consistency, with $\phi =Prov(\mathrm{\#}(\rho ))$)
2. $T⊩\rho \to \mathrm{\neg }Prov(\mathrm{\#}(\rho ))$ (by construction of $\rho$)
3. $T⊩Prov(\mathrm{\#}(\rho \to \mathrm{\neg }Prov(\mathrm{\#}(\rho )))$ (by condition no. 1 and theorem 2)
4. $T⊩Prov(\mathrm{\#}(\rho ))\to Prov(\mathrm{\#}(\mathrm{\neg }Prov(\mathrm{\#}(\rho )))$ (by condition no. 3 and theorem 3)
5. $T⊩Prov(\mathrm{\#}(\rho ))\to \mathrm{\neg }Prov(\mathrm{\#}(Prov(\mathrm{\#}(\rho )))$ (by theorems 1 and 4)
6. $T⊩Prov(\mathrm{\#}(\rho ))\to Prov(\mathrm{\#}(Prov(\mathrm{\#}(\rho )))$ (by condition no. 2)
7. $T⊩\mathrm{\neg }Prov(\mathrm{\#}(\rho ))$ (by theorems 5 and 6)
8. $T⊩\mathrm{\neg }Prov(\mathrm{\#}(\rho ))\to \rho$ (by construction of $\rho$)
9. $T⊩\rho$ (by theorems 7 and 8)
10. $T⊩Prov(\mathrm{\#}(\rho ))$ (by condition 1 and theorem 9)

Thus Template:Math proves both $Prov(\mathrm{\#}(\rho ))$ and $\mathrm{\neg }Prov(\mathrm{\#}(\rho ))$, hence is Template:Math inconsistent.

References

• Smith, Peter (2007). An introduction to Gödel's incompleteness theorems. Cambridge University Press. Template:ISBN