Simple yet Profound Metatheorem
in [Logic]
|
Prev: Obections to Cantor's Theory (Wikipedia article)
Next: Why Has None of Computer Science been Formalized?
From: H. J. Sander Bruggink on 16 Dec 2005 10:02 sradhakr wrote: > H. J. Sander Bruggink wrote: >>Fine, show me that proof of P&~P, then. No answer? >>>In other words, the claimed proof shows that from the hypothesis P&~P >>>one can conclude ~(P&~P). But from the hypothesis P&~P one can conclude >>>any proposition, so what is the basis for the claimed proof? >> >>Yes, for any proposition Q, you can prove (P&~P) -> Q. >>What's your point? >> > > That therefore no valid proof of ~(P&~P) should start with the > hypothesis P&~P. Understand this point before you hit the keyboard > again. Please provide that proof of P&~P before *you* hit the keyboard again. I keep asking you, because I am confident that you'll see your own error if you'd only try. Hint: you'll probably come up with a proof of [A] (P&~P) -> (P&~P), rather than a proof of [B] P&~P [A] is valid, of course, but [B] isn't. groente -- Sander
From: G. Frege on 16 Dec 2005 10:22 On 16 Dec 2005 05:56:11 -0800, "sradhakr" <sradhakr(a)in.ibm.com> wrote: >>> >>> That is precisely the point of my objection. If the claimed "proof" >>> of ~(P&~P) is allowed to go through, then just about any proposition, >>> including P&~P should also be provable. >>> "Unproven statements carry little weight in the world of mathematics." - Amir D. Aczel >> >> ...show me that proof of P&~P, then. >> Please do it! :-) >>> >>> In other words, the claimed proof shows that from the hypothesis P&~P >>> one can conclude ~(P&~P). But from the hypothesis P&~P one can conclude >>> any proposition, so what is the basis for the claimed proof? >>> The basis (or a core component) is the rule ~I ("RAA"). (~I) [A] : _|_ ----- ~A (Note that the assumption A is "discharged" by the application of the rule. This is denoted in by "[ ]" here.) Here's a variant of the given proof in Gentzen's original calculus of natural deduction for intuitionistic logic (NJ): (1) (1) P & ~P P & ~P ------ &E ------ &E P ~P ---------------- ~E _|_ --------- ~I (1) ~(P & ~P) Hence: |- ~(P & ~P). Now... >> >> ...for any proposition Q, you can prove (P&~P) -> Q. >> Proof (again in Gentzen's system): (1) (1) P & ~P P & ~P ------ &E ------ &E P ~P ---------------- ~E _|_ ----- (absurdity rule) Q -------------- ->I (1) (P & ~P) -> Q So... >> >> ...what's your point? >> > That therefore no valid proof of ~(P&~P) should start with the > hypothesis P&~P. Understand this point before you hit the keyboard > again. > It seems that you are not very familiar with systems/calculi of natural deduction: there you may start with *any* _assumption_ (as long as it's a wff of the system). Please take charge of this deplorable state of affairs "before you hit the keyboard again". F. -- "I do tend to feel Hughes & Cresswell is a more authoritative source than you." (D. Ullrich)
From: G. Frege on 16 Dec 2005 10:26 On Fri, 16 Dec 2005 21:52:27 +1300, Barb Knox <see(a)sig.below> wrote: > > OK, here's a Fitch-style Intuitionistic ND proof: > > 1. | P ^ ~P A > |------- > 2. | P 1 ^E > 3. | ~P 1 ^E > 4. ~(P ^ ~P) 1,2,3 RAA > This is... > > ...a perfectly valid Intuitionistic proof. > Right. F. -- "I do tend to feel Hughes & Cresswell is a more authoritative source than you." (D. Ullrich)
From: Torkel Franzen on 16 Dec 2005 10:37 "sradhakr" <sradhakr(a)in.ibm.com> writes: > But what, precisely, is the "absurdity" that you deduce > from P&~P, in order to conclude ~(P&~P) in the claimed proof? P and ~P. > The fact > that you can deduce an arbitrary proposition from P&~P? Completely irrelevant, since we deduce ~(P&~P) without assuming any such fact.
From: sradhakr on 16 Dec 2005 10:48
G. Frege wrote: > On 16 Dec 2005 05:56:11 -0800, "sradhakr" <sradhakr(a)in.ibm.com> wrote: > > > >>> > >>> That is precisely the point of my objection. If the claimed "proof" > >>> of ~(P&~P) is allowed to go through, then just about any proposition, > >>> including P&~P should also be provable. > >>> > > "Unproven statements carry little weight in the world of > mathematics." - Amir D. Aczel > > >> > >> ...show me that proof of P&~P, then. > >> > > Please do it! :-) > > >>> > >>> In other words, the claimed proof shows that from the hypothesis P&~P > >>> one can conclude ~(P&~P). But from the hypothesis P&~P one can conclude > >>> any proposition, so what is the basis for the claimed proof? > >>> > The basis (or a core component) is the rule ~I ("RAA"). > > (~I) > [A] > : > _|_ > ----- > ~A > > (Note that the assumption A is "discharged" by the application of > the rule. This is denoted in by "[ ]" here.) > > Here's a variant of the given proof in Gentzen's original calculus of > natural deduction for intuitionistic logic (NJ): > > (1) (1) > P & ~P P & ~P > ------ &E ------ &E > P ~P > ---------------- ~E > _|_ > --------- ~I (1) > ~(P & ~P) > > Hence: > > |- ~(P & ~P). > > Now... > >> > >> ...for any proposition Q, you can prove (P&~P) -> Q. > >> > > Proof (again in Gentzen's system): > > (1) (1) > P & ~P P & ~P > ------ &E ------ &E > P ~P > ---------------- ~E > _|_ > ----- (absurdity rule) > Q > -------------- ->I (1) > (P & ~P) -> Q > > So... > >> > >> ...what's your point? > >> > > That therefore no valid proof of ~(P&~P) should start with the > > hypothesis P&~P. Understand this point before you hit the keyboard > > again. > > > It seems that you are not very familiar with systems/calculi of > natural deduction: there you may start with *any* _assumption_ > (as long as it's a wff of the system). > > Please take charge of this deplorable state of affairs "before you hit > the keyboard again". > > My dear "G. Frege", You are very good at parrotting the status quo and loudly proclaiming its validity. But I am asking you to *use your own brain* and think about what you have written above. See my reply to Torkel Franzen to understand what my problem is. In short, what does the "absurdity" or "_|_" stand for in your "proof" of ~(P&~P)? The fact that you can deduce an arbitrary proposition from P&~P? If you refuse to explain what _|_ is, you have done little more than a bald assertion of ~(P&~P), without proof. If _|_ means that "An arbitrary proposition Q follows" (from the truth of P&~P), then you have used EFQ and your "proof" becomes indistinguishable from one in which you *subsititute* ~(P&~P) for _|_ ( or more precisely the proposition Q that _|_ entails). i.e., what you are saying is, _|_ follows, so any propoisition Q follows, and in particular, ~(P&~P) follows. Regards, RS. |