From owner-qed Thu Aug 25 06:07:54 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id GAA19722 for qed-out; Thu, 25 Aug 1994 06:05:58 -0500 Received: from ANLVM.CTD.ANL.GOV (anlvm.ctd.anl.gov [146.137.96.2]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id GAA19715 for ; Thu, 25 Aug 1994 06:05:53 -0500 Date: Thu, 25 Aug 1994 06:05:53 -0500 From: <@ANLVM.CTD.ANL.GOV:POSTMAST@PLEARN.EDU.PL> Resent-Message-Id: <199408251105.GAA19715@antares.mcs.anl.gov> Message-Id: <199408251105.GAA19715@antares.mcs.anl.gov> Received: from ANLVM by ANLVM.CTD.ANL.GOV (IBM VM SMTP R1.2.2ANL-MX) with BSMTP id 1682; Thu, 25 Aug 94 06:05:43 CDT Received: from PLEARN.EDU.PL by ANLVM (Mailer R2.07B) with BSMTP id 8705; Thu, 25 Aug 94 06:05:43 CDT Received: from PLEARN.BITNET (NJE origin POSTMAST@PLEARN) by PLEARN.EDU.PL (LMail V1.2a/1.8a) with BSMTP id 0593; Thu, 25 Aug 1994 13:06:52 +0200 Resent-Date: Thu, 25 Aug 94 13:06:44 CET Resent-From: POSTMAST%PLEARN.BITNET@ANLVM.CTD.ANL.GOV Resent-To: qed@mcs.anl.gov Apparently-To: Sender: owner-qed@mcs.anl.gov Precedence: bulk HELO ANLVM TICK 3817 MAIL FROM: RCPT TO: 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 ; 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