From: Torkel Franzen Subject: Re: Has mathematics been proved inconsistent? Date: 02 Aug 2000 10:16:13 +0200 Newsgroups: sci.math Summary: [missing] Stephen Montgomery-Smith writes: > I tried to read the HTML document, but on my browser, I don't > think the symbols came out right. I couldn't follow the > argument. It's clear from the context that à is implication and ^ is conjunction, so the argument goes 1. p v p -> p (axiom of P and PM) 2. (~p -> p) -> p (equivalent periphrasis for 1) 3.Bew [R (q); q] -> ~Bew [R (q); q] (follows from the content of [R (q); q]), as Goedel notes on p. 175) 4.~Bew [R (q); q] -> ~Bew (~Bew [R (q); q]) (follows from content of [R (q); q]) [footnote6] 5. ~Bew [R (q); q] (by 2, 3 and substitution) 6. Bew (~Bew [R (q); q]) (by 5) 7. ~Bew (~Bew [R (q); q]) (by 5 and 4) 8. Bew (~Bew [R (q); q]) & ~Bew (~Bew [R (q); q]) (by 6 and 7) Here [R(q);q] (Godel's notation) denotes the formula obtained by substituting the numeral corresponding to the number q for the variable in the q:th formula in an enumeration of all formulas with one free variable, and Bew(x) is the provability predicate. It is presupposed in the argument that q has been chosen so that R(q) is ~Bew([R(x);x]). The mistake in the argument consists in a natural and common confusion. ============================================================================== From: lerma@math.nwu.edu (Miguel A. Lerma) Subject: Re: Has mathematics been proved inconsistent? Date: 2 Aug 2000 14:25:26 GMT Newsgroups: sci.math Torkel Franzen (torkel@sm.luth.se) wrote: : Stephen Montgomery-Smith writes: : : > I tried to read the HTML document, but on my browser, I don't : > think the symbols came out right. I couldn't follow the : > argument. : : It's clear from the context that à is implication and ^ is : conjunction, so the argument goes : : 1. p v p -> p (axiom of P and PM) : : 2. (~p -> p) -> p (equivalent periphrasis for 1) : : 3.Bew [R (q); q] -> ~Bew [R (q); q] : (follows from the content of [R (q); q]), as Goedel notes on p. 175) I think the first mistake is here - note that the statement in line 3 is logically equivalent to ~Bew [R (q); q] (which is precisely Goedel's undecidable sentence). If the purpose is to prove that PM (or P) is inconsistent, it is necessary to prove that 3 is derivable from PM. But claiming that 3 "follows from the content of [R (q); q]" is just a metamathematical consideration, not a formal derivation. In a sense the author is confusing "metamathematically known to be true" with "derivable in the system". : 4.~Bew [R (q); q] -> ~Bew (~Bew [R (q); q]) : (follows from content of [R (q); q]) [footnote6] : : 5. ~Bew [R (q); q] (by 2, 3 and substitution) : : 6. Bew (~Bew [R (q); q]) (by 5) : : 7. ~Bew (~Bew [R (q); q]) (by 5 and 4) : : 8. Bew (~Bew [R (q); q]) & ~Bew (~Bew [R (q); q]) (by 6 and 7) : : : Here [R(q);q] (Godel's notation) denotes the formula obtained by : substituting the numeral corresponding to the number q for the : variable in the q:th formula in an enumeration of all formulas with : one free variable, and Bew(x) is the provability predicate. It is : presupposed in the argument that q has been chosen so that R(q) : is ~Bew([R(x);x]). Miguel A. Lerma ============================================================================== From: Torkel Franzen Subject: Re: Has mathematics been proved inconsistent? Date: 02 Aug 2000 20:27:00 +0200 Newsgroups: sci.math lerma@math.nwu.edu (Miguel A. Lerma) writes: > If the purpose is to prove that PM (or P) is inconsistent, it is > necessary to prove that 3 is derivable from PM. But claiming that > 3 "follows from the content of [R (q); q]" is just a metamathematical > consideration, not a formal derivation. In a sense the author is > confusing "metamathematically known to be true" with "derivable in > the system". You're right that the mistake lies in not distinguishing between what is shown to be provable in the theory and what is shown to follow from the assumption that the theory is sound. And indeed it is only because of Godel's theorem that we have come to appreciate this distinction.