Simple yet Profound Metatheorem
in [Logic]
|
Prev: Obections to Cantor's Theory (Wikipedia article)
Next: Why Has None of Computer Science been Formalized?
From: G. Frege on 16 Dec 2005 10:44 On 16 Dec 2005 01:36:20 -0800, "sradhakr" <sradhakr(a)in.ibm.com> wrote: >>> >>> [...] show me a valid proof of the law of non-contradiction i.e., >>> of ~(P&~P), in [a system of Intuitionistic Logic]. >>> Ok. First let's state the axioms (or rather axiom schemata) of such a system: A1 A -> (B -> A) A2 (A -> (B -> C) -> ((A -> B) -> (A -> C)) A3 A & B -> A A4 A & B -> B A5 A -> (B -> (A & B)) A6 A -> A v B A7 B -> A v B A8 (A -> C) -> ((B -> C) -> (A v B -> C)) A9 (A <-> B) -> (A -> B) A10 (A <-> B) -> (B -> A) A11 (A -> B) -> ((B -> A) -> (A <-> B)) A12 (A -> B) -> ((A -> ~B) -> ~A) A13 ~A -> (A -> B) Rule of derivation: MP Source: http://plato.stanford.edu/entries/logic-intuitionistic/ Theorem: ~(P & ~P) Proof: (1) P & ~P -> P Ax. A3 (2) P & ~P -> ~P Ax. A4 (3) (P & ~P -> P) -> ((P & ~P -> ~P) -> ~(P & ~P)) Ax. A11 (4) (P & ~P -> ~P) -> ~(P & ~P) MP 1,3 (5) ~(P & ~P) MP 2,4 There you are. F. -- "I do tend to feel Hughes & Cresswell is a more authoritative source than you." (D. Ullrich)
From: Frederick Williams on 16 Dec 2005 10:55 Charlie-Boo wrote: > > ... theoreticians such as > myself have been looking for since the 1930's. You must be getting on in years. -- Remove "antispam" and ".invalid" for e-mail address.
From: sradhakr on 16 Dec 2005 10:58 Torkel Franzen wrote: > "sradhakr" <sradhakr(a)in.ibm.com> writes: > > > But what, precisely, is the "absurdity" that you deduce > > from P&~P, in order to conclude ~(P&~P) in the claimed proof? > > P and ~P. > > > The fact > > that you can deduce an arbitrary proposition from P&~P? > > Completely irrelevant, since we deduce ~(P&~P) without assuming > any such fact. OK, so you refuse to explain what you mean by the "absurdity", or " _|_" that is used in the claimed proof. Then, as far as I am concerened, all you have done is a bald assertion of ~(P&~P), without proof. If _|_ means that an arbitrary proposition Q can in principle be deduced, intuitionistic logic requires you to actually demonstrate this fact by doing it, i.e., by deducing an arbitrary propoistion Q from P&~P (truth=provability). The consequent conclusion of ~(P&~P) then becomes questionable, to say the least. And I do remember reading about intuitionistic systems where _|_ means precisely what I have stated above. Regards, RS
From: Torkel Franzen on 16 Dec 2005 11:09 "sradhakr" <sradhakr(a)in.ibm.com> writes: > OK, so you refuse to explain what you mean by the "absurdity", or " > _|_" that is used in the claimed proof. Any statement whatever that we know to be false. Ex falso quodlibet is irrelevant.
From: G. Frege on 16 Dec 2005 11:06
On 16 Dec 2005 05:05:30 -0800, "sradhakr" <sradhakr(a)in.ibm.com> wrote: > > 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. > Please show! "Unproven statements carry little weight in the world of mathematics." - Amir D. Aczel > > In other words, the claimed proof shows that from the [assumption] P&~P > one can conclude ~(P&~P). But from the hypothesis P&~P one can conclude > any proposition [...]. > You are mixing up different notions. Actually, two different rules are involved here: (RAA) [A] : B & ~B ------ ~A Note that the assumption A is "discharged" by the application of the rule. This is denoted in by "[ ]". (EFQ) A & ~A ------ B Note that h e r e nothing is "discharged"! So with this two rules (plus CP) we may prove the following two (meta-)theorems: |- ~(A & ~A) Proof (Lemmon style): 1 (1) A & ~A assumption (2) ~(A & ~A) 1,1 RAA and |- A & ~A -> B Proof (Lemmon style): 1 (1) A & ~A assumption 1 (2) B 1 EFQ (3) A & ~A -> B 1,2 CP If we stop with our proof at line (2), we would just get: A & ~A |- B. F. -- "I do tend to feel Hughes & Cresswell is a more authoritative source than you." (D. Ullrich) |