Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from antares.mcs.anl.gov (actually antares9.mcs.anl.gov !OR! owner-qed@mcs.anl.gov) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Sun, 14 Aug 1994 18:48:10 +0100
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 <qed@mcs.anl.gov>; 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: <m0qZjam-0003TrC@emu.pmms.cam.ac.uk>
Date: Sun, 14 Aug 94 18:43 BST
From: Thomas Forster <T.Forster@pmms.cam.ac.uk>
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