# What happens when we drop the condition that proofs are finite strings of inferences in Gödel's incompleteness theorem?

Gödel's incompleteness theorem shows that there are sentences that are undecideable, that is they nor their negation can be proved.

This theorem operates purely syntactically or formally, that it doesn't use a model. No semantics are involved.

Now a formal proof is a finite string of inferences. What happens if this condition is dropped - that is use an infinite number of inferences? To make sense of this one has to use a theory of the infinite, because the inferences are ordered one should use the ordinal theory and not the cardinal.

Is there an infinite ordinal for which all sentences become decidable?

Is this essentially how Gentzen's proof of the consistency of PA works - which can only mean that all sentences are decidable?

What can this mean when proofs are actually finite inferences?

## 1 Answer

1. If you allow infinitary rules like the omega-rule, more becomes provable so PA plus the omega-rule proves the Gödel-sentence for PA. But PA plus the omega-rule still isn't complete -- a result that goes back to Rosser's 1937 JSL paper on Gödel theorems for non-constructive logics. Dan Isaacson's paper on the omega rule might be helpful here: "Some considerations on arithmetical truth and the ω-rule", in Michael Detlefsen (ed.), Proof, Logic and Formalization, Routledge, London, 1991, pp. 94-138.

2. Gentzen's proof of the consistency of PA is done in a framework which assumes a certain amount of transfinite induction (more transfinite induction that is available via coding within PA itself). But proofs by transfinite induction are still finite strings of sentences (consider such proofs in ZF, for example!).

• Proofs by transinfinite induction I agree can be finite. But if Gentzen was doing this over the length of proofs in PA - which I assume he was as I can't see anything else to carry the induction over - then what does that mean? Not the meta-proof but the proof inducted. – Mozibur Ullah Jun 9 '13 at 13:24
• No the induction is over an ordering of finite proofs where the ordering is of order-type epsilon-zero. – Peter Smith Jun 9 '13 at 13:56
• ok, all finite proofs are in bijection with the set of finite rooted trees, which has order-type epsilon-zero. – Mozibur Ullah Jun 9 '13 at 15:51
• @PeterSmith What is wrong with this proof that PA plus the omega rule is complete? m-phi.blogspot.com/2011/03/… – Keshav Srinivasan Aug 4 '13 at 2:21