Wikipedia: Goedels Incompleteness Theorem/Talk

May I suggest that someone also writes another article on [Goedels Consistency Theorem]??

: Thanks a lot for the helpful hints! --AxelBoldt

(Regarding axiom of choice and continuum hypothesis)

[COMMENT: True enough, but not a very good example, for several reasons. That the axiom of choice is independent of the remaining axioms of set theory was generally assumed long before Gödel's theorem.]

: I took the axiom of choice out and left the continuum hypothesis in. Should we list another example? --AxelBoldt

COMMENT: Examples from set theory in general are a bit misleading, because Gödel's theorem is specifically about arithmetical statements. The theorem was not used at all in proving the independence of the continuum hypothesis. On the other hand, in recent decades much work has been done on finding combinatorial statements of ordinary mathematics that are undecidable in standard theories, beginning with a result by Paris and Harrington about the unprovability in PA of a version of the finite Ramsey theorem.

[COMMENT: So how is this relevant to Objectivism? Does Objectivism have the aim of proving all mathematical truths?]

I don't even know what Objectivism is :-) --AxelBoldt

: Objectivism is a philosophical system created by Ayn Rand. It is heavily based on the work of Aristotle. The two viewpoints are irreconcilable in terms of mathematics (see axiom 1 of the Objectivist page), but then Objectivism is as much a "framework for living" as anything else, and Goedel didn't directly address "self-esteem" in any of his work. - MB

(Regarding "stronger theory needed to prove consistency of some other theory")

[COMMENT: This does not at all follow. What follows is only that the consistency of T cannot be proved in T itself, not that it can only be proved in a stronger theory. As for "questionable", nothing in Gödel's theorem says anything about what is or is not questionable.]

: Ok, I removed "stronger" and "questionable". Please double check. --AxelBoldt

[COMMENT: Actually the proof applies to all extensions of a weak subtheory of Peano Arithmetic.]

: I don't know what that is. Any suggestion for improvements of my statement "the theory should be at least as strong as Peano's Axioms"? --AxelBoldt

COMMENT: The usual formula is "which includes a certain amount of arithmetic", which leaves the matter conveniently vague.

[COMMENT: What is meant by a "formally correct variant" of a paradox?]

: Deleted. --AxelBoldt

[COMMENT: Turing did not use Gödel's construction. He did use diagonalization, which was not Gödel's invention.]

: With "diagonalization", you basically mean the Barber's paradox?

: How about this: "In the proof, Gödel used a technique called diagonalization, which is a formalization of Barber's paradox and was used earlier by Russell to expose inconsistencies in naive set theory and later by Turing to solve the Entscheidungsproblem." --AxelBoldt

COMMENT: The diagonalization argument was introduced by Cantor, and is usually credited to him.

(Regarding the last sentence of the proof sketch:)

[COMMENT: This is not correct. The Godel sentence for T may be refutable in a consistent T. This is where Rosser's strengthening comes in.]

: Where did I cheat? How should the paragraph be improved without obscuring the central proof idea too much? --AxelBoldt

COMMENT: If the Gödel sentence G is refutable in T, T proves "there is a proof in T of G" but also proves "n is not a proof in T of G" for every n. Hence Gödel used the assumption that T is "omega-consistent", meaning that such a situation cannot arise.

Now comes the trick: a statement form F(x) is called self-false if F(G(F)), i.e. the form F applied to its own Gödel number, is not provable. This concept can be defined formally, and therefore we can construct a statement form SF(x) which embodies the concept: SF(x) is provable if and only if x is the Gödel number of a self-false statement form. Then define the statement p = SF(G(SF)). This is the statement p that was mentioned above. [COMMENT: This is not a correct characterization of the Gödel formula. The suggestion seems to be that the Gödel sentence is a fixed point of "x is self-false", but this is incoherent, since the Gödel sentence has no free variable. The Gödel sentence, rather, is a fixed point of "x is not provable". Also note that the Gödel sentence, which is equivalent in T to "T is consistent", may be refutable in T even if T is consistent.]

: No, p says that "the property of being self-false, i.e. the statement form SF(x), is itself self-false", or short: p = SF(G(SF)). This sentence p is in fact a fixed point of "x is not provable" (and the most direct way to construct such a fixed point). --AxelBoldt

COMMENT: Yes, you're right, I quite missed that this was an alternative description of Gödel's own construction.

[COMMENT: this assumption is insufficient to support the conclusion that the negation of the Godel statement is not provable.]

: Yes, we really need ω-consistency, but I didn't want to interrupt the flow of the proof sketch. A remark earlier in sketch says that there are technical difficulties and that omega-consistency is the key word to look for in Goedel's and Rosser's work.

Suggestions: 1. "sufficiently complex to allow one to do basic mathematics" - much better to replace "mathematics" with "arithmetics" here, it's clearer to a layman reader, more precise, and closer to the technical truth. 2. Presenting the second incompleteness theorem as merely a "consequence" of the first seems wrong to me. Much better to explicitly explain that there are in fact TWO theorems, that "Goedel's incompleteness theorem" usually refers to the first theorem, and that the second theorem works by by formalising the first theorem in its own stead inside an axiomatic system. -- AV

: I agree with both points. Do you want to go ahead and make the changes? --AxelBoldt

-- I'll make the first, simple suggestion; no time now to rewrite the whole article to conform to the second suggestion. If noone else does it, I'll come back to this in a day or two and will rewrite. -- AV