Return-Path: 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; Fri, 28 Oct 1994 12:28:50 +0000 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 ; 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