From owner-qed Thu Aug 25 09:21:45 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id JAA23290 for qed-out; Thu, 25 Aug 1994 09:21:32 -0500 Received: from life.ai.mit.edu (life.ai.mit.edu [128.52.32.80]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id JAA23283 for ; Thu, 25 Aug 1994 09:21:25 -0500 Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI-4.10) for qed@mcs.anl.gov id AA03903; Thu, 25 Aug 94 10:21:23 EDT From: dam@ai.mit.edu (David McAllester) Received: by spock (4.1/AI-4.10) id AA00961; Thu, 25 Aug 94 10:21:22 EDT Date: Thu, 25 Aug 94 10:21:22 EDT Message-Id: <9408251421.AA00961@spock> To: sf@CSLI.Stanford.EDU Cc: qed@mcs.anl.gov, sf@CSLI.Stanford.EDU In-Reply-To: Solomon Feferman's message of Wed, 24 Aug 94 18:02:44 PDT Subject: Types, sorts and variable types Sender: owner-qed@mcs.anl.gov Precedence: bulk What will be important is to have a rich formal language which reflects the everyday world of mathematics, where there is no concern with the "ultimate" building blocks of mathematical concepts (as many suppose sets and membership to be). Then one has to inquire what principles are commonly appealed to in a given body of mathematics when it comes to representing and checking proofs. The first part would be akin to what some people have tried to do in AI with the representation of common-sense knowledge. Can I rephrase this as "definitions form the foundation" and "definitions should be natural"? David McAllester