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 19 Dec 2005 18:08 On 16 Dec 2005 22:52:56 -0800, "sradhakr" <sradhakr(a)in.ibm.com> wrote: > > So the outline of an intuitionistic proof of ~(P&~P) would be as follows. > > (1) Suppose ... that P&~P, i.e., suppose that [P&~P is] provable". > > (2) The said proof of P&~P can be converted into the proof of an > arbitrary proposition Q. > : > No, o u r proves of ~(P & ~P) don't rely on such a reasoning. O u r reasoning is: Assume P & ~P. Hence P and ~P. Contradiction! Hence ~(P & ~P) (by RAA). (You might compare that reasoning with the original proof in a system of natural deduction for intuitionistic logic given by Barb Knox.) F. P.S. The general form of the reasoning we adopted is: Assume A. Derive B and ~B, for some formula B. Hence ~A (by RAA).
From: H. J. Sander Bruggink on 20 Dec 2005 05:52 Charlie-Boo wrote: > Torkel Franzen wrote: >> You mistakenly take the argument to be about classical propositional >>logic. > > > So "~(A<->~A) is a propositional calculus wff" is wrong? (I never used > the word "classical".) But you did talk about "truth tables" and "resolution", both of which are proof methods for classical propositional logic, and not intuitionistic propositional logic. groente -- Sander
From: Charlie-Boo on 20 Dec 2005 08:25 H. J. Sander Bruggink wrote: > Charlie-Boo wrote: > > Torkel Franzen wrote: > > >> You mistakenly take the argument to be about classical propositional > >>logic. > > > > > > So "~(A<->~A) is a propositional calculus wff" is wrong? (I never used > > the word "classical".) > But you did talk about "truth tables" and "resolution", both > of which are proof methods for classical propositional logic, > and not intuitionistic propositional logic. Please give a proof of a propositional calculus proposition that cannot be done using case analysis (examination of the truth tables.) C-B > groente > -- Sander
From: Charlie-Boo on 20 Dec 2005 08:35 David C. Ullrich wrote: > On 19 Dec 2005 07:31:22 -0800, "Charlie-Boo" wrote: > I don't know whether you've noticed this, but others have: Name 2. > You complain that I'm just quibbling about syntax, > and at the same time you ignore most of my comments > about the substance of your Simple yet Profound Metatheorem... Glad you agree it's profound. > Oh for heaven's sake. How was I supposed to know that that two > []'s meant entirely different things? Sorry, I thought you knew all about Logic. > >> > Thm. ((|- P) = (|- Q)) => |- (P=Q) > > > >> This is obviously false. > >> If neither P nor Q is provable (so that > >> ((|- P) = (|- Q)) is true) it certainly > >> does not follow that P==Q _is_ provable. > > > >Let's suppose that P is "1>2" and Q is "2>3". Then P==Q is > >(1>2)==(2>3) which IS provable. > Huh? I said, let's suppose that P is "1>2" and Q is "2>3". Then P==Q is (1>2)==(2>3) which IS provable. > I didn't say that it is never the case that P==Q is > provable. I said that this does not follow from the assumption > that neither P nor Q is provable. I was just illustrating my thinking with a specific example. A better counterexample for you (than meaningless propositional variables) would be P is any Godel sentence and Q is FALSE. > David C. Ullrich
From: Torkel Franzen on 20 Dec 2005 08:53
"Charlie-Boo" <chvol(a)aol.com> writes: > Please give a proof of a propositional calculus proposition that cannot > be done using case analysis (examination of the truth tables.) There are no truth tables for intuitionistic propositional logic. |