From owner-qed Thu Oct 27 13:14:05 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id NAA27906 for qed-out; Thu, 27 Oct 1994 13:13:45 -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 NAA27898 for <qed@mcs.anl.gov>; Thu, 27 Oct 1994 13:13:38 -0500
Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI-4.10) for qed@mcs.anl.gov id AA26061; Thu, 27 Oct 94 14:13:35 EDT
From: dam@ai.mit.edu (David McAllester)
Received: by spock (4.1/AI-4.10) id AA12927; Thu, 27 Oct 94 14:13:34 EDT
Date: Thu, 27 Oct 94 14:13:34 EDT
Message-Id: <9410271813.AA12927@spock>
To: qed@mcs.anl.gov
Subject: The value of Platonism
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

Well there has been a lot of discussion.  I'll just try to summarize
my position with four propositions.

1.  Thinking Platonically makes it easier (for people) to prove
theorems.

2.  Platonism is harmless --- all Platonic proofs can be formalized.

3.  Robots (verification systems) should be Platonists --- their statements
should be about "sets" and "functions" and they should never
talk about syntactic rules of inference when discussing "ordinary"
mathematics.

4. In summary, Platonism is desirable in every way.

	David