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 15 Dec 2005 15:16 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. You are way too loose with your tongue. 1. "Various people have asked what the heck this means.": Only one person asked a question, viz, "What does this mean?". 2. "instead of replying with questions.": I had yet to respond to that one question. 3. I posed one question, in response to the statement that my theorem is ill-formed. As the statement did not say what constructs in the theorem are ill-formed, I asked if he was referring to the use of |- as an operator in a wff. At no point did I reply to a question with a question. > 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? > 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.) > 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
From: Barb Knox on 15 Dec 2005 15:30 In article <1134676919.959126.261450(a)z14g2000cwz.googlegroups.com>, "Charlie-Boo" <chvol(a)aol.com> wrote: >Dan Christensen wrote: >> "Charlie-Boo" <chvol(a)aol.com> wrote in message > >> > Prove ( P = |- Q ) => |- ( P = Q ) > >> What does this mean? I am not familiar with the notation. >> >> Dan > >P and Q are variables that range over wffs >|- means "It is provable that" >= is logical equivalence >=> is implication > >Check out any text on Logic, especially Modal Logic e.g. The >Unprovability of Consistency, or The Logic of Provability by Boolos. OK then, using some modal logic for provability and a more-common logical notation, you're claiming: (*) (P <-> []Q) -> [](P <-> Q). 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. 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. 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). >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: Charlie-Boo on 15 Dec 2005 16:37 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 []. > 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) > 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. Since that means (|-P)=(|-Q) I thought that would imply |-(P=Q) but maybe not. Do you agree that P = |-P ? 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! C-B > you can dispense with > all the modal machinery and just use some existing well-thought-out > constructive logic (e.g. Intuitionistic). > > >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: sradhakr on 16 Dec 2005 01:03 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. Any "proof" of ~(P&~P) that you produce from contradictory premises is not a valid proof in these logics. E.g. see Appendix A of http://arxiv.org/abs/math.LO/0506475 which reproduces the argument given in my published paper in IJQI, Vol. 3, No. 1 (2005) pp. 263-267 ("The quantum superposition principle justified in new non-Aristotelian finitary logic"). Regards, RS
From: Barb Knox on 16 Dec 2005 03:52
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)? [snip] -- --------------------------- | 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 | ----------------------------- |