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

  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. Jun 9, 2013 at 13:24
  • 1
    No the induction is over an ordering of finite proofs where the ordering is of order-type epsilon-zero. Jun 9, 2013 at 13:56
  • ok, all finite proofs are in bijection with the set of finite rooted trees, which has order-type epsilon-zero. Jun 9, 2013 at 15:51
  • 1
    @PeterSmith What is wrong with this proof that PA plus the omega rule is complete? m-phi.blogspot.com/2011/03/… Aug 4, 2013 at 2:21

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .