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 be a formal theory of arithmetic with a formalized provability predicate , which is expressed as a formula of with one free number variable. For each formula in the theory, let be the Gödel number of . The Hilbert–Bernays  provability conditions are: Note that Prov is predicate of numbers, and it is a provability predicate in the sense that the intended interpretation of Prov(#(φ)) is that there exists a number that codes for a proof of φ. Formally what is required of Prov is the above three conditions. 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 formula_1 such that formula_2. Proving Godel's first incompleteness theorem. For the first theorem only the first and third conditions are needed. The condition that is ω-consistent is generalized by the condition that if for every formula , if proves , then proves . Note that this indeed holds for an -consistent because means that there is a number coding for the proof of , and if is -consistent then going through all natural numbers one can actually find such a particular number , and then  one can use to construct an actual proof of in . Suppose T could have proven formula_1. We then would have the following theorems in : Thus proves both formula_8 and formula_9. But if is consistent, this is impossible, and we are forced to conclude that does not prove formula_1. Now let us suppose could have proven formula_11. We then would have the following theorems in : Thus proves both formula_1 and formula_11. But if is consistent, this is impossible, and we are forced to conclude that does not prove formula_11. To conclude, can prove neither formula_1 nor formula_11. Using Rosser's trick . Using Rosser's trick, one needs not assume that is -consistent. However, one would need to show that the first and third provability conditions holds for , Rosser's provability predicate, rather than for the naive provability predicate Prov. This follows from the fact that for every formula , holds if and only if holds. An additional condition used is that proves that implies . This condition holds for every that includes logic and very basic arithmetics (as elaborated in Rosser's trick#The Rosser sentence). Using Rosser's trick, 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 could have proven formula_11. We then would have the following theorems in : Thus proves both formula_27 and formula_28. But if is consistent, this is impossible, and we are forced to conclude that does not prove formula_11. The second theorem. We assume that proves its own consistency, i.e. that: For every formula : It is possible to show by using condition no. 1  on the latter theorem, followed by repeated use of condition no. 3, that: And using proving its own consistency it follows that: We now use this to show that is not consistent: Thus proves both formula_8 and formula_9, hence is inconsistent.