FOM: ultrafinitism

[Kanovei]

> Date: Thu, 2 Nov 2000 01:58:52 +0100
> From: Robert Black <Robert.Black at nottingham.ac.uk>
 
> Professors Sazanov and Kanovei both seem to be defending some form of
> ultrafinitism. That's fine, it's a good old Russian tradition, 

I don't know what "ultraintuitionism" is and what this has to do 
with "old Russian tradition", do you mean some Western tales around 
Dostoevsky ? 

> What is odd, though, is
> that they both seem to think that this viewpoint is just obviously true,

My point is that he who claims that there is (ontologically) a 
statement true but not provable, must present the statement 
and explain what the details of the assertion mean. 

> whereas it's (1) *radically* revisionary of what we ordinarily think  

Is this my request any way revisionary from the scientific standards ?

> (2) to my knowledge at least has never achieved any adequate formal
> expression

If you mean any formal theory which distinguishes truth and 
provability then there are plenty of them, but I have nothing to 
do with that.

> mathematical proof has to do with formal provability in, say, ZFC, and if
> the latter is to be understood not in terms of the existence of abstract
> structures but in terms of concrete, feasible proofs made of dried ink, 

Mathematical proofs can include components maintained in ink, 
in latex, as computer programs, at blackboard, in transparencies, 
in verbal explanations, ascii texts sent by email, etc., the 
physical carrier of the proof is not a topic of interest.

> there any reason at all to think that formalizations in ZFC of currently
> accepted proofs would fit into the universe?  

Specialists in computer provers may be interested in questions 
like this but 
what this has to do with the misthesis of "true but unprovable"? 

V.Kanovei