Re: Gödel's theorems in Wikipedia

Chris Menzel wrote:
Gödel's theorems are theorems in first-order logic, and must ultimately be understood in that context.

That's wrong, of course.  The theorems apply to any extension of basic
arithmetic, including higher-order logic.  Indeed, the theorems were
originally proved relative to the higher-order logic of Principia
Mathematica.

That reminds me of something. I've never actually studied Gentzen's original consistency proof, but I'm fairly certain that the fact that only quantifier free induction is needed was pointed out later by Kreisel. I didn't mention this because I thought it was more important to provide current technical information than precise historical accounts. Perhaps people here have an opinion on whether this is the correct choice.

Anyhow, what do you think, should the section on Gentzen's theorem include a proof sketch using infinitary derivations (omega-logic) a la Schütte? Or would it simply needlessly confuse people?

--
Aatu Koskensilta (aatu.koskensilta@xxxxxxxxx)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
.

Relevant Pages

  • Re: Metamathematically True or False?
    ... about the standard model, ... > of completeness the completeness theorem is automatically relevant. ... > sigma-1-complete if it's an extension of Q, ... >> are NOT theorems of Q! ...
    (sci.logic)
  • Re: Contradiction or paradox
    ... extension to Godel's theorems published." ... the question is moot. ... What is shorter and simpler than "If the logic is consistent and ...
    (sci.logic)
  • Re: Hessian, Eigenvalue criterion to find extrema
    ... want to apply theorems of calculus, D *is* a subset of R^n. ... one of your books. ... What is the context (i.e., what is the course material about up to ...
    (sci.math)
  • Re: Contradiction or paradox
    ... "is used to derive the shortest, simplest proof of Rosser's ... extension to Godel's theorems published." ...
    (sci.logic)