Simple yet Profound Metatheorem
in [Logic]
|
Prev: Obections to Cantor's Theory (Wikipedia article)
Next: Why Has None of Computer Science been Formalized?
From: Charlie-Boo on 4 Jan 2006 22:29 H. J. Sander Bruggink wrote: > Charlie-Boo wrote: > > > Thanks. These endless variations in syntax not only gain you nothing, > > they do even less than simple case analysis. > > Aah, so you think that logics that prove more theorems > are always better? In that case, I suggest you look into > logics known as "inconsistent logics", because you can > prove anything you want in those logics. Case analysis does not prove anything that would deem the system inconsistent. C-B > > And still the idiots try to defend it. LOL > > And still those idiots try to defend classical logic. > LOL. (You can't even prove P & ~P in that!) :-) Yes, idiots abound. > groente > -- Sander
From: Charlie-Boo on 5 Jan 2006 22:03 H. J. Sander Bruggink & Charlie-Boo wrote: > > You are attacking the messenger.I will not be dragged into that. > What are you the messenger of, then? That Frege is wasting his time by endlessly proving propositional calculus wffs and should try something new and nontrivial like formalizing Smullyan's hundreds of theorems like I do. BTW Do you realize that almost all of Mathematical Logic can be reduced by an order of magnitide by expressing it in computability terms? (Occam's Razor) Corollary Message: Academia is Stupid! Shows you what inbreeding gets you. > > (Actually, I usually use > > mathworld.) > > Ok, mathworld is fine. Wolfram is nice to me when we hang out in Boston. (He likes skunk.) > >>Yes, you even explicitly > >>denied that you were talking about *classical* propositional > >>logic, what you said was WRONG. > So "~(A<->~A) is a propositional calculus wff" is wrong? > (I never used the word "classical".) > > C-B > [/quote] I didn't deny that it was classical. I denied that I used the word "classical". (I naturally denied the lesser statement.) > groente > -- Sander
From: Barb Knox on 6 Jan 2006 22:16 In article <1134682648.760706.220660(a)g43g2000cwa.googlegroups.com>, "Charlie-Boo" <chvol(a)aol.com> wrote: >Barb Knox wrote: > >> OK then, using some modal logic for provability and a more-common >> logical notation, you're claiming: >> (*) (P <-> []Q) -> [](P <-> Q). > >Yes, but I use the standard symbol |- for provable instead of box []. Maybe "standard" for you, but as others have pointed out, you appear to be importing meta-level notations (|-) into the object level, which just doesn't make sense. >> Letting P be []Q, this implies: >> (1) ([]Q <-> []Q) -> []([]Q <-> Q), i.e. >> []([]Q <-> Q). > >> This is false in any system where provability is different from truth. > >No. It isn't []Q <-> Q. It's []([]Q < - >Q) What are you disagreeing with? I wrote []([]Q <-> Q). Of course, in S4 model logic, []P->P, so you also get []Q<->Q. >> And indeed, []([]Q -> Q) says the system can prove its own consistency, >> which means (via Goedel) that it either is in fact inconsistent or is >> weaker than arithmetic. > >This seems valid. I really need only the "hint": that P = |-P. But it doesn't. In S4, []P->P and []P->[][]P, but it is NOT the case that P->[]P. Truth does not in general imply provability. >Since that means (|-P)=(|-Q) I thought that would imply |-(P=Q) but >maybe not. Do you agree that P = |-P ? No, as above. >This is what I use to derive >Incompleteness results from any Theory of Computation theorem of the >form "(relation) is / isn't recursively enumerable." > >> If you want provability and truth to be the same, > >Only for P! What is that supposed to mean? "P" is a propositional variable, so you're saying "only for everything". >C-B > >> you can dispense with >> all the modal machinery and just use some existing well-thought-out >> constructive logic (e.g. Intuitionistic). I still think this is good advice if you're in fact interested in systems where truth and proveability are the same. >> >C-B >> > >> >> > (P and Q have the same sets of free variables.) This simple theorem (I >> >> > created 12/1/05) provides the link between Theory of Computation and >> >> > Proof Theory (Incompleteness in Logic) that theoreticians such as >> >> > myself have been looking for since the 1930's. (Each Theory of >> >> > Computation theorem becomes an Incompleteness theorem in Logic, >> >> > providing almost trivial formal derivation of the exact results of >> >> > Godel, Rosser and Smullyan.) >> >> > >> >> > C-B >> >> > >> >> > Hint: Consider the equivalent ( P = |-Q ) => ( P = |- P ) -- --------------------------- | BBB b \ Barbara at LivingHistory stop co stop uk | B B aa rrr b | | BBB a a r bbb | Quidquid latine dictum sit, | B B a a r b b | altum viditur. | BBB aa a r bbb | -----------------------------
From: H. J. Sander Bruggink on 9 Jan 2006 04:39 Charlie-Boo wrote: > H. J. Sander Bruggink wrote: > >>Charlie-Boo wrote: >> >> >>>Thanks. These endless variations in syntax not only gain you nothing, >>>they do even less than simple case analysis. >> >>Aah, so you think that logics that prove more theorems >>are always better? In that case, I suggest you look into >>logics known as "inconsistent logics", because you can >>prove anything you want in those logics. > > > Case analysis does not prove anything that would deem the system > inconsistent. You didn't really get the point of my remark, did you? As usual. Let me restate: the fact that "case analysis" (i.e. classical logic) proves more theorems than intuitionistic logic, does *not* make it a better logic. Sometimes we don't want P v ~P to be valid. The fact that this has to be explained to someone who is "formalizing computer science" is quite funny, btw. groente -- Sander
From: Charlie-Boo on 9 Jan 2006 09:13
H. J. Sander Bruggink & Charlie-Boo wrote: > > Case analysis does not prove anything that would deem the system > > inconsistent. > > You didn't really get the point of my remark, did you? Are you attacking the messenger again? > As usual. > > Let me restate: the fact that "case analysis" (i.e. > classical logic) proves more theorems than intuitionistic > logic, does *not* make it a better logic. But given my above comment about consistency it is. You get more valid conclusions. Playing around with subsets is like Frege endlessly proving propositional calculus wffs (instead of doing something new and nontrivial like formalizing Smullyan's hundreds of theorems as I do.) (Note that I deal in general principles that quickly reveal the folly of these various regurgitations.) > Sometimes we don't > want P v ~P to be valid. > > The fact that this has to be explained to someone who is > "formalizing computer science" is quite funny, btw. Then you need to show that I am not one of them or that you have somehow contradicted my formalization. C-B > groente > -- Sander |