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 17 Dec 2005 23:52 Daryl McCullough wrote: > sradhakr says... > > >So the outline of an intuitionistic proof of ~(P&~P) would be as follows. > > > >(1) Suppose, to the contrary, that P&~P, i.e., suppose that "Both P and > >~P are provable".. > > > >(2) The said proof of P&~P can be converted into the proof of an > >arbitrary proposition Q.. > > > >(3) Therefore a proof of P&~P cannot exist. Hence, ~(P&~P). > > If you interpret ~A as (A -> False), then you can prove > ~(P&~P) as follows > > First, prove the general schema > > (P & (P -> Q)) -> Q I really doubt whether you can claim that anything is proven in a *meaningful* sense without the use of the law of non-contradiction. For example, suppose I make the following assertions, given your proof of the above schema: (1) P (2) P -> Q (3) ~Q Now you can object that the conclusion (3) is not acceptable because it contradicts the given schema. But you need the law of non-contradiction in order to make the said objection. The "proof" may go through formally, but your argument for the law of non-contradiction below actually requires that "False cannot be the case" in a meaningful sense. > > Then a special case is > > (P & (P -> False)) -> False > > which is the same thing as > > ~(P&~P) To arrive at this conclusion a reductio is tacitly presumed. When you interpret ~P as P->False, what you mean is that "Any proof of P can be converted to a proof of False", which in turn yields "A proof of P is impossible", or "The hypothesis that a proof of P exists is absurd". So my previous post also applies to this argument. I think I can now make clear the level at which I am attacking the above proof. The problem, I claim, is that you need a prior conception that "False" cannot be the case, which, in turn, is a prior conception of truth *without proof". I cannot conceive of any way in which you can *prove* False without the use of the law of non-contradiction. The prior assumption that False cannot be the case is OK from the point of view of Platonism, where you can perceive the absurdity of a contradictory proposition. But how is it justified from the intuitionistic standpoint? Remember that intuitionism requires all truths to be stated with proof and we are trying to prove the law of non-contradiction here. If we don't have any prior conception that False cannot be the case, the argument given in my previous post shows that you can interpret the given proof in two ways -- one favourable and the other unfavourable. When we choose to make the favourable interpretation, we are tacitly asserting that we wish the law of non-contradiction to be true, and this is nothing more than an axiomatic assertion, without proof. It seems to me that this business of trying to "prove" the law of non-contradiction in a non-circular, meaningful sense is doomed from the start. Regards, RS > > So you don't need the rule "From False, conclude anything". > > What is False? You can think of it as a primitive > propositional constant, with the axiom schema > > False -> Q > > for every proposition Q. Or you can think of False as the > second-order statement "forall propositions Q, Q". > > -- > Daryl McCullough > Ithaca, NY
From: sradhakr on 17 Dec 2005 23:59 sradhakr wrote: > I cannot conceive of any way in which you can *prove* > False without the use of the law of non-contradiction. Correction. That should read: I cannot conceive of any way in which you can *prove* that "False is not the case" without the use of the law of non-contradiction. Regards, RS
From: sradhakr on 18 Dec 2005 00:35 Torkel Franzen wrote: > "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. Please see my reply to Daryl McCullough's post below; I think this greatly clarifies my argument. Regards, RS
From: Torkel Franzen on 18 Dec 2005 02:02 "sradhakr" <sradhakr(a)in.ibm.com> writes: > Please see my reply to Daryl McCullough's post below; I think this > greatly clarifies my argument. My question is again why you don't consider some derivation that actually uses the absurdity rule instead of miring yourself in an argument that we cannot claim that P->P is proved in a meaningful sense without the use of the law of non-contradiction.
From: sradhakr on 18 Dec 2005 05:04
Torkel Franzen wrote: > "sradhakr" <sradhakr(a)in.ibm.com> writes: > > > Please see my reply to Daryl McCullough's post below; I think this > > greatly clarifies my argument. > > My question is again why you don't consider some derivation that > actually uses the absurdity rule instead of miring yourself in an > argument that we cannot claim that P->P is proved in a meaningful sense > without the use of the law of non-contradiction. OK. I will accept your advice and look at othe rintuitionistic systems.. Regaards, RS |