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 23 Dec 2005 06:25 Torkel Franzen wrote: > "sradhakr" <sradhakr(a)in.ibm.com> writes: > > > OK. I will accept your advice and look at othe rintuitionistic > > systems.. > > No need to look at other systems, just at other examples. Many are > skeptical of the intuitionistic justifiability of the absurdity rule. > A relevant example is the intuitionistic proof of ~A & (A v B) -> B. > Can it be justified in intuitionistic terms? I think the proof is justified *provided* the law of non-contradiction holds, which is the case in most situations. It is only when ex falso quodlibet is applied, that is, when one makes the assumption A&~A (or equivalently, the contradictory assumptions A and ~A) that an arbitrary proposition B results. In my opinion, this situation can be rectified by not allowing *any* proof that starts with A&~A as a hypothesis. This may be justified as follows: To the intuitionist, it is inconceivable that both A and ~A can be proven. So if the intuitionist is totally unable to conceive of A&~A being the case, then surely he is not justified in using A&~A as a hypothesis in any proof as well? Thus when the intuitionist starts a proof with "Suppose A&~A", he has no idea of what this means, i.e. has no mental construct that would justify such a situation. One can justifiably argue that such a hypothesis is not legal to the intuitionist. So ex falso quodlibet can be thrown out this way. However, this would mean that the intuitionist also has no means of *formally* proving the law of non-contradiction. The truth ("proof") of this law to the intuitionist is simply the conviction that it is inconceivable to the human mind that P&~P can be true. Therefore in intuionistic formal systems, ~(P&~P) should simply be an axiomatic assertion with no claim to a *formal* proof. ~(P&~P) should be interpreted as "It is impossible to prove P&~P", and *not* as "A hypothetical proof of P&~P can be converted to the proof of an absurdity". The existing "proof" by reductio ad absurdum suffers from the flaw that it presumes the law of non-contradiction. Thus when one deduces P and ~P from P&~P and then claims that this is a contradiction/absurdity, then one *assumes* without proof that "a proof of P and a proof of ~P is impossible", which, in my book, is just an assumption of ~(P&~P). However, I am not sure that banning the use of P&~P as a hypothesis will not result in other problems for intuitionistic logic. Regards, RS
From: Torkel Franzen on 23 Dec 2005 06:29 "sradhakr" <sradhakr(a)in.ibm.com> writes: > I think the proof is justified *provided* the law of non-contradiction > holds, which is the case in most situations. What proof do you have in mind here?
From: sradhakr on 23 Dec 2005 06:38 Torkel Franzen wrote: > "sradhakr" <sradhakr(a)in.ibm.com> writes: > > > > I think the proof is justified *provided* the law of non-contradiction > > holds, which is the case in most situations. > > What proof do you have in mind here? I am talking of the proof of the propositon ~A & (AvB) -> B I am saying that you can go from this proposition to ex falso quodlibet only when you are allowed to make the contradictory hypothesis A&~A. If this is not allowed, i.e., if one is only allowed to hypothesize either A or ~A with the law of non-contradiction enforced, the above proposition will not allow us to conclude B. Regards, RS
From: Torkel Franzen on 23 Dec 2005 06:41 "sradhakr" <sradhakr(a)in.ibm.com> writes: > I am talking of the proof of the propositon > > ~A & (AvB) -> B Which proof, exactly?
From: sradhakr on 23 Dec 2005 06:54
Torkel Franzen wrote: > "sradhakr" <sradhakr(a)in.ibm.com> writes: > > > > I am talking of the proof of the propositon > > > > ~A & (AvB) -> B > > Which proof, exactly? You got me there. Let us see. If the law of non-contradiction is asserted axiomatically, then the above is simply another version of this law and so can be considered "proven", given non-contradiction. But I will admit I haven't thought through fully the consequences of my proposal for intuitionistic logic, i.e., whether it is viable. In my book *all* truths are axiomatic in nature, and it is better not to talk of a mystical conception of "proof" that no one is able to understand or convey (as in intuitionism). The very purpose of explaining truth as proof is defeated if one is not able to give a precise, formal notion of provability that is equivalent to truth. I am rushing off on a long trip right now and will get back to you tomorrow. Please let me know what you think. Regards, RS |