From owner-qed Mon Nov 7 12:57:22 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id MAA20709 for qed-out; Mon, 7 Nov 1994 12:55:30 -0600 Received: from tuminfo2.informatik.tu-muenchen.de (root@tuminfo2.informatik.tu-muenchen.de [131.159.0.81]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id MAA20694 for ; Mon, 7 Nov 1994 12:55:06 -0600 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <326453-2>; Mon, 7 Nov 1994 19:54:36 +0100 Received: by sunbroy14.informatik.tu-muenchen.de id <8082>; Mon, 7 Nov 1994 19:54:29 +0100 From: Konrad Slind To: qed@mcs.anl.gov In-reply-to: <9411071751.AA01103@spock> (dam@ai.mit.edu) Subject: Re: Remarks on David's Mail of Oct. 25 Message-Id: <94Nov7.195429met.8082@sunbroy14.informatik.tu-muenchen.de> Date: Mon, 7 Nov 1994 19:54:25 +0100 Sender: owner-qed@mcs.anl.gov Precedence: bulk David McAllester writes: > Ultimately I agree with de Bruijn that mathematics is just language > (plus a brain for manipulating mentalese). But language can be > Platonic or formal. For me, Platonic language is easier to think > with. That may well be true, but I think that formalism creeps in as soon as you have to share your thoughts with others. And that's what QED is supposed to be about. So what are these Platonic objects that all of our proof systems are supposed to evince a shared understanding of? >From the point of view of a QED user, "Platonism" or "mentalese" is nothing more than the feeling one would get from using a good (perhaps unrealizably good) implementation. Konrad.