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
------------------------------------------------------------