From owner-qed Sun Aug 14 14:50:44 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id OAA05687 for qed-out; Sun, 14 Aug 1994 14:49:57 -0500 Received: from linus.mitre.org (linus.mitre.org [129.83.10.1]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id OAA05682 for ; Sun, 14 Aug 1994 14:49:51 -0500 Received: from nausicaa.mitre.org (nausicaa.mitre.org [129.83.10.45]) by linus.mitre.org (8.6.7/RCF-6S) with ESMTP id PAA10432; Sun, 14 Aug 1994 15:49:47 -0400 Received: from localhost (localhost [127.0.0.1]) by nausicaa.mitre.org (8.6.7/RCF-6C) with ESMTP id PAA03690; Sun, 14 Aug 1994 15:49:46 -0400 Message-Id: <199408141949.PAA03690@nausicaa.mitre.org> To: qed@mcs.anl.gov cc: jt@linus.mitre.org Subject: Re: set theory vs type theory Date: Sun, 14 Aug 1994 15:49:44 -0400 From: "F. Javier Thayer" Sender: owner-qed@mcs.anl.gov Precedence: bulk -------- Type theory offers a lot of structure to allow indexing schemes for theorems and to provide hints and cues for applicability of these known theorems. For instance, IMPS uses these cues extensively in its macete lookup mechanism. Unfortunately, much of mathematics is hard to encase within a fixed type system. For instance, most of topology or geometry cannot be considered the study of a single toplogical or geometric object. In fact, it is frequently the case that one considers whole families of the these objects. I don't know how to treat these within a simple type theory without fundamentally cheating (that is, without establishing some imbedding of them in set theory.) This problem is especially annoying if one is to handle in a conventional way any of the structure theorems of basic mathematics, such as the structure theorem for finitely generated abelian groups.