4 ms·

Carl Hewitt isn't just some random crank, he is the author of PLANNER, a breakthrough programming language in the early AI days, that gave rise to Prolog later

by stiff 13y ago

Carl Hewitt isn't just some random crank, he is the author of PLANNER, a breakthrough programming language in the early AI days, that gave rise to Prolog later on. This is a pretty interesting paper and it doesn't claim any big breakthrough in the sense of invalidating any great mathematical result. I can try to explain what it is about, at least the beginning of the quoted fragment: 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. He then shows that from this consistency proof paradoxically follows the conclusion that mathematics is inconsistent, because this proof contradicts Goedel theorem "if mathematics is consistent, then it cannot infer its own consistency". He resolves the contradiction of Goedels proof by his proof by restricting the logical system in which they are done to exclude self-referential sentences. Then, and I think this is really the gist of this work of his, he goes on to describe an approach that tries to somehow reduce the bad impact of including inconsistencies in the logical system, instead of trying to completely eliminate inconsistencies, as it was the goal traditionally.

gphilip 13y ago
> 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 https://en.wikipedia.org/wiki/Russell's_paradox [2] https://en.wikipedia.org/wiki/Curry's_paradox https://en.wikipedia.org/wiki/Curry's_paradox [3] https://en.wikipedia.org/wiki/History_of_type_theory https://en.wikipedia.org/wiki/History_of_type_theory
- stiff 13y ago
  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/edit 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.
  - zepolud 13y ago
    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.
    - stiff 13y ago
      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?

by stiff 13y ago

gphilip 13y ago

> 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 https://en.wikipedia.org/wiki/Russell's_paradox [2] https://en.wikipedia.org/wiki/Curry's_paradox https://en.wikipedia.org/wiki/Curry's_paradox [3] https://en.wikipedia.org/wiki/History_of_type_theory https://en.wikipedia.org/wiki/History_of_type_theory

stiff 13y ago
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/edit 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.
- zepolud 13y ago
  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.
  - stiff 13y ago
    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?