From owner-qed Fri Aug 19 06:08:52 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id GAA05260 for qed-out; Fri, 19 Aug 1994 06:05:39 -0500 Received: from svin07.win.tue.nl (root@svin07.win.tue.nl [131.155.70.232]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id GAA05254 for ; Fri, 19 Aug 1994 06:05:29 -0500 Received: from pc8012.win.tue.nl by svin07.win.tue.nl (8.6.8/1.45) id NAA18167; Fri, 19 Aug 1994 13:05:23 +0200 Date: Fri, 19 Aug 1994 13:03:52 From: debruijn@win.tue.nl (N.G. de Bruijn) To: boyer@CLI.COM, jt@linus.mitre.org, T.Forster@pnms.cam.ac.uk, Gerard.Huet@inria.fr, qed@mcs.anl.gov Subject: Automath restaurant Message-ID: Sender: owner-qed@mcs.anl.gov Precedence: bulk To:boyer@cli.com,jt@linus.mitre.org, T.Forster@pmms.cam.ac.uk, Gerard.Huet@inria.fr, qed@mcs.anl.gov N.G. de Bruijn to Robert S. Boyer Eindhoven, 19 August 1994. Dear Bob, In your message of 15 Aug 94 13:38:46 you write >In some of de Bruijn's informal writings, you find the remark >that Automath is like a cafeteria, which will serve all >mathematical customers. However, he adds, cryptically, that it >serves some customers much better than others. I think that >what that means is that you can in principle encode any theory, >including set theory in type theory, but you will make practical >progress much more happily if you use the "native" notion of >function in its natural, constructive way rather than encoding >your own notion of function. Indeed, that was one of the things I meant. Another one is that in type systems like Automath the notion of elementhood can be seen as typing. Customers who like typed sets (let me call these customers TSC's) introduce a real variable by a single block opener, like "let x be a real number", where "real number" is taken as a type. So for the TSC's it is the introduction of a typed variable. The customers who prefer to think in terms of untyped sets (let me call them USC's), however, have to order by means of two block openers: "let x be a set" and "assume this x is a real number". In their case we have to realize that "x is a real number" is a property of the set x. The first one of the two block openers is the introduction of a typed variable (where the type is "set"), the second one is an assumption. I do not think the TSC's have anything to complain. It is not the fault of the restaurant that they get what they order. And they can enjoy their food all the same. They get it served with some extra plates and extra cutlery, but who cares? One gets accustomed to such little inconveniences, in particular when they are automated. Another matter is that I think that although many mathematicians have been taught to say that they are USC's, they entirely behave like TSC's. Few of them are fundamentalists. In his note "Types Considered Harmful" L. Lamport writes > Here, we can only assure the reader that mathematicians have gotten > along quite well for two thousand years without types, and they > still can today. Modifying a well-known joke, it makes me remark that history is a tricky subject, in particular if it is about the past. History is just a picture we have. My own picture is the other way round. I think that before Cantor no mathematician would have interpreted his mathematical objects as untyped sets. That idea evolved in the first half of the 20th century among logicians. And today? Since the teaching of Bourbaki very many pure mathematicians feel that they should think that all their objects are untyped sets, but what does that really mean for them? Talking about fundamentalists, I think that the USC's are not yet fundamental enough. There are several things that Platonists would call "ideas" and that have not been coded as sets yet. Candidates may be propositions, proofs, theorems, axioms, definitions, contexts, theories. But the owner of the restaurant does not care much about the tastes or the historic insights of his customers. They can all get what they order. Even if they would order a number of contradictory items, it would be entirely their own responsibility. By the way, I always talked about a restaurant, and not about a cafeteria. The well-known prototype on 42nd Street (at the intersection with 3rd Avenue?) in New York City is called AUTOMAT, without H. Yours, N.G. de Bruijn. N.G. de Bruijn, emeritus professor of mathematics e-mail address(at University): wsdwnb@win.tue.nl Office address (I am there at most twice a week) EINDHOVEN UNIVERSITY OF TECHNOLOGY Department of Mathematics and Computing Science PO Box 513, 5600 MB EINDHOVEN, The Netherlands FAX 31-40-436685, TELEX 51163 Home address Eikenlaan 2, 5671AB Nuenen, The Netherlands Tel. 31-40-831650 ------------------------------------------------------------