Formalization is often presented (1) as a further stage after axiomatization. (It is often said that euclidian geometry was already axiomatized, but not yet formalized ( or not enough), and that the complete formalization of geometry was only achieved much later, by Tarsky for example) (2) it is is also presented as the full completion of axiomatization.
Reference : " if geometry is to be deductive, the deduction must everywhere be independant of the meaning of geometrical concepts , just as it must be independant of the diagrams; only the relations specified in the propositions and definitions employed may legitimately be taken into account" Pasch ( quoted by Wilder, Introduction To The Foundations Of Mathematics, Part I The axiomatic method, I, §1 Evolution of the method. )
My question is : why is this further stage needed? why formalizing mathematics? ( what is the interest in ordinary mathematical practice? why should a fully axiomatized mathematical theory be also formalized?)
Remark.- My question is not equivalent to " is the formalist view of mathematics correct?" I'm looking for an answer mathematicians could agree on , whatever might be their own commitment to a particular philosophy of mathematics?
Best Answer
It's misleading to say that Euclid axiomatized Euclidean geometry. He tried, but used so many undefined and ambiguous terms that it's only fair to say that he failed. Still, he was the first to give a good try. However, it was not until mathematicians had a proper notion of first-order logic (both its syntax and semantics), that proper axiomatization could really begin. And only when they started treating syntactic objects, namely finite strings of symbols, themselves as mathematical objects, could they actually start expressing the notion of formalization as a mathematical notion.
And only then can we prove mathematical facts about formal systems, rather than just prove mathematical facts within some foundational system. I believe Mauro was alluding to such a distinction in his comments, in that Hilbert's axiomatization of geometry was an attempt to assert axioms within an overarching (and unspecified) foundational system, and not a stand-alone axiomatization of Euclidean geometry unlike Tarski's.
Furthermore, your question has the false premise that Tarski's axiomatization of Euclidean geometry is a completion of Hilbert's. It's not! Tarski's theory is in fact complete and decidable, whereas any reasonable presentation of Hilbert's is neither (roughly because Hilbert's axioms involved the natural numbers, and any reasonable axiomatization of the natural numbers is essentially incomplete).
But anyway, the goal of axiomatization of a structure is to make fully precise what are the assumptions we are using about that structure, when we prove properties of that structure. And the goal of formalization of any system (not just first-order theories) is usually to define it precisely within the foundational system itself. Typically all we need is that it can be captured by a total program, but many times we can even capture it by a primitive recursive program. For example, PA has a proof verifier program, which is one key reason why it is essentially incomplete.
In short: If you don't formalize a system, you can still use it but you can't study it!