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 19 Dec 2005 02:03 Daryl McCullough wrote: > sradhakr says... > [snip] > > 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. > So this is precisely our point of disagreement. Let us leave it at this. You are asserting that in the event that all propositions are provable, the intuitionist will claim that ~(P&~P) is stilll true by virtue of the fact that he has an "intuitionistically valid" proof of ~(P&~P). I use the quotes because my argument is that the assumed validity in this case is questionable from my reading of what the intuitoinist has in mind when he asserts the truth of ~(P&~P) (which, according to me, is that a proof of P *and* a proof of ~P, i.e., a proof of P&~P, is impossible). You obviously do not accept this. I could dig out many web sites that would support my interpretation. See, for example the following Wikipedia site, which I picked from a very cursory Google search:: http://en.wikipedia.org/wiki/Intuitionistic_logic Quoting from this site, "The interpretation of negation in intuitionistic logic is different from its counterpart in classical logic. In classical logic, ¬P asserts that P is false; in intuitionistic logic, ¬P asserts that a proof of P is impossible." According to your interpretation of intuitionistic truth, the intuitonist will completely deny that there is any notion of "absurdity", apriori or otherwise. In other words, according to you, the intuitionist does not see any absurdity in the provability of P&~P (or the provability of every proposition and its negation, which is the same thing). Alternatively, if you claim that he does see an absurdity, but nevertheless still holds every proposition to be "true" (by virtue of its hypothesized provability in your intuitionistic system), then you are claiming that the intuitionist can accept that absurdities can be true. Surely this does not square with the perception that intuitionistic truths have to be meaningful to the human mind? Regards, RS > 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
From: Daryl McCullough on 19 Dec 2005 06:20 sradhakr says... >You are asserting that in the event that all propositions are >provable, the intuitionist will claim that ~(P&~P) is stilll true by >virtue of the fact that he has an "intuitionistically valid" proof of >~(P&~P). It is also true by its *meaning*. ~(P&~P) is equivalent to ~False, which is equivalent to False -> False, which just says "If False is provable, then False is provable", which is true whether or not False is provable. >http://en.wikipedia.org/wiki/Intuitionistic_logic > >Quoting from this site, > >"The interpretation of negation in intuitionistic logic is different >from its counterpart in classical logic. In classical logic, =ACP >asserts that P is false; in intuitionistic logic, =ACP asserts that a >proof of P is impossible." That's true in the context of consistent theories, which are really the only ones people are interested in. >According to your interpretation of intuitionistic truth, the >intuitonist will completely deny that there is any notion of >"absurdity", apriori or otherwise. No, they will say that "All things are provable" is absurd; any system that allows you to prove every statement is an absurd system. >In other words, according to you, the intuitionist does not see >any absurdity in the provability of P&~P I didn't say that. -- Daryl McCullough Ithaca, NY
From: Aatu Koskensilta on 19 Dec 2005 09:49 Daryl McCullough wrote: > sradhakr says... > >>http://en.wikipedia.org/wiki/Intuitionistic_logic >> >>Quoting from this site, >> >>"The interpretation of negation in intuitionistic logic is different >>from its counterpart in classical logic. In classical logic, ~P >>asserts that P is false; in intuitionistic logic, ~P asserts that a >>proof of P is impossible." > > That's true in the context of consistent theories, which are > really the only ones people are interested in. The proofs relevant to the intuitionistic understanding of negation are not formal proofs. -- Aatu Koskensilta (aatu.koskensilta(a)xortec.fi) "Wovon man nicht sprechen kann, daruber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Charlie-Boo on 19 Dec 2005 10:31 David C. Ullrich wrote: > On 16 Dec 2005 11:07:53 -0800, "Charlie-Boo" wrote: > All you have to do is explain what your notation means. [] means necessity. |- means provability. Since "There is an overwhelming diversity of systems of modal propositional logic. Their accounts of theorem differ from one another. [We can] take the box of modal logic to mean 'it is provable' rather than 'it is necessary'.'" (The Unprovability of Consistency, George Boolos) but |- always means provable, I use |- for provable rather than []. > >> Or, in extremely bad notation: |- (|-Q == Q) > >> (bad notation because the first |- means |-, while > >> the second |- refers to some encoding of provability) > >And [] ( []Q == Q ) ? > Is it extemely bad notation? No. Don't you see the parallel? If |- (|-Q == Q) is extremely bad notation because the first |- means |- while the second |- refers to some encoding of provability, then [] ( []Q == Q ) is extremely bad notation because the first [] means |- while the second [] refers to some encoding of provability. I'll have to break the bad news to Boolos, Kripke, Solovay et, al. > >( P = |- Q) => ( P = |-P) because P must be r.e. > Uh, this is gibberish. A set of natural numbers is or is not > r.e. What the hell does it mean to say that a wff is r.e.? Since the relation (over its free variables) |-Q is recursively enumerable for any Q, and P = |-Q, then relation P is recursively enumerable. (Wffs express relations.) > "red herrings about syntax". Right. There's nothing more trivial than a purported syntax error, yet you use it to trump all other considerations and proof that the author doesn't know anything about the subject. And when you consider the fact that there is so little formal standardization in logic (there is no ANSI for mathematicians), it's silly to even claim that a certain syntax can't be used because it is not "standard". I once surveyed about 20 proofs of the Recursion Theorem to determine the most common syntax used to express it. I couldn't. Every proof used a different syntax. Try it and you'll see. Even referring to "Godel's 1st. Incompleteness Theorem" is wrong, because there are two 1st. theorems in Godel's 1931 paper - based on soundness and based on w-consistency. (Someone once published a survey of syntaxes used in logic and the variations were enormous. Also note the Boolos quote above.) A more productive attitude is "Let's represent . . . with the syntax . . . as that is probably more commonly used. Then . . ." > > 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. > ************************ > > David C. Ullrich
From: David C. Ullrich on 19 Dec 2005 11:27
On 19 Dec 2005 07:31:22 -0800, "Charlie-Boo" <chvol(a)aol.com> wrote: I don't know whether you've noticed this, but others have: 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... >David C. Ullrich wrote: >> On 16 Dec 2005 11:07:53 -0800, "Charlie-Boo" wrote: > >> All you have to do is explain what your notation means. > >[] means necessity. |- means provability. Since "There is an >overwhelming diversity of systems of modal propositional logic. Their >accounts of theorem differ from one another. [We can] take the box of >modal logic to mean 'it is provable' rather than 'it is >necessary'.'" (The Unprovability of Consistency, George Boolos) >but |- always means provable, I use |- for provable rather than []. Yes, we can take [] to represent various things, including provability. What's your point? Did I say we couldn't do that? (Was I supposed to know somehow that that's what you meant by the [] below?) >> >> Or, in extremely bad notation: |- (|-Q == Q) >> >> (bad notation because the first |- means |-, while >> >> the second |- refers to some encoding of provability) > >> >And [] ( []Q == Q ) ? > >> Is it extemely bad notation? No. > >Don't you see the parallel? If |- (|-Q == Q) is extremely bad >notation because the first |- means |- while the second |- refers to >some encoding of provability, then [] ( []Q == Q ) is extremely bad >notation because the first [] means |- while the second [] refers to >some encoding of provability. Oh for heaven's sake. How was I supposed to know that that two []'s meant entirely different things? Yes, if that's the case then it's extremely bad notation. _Incredibly_ bad notation, actually. It's been pointed out that when you use |- to mean two different things that makes things impossible to parse. You decide to introduce a new symbol for |-. Instead of taking advantage of the new symbol by letting it denote one thing and letting |- denote the other thing you decide that the new symbol should _also_ mean two things. Good idea. >I'll have to break the bad news to Boolos, Kripke, Solovay et, al. Do they use one symbol two mean two different things in the same expression? I doubt it. >> >( P = |- Q) => ( P = |-P) because P must be r.e. > >> Uh, this is gibberish. A set of natural numbers is or is not >> r.e. What the hell does it mean to say that a wff is r.e.? > >Since the relation (over its free variables) |-Q is recursively >enumerable for any Q, and P = |-Q, then relation P is recursively >enumerable. (Wffs express relations.) This is gibberish. |-Q is not a wff, it has no free variables. It is an assertion about a wff. >> "red herrings about syntax". Right. > >There's nothing more trivial than a purported syntax error, yet you >use it to trump all other considerations and proof that the author >doesn't know anything about the subject. And when you consider the >fact that there is so little formal standardization in logic (there is >no ANSI for mathematicians), it's silly to even claim that a certain >syntax can't be used because it is not "standard". I haven't said you couldn't use any particular notation. I _said_ all you had to do was explain what the notation meant. But one thing you _cannot_ do is use one notation to mean two different things. Complaining about that is not complaining that you're not using the right symbols for concepts, it's complaining that you're insisting on using an _ambiguous_ syntax. This is really a pretty feeble response to my explanations of why, once we sort out what you mean, the things you've been saying are nonsense. >I once surveyed about 20 proofs of the Recursion Theorem to determine >the most common syntax used to express it. I couldn't. Every proof >used a different syntax. Try it and you'll see. Even referring to >"Godel's 1st. Incompleteness Theorem" is wrong, because there are >two 1st. theorems in Godel's 1931 paper - based on soundness and >based on w-consistency. (Someone once published a survey of syntaxes >used in logic and the variations were enormous. Also note the Boolos >quote above.) > >A more productive attitude is "Let's represent . . . with the >syntax . . . as that is probably more commonly used. Then . . ." > >> > 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 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. >> ************************ >> >> David C. Ullrich ************************ David C. Ullrich |