[FOM] Formalization Thesis

S. S. Kutateladze sskut at math.nsc.ru
Fri Dec 28 02:26:52 EST 2007

Timothy Y. Chow asks

... does that mean that you concede the point about category theory
 and are arguing only that model theory cannot be accurately captured by
set-theoretic statements?
No it  does not. Model theory includes reflections about formal
theories and their relations to the core of mathematics.

Timothy Y. Chow asks:
Do you claim, then, that
 while theorems of all other branches of mathematics (group theory, number
 theory, topology, analysis, ...) can be translated into (say) Mizar and
formally verified, theorems of model theory cannot be so translated?


I explain simply that  all branches of mathematics cannot be translated
fully neither into set theory  nor into any unique formal theory.
Category theory yields an illustration, as well as model theory.

Your thesis is definitely precise  when you speak of ZFC, but
obviously false. It is senseless or banal on  calling the quest for precision quibbling.
Euclid was and will ever be a piece of mathematics but
his Elements lacks the definition of triangle. His formalization was
not final. There are no grounds to believe that the present-day formalizations
are final either.

This is not anyone's radical claim. It is a lesson of history.

Sobolev Institute of Mathematics
Novosibirsk State University
            mailto: sskut at math.nsc.ru
            copyto: sskut at academ.org       

More information about the FOM mailing list