Simple yet Profound Metatheorem
in [Logic]
|
Prev: Obections to Cantor's Theory (Wikipedia article)
Next: Why Has None of Computer Science been Formalized?
From: Torkel Franzen on 17 Dec 2005 02:07 "sradhakr" <sradhakr(a)in.ibm.com> writes: > My understanding is that ALL proofs of ~(P&~P) in inutionism have to > start with the hypothesis P&~P and claim that this is absurd. this is > mandated by the intuitionistic conception of negation. ~(P&~P) is provable in minimal logic. Your misgivings about ex falso quodlibet are irrelevant in the case of this particular proof. Pick some derivation where the rule is actually used, as in the inference from P v Q and ~P to Q.
From: Charlie-Boo on 17 Dec 2005 03:23 Torkel Franzen wrote: > "Charlie-Boo" <chvol(a)aol.com> writes: > > > ~(A<->~A) is a propositional calculus wff, you're talking about proving > > it, and all propositional calculus proofs are simply case analysis > > (examining a finite set of possiblities), which I believe is completely > > implemented by resolution. > > This is just to say that you know nothing about constructive logic. What do you disagree with in the above? C-B
From: Torkel Franzen on 17 Dec 2005 03:46 "Charlie-Boo" <chvol(a)aol.com> writes: > What do you disagree with in the above? You mistakenly take the argument to be about classical propositional logic.
From: Charlie-Boo on 17 Dec 2005 06:53 Torkel Franzen wrote: > "Charlie-Boo" <chvol(a)aol.com> writes: > > > What do you disagree with in the above? > > 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".) C-B
From: Torkel Franzen on 17 Dec 2005 06:54
"Charlie-Boo" <chvol(a)aol.com> writes: > (I never used the word "classical".) Of course not. |