[FOM] Proof. was: Checkers is a draw

[Vladimir Sazonov]

Quoting Bill Taylor <W.Taylor at math.canterbury.ac.nz> Sun, 29 Jul 2007:

> OC the ultrafinitist, wrapped up in semi-formal notions of feasibility,
> will insist that the "in principle"s above are REAL distinctions, and will
> cut his formal cloth appropriately; but most of the rest of us have no
> difficulty with the "in principle" concept, and will regard journal
> proofs as real proofs, even though strictly formally they fall short.

If to consider that "in principle" means "in principle feasible" and to 
admit what contemporary computers can do as feasible then, I think, 
this will impose no real restrictions on the mathematical practice. 
Also any proofs which are non-feasible in this sense (like those 
obtained after cut elimination) can be treated metamathematically (as 
feasible proof of non-feasible proof existence). Additionally, any kind 
of abbreviations used in proofs can be treated as explicitly included 
in the formal rules of logic making therefore easier the full and 
feasible formalizability.

Of course requiring from mathematical proofs to be absolutely formal 
(that is, not only potentially formalizable) would be killing for 
mathematics. It is not so much like to computer programming where 
potential formalizability is insufficient. But for mathematics this is 
unnecessary anyway.


Vladimir Sazonov


----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.