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 29 Dec 2005 14:39 Daryl McCullough wrote: > Charlie-Boo says... > >Daryl McCullough wrote: > >> No, it's the other way around. There are formulas that are provable > >> using truth tables (case analysis) but are not provable > >> intuitionistically. The examples are > >> > >> Excluded Middle: A or ~A > >> Pierce's Law: ((P -> Q) -> P) -> P > > > >Thanks. These endless variations in syntax not only gain you nothing, > >they do even less than simple case analysis. > > What "variations in syntax" are you talking about? Different systems - axioms, rules, methods of creating conclusions. > Intuitionistic analysis is not a "variation in syntax", > it has a different *semantics* than classical logic, and > case analysis is not a valid way to decide validity in > intuitionistic analysis. I am talking about the net result - the output - the wffs (formulas, sentences) that are ultimately proven. Frege wastes time with endless systems that do no more - even do less - than simple case analysis and have been around since the 1800's. I'm trying to talk him into trying something new and not so trivial e.g. giving formal proofs of Smullyan's dozens of theorems (as I do.) Why would he only stick with such repetition? Why? C-B > The inuitionistic meaning of > > P -> Q > > is *not* the same as the intuitionistic meaning of > > ~P or Q > > so converting the first into the second and performing a case > analysis doesn't make any sense, intuitionistically. > > Case analysis is valid intuitionistically provided that for > every atomic proposition P we can prove P or ~P. > > -- > Daryl McCullough > Ithaca, NY
From: Charlie-Boo on 29 Dec 2005 14:41 Torkel Franzen wrote: > "Charlie-Boo" writes: > > No I don't. My original point remains undisputed. > It is indisputable. Since you have sunken into the hell of sarcasm, there's no way to tell your real intent. C-B
From: Charlie-Boo on 29 Dec 2005 14:50 H. J. Sander Bruggink wrote: > H. J. Sander Bruggink wrote: > > Charlie-Boo wrote: > > >> New Question: Just curious - is there even a wff such that you can > >> prove it to be intuitionistically valid but I can't prove the wff > >> using case analysis? > > > > No, there isn't. > > Sorry, I read the question as: "is there even a wff such that > you can prove it to be intuitionistically valid but I can't > prove the wff *to be classically valid* using case analysis? That's it. No problem. C-B > groente > -- Sander
From: Charlie-Boo on 29 Dec 2005 14:59 Daryl McCullough wrote: > Charlie-Boo says... > > > >Torkel Franzen wrote: > > >> There are no truth tables for intuitionistic propositional logic. > > > >That has no relevance. > > If you are interested in intuitionistic propositional logic, > then it is certainly relevant. If you are *not* interested > in intuitionistic propositional logic, then what is the > point of your claim that every wff that is provable > in intuitionistic logic is also provable using truth tables? Change "you are not interested in" to "there's nothing gained in the final analysis", then the answer is: It shows that Frege is wasting his time since nobody has ever come up with a wff that he produces that case analysis does not. Case closed. Coming Soon: "Metamathematically True or False?" C-B > -- > Daryl McCullough > Ithaca, NY
From: Charlie-Boo on 29 Dec 2005 15:08
David C. Ullrich wrote: > On 20 Dec 2005 05:35:47 -0800, "Charlie-Boo" wrote: > > A better > >counterexample for you (than meaningless propositional variables) would > >be P is any Godel sentence and Q is FALSE. > > A counterexample that depends on an _actual_ deep theorem is > "better" than a simple and totally elementary counterexample? > Fascinating. It's just a cop-out to talk about variables with no meaning rather than actual assertions about something. By that logic, you can say that a system is incomplete because it has a propositional variable with no meaning and thus no proof of it or its negation. That's not what we're talking about. C-B > ************************ > > David C. Ullrich |