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 11:57 G. Frege wrote: > On 16 Dec 2005 07:58:49 -0800, "sradhakr" <sradhakr(a)in.ibm.com> wrote: > > > > > OK, so you refuse to explain what you mean by the "absurdity", or > > "_|_" that is used in the claimed proof. > > > Sorry, but you seem to overlook the fact that "_|_" is nowhere used in > the original proof (posted by Barb Knox): > > --------------------------------------------------------- > > 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 > > --------------------------------------------------------- > > Right. Then this " RAA proof" is litte more than a bald assertion of ~(P&~P), with no explanation for what precisely is the "absurdity" that is claimed to follow from P&~P. It should already be pretty clear to you, as I explained in my reply to Barb Knox, that the very concept of "proof" requires ~(P&~P) as a presumption.So there really can be no non-circular, *meaningful* proof of ~(P&~P). I can invent a system of logic where I assert "abracadabra; therefore ~(P&~P)" as a vaild deduction; that is acceptable from the point of view of the philosophy of formalism, but not intuitionism (which insists that truths have to be meaningful to the human mind). The above is just nothing more than abracadabra.. But there is no point in my trying to explain this to you any further. I hope you understand the gist of what I am trying to convey. Regards, RS
From: G. Frege on 16 Dec 2005 11:53 On 16 Dec 2005 08:47:03 -0800, "sradhakr" <sradhakr(a)in.ibm.com> wrote something. Look man, you claimed (besides other nonsensical things): "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." This is just nonsense. Sorry. F. -- "I do tend to feel Hughes & Cresswell is a more authoritative source than you." (D. Ullrich)
From: G. Frege on 16 Dec 2005 12:12 On 16 Dec 2005 08:57:54 -0800, "sradhakr" <sradhakr(a)in.ibm.com> wrote something. So how do you like the following proof (in a variant of Gentzen's calculus of natural deduction for intuitionistic logic where "~" is _defined_ with: ~A =df A -> _|_. See Daryl McCullough post.) Theorem: ~(P & ~P) Proof: (1) P & ~P assumption (2) P & (P -> _|_) 1 Def. ~ (3) P 2 &E (4) P -> _|_ 2 &E (5) _|_ 3,4 ->E (MP) (6) P & ~P -> _|_ 1,5 ->I (CP) (7) ~(P & ~P) 6 Def. ~ You see, we did NOT make use of any "RAA-rule". Note that by the application of ->I (or CP) the assumption "A & ~A" in line (1) is "discharged": S, A |- B ----------- ->I S |- A -> B F. -- "I do tend to feel Hughes & Cresswell is a more authoritative source than you." (D. Ullrich)
From: Charlie-Boo on 16 Dec 2005 14:07 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.) But isn't true=true and false=false and ~(true=false)? > 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 ) ? > >> >(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? 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!* I still have faith in the original theorem (above.) ( P = |- Q) => ( P = |-P) because P must be 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.") C-B (I'll be glad to provide further details if anyone is interested.) * However, what is wrong with: Thm. ( |- (P=Q) ) =>((|- 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 Thm. ((|- P) = (|- Q)) => |- (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
From: G. Frege on 16 Dec 2005 16:23
On 16 Dec 2005 01:36:20 -0800, "sradhakr" <sradhakr(a)in.ibm.com> wrote: > > *Any* proposition can be proven in intuitionistic logic if you start > with the [assumption] P&~P. > No. That's false. But it is true that any proposition can be derived as a /conclusion/ from the /premiss/ P & ~P. Comment: Obviously you are not very familiar with systems of natural deduction. There assumptions can be "discharged". Hence the do not count as premisses of the final argument. > > The above "proof" is fundamentally flawed and *should not* be accepted > as a valid proof of ~(P&~P). > Nonsense. The proof is completely valid. > > [...] What you could do is to make a straightforward, bald assertion > of ~(P&~P) without claiming to prove it. > In logic we would call such a statement an /axiom/ then. B u t we do not have to do that, since we can actually prove the statement in the usual systems (calculi) of intuitionistic logic. (See the other posts where several proofs in several different systems [calculi] of intuitionistic logic have been posted.) F. -- "I do tend to feel Hughes & Cresswell is a more authoritative source than you." (D. Ullrich) |