[FOM] Formalization Thesis - questions

[Vladimir Sazonov]

catarina dutilh wrote:

> 1. At some point somebody remarked (I forgot who it was) that 
> formalizations may come in degrees, i.e. that something (a proof, an 
> argument, a theory) can be more formal(ized) that something else, and 
> yet, less formal(ized) than a third thing. Does this sound right?


I did not follow everything in this thread. But it seems it was I who 
discussed something like that in my first posting with the subject 
"Formalization Thesis vs Formal nature of mathematics"

1. My first idea was that we can formalize only something informal (our 
intuition).

2. "Formal" or "rigorous" in mathematics means separation of the form 
of our reasoning from its content (the intuition, imagination, etc.) 
and checking correctness of the reasoning only on the base of its form.

3. The categories of form vs content are rather general. The formal 
systems like FOL, PA, ZFC are only a limit case of the general idea of 
form.

4. Mathematics was always (sufficiently) formal in this general sense, 
however possibly far from the contemporary limit case mentioned above. 
Thus, we can speak on degrees of formality.

5. But nowadays, when we know the limit concept of formality when 
correctness of proofs can be checked (in principle) by computer, any 
mathematical proof (as always written rather informally, or formally in 
the above general sense) is confirmed as genuine mathematical only if 
we are sure that the problem of its full or "absolute" formalization 
(to be checked by computer) is evidently resolvable. This is just the 
question of time and perseverance. Typically this assurance is 
considered as sufficient and mathematicians do nothing for full 
formalization. Anyway, when a proof is accepted to be mathematical in 
the contemporary sense of this word this means that it is fully 
formalizABLE. (I know NO exception to this thesis.)

6. By this reason I do not understand Formalization Thesis. This is 
TAUTOLOGY: Any mathematical (i.e. fully formalizable) proof is fully 
formalizable. The only real question (requiring only time and 
perseverance) is to present the full formalization (which evidently 
exists once it was confirmed - in our time - that the proof is 
mathematical).

7. Therefore, instead of Formalization Thesis I prefer to consider more 
fundamental question on Formal nature of mathematics (or on Formalist 
View on Mathematics, FVM).


Vladimir Sazonov

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