: (by construction of and theorem 1) (by ω-consistency) Thus proves both and . But if is consistent, this is impossible, and we are forced to conclude that does not prove . To conclude, can prove neither nor . 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 . We then would have the following theorems in : (by construction of and theorem 1) (by theorem 2 and the additional condition following the definition of Rosser's provability predicate) (by condition no. 1 and theorem 1) Thus proves both and . But if is consistent, this is impossible, and we are forced to conclude that does not prove . The second theorem We assume that proves its own consistency, i.e. that: . For every formula : (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: And using proving its own consistency it follows that: We now use this to show that is not consistent: (following proving its own consistency, with ) (by construction of ) (by condition no. 1 and theorem 2) (by condition no. 3 and theorem 3) (by theorems 1 and 4) (by condition no. 2) (by theorems 5 and 6) (by construction of ) (by theorems 7 and 8) (by condition 1 and theorem 9) Thus proves both and , hence is inconsistent. References Smith, Peter (2007). An introduction to Gödel's incompleteness theorems. Cambridge University Press. Mathematical logic Provability logic