Types, sorts and variable types

Solomon Feferman (@ANLVM.CTD.ANL.GOV:POSTMAST@PLEARN.EDU.PL)
Thu, 25 Aug 1994 06:05:53 -0500

HELO ANLVM
TICK 3817
MAIL FROM:<owner-qed@mcs.anl.gov>
RCPT TO:<ROMAT@PLEARN>
DATA
Received: from ANLVM by ANLVM (Mailer R2.07B) with BSMTP id 3817; Fri, 19 Aug
94 08:23:17 CDT
Received: from antares.mcs.anl.gov by ANLVM.CTD.ANL.GOV (IBM VM SMTP
R1.2.2ANL-MX) with TCP; Fri, 19 Aug 94 08:23:16 CDT
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 <qed@mcs.anl.gov>;
Fri, 19 Aug 1994 08:22:23 -0500
Date: Fri, 19 Aug 94 08:22:22 -0500
From: kunen%cs.wisc.edu@ANLVM.CTD.ANL.GOV (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

----------------------------Original message----------------------------

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