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 18 Dec 2005 05:18 "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?
From: Daryl McCullough on 18 Dec 2005 08:06 sradhakr says... >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. You can make whatever assertions you like. The question is a matter of proof. A random collection of assertions is not a proof. >But you need the law of non-contradiction >in order to make the said objection. The law of contradiction isn't relevant to the question of whether (1), (2), (3) is a valid proof. >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. No, that's irrelevant to the proof of ~(P&~P). >> 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. No, it's not. >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" No, a proof of ~P is *not* a proof that "A proof of P is impossible". If you have inconsistent axioms, then you can prove both P and also ~P. A proof of ~P amounts to a proof that "P implies anything". So if *anything* is not provable, then P is not provable. But it's possible that your axioms allow *everything* to be proved. >The problem, I claim, is that you need a prior conception that "False" >cannot be the case Nothing in my proof depends on the assumption that False cannot be the case. >I cannot conceive of any way in which you can *prove* >False without the use of the law of non-contradiction. Hopefully, you can't prove False, so it is *good* that you cannot conceive of any way to prove it. >But how is it justified from the intuitionistic >standpoint? Intuitionistic proof doesn't require the assumption that False cannot be the case, it only requires the assumption that "False implies anything", which is true by definition of "False". >Remember that intuitionism requires all truths to be stated >with proof and we are trying to prove the law of non-contradiction >here. The law of non-contradiction is just (P & (P -> False)) -> False >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. I couldn't make any sense of that post. Whether ~(P&~P) is provable or not does not depend on "interpretations", it depends on your rules of inference and your axioms. >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. Well, I have no idea what you are talking about. I gave you a proof of ~(P&~P), and that proof was noncircular. So what you are saying doesn't make any sense to me. I think you are talking about *interpretations* rather than *proof*. There is no circularity in the proof of ~(P&~P). It doesn't rely in any way on the notion that "There is no proof of False", so your complaints about it are just silly. Now, when it comes to *interpretations*, you can legitimately ask: "How do we know that it is never the case that P&~P?" Well, what we can say is that if, for any statement Q, it is not the case that Q, then in particular it is not the case that P&~P. If *anything* is not true, then False is not true. That's the best you can do. -- Daryl McCullough Ithaca, NY
From: sradhakr on 18 Dec 2005 13:42 Daryl McCullough wrote: > sradhakr says... > > >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. > > You can make whatever assertions you like. The question is > a matter of proof. A random collection of assertions is not > a proof. > The question is whether you can deny (3) without any use of the law of nnn-contradiction,, given (1) and (2), and your prooof schema. > >But you need the law of non-contradiction > >in order to make the said objection. > > The law of contradiction isn't relevant to the question of whether > (1), (2), (3) is a valid proof. I never questioned the formal vailidity of your proof. > > >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. > > No, that's irrelevant to the proof of ~(P&~P). I see from your replies below that you do indeed admit the possiblity of "False" being the case despite your formal proof of ~(P&~P). I doubt whether your notion of "proof" is the same as the intuitionistic "truth=provability". Your attitude is that of a formalist, not an intuitionist. Please see my replies below. > > >> 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. > > No, it's not. > > >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" > > No, a proof of ~P is *not* a proof that "A proof of P is impossible". > If you have inconsistent axioms, then you can prove both P and > also ~P. Sure you can. But the "proof" you are talking about is not the intuitionistic notion of "proof" as in "truth=provability". > > A proof of ~P amounts to a proof that "P implies anything". So > if *anything* is not provable, then P is not provable. But it's > possible that your axioms allow *everything* to be proved. > > >The problem, I claim, is that you need a prior conception that "False" > >cannot be the case > > Nothing in my proof depends on the assumption that False cannot > be the case. > Accepted that your proof is formally valid without anybody ever knowing what "False" is. You can replace "False" by a completely meaningless string of alphabets and still your proof is formally valid. The argument is about whether your concept of formal proof is what the intuitionist intends in his "truth=provability". > >I cannot conceive of any way in which you can *prove* > >False without the use of the law of non-contradiction. > > Hopefully, you can't prove False, so it is *good* that > you cannot conceive of any way to prove it. > > >But how is it justified from the intuitionistic > >standpoint? > > Intuitionistic proof doesn't require the assumption that > False cannot be the case, it only requires the assumption > that "False implies anything", which is true by definition > of "False". > > >Remember that intuitionism requires all truths to be stated > >with proof and we are trying to prove the law of non-contradiction > >here. > > The law of non-contradiction is just > > (P & (P -> False)) -> False > > >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. > > I couldn't make any sense of that post. Whether ~(P&~P) is provable > or not does not depend on "interpretations", it depends on your > rules of inference and your axioms. Whether ~(P&~P) is provable in any particular formal system depends on the rules of inference and axioms of that formal system. But the argument is whether your proof in this or that formal system is compatible with intuitionistic principles, i.e., is it what the intuitionist means by "truth=provability". > > >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. > > Well, I have no idea what you are talking about. I gave you > a proof of ~(P&~P), and that proof was noncircular. So what > you are saying doesn't make any sense to me. > > I think you are talking about *interpretations* rather than > *proof*. There is no circularity in the proof of ~(P&~P). It > doesn't rely in any way on the notion that "There is no > proof of False", so your complaints about it are just silly. If you admit the possibility of "False" being the case and carry through your proof,,then your conclusion of ~(P&~P) could well be merely a trivial consequence of every proposition being provable as was pointed out in my previous post (whose point you really did not understand). You claim that you are not bothered about this possiblility. Well, you should be bothered. Why? If it is indeed the case that every proposition is provable, the intuitionist would conclude that ~(P&~P) is *false* despite your formally valid proof of ~(P&~P). So very clearly, your notion of "provability" does not coincide with the intuitionistic notion of "truth". > > Now, when it comes to *interpretations*, you can legitimately > ask: "How do we know that it is never the case that P&~P?" > Well, what we can say is that if, for any statement Q, > it is not the case that Q, then in particular it is not > the case that P&~P. If *anything* is not true, then False > is not true. That's the best you can do. > In that case the intuitionist *ought to* conclude that you have not *proven* ~(P&~P), in the intuitionistic sense of "proven" (because you admit the possiblity that ~(P&~P) could be *false* in the intuitionistic sense, despite your proof of ~(P&~P)). Please correct me if you feel I am wrong. Regards, RS
From: Charlie-Boo on 18 Dec 2005 14:01 Daryl McCullough wrote: > Charlie-Boo says... > > > Thm. ( P = |- Q) => ( P = |-P) > >1. P = |-Q Premise > >2. |-P = |-|-Q ( w = v ) => ( (|-w) = (|-v) ) , 1 > >3. |-P = |-Q ( |-w ) = ( |- |- w) , 2 > >4. P = |-P Substitution 1,3 > > qed > > Let's change notation to []P to mean "P is provable". > Let's use <-> to mean logical equivalence. > The usual properties of provability are these: > > 1. []Q -> [][]Q > (not <->) > 2. [](P->Q) -> []P -> []Q > > [][]Q -> []Q is not usually assumed. Thanks (although I don't know the consequence of something being "usually assumed" or not.) Assuming for a moment that P and Q have the same non-empty set of free variables and we take them as being universally quantified below, i.e. assertion f(P,Q) means (for all . . .)f(P,Q). Do you agree that: 1. If (P is true iff Q is provable ) then the set expressed by P is r.e.? 2. If the set expressed by P is r.e. then (P is true iff P is provable)? 3. How would you represent 1 and 2? C-B > -- > Daryl McCullough > Ithaca, NY
From: Daryl McCullough on 18 Dec 2005 19:14
sradhakr says... >I see from your replies below that you do indeed admit the possiblity >of "False" being the case despite your formal proof of ~(P&~P). I doubt >whether your notion of "proof" is the same as the intuitionistic >"truth=provability". On the contrary, the proof of ~(P&~P) is intuitionistically valid. Where intuitionism differs from classical logic is that it does not assume ~~P -> P >Sure you can. But the "proof" you are talking about is not the >intuitionistic notion of "proof" as in "truth=provability". I'm talking about the intuitionistic notion. ~(P&~P) is true under the intuitionistic notion of the meaning of the operators ~ and &. >Accepted that your proof is formally valid without anybody ever knowing >what "False" is. Then your complaint is not with the proof of ~(P&~P) If you have any complaint it is with some other fact about False or about negation. >You can replace "False" by a completely meaningless >string of alphabets and still your proof is formally valid. That's right. This particular proof doesn't use any specific fact about False. But surely if (P&(P -> Q)) -> Q is true for an arbitrary proposition Q, then it is *also* true for the specific case Q = False. >Whether ~(P&~P) is provable in any particular formal system depends on >the rules of inference and axioms of that formal system. But the >argument is whether your proof in this or that formal system is >compatible with intuitionistic principles, i.e., is it what the >intuitionist means by "truth=provability". The answer is "yes". The proof is perfectly valid both classically and intuitionistically. >If you admit the possibility of "False" being the case and carry >through your proof,,then your conclusion of ~(P&~P) could well be >merely a trivial consequence of every proposition being provable as was >pointed out in my previous post (whose point you really did not >understand). I certainly don't understand the point. ~(P&~P) is always provable, even if your axioms are inconsistent. >If it is indeed the case that every proposition is provable, >the intuitionist would conclude that ~(P&~P) is *false*. No, they wouldn't. ~(P&~P) is always true. You are making claims about what an inuitionist would conclude which are just false. >So very clearly, your notion of "provability" does not >coincide with the intuitionistic notion of "truth". I would say, on the contrary, that you have no real understanding of the inutionistic notion of truth. >> Now, when it comes to *interpretations*, you can legitimately >> ask: "How do we know that it is never the case that P&~P?" >> Well, what we can say is that if, for any statement Q, >> it is not the case that Q, then in particular it is not >> the case that P&~P. If *anything* is not true, then False >> is not true. That's the best you can do. >> >In that case the intuitionist *ought to* conclude that you have not >*proven* ~(P&~P) I gave the inuitionistic proof of that statement. So I really don't know what you are talking about. -- Daryl McCullough Ithaca, NY |