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 17 Dec 2005 07:13 Torkel Franzen wrote: > "Charlie-Boo" writes: > > > (I never used the word "classical".) > > Of course not. And: So "~(A<->~A) is a propositional calculus wff" is wrong? C-B
From: Torkel Franzen on 17 Dec 2005 08:31 "Charlie-Boo" <chvol(a)aol.com> writes: > And: So "~(A<->~A) is a propositional calculus wff" is wrong? Aha, I see! You mistakenly thought that the argument was about classical logic!
From: David C. Ullrich on 17 Dec 2005 08:56 On 16 Dec 2005 11:07:53 -0800, "Charlie-Boo" <chvol(a)aol.com> wrote: >David C. Ullrich wrote: > >> 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. > >Show me how to underline = in a post and I'll be glad to (seriously.) All you have to do is explain what your notation means. Also probably when I have a conjecture about what you mean by the notation and it's _not_ what you actually meant saying yes it is is probably not a good idea. But never mind that - your "=" meant logical equivalence, fine (if you insist). >But isn't true=true and false=false and ~(true=false)? I have no idea, because the fact that you insist on using "=" to denote something other than equality means that I have no idea what you're asking. >> Or, in extremely bad notation: |- (|-Q == Q) >> >> (bad notation because the first |- means |-, while >> the second |- refers to some encoding of provability...) > >And [] ( []Q == Q ) ? What about it? (Is it extemely bad notation? No. Does it mean the same thing as |-(|- Q == Q)? No. Is it a theorem of any system of modal logic known to man? No. If your question is not answered above, what _did_ you mean to ask?) >> >> >(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? > >Too hard of a question? Right. The question is equivalent to "Would it be awesome if 2 + 2 = 5?" That is indeed a very difficult question. >What I really need is the "hint" ( P = |- Q) => ( P = |-P ) to >effect the translation from Theory of Computation theorems to >Incompleteness in Logic theorems. (And since I axiomatize Theory of >Computation theorems in http://arxiv.org/html/cs.LO/0003071 , that >paper plus this theorem provides an axiomatization of Incompleteness in >Logic results, including the theorems of Godel, Rosser, Smullyan and >others.) > >Since P = |- Q then (P = |- P) means (|- P) = (|- Q). I thought that >maybe (|- P) = (|- Q) is equivalent to |- (P=Q) and added it to spice >up the theorem as ( P = |-Q ) => |- (P=Q), but Barbara Knox (and you) >posted a very nice proof to the contrary!* Poor Charlie. You announce that you've _proved_ a "simple yet profound" metatheorem. Turns out that part of the "proof" was just something you "thought" was so. And you wonder why nobody takes you seriously. >I still have faith in the >original theorem (above.) What is the "original theorem"? There are many things "above". >( P = |- Q) => ( P = |-P) because P must be r.e. Uh, this is gibberish. A set of natural numbers is or is not r.e. What the hell does it mean to say that a wff is r.e.? >I just spent a few >minutes thinking about it in terms of pure Logic (Modal Logic, >actually), and came up with: > > Thm. ( P = |- Q) => ( P = |-P) >1. P = |-Q Premise >2. |-P = |-|-Q ( w = v ) => ( (|-w) = (|-v) ) , 1 >3. |-P = |-Q ( |-w ) = ( |- |- w) , 2 >4. P = |-P Substitution 1,3 > qed > >Now do you agree? (Just cut out the red herrings about syntax. Or >admit "I don't know anything about Logic but I know what the symbols >are.") "red herrings about syntax". Right. First, that doesn't have anything to do with modal logic that I can see. Second, I can't parse most of it, because of your idiosyncratic notation (I can't tell which |-'s are actually assertions and which are abbreviations for an encoding of provability.) >C-B > >(I'll be glad to provide further details if anyone is interested.) > >* However, what is wrong with: > > Thm. ( |- (P=Q) ) =>((|- P) = (|- Q)) If my guess regarding what you mean is correct then this is a true fact, not that the "derivation" below makes much sense. >1. |- (P=Q) Premise >2. |- (P => Q) Definition 1 >3. |- (Q => P) Commutativity and Definition 1 >4. (|-P) => (|-Q) Deduction Theorem 2 >5. (|-Q) => (|-P) Deduction Theorem 3 >6. (|-P) = (|-Q) Definition 4,5 > qed > > Thm. ((|- P) = (|- Q)) => |- (P=Q) This on the other hand is obviously false. It's 75 percent true: If P is provable and Q is provable (so that ((|- P) == (|- Q)) is true) then P==Q is certainly provable. And if P is provable and Q is not provable (so that ((|- P) = (|- Q)) is false) then P == Q is certainly not provable; similarly if Q is provable and P is not. But if neither P nor Q is provable (so that ((|- P) = (|- Q)) is true) it certainly does not follow that P==Q _is_ provable. (For example, suppose P and Q are both atomic formulas in the predicate calculus: P = p and Q = q, where _those_ equal signs denote _equality_. Then P is not provable, Q is not provable, and neither is P == Q.) >1. ((|- P) = (|- Q)) Premise >2. (|- P) => (|-Q) Definition 1 >3. (|-Q) => (|-P) Commutativity and Definition 1 >4. |- (P=>Q) Deduction Theorem 2 >5. |- (Q=>P) Deduction Theorem 3 >6. |- (P=Q) Definition 4,5 > qed > >Thus ( |- (P=Q) ) <=> ( (|- P) = (|- Q) ), no? > >> David C. Ullrich ************************ David C. Ullrich
From: Daryl McCullough on 17 Dec 2005 09:07 sradhakr says... >So the outline of an intuitionistic proof of ~(P&~P) would be as follows. > >(1) Suppose, to the contrary, that P&~P, i.e., suppose that "Both P and >~P are provable".. > >(2) The said proof of P&~P can be converted into the proof of an >arbitrary proposition Q.. > >(3) Therefore a proof of P&~P cannot exist. Hence, ~(P&~P). If you interpret ~A as (A -> False), then you can prove ~(P&~P) as follows First, prove the general schema (P & (P -> Q)) -> Q Then a special case is (P & (P -> False)) -> False which is the same thing as ~(P&~P) So you don't need the rule "From False, conclude anything". What is False? You can think of it as a primitive propositional constant, with the axiom schema False -> Q for every proposition Q. Or you can think of False as the second-order statement "forall propositions Q, Q". -- Daryl McCullough Ithaca, NY
From: Daryl McCullough on 17 Dec 2005 10:00
Charlie-Boo says... > Thm. ( P = |- Q) => ( P = |-P) >1. P = |-Q Premise >2. |-P = |-|-Q ( w = v ) => ( (|-w) = (|-v) ) , 1 >3. |-P = |-Q ( |-w ) = ( |- |- w) , 2 >4. P = |-P Substitution 1,3 > qed Let's change notation to []P to mean "P is provable". Let's use <-> to mean logical equivalence. The usual properties of provability are these: 1. []Q -> [][]Q (not <->) 2. [](P->Q) -> []P -> []Q [][]Q -> []Q is not usually assumed. -- Daryl McCullough Ithaca, NY |