A theory (r.e., extending ) is reflexive iff it proves the consistency of all its finite subtheories. It is essentially reflexive iff each r.e. extension is reflexive.
Then is essentially reflexive and therefore no consistent extension of is finitely axiomatizable. This is obtained by showing that, in spite of Tarski’s undefinability of truth theorem, there are (provably in ) –truth predicates for all .
We defined Rosser sentences and showed their undecidability. We also showed Löb’s theorem that if is an r.e. theory and , then . This gives another proof of the second incompleteness theorem.
Finally, we showed that the length of proofs of -sentences is not bounded by any recursive function: For any r.e. and consistent, and any recursive function , there is a -sentence provable in but such that any proof of in has length > .