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

Question

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?

Answer 1

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!).