From owner-qed Fri Aug 19 08:22:54 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id IAA07485 for qed-out; Fri, 19 Aug 1994 08:22:29 -0500
Received: from head.cs.wisc.edu (head.cs.wisc.edu [128.105.9.41]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id IAA07480 for ; Fri, 19 Aug 1994 08:22:23 -0500
Date: Fri, 19 Aug 94 08:22:22 -0500
From: kunen@cs.wisc.edu (Ken Kunen)
Message-Id: <9408191322.AA06591@head.cs.wisc.edu>
Received: by head.cs.wisc.edu; Fri, 19 Aug 94 08:22:22 -0500
To: qed@mcs.anl.gov
Subject: types
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
N.G. de Bruijn says:
>> 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?
What it means is that we understand:
1. All of standard math can, in theory, be formalized within ZFC.
2. Doing so would be extremely painful in practice.
The importance of (1) is that to prove an independence result, such as:
CH is independent of "standard mathematical reasoning" ,
we need only produce a model for:
ZFC + not CH,
which is a fairly simple theory in ordinary untyped predicate logic.
This is a lot easier than working with models for a logic with
some complex type structure.
Fact (2) doesn't bother mathematicians, since in practice they
never formalize anything, so they are happy to be aware of (1)
and continue to think informally in terms of types.
Even books (such as mine) on pure set theory often use typing to facilitate
the exposition. For example, borrowing from Fortran, we say:
"we use Greek letters alpha,beta,gamma ... to vary over ordinals".
Ken Kunen