From owner-qed Fri Oct 28 07:22:19 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id HAA10065 for qed-out; Fri, 28 Oct 1994 07:20:54 -0500
Received: from compu735.mathematik.hu-berlin.de (compu735.mathematik.hu-berlin.de [141.20.54.12]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id HAA10056 for <qed@mcs.anl.gov>; Fri, 28 Oct 1994 07:20:12 -0500
Received: from kummer.mathematik.hu-berlin.de by compu735.mathematik.hu-berlin.de with SMTP
	(1.37.109.8/16.2/4.93/main) id AA09804; Fri, 28 Oct 1994 13:19:31 +0100
Received: from wega.mathematik.hu-berlin.de by mathematik.hu-berlin.de (4.1/SMI-4.1/JG)
	id AA10719; Fri, 28 Oct 94 13:19:40 +0100
Date: Fri, 28 Oct 94 13:19:40 +0100
From: dahn@mathematik.hu-berlin.de (Dahn)
Message-Id: <9410281219.AA10719@mathematik.hu-berlin.de>
To: qed@mcs.anl.gov
Subject: Re: The value of Platonism
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

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

There are no Platonic proofs - just correct or incorrect proofs.

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

Modifying a remark by Bertolt Brecht:
Ask yourself: Does Platonism change the way you prove theorems?
If not - the problem is irrelevant,
If yes - you need Platonism.

> 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.
This is important! Verification systems can (in general) only talk about rules of inference - but they should hide this carefully from the normal QED user. The same way your mailtool makes you think you read a letter when you are actually looking at a bitstream.

Ingo Dahn