From owner-qed Sun Aug 14 12:44:51 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id MAA04844 for qed-out; Sun, 14 Aug 1994 12:44:25 -0500 Received: from emu.pmms.cam.ac.uk (emu.pmms.cam.ac.uk [131.111.24.1]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id MAA04839 for ; Sun, 14 Aug 1994 12:44:20 -0500 Received: by emu.pmms.cam.ac.uk (UK-Smail 3.1.25.1/1); Sun, 14 Aug 94 18:43 BST Message-Id: Date: Sun, 14 Aug 94 18:43 BST From: Thomas Forster To: boyer@CLI.COM, qed@mcs.anl.gov Subject: Re: set theory Sender: owner-qed@mcs.anl.gov Precedence: bulk The point is that type theory is unimplemented mathematics, and set theory is implemented mathematics. Which you want depends on what you are trying to do. Mostly (ask any mathematician!) you don't want set theory, but it does have its uses..... Thomas Forster