Re: Remarks on David's Mail of Oct. 25

Konrad Slind (
Mon, 7 Nov 1994 19:54:25 +0100

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.


Forwarded: Fri, 07 Jan 1994 08:57:22 -0600
Forwarded: "mccune "