Comment by gphilip | Hacker News Reader

Comment by gphilip | Hacker News Reader

Parent Full thread

> In the first paragraph, he shows that if you allow proofs by contradiction, you can use them for every theory claimed to be inconsistent to show it indeed is consistent. This is so, because to prove by contradiction means to infer "not A" if from "A" follows "B" and "not B". So, if from "mathematics is inconsistent" follows "theorem A is true" and "theorem A is false", it follows that "mathematics is consistent". He claims that this shows consistency isn't rigorously proved in classical mathematics but is just assumed, since classical mathematics allows proofs by contradiction.

So the first paragraph is about showing that if one allows statements about mathematics (e.g: "Mathematics is consistent") and statements in mathematics (e.g: "proposition A is true", for some statement A which can be expressed entirely "within" mathematics) to freely mix together on the same footing, then things become inconsistent? But this is well-known for over a century; see, e.g: Russell's Paradox [1]. And (if I understand it correctly), one doesn't need Proof by Contradiction for this inconsistency to occur---it suffices to allow meta-statements and "plain" statements to mix together; see Curry's Paradox [2]. And ways to work with metamathematical statements while avoiding this paradox where also worked out a long time back [3]. That the first paragraph of the OP mentions none of this seems ... surprising, to say the least.

[1] https://en.wikipedia.org/wiki/Russell's_paradox [2] https://en.wikipedia.org/wiki/Curry's_paradox [3] https://en.wikipedia.org/wiki/History_of_type_theory

This is just an abstract. I think the novelty he perceives is combining all this into a proof of consistency of mathematics. Page 6 of his paper mentions everything you have just written about:

https://docs.google.com/file/d/0B79uetkQ_hCKbkFpbFJQVFhvdU0/...

This guy spent a few decades working in mathematical logic. He might overestimate the importance of some things, but I would be careful assuming he suddenly stopped understanding simple technical arguments.

He mentions those in relation to his own pet theories but in no way does he address GP's argument.

What his theorem boils down to is:

1. Let A be a formal system capable of describing the natural numbers. 2. Assume A is inconsistent. It follows that there exists such Φ that A ⊢ Φ and A ⊢ ¬Φ 3. ????? 4. A is consistent!

At step 3. he appears to conflate A⊢Φ ∧ A⊢¬Φ with Φ∧¬Φ and use it to refute the assumption in 2. But Φ∧¬Φ is not generally true outside the context of A and therefore the refutation does not follow.

My understanding is that if proof by contradiction is allowed in A, Φ ∨ ¬Φ is a true sentence in A, so if you try to include the sentence "A is inconsistent" in A, it follows that A ⊢ Φ and A ⊢ ¬Φ, therefore in A Φ ∧ ¬Φ is true, but this contradicts Φ ∨ ¬Φ, therefore A is consistent. In other words, it is impossible to show the inconsistency of any system that includes the law of excluded middle.

This is really trivial in the end. Inconsistency is "Φ ∧ ¬Φ", law of excluded middle is "Φ ∨ ¬Φ", so in the assumption of law of excluded middle is hidden the assumption of consistency. That's what he means by

The above theorem means that the assumption of consistency is deeply embedded in the structure of classical mathematics

Edit: I agree with you in the end, the proof is valid, but the conclusion does not hold in A, but one "level" above, so it does not contradict Goedels theorem. Am I reading this right?

Reply on news.ycombinator.com