rance@cornell.UUCP (W. Rance Cleaveland) (07/08/85)
> EVERYONE should know how to do proofs with quantifiers! For one thing, it's > taught in the introductory CS math courses most places, and for another, > it'll probably be on that test you're going to take, if it's any good... > I mean, everyone should know that > > "For all x, y" > > is the same as > > "It is not the case that there exists an x such that not(y)". Sorry to be pedantic, but when one's thesis topic comes up, can one help it? Mr. Roskos has (un?)knowingly raised a philosophical issue which has caused a great deal of acrimony among logicians and foundational mathematicians for at least a century, the issue being "should logic be constructive?" In layman's terms, the debate turns on whether, as so-called classical logicians say, establishing the truth of something is the same as establishing that the negated statement is false, or whether, as constructive (or "intuitionistic") logicians say, establishing the truth of something requires that you, well, establish the truth of something. To use Mr. Roskos' example, proving "For all x, y" classically reduces to proving "There does not exist an x such that not(y)" while constructively proving the former statement requires that one pick an arbitrary x and prove y (since x is arbitrary, the proof that y holds will work for any x, hence all x.). The difference? In the above example, the constructive philosophy requires that we give a procedure for proving y for any x, while the classical frame- work has no such requirement. In this sense then, constructive logic has an inherent computational flavor, while constructive logic does not.... Yeah, this probably doesn't belong on net.singles; at least, I've never had any success starting a romantic conversation with "Whose your favorite logi- cian?" Still, maybe some of you out there.... |-). Regards, Rance Cleaveland
bill@persci.UUCP (07/09/85)
In article <2958@cornell.UUCP> rance@cornell.UUCP (W. Rance Cleaveland) writes: >[...] >Yeah, this probably doesn't belong on net.singles; at least, I've never had >any success starting a romantic conversation with "Whose your favorite logi- >cian?" Maybe not, but I had *fantastic* success once with: "Why do you hate computers?" (Well, circumstances dictated it.. I just followed through..) -- Bill Swan {ihnp4,decvax,allegra,...}!uw-beaver!tikal!persci!bill
dgary@ecsvax.UUCP (D Gary Grady) (07/09/85)
> Yeah, this probably doesn't belong on net.singles; at least, I've never had > any success starting a romantic conversation with "Whose your favorite logi- > cian?" Still, maybe some of you out there.... |-). > > Regards, > Rance Cleaveland An introductory logic book I've seen quotes a hilarious episode from the book "The Many Loves of Dobie Gillis" (I think that's right) by Max Shulman. In it, Dobie resolves to secure the ideal wife by finding an attractive woman and teaching her to be logical (believing this to be an easier course than the reverse). The woman he pursues is his roommate's girlfriend. He persuades the roommate to give her up by offering him a raccoon coat (a recent fad at their college) as a bribe. Then Dobie proceeds to indoctrinate the young lady in logic both formal and material. All goes well until the day she announces she's returning to her old flame, the roommate. Dobie is crushed and tries to talk her out of it, but for each plea he makes, the woman spouts a rejoinder identifying the logical fallacy in his argument. "Argumentum ad misericordiam," she scolds. "Argumentum ad hominem. Argumentum ad vericumdiam." Finally, defeated, he asks her what reason she would have to go back to his roommate. "It's simple," she tells him. "He owns a raccoon coat." -- D Gary Grady Duke U Comp Center, Durham, NC 27706 (919) 684-3695 USENET: {seismo,decvax,ihnp4,akgua,etc.}!mcnc!ecsvax!dgary
jer@peora.UUCP (J. Eric Roskos) (07/09/85)
Gee, I didn't know there were any intuitionists out there. I remember references to intuitionistic logic in Mendelson's text, though they were just cursory. >Yeah, this probably doesn't belong on net.singles; at least, I've never had >any success starting a romantic conversation with "Whose your favorite logi- >cian?" Still, maybe some of you out there.... |-). I have, though! In fact, that is close to how I met my most recent SO; one day I was working on the University computer, and saw this person who had "Logical" in her login name. So I asked her, "What kind of logic does a Logical <name> use?" And this was how we met. Now... to get down to what you were talking about here... I have some reservations about claiming that there is any problem with my stating the "classical" notion that A(x)y <=> ~E(x)~y; I mean, you can make complete & consistent logics that contain the above, can't you? It seems to me merely a philosophical question; the fact that the logics exist and are "ok" in this formal sense should be enough as far as mathematics is concerned, I would think. > Mr. Roskos has (un?)knowingly raised a philosophical issue ^^ >The difference? In the above example, the constructive philosophy requires >that we give a procedure for proving y for any x, while the classical frame- >work has no such requirement. In this sense then, constructive logic has an >inherent computational flavor, while constructive logic does not.... I am not much of an expert on this constructive logic, but don't there exist proofs for which no effective procedure exists? Consider any theorem containing an existential quantifier which can only be proved by choosing elements out of the universe at random and trying them to see if they make the quantified predicate "true"; e.g., theorems that say something like "There exists a number with property x," where it is not possible to compute the number given the property effectively. Or does this relate to the question of whether there exist any languages recognizable by a nondeterministic finite-state automaton that aren't recognizable by a deterministic one in polynomial time? I am not sure, though there seem to be vague analogies there, since the epsilon- transitions in an NFA are roughly analogous to "guesses," as are (I think) the non-polynomial equvalent DFAs (which just try all the guesses by enumeration rather than by nondeterministic transitions). But I don't know for sure... it has been several years since I studied that stuff, and now I am left with mostly just the intuitive recollections... If you post a reply to this (which will go to net.math), please mail me a copy too, since I don't read net.math, since I'm not a mathematician really. -- Shyy-Anzr: J. Eric Roskos UUCP: ..!{decvax,ucbvax,ihnp4}!vax135!petsd!peora!jer US Mail: MS 795; Perkin-Elmer SDC; 2486 Sand Lake Road, Orlando, FL 32809-7642 "Gurl zhfg hcjneq fgvyy, naq bajneq, Jub jbhyq xrrc noernfg bs gehgu." -- WEY
rance@cornell.UUCP (W. Rance Cleaveland) (07/10/85)
> Classical logic is indeed consistent and complete (as, indeed, are many logics) and you are right that the "problem" I allude to is a philosophical one. On the other hand, I believe that one should approach logic first from a philosophical perspective and decide first what sorts of intuitive underpinings one wants one's notion of logic to have. Classical logic takes truth as a given, which is to say that truth is defined in terms of truth valuations ("truth tables"). In this setting, then, a proposition must either be true or false, and it is this requirement which gives some of us pause. Constructive logic, on the other hand, defines truth as provability; we know only that which we can prove, and we prove things by giving constructions. What I'm trying to say, I guess, is that while completeness and consistency are certainly germane to the dis- cussion of logics, other issues are important as well. Incidentally, Ax(y) <=> -Ex(-y) is not true constructively because it cannot be proven constructively, that is, without recourse to the law of the excluded middle. Intuitively, the constructions which establish the truth of either side of the bi-implication are inherently different, and while one for Ax(y) can be translated into one for -Ex(-y), thereby establishing Ax(y)=>-E(-y), the converse does not hold. Historically, constructive logic was de rigeur until the time of Cantor (late 1800's). For the Greeks, for instance, truth reduced to constructibility with a compass and straight-edge, and until Cantor began talking about point sets and sets of sets mathematicians were under tremendous peer pressure to give constructive accounts of their work. (Cantor in fact was sharply crit- cized by many of his contemporaries for his unorthodox work, and several authors have speculated that the professional ostracism he underwent con- tributed to his ultimate mental breakdown.) > >The difference? In the above example, the constructive philosophy requires > >that we give a procedure for proving y for any x, while the classical frame- > >work has no such requirement. In this sense then, constructive logic has an > >inherent computational flavor, while constructive logic does not.... > > I am not much of an expert on this constructive logic, but don't there exist > proofs for which no effective procedure exists? Consider any theorem > containing an existential quantifier which can only be proved by choosing > elements out of the universe at random and trying them to see if they make > the quantified predicate "true"; e.g., theorems that say something like > "There exists a number with property x," where it is not possible to compute > the number given the property effectively. > Constructively proof is equivalent to procedure, so this point is moot in a constructive setting. However, in the situation you describe to prove an existentially quantified statement in the manner you propose you must give some assurance that eventually you will pick a number satisfying property x. If you can demonstrate that this process terminates then you have given an effective procedure for computing x, and constructively you are fine. > Or does this relate to the question of whether there exist any languages > recognizable by a nondeterministic finite-state automaton that aren't > recognizable by a deterministic one in polynomial time? I am not sure, > though there seem to be vague analogies there, since the epsilon- > transitions in an NFA are roughly analogous to "guesses," as are (I think) > the non-polynomial equvalent DFAs (which just try all the guesses by > enumeration rather than by nondeterministic transitions). But I don't know > for sure... it has been several years since I studied that stuff, and now > I am left with mostly just the intuitive recollections... > > -- Ah, P=NP. There's not really any connection between complexity theory and logic, except that some logics yield inherently more complex proofs than others.... (For someone who hasn't studied the stuff in a while, thought, your recollections are admirable :-)). Regards, Rance Cleaveland
simon@psuvax1.UUCP (Janos Simon) (07/19/85)
<3033@cornell19 Jul 85 17:56:15 GMT Reply-To: simon@psuvax1.UUCP (Janos Simon) Organization: Pennsylvania State Univ. Lines: 18 Xref: cadre net.math:829 Summary:Connection between logic and complexity [] This is probably getting way too technical, but the statement in <3033@cornell> that complexity theory has nothing to do with logic is false ( Didn't Juris teach you that at Cornell ? :-) ). In fact, the historic paper by Cook on NP is called "The complexity of theorem-proving procedures". More to the point, a complete problem for co-NP (languages with their complement in NP) is to decide whether a boolean formula is a tautology. At the same time, short, effective proofs are essentially NP. So, if there is a proof method for tautologies that yields short proofs that can be checked easily, NP=co-NP (and conversely). There are many results along these lines - the most recent, and most exciting is the thesis by Buss (abstract in the latest STOC proceedings) where he proves that in some logics (weak theories of arithmetic) certain objects are defineable iff things like P=NP happen. So, a possible proof that P\=NP could have the form "it is impossible to prove, using these axioms, this theorem" js
rance@cornell.UUCP (W. Rance Cleaveland) (07/23/85)
> This is probably getting way too technical, but the statement in <3033@cornell> > that complexity theory has nothing to do with logic is false ( Didn't Juris > teach you that at Cornell ? :-) ). > > In fact, the historic paper by Cook on NP is called > "The complexity of theorem-proving procedures". More to the point, a complete > problem for co-NP (languages with their complement in NP) is to decide whether > a boolean formula is a tautology. Hmm. I think you misunderstood my remarks about the connection between logics and complexity (maybe I wasn't as clear as I could have been). My point was that the question of constructive vs classical logic has no real con- nection with complexity theory. There are certainly many interesting problems in classical (i.e. truth-valued) logic which have implications in complexity theory (and yes, we learn all about them at Cornell).... Regards, Rance Cleaveland