Simple yet Profound Metatheorem
in [Logic]
|
Prev: Obections to Cantor's Theory (Wikipedia article)
Next: Why Has None of Computer Science been Formalized?
From: G. Frege on 16 Dec 2005 11:25 On 16 Dec 2005 07:48:29 -0800, "sradhakr" <sradhakr(a)in.ibm.com> wrote: > > My dear G. Frege, You are very good at parroting the status quo and > loudly proclaiming its validity. > So you suggest there's something WRONG with the status quo? :-) > > But I am asking you to *use your own brain* and think about what you > have written above. > Oh, I do. (Or at least I hope that I do. :-) > > See my reply to Torkel Franzen to understand what my problem is. > Actually, it seems pretty clear to me, what your problem is: You simply don't know what you are talking about! > > In short, what does the "absurdity" or "_|_" stand for in your proof > of ~(P&~P)? > Gentzen called it "the false statement". On the other hand, it's just a /primitive/ of our system (NJ). So don't worry about it. Actually, a l l we have to know about it from a "proof theoretic" point of view are the following /rules of derivation/: (~E) A ~A ------- _|_ (~I) [A] : _|_ ----- ~A (rule _|_) _|_ ----- A > > The fact that you can deduce an arbitrary proposition from P&~P? > Huh? (That is a consequence of rule _|_, so what?) > > If you refuse to explain what _|_ is, you have done little more than > a bald assertion of ~(P&~P), without proof. > It seems pretty clear to me that you don't know what you are talking about. (Do you k n o w the definition of /proof/ in logic?) [rest deleted] F. -- "I do tend to feel Hughes & Cresswell is a more authoritative source than you." (D. Ullrich)
From: G. Frege on 16 Dec 2005 11:33 On 16 Dec 2005 07:58:49 -0800, "sradhakr" <sradhakr(a)in.ibm.com> wrote: > > OK, so you refuse to explain what you mean by the "absurdity", or > "_|_" that is used in the claimed proof. > Sorry, but you seem to overlook the fact that "_|_" is nowhere used in the original proof (posted by Barb Knox): --------------------------------------------------------- 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 --------------------------------------------------------- F. -- "I do tend to feel Hughes & Cresswell is a more authoritative source than you." (D. Ullrich)
From: G. Frege on 16 Dec 2005 11:35 On Fri, 16 Dec 2005 16:02:48 +0100, "H. J. Sander Bruggink" <bruggink(a)phil.uu.nl> wrote: > > Please provide that proof of P&~P before *you* hit the > keyboard again. > Still waiting... ;-) F. -- "I do tend to feel Hughes & Cresswell is a more authoritative source than you." (D. Ullrich)
From: sradhakr on 16 Dec 2005 11:47 G. Frege wrote: > On 16 Dec 2005 07:48:29 -0800, "sradhakr" <sradhakr(a)in.ibm.com> wrote: > > > > > My dear G. Frege, You are very good at parroting the status quo and > > loudly proclaiming its validity. > > > So you suggest there's something WRONG with the status quo? :-) > YES. That is how progress is made, isn't it? But not due to people like you. > > > > But I am asking you to *use your own brain* and think about what you > > have written above. > > > Oh, I do. (Or at least I hope that I do. :-) > There does not seem to be any evidence of it. > > > > See my reply to Torkel Franzen to understand what my problem is. > > > Actually, it seems pretty clear to me, what your problem is: You > simply don't know what you are talking about! Bullshit. > > > > > In short, what does the "absurdity" or "_|_" stand for in your proof > > of ~(P&~P)? > > > Gentzen called it "the false statement". On the other hand, it's just > a /primitive/ of our system (NJ). So don't worry about it. ???????? Don't worry, be happy, seems to be your philosophy. Good for you , bot not for me.. I am *questioning* the claimed proof, and I require precise meanings. After all the very philosophy of intuitionism requires the concepts of "truth" and "proof" to be meaningful. > > Actually, a l l we have to know about it from a "proof theoretic" > point of view are the following /rules of derivation/: > > (~E) > A ~A > ------- > _|_ > > (~I) > [A] > : > _|_ > ----- > ~A > > (rule _|_) > > _|_ > ----- > A > > > > > The fact that you can deduce an arbitrary proposition from P&~P? > > > Huh? (That is a consequence of rule _|_, so what?) There are in fact intuitionistic systems where _|_ or the absurdity, means precisely what I have stated above. But even in the above system _|_ is unexplained. Note: I AM QUESTIONING THE SYSTEM, and not blindly following its dictats. This may be too much for you to understand and absorb, but let me try to explain. If the syetem lays down rules like the " _|_ rule" and asks me to blindly accept it, I will not do so. I will look for meanings, in the true spirit of intuitionistic proof. > > > > > If you refuse to explain what _|_ is, you have done little more than > > a bald assertion of ~(P&~P), without proof. > > > It seems pretty clear to me that you don't know what you are talking > about. (Do you k n o w the definition of /proof/ in logic?) What a joker. Actually I will admit that if you ask me to take a test right now in natural deduction, I will probably flunk it. That is because I now need an intermincable amount of time to complete each answer (I am now 48). But understanding logic is not just about absorbing the status quo. You have to use your God-given brain and think about what you are doing. That is where you lose out. > > [rest deleted] > > > F. > > -- > "I do tend to feel Hughes & Cresswell is a more authoritative > source than you." (D. Ullrich)
From: Daryl McCullough on 16 Dec 2005 11:35
sradhakr says... >OK, so you refuse to explain what you mean by the "absurdity", or " >_|_" that is used in the claimed proof. Then, as far as I am >concerened, all you have done is a bald assertion of ~(P&~P), without >proof. I'm not sure if this helps, but in some formalizations of logic, ~P is defined to be P -> _|_ Then the conclusion ~(P&~P) becomes (P & (P -> _|_)) -> _|_ which is just a special case of the more general rule (P & (P -> Q)) -> Q The special proposition _|_ is *defined* via the rule that for every proposition Q, we have _|_ -> Q This is all perfectly valid constructively. What is not valid constructively is ~(~P) -> P which written in terms of _|_ becomes ((P -> _|_) -> _|_) -> P That doesn't follow from the definition of _|_. An interesting axiom that is not valid constructively is Pierce's law: ((P -> Q) -> P) -> P Even though negation is not mentioned at all in Pierce's law, it is impossible to prove Pierce's law without using something equivalent to ~(~P) -> P. -- Daryl McCullough Ithaca, NY |