Path: utzoo!attcan!uunet!mcvax!ukc!strath-cs!glasgow!jack From: jack@cs.glasgow.ac.uk (Jack Campin) Newsgroups: comp.ai Subject: Re: Fun with the semantics of paradox Message-ID: <2427@crete.cs.glasgow.ac.uk> Date: 15 Feb 89 13:47:47 GMT References: <1883@buengc.BU.EDU> <2996@uhccux.uhcc.hawaii.edu> <905@ubu.warwick.UUCP> <479@aipna.ed.ac.uk> <1036@hudson.acc.virginia.edu> <3715@uklirb.UUCP> <44071@linus.UUCP> <3091@silver.bacs.indiana.edu> <44270@linus.UUCP> <17219@iuvax.cs.indiana.edu> <44583@linus Reply-To: jack@cs.glasgow.ac.uk (Jack Campin) Organization: COMANDOS Project, Glesga Yoonie, Unthank Lines: 87 Summary: Expires: Sender: Followup-To: Keywords: > I was hoping to propel us into a journey of discovery of intuitionist > logic [...] If I understand Kripke's ideas, intuitionist logic admits a > powerful new method of proof based on a formalization of analogy. Firstly: intuitionistic logic is not Kripke's invention, as this seems to imply. He made important contributions to it in the mid-sixties but is hardly the dominating figure in it. It's a formalization, done by Arend Heyting before Kripke was born, of an approach to the foundations of mathematics due to L. E. J. Brouwer, dating back to 1920 or so. Secondly: it has NOTHING WHATEVER to do with analogy. It is a logic designed for an ontology of potentially infinite formal constructions. It even has something surprising to say about Rolle's Theorem, but I'm not going to say what. Read it up. The net is no place for detailed tutorials. Here are some places to look to find out more about it; they get tougher, and more recent, as you go down the list. There is a VAST literature on it, with connections to everything from the theory of meaning to polymorphically typed lambda calculus. Almost any book on the philosophy of mathematics will have something about it (usually borrowed from Heyting). A. Heyting: "Intuitionism - an introduction", North-Holland (short and zippy but predates the modern semantics of Beth and Kripke) M. A. E. Dummett: "Elements of Intuitionism", Oxford University Press (for the philosophical issues) M. C. Fitting: "Intuitionistic Logic Model Theory and Forcing", North- Holland (good for the Beth-Kripke semantics) D. van Dalen: article in volume II of the "Handbook of Philosophical Logic", D. Reidel (maybe the best introduction for logicians) D. Bridges and F. Richman: "Varieties of Constructive Mathematics", Cambridge University Press (more specifically mathematical) M. Beeson: "Foundations of Constructive Mathematics", Springer-Verlag (huge encyclopaedia) J. Lambek and P. J. Scott: "Introduction to Higher Order Categorical Logic", Cambridge UP (for the link with lambda calculus and the most recent semantics for intuitionistic logic) A. S. Troelstra & D. van Dalen: "Constructivism in Mathematics", North-Holland (a new and even huger encyclopaedia; I haven't seen this yet) J. L. Bell: "Toposes and Local Set Theories", Oxford UP (I haven't seen this yet; covers the same ground as Lambek & Scott, but Bell can write much more intelligibly than Lambek) > I suspect that intuitionists are reasoning by analogy when they turn up > those delicious true but underivable theorems. From an intuitionistic standpoint, this is gibberish. Intuitionists identify the notions of truth and proof; there is no transcendent arbiter of truth like a set-theoretic model. As there are many intuitionistic formalisms of varying degrees of power, naturally they don't all prove the same things; this also occurs in classical foundational approaches, but has different implications for an intuitionist, as they can't measure the success of a formalism by its degree of approximation to a divine cribsheet of mathematical truths. Intuitionists take two different attitudes to this problem. Brouwer thought there was no way to close off the limits of provability - mathematical ingenuity could always come up with new and stronger principles of proof, so statements are never definitively underivable. On the other hand people like Martin-Lof think there can be a final, definitive theory of all mathematics, and what it can't prove is meaningless (Martin-Lof said he'd found it, about five times :-). On either account, "true but unprovable" is a vacuous concept. There is one place where analogy comes into (classical) undecidability, but not *proof* by analogy. I posted Friedman's example of a PA-undecidable sentence to sci.logic two weeks ago; it is in a precise sense a finite analogue of a theorem about infinite objects. But Friedman's proof of its PA- undecidability - a proof using principles that would make any intuitionist's toes curl, incidentally - is not remotely an analogue of the infinitistic original, still less a "proof by analogy", and the analogy isn't what makes Friedman's theorem PA-undecidable. I don't believe there *are* any proofs by analogy, anyway. The whole point of logic is to undercut "obvious" analogies, like that between words of identical grammatical category, to show why you can't reason about them in the same way; aren't "proofs by analogy" all like: Nobody is taller than Jim Jim is taller than Mary so: Nobody is taller than Mary??? -- Jack Campin * Computing Science Department, Glasgow University, 17 Lilybank Gardens, Glasgow G12 8QQ, SCOTLAND. 041 339 8855 x6045 wk 041 556 1878 ho INTERNET: jack%cs.glasgow.ac.uk@nss.cs.ucl.ac.uk USENET: jack@glasgow.uucp JANET: jack@uk.ac.glasgow.cs PLINGnet: ...mcvax!ukc!cs.glasgow.ac.uk!jack