[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
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