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 23 Dec 2005 15:22 On 23 Dec 2005 11:59:09 -0800, "sradhakr" <sradhakr(a)in.ibm.com> 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 >> >> ? >> > I am talking about the proof using the law of non-contradiction. > Could you please write down this proof? (Note that I'm asking for a formal /proof/ in a logical system/calculus of intuitionistic logic.) > > From ~A and the law of non-contradiction ~(A & ~A), we conclude > that a proof of A is impossible. > How would you write down this statement in a /formal/ proof? (See comment above.) F. -- "I do tend to feel Hughes & Cresswell is a more authoritative source than you." (David C. Ullrich)
From: sradhakr on 23 Dec 2005 16:01 G. Frege wrote: > On 23 Dec 2005 11:59:09 -0800, "sradhakr" <sradhakr(a)in.ibm.com> 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 > >> > >> ? > >> > > I am talking about the proof using the law of non-contradiction. > > > Could you please write down this proof? (Note that I'm asking for a > formal /proof/ in a logical system/calculus of intuitionistic logic.) > > > > > From ~A and the law of non-contradiction ~(A & ~A), we conclude > > that a proof of A is impossible. > > > How would you write down this statement in a /formal/ proof? (See > comment above.) > > I can take up this challenge, but I need time to think through the basic idea that I have suggested in my previous post. The challenge is to develop a system of intuitionistic logic in which the use of a contradiction (P&~P) as a hypothesis is banned in any valid proof (which results in the invalidation of EFQ as well as the non-provability of the law of non-contradiction, see my previous post). So if ~(P&~P) is asserted axiomatically, without formal proof, can we get all the important results of intuitionistic logic without EFQ? Or will there be some irredeemable inconsistency? I intend to think about this idea. Why don't you help me develop it? Actually I am running out of steam justifying my work (on the logic NAFL) to my bosses in IBM and I could use some feedback/interaction from the academic community. Regards, RS
From: sradhakr on 24 Dec 2005 00:03 sradhakr wrote: > G. Frege wrote: > > On 23 Dec 2005 11:59:09 -0800, "sradhakr" <sradhakr(a)in.ibm.com> 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 > > >> > > >> ? > > >> > > > I am talking about the proof using the law of non-contradiction. > > > > > Could you please write down this proof? (Note that I'm asking for a > > formal /proof/ in a logical system/calculus of intuitionistic logic.) > > > > > > > > From ~A and the law of non-contradiction ~(A & ~A), we conclude > > > that a proof of A is impossible. > > > > > How would you write down this statement in a /formal/ proof? (See > > comment above.) > > > > > I can take up this challenge, but I need time to think through the > basic idea that I have suggested in my previous post. The challenge is > to develop a system of intuitionistic logic in which the use of a > contradiction (P&~P) as a hypothesis is banned in any valid proof > (which results in the invalidation of EFQ as well as the > non-provability of the law of non-contradiction, see my previous post). > So if ~(P&~P) is asserted axiomatically, without formal proof, can we > get all the important results of intuitionistic logic without EFQ? Or > will there be some irredeemable inconsistency? I intend to think about > this idea. Why don't you help me develop it? Actually I am running out > of steam justifying my work (on the logic NAFL) to my bosses in IBM and > I could use some feedback/interaction from the academic community. > Hmmm..... I already foresee some problems. There may be difficulties with the intuitionistic interpretation of negation and implication in my proposed formulation. Secondly, the law of non-contradiction, when interpreted the way I want it, asserts that "P&~P is impossible" i.e., "There are no contradictions". Which is to say that every legitimate intuitionistic theory must prove its own consistency. But this would clash with Godel's second incomleteness theorem when the theory in question is the intutionistic version of arithmetic (Heyting Arithmetic?). If I am not mistaken, Godel's incompleteness theorem applies to this theory. I strongly suspect that if one asserts that the truth of ~(P&~P) is axiomatic rather than provable, then one thing will lead to another and eventually we will end up with my proposed logic NAFL.. Regards, RS
From: G. Frege on 24 Dec 2005 19:19 On 23 Dec 2005 21:03:02 -0800, "sradhakr" <sradhakr(a)in.ibm.com> wrote: Sradhakr: I am talking of the proof of the proposition ~A & (A v B) -> B. Torkel Franzen: Which proof, exactly? G. Frege: Could you please write down this proof? (Note that I'm asking for a formal /proof/ in a logical system/calculus of intuitionistic logic. Sradhakr: I can take up this challenge [...] Hmmm..... I already foresee some problems. [...] Ok, so you talked about a non-existing proof, fine. (Though this might lead to some confusion, I guess.) F. -- "I do tend to feel Hughes & Cresswell is a more authoritative source than you." (David C. Ullrich)
From: Charlie-Boo on 29 Dec 2005 14:21
H. J. Sander Bruggink wrote: > Charlie-Boo wrote: > > H. J. Sander Bruggink wrote: > >>Please show, by a "case analysis", that P->P is > >>intuitionistically valid. > > > > I didn't say anything about "intuitionistically valid". (Got it? > > Good!) > > No of course not. You didn't even know what it was. > (I suppose you looked it up in wikipedia, by now, right?) You are attacking the messenger. I will not be dragged into that. Just answer the mathematical question. (Actually, I usually use mathworld.) > > I said you could prove using case analysis any propositional > > calculus wff that can be proven using the various rules of inference. > > Yes, you said that, and because you said it in a subthread > about *intuitionistic* propositional logic, and even explicitly > denied that you were talking about *classical* propositional > logic, what you said was WRONG. I denied that? > > P => P is ~P v P > > This is not a valid equivalence in IL. As Charlie Brown (my alter-ego) says, "AAAHHHHHHHHH" > > P ~P ~P v P > > > > true false true > > false true true > > > > See, you can prove P => P using case analysis, as I said. > > No, you didn't prove anything, because proof tables are not > valid for IL. (In fact, ~P v P isn't valid in IL). AAAAAAAAAAAAAAAAAHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHH!!!!!!! > (But at least three people mentioned this already, right, so > you could have expected this answer.) > > > > > Now why don't YOU admit that? > > Because it isn't true. It's only true for *classical* > propositional logic, and you explicitly denied that you were > talking about that. Quote, please. (Then what was I talking about?) > > New Question: Just curious - is there even a wff such that you can > > prove it to be intuitionistically valid but I can't prove the wff > > using case analysis? > > No, there isn't. That's my contention. Thank you sir. (I take back the "AA . . ..HHH"''s.) QED C-B > groente > -- Sander |