[FOM] Proof. was: Checkers is a draw
Vladimir Sazonov
V.Sazonov at csc.liv.ac.uk
Sun Jul 29 14:07:37 EDT 2007
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.
More information about the FOM
mailing list