# [FOM] Formalization Thesis - questions

Thu Jan 3 20:16:51 EST 2008

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).