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 23 Dec 2005 07:15 sradhakr wrote: > Torkel Franzen wrote: > > "sradhakr" <sradhakr(a)in.ibm.com> writes: > > > > > > > I am talking of the proof of the propositon > > > > > > ~A & (AvB) -> B > > > > Which proof, exactly? > > You got me there. Let us see. If the law of non-contradiction is > asserted axiomatically, then the above is simply another version of > this law and so can be considered "proven", given non-contradiction. > But I will admit I haven't thought through fully the consequences of my > proposal for intuitionistic logic, i.e., whether it is viable. In my > book *all* truths are axiomatic in nature, and it is better not to talk > of a mystical conception of "proof" that no one is able to understand > or convey (as in intuitionism). The very purpose of explaining truth as > proof is defeated if one is not able to give a precise, formal notion > of provability that is equivalent to truth. > > I am rushing off on a long trip right now and will get back to you > tomorrow. Please let me know what you think. > Actually, given non-contradiction (in the sense that "a proof of A and a proof of ~A is impossible"), the above only expresses the trivial result that "A proof of B can be converted to a proof of B", i.e., B -> B. Because if you have a proof of ~A, then you can have a proof of AvB if and only if if you have a proof of B. Regards, RS
From: Torkel Franzen on 23 Dec 2005 08:37 "sradhakr" <sradhakr(a)in.ibm.com> writes: > If the law of non-contradiction is > asserted axiomatically, then the above is simply another version of > this law and so can be considered "proven", given non-contradiction. This makes no obvious sense. > But I will admit I haven't thought through fully the consequences of my > proposal for intuitionistic logic, i.e., whether it is viable. In my > book *all* truths are axiomatic in nature, and it is better not to talk > of a mystical conception of "proof" that no one is able to understand > or convey (as in intuitionism). There is nothing mystical about a standard proof of ~A & (AvB) -> B in intuitionistic logic. We just apply the inference rules.
From: G. Frege on 23 Dec 2005 13:34 On 23 Dec 2005 14:37:51 +0100, Torkel Franzen <torkel(a)sm.luth.se> wrote: > > There is nothing mystical about a standard proof of ~A & (AvB) -> B > in intuitionistic logic. We just apply the inference rules. > 1 (1) ~P & (P v Q) A 1 (2) ~P 1 &E 1 (3) P v Q 1 &E 4 (4) P A (1st dijunct) 1,4 (5) _|_ 2,4 ~E 1,4 (6) Q 5 EFQ 7 (7) Q A (2nd disjunct) 1 (8) Q 3,4,6,7,7 vE (9) ~P & (P v Q) -> Q 1,8 ->I F. -- "I do tend to feel Hughes & Cresswell is a more authoritative source than you." (David C. Ullrich)
From: G. Frege on 23 Dec 2005 13:44 On 23 Dec 2005 12:41:17 +0100, Torkel Franzen <torkel(a)sm.luth.se> wrote: >> >> I am talking of the proof of the propositon >> >> ~A & (A v B) -> B >> > Which proof, exactly? > Who knows? Maybe he's talking about (1) ~A & (A v B) ------------ &E (2) ~A A ------------ ~E (1) _|_ ~A & (A v B) ----- EFQ (3) ------------ &E B B A v B ----------------------------- vE (2,3) B ----------------- ->I (1) ~A & (A v B) -> B ? F. -- "I do tend to feel Hughes & Cresswell is a more authoritative source than you." (David C. Ullrich)
From: sradhakr on 23 Dec 2005 14:59
G. Frege wrote: > On 23 Dec 2005 12:41:17 +0100, Torkel Franzen <torkel(a)sm.luth.se> > wrote: > > >> > >> I am talking of the proof of the propositon > >> > >> ~A & (A v B) -> B > >> > > Which proof, exactly? > > > > Who knows? > > Maybe he's talking about > > (1) > ~A & (A v B) > ------------ &E (2) > ~A A > ------------ ~E (1) > _|_ ~A & (A v B) > ----- EFQ (3) ------------ &E > B B A v B > ----------------------------- vE (2,3) > B > ----------------- ->I (1) > ~A & (A v B) -> B > > ? > > > F. > I am talking about the proof using the law of non-contradiction. Thus from the hypothesis ~A&(AvB) we conclude ~A and AvB.. AvB implies that we have a proof of A or a proof of B. From ~A and the law of non-contradiction ~(A&~A), we conclude that a proof of A is impossible. Since the first possibility in AvB has been eliminated, it follows that we have a proof of B. Now discharge the hypothesis and conclude ~A&(AvB)->B. There is no use of EFQ in this proof. See my previous post in which I advocate use of ~(A&~A) (interpreted as: "a proof of A&~A is impossible") as an axiomatic assertion, without formal proof. The very fact that this modification eliminates the need for EFQ in the proof of ~A&(AvB) -> B indicates that the existing intuitionistic proof of ~(A&~A) makes a tacit use of EFQ, which is what I have been objecting to all along. Regards, RS Regards, RS |