Re: The value of Platonism

Dahn (
Fri, 28 Oct 94 13:19:40 +0100

> 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