Simple yet Profound Metatheorem
in [Logic]
|
Prev: Obections to Cantor's Theory (Wikipedia article)
Next: Why Has None of Computer Science been Formalized?
From: sradhakr on 16 Dec 2005 04:36 Barb Knox wrote: > In article <1134713007.253164.75100(a)z14g2000cwz.googlegroups.com>, > "sradhakr" <sradhakr(a)in.ibm.com> wrote: > > >Barb Knox wrote: > > > >> If you want provability and truth to be the same, you can dispense with > >> all the modal machinery and just use some existing well-thought-out > >> constructive logic (e.g. Intuitionistic). > >> > >False. Truth and provability are *not* the same in > >intuitionistic/constructive logics. If you claim otherwise, show me a > >valid proof of the law of non-contradiction i.e., of ~(P&~P), in these > >logics. > > 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 > > > >Any "proof" of ~(P&~P) that you produce from contradictory > >premises is not a valid proof in these logics. > > Eh? I've given a perfectly valid Intuitionistic proof. On what grounds > do you object to it (if you do)? > *Any* proposition can be proven in intiuitionistic logic if you start with the premise P&~P. The above "proof" is fundamentally flawed and *should not* be accepted as a valid proof of ~(P&~P). The above "proof" is indistinguishable from the case where you deduce an *arbitrary* proposition (say, denoted by the "absurdity symbol") from P&~P and then *substituted* ~(P&~P) for the absurdity symbol and claimed that as a proof of ~(P&~P). It is obvious that any proposition can be proved that way. Indeed, if you think carefully, you will see that the very concept of "proof" requires the law of non-contradiction in the first place and you have already *presumed* ~(P&~P) in your so-called proof-- it is totally absurd to claim an RAA proof of ~(P&~P). What you could do is to make a straightforward, bald assertion of ~(P&~P) without claiming to prove it. But that would violate the intuitionistic philosophy of truth as provability. See the reference that I have cited in my earlier post for my objections to ~(P&~P) as a theorem of a theory T in which P is undecidable (i.e., neither provable nor refutable in T). Regards, RS
From: David C. Ullrich on 16 Dec 2005 06:58 On 15 Dec 2005 12:16:35 -0800, "Charlie-Boo" <chvol(a)aol.com> wrote: >David C. Ullrich wrote: >> On 14 Dec 2005 18:10:58 -0800, "Charlie-Boo" <chvol(a)aol.com> wrote: > >> >Prove ( P = |- Q ) => |- ( P = Q ) >> >> Various people have asked what the heck this means. >> You should _say_ what it means, instead of replying >> with questions. > >[...] > >> Hint: My best attempt at deciphering it leads to >> something obviously false: >> >> "If P equals 'Q has a proof' then there is a >> proof of 'P equals Q'." > >That's it. What was so hard about that? Very curious - a minute ago I saw you say that it meant something else. >> Obviously false, since if P equals 'Q has a proof' >> then P does not equal Q. > >Why is that false? (Once again, what you are so adamantly convinced of >is just not so.) If this is not clearly false you must be assuming that I'm being as sloppy with the language as you are. I'm not - when I say "equals" I mean "equals", not "is logically equivalent to". For example, P is not equal to P&P, although they're certainly equivalent. Evidently from what you say elsewhere in the thread what you really mean, and what you thought I meant, is this: "If P is equivalent to 'Q has a proof' then there is a proof of 'P is equivalent to Q'." This is also false, as has been pointed out, although it's not quite so _obviously_ false as my first interpretation, where I was assuming that "=" referred to equality. Why is it false? Consider the special case where P literally equals "Q is provable". Then your theorem implies this, for any Q: (*) "It is provable that 'Q is provable' is equivalent to Q." Or, in extremely bad notation: (*) |- (|-Q == Q) (bad notation because the first |- means |-, while the second |- refers to some encoding of provability...) This is false. It contradicts the incompleteness theorem, for example, which says that in any system satisfying this and that there exists Q which is true but not provable. >> So that must not be what you mean. > >Thanks for the vote of confidence. > >> >(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.) >> >> Awesome. > >Would it be awesome (interesting, new, useful) if it were true? > >C-B > >> >Hint: Consider the equivalent ( P = |-Q ) => ( P = |- P ) >> >> >> ************************ >> >> David C. Ullrich ************************ David C. Ullrich
From: H. J. Sander Bruggink on 16 Dec 2005 07:38 sradhakr wrote: > Barb Knox wrote: > >>In article <1134713007.253164.75100(a)z14g2000cwz.googlegroups.com>, >> "sradhakr" <sradhakr(a)in.ibm.com> wrote: >>>Any "proof" of ~(P&~P) that you produce from contradictory >>>premises is not a valid proof in these logics. >> >>Eh? I've given a perfectly valid Intuitionistic proof. On what grounds >>do you object to it (if you do)? >> > *Any* proposition can be proven in intiuitionistic logic if you start > with the premise P&~P. Ok, please produce, in the same way, a proof of the proposition P&~P, then. (I mean "P&~P", *not* "(P&~P) -> (P&~P)".) [snip more nonsense] groente -- Sander
From: H. J. Sander Bruggink on 16 Dec 2005 07:46 Charlie-Boo 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 []. Actually, [] is the standard symbol, not |-. [snip] > This seems valid. I really need only the "hint": that P = |-P. > Since that means (|-P)=(|-Q) I thought that would imply |-(P=Q) but > maybe not. Do you agree that P = |-P ? NO! Provability is *not* the same as truth! [snip] groente -- Sander
From: sradhakr on 16 Dec 2005 08:05
H. J. Sander Bruggink wrote: > sradhakr wrote: > > Barb Knox wrote: > > > >>In article <1134713007.253164.75100(a)z14g2000cwz.googlegroups.com>, > >> "sradhakr" <sradhakr(a)in.ibm.com> wrote: > >>>Any "proof" of ~(P&~P) that you produce from contradictory > >>>premises is not a valid proof in these logics. > >> > >>Eh? I've given a perfectly valid Intuitionistic proof. On what grounds > >>do you object to it (if you do)? > >> > > *Any* proposition can be proven in intiuitionistic logic if you start > > with the premise P&~P. > > Ok, please produce, in the same way, a proof of the > proposition P&~P, then. > (I mean "P&~P", *not* "(P&~P) -> (P&~P)".) > 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. 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? > [snip more nonsense] > ?????? If you have something meaningful to say, say it. Otherwiise just keep shut. Regards, RS |