[FOM] Formalization Thesis
Timothy Y. Chow
tchow at alum.mit.edu
Thu Dec 27 22:59:51 EST 2007
On Fri, 28 Dec 2007, S. S. Kutateladze wrote:
> Timothy Y. Chow wrote :
> I said at the outset that I didn't want to quibble over the
> precise choice of set theory. Pick a slightly stronger set theory than
> ZFC and your objection evaporates.
> No it is not. Even if you imply Cantorian paradise of any many,
> when speaking of quibbling..
> Model theory speaks about truth, semantics, verification, etc, that
> are not ``any many.''
That remark of mine that you quote here was directed at your claim that
category theory cannot be faithfully translated into (a sufficiently
strong) set theory, not at your claim that model theory cannot be
formalized in ZFC. Since you don't say anything here about category
theory, does that mean that you concede the point about category theory
and are arguing only that model theory cannot be accurately captured by
In any case, your claim that model theory is a counterexample to the
Formalization Thesis is quite surprising to me. 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?
That is a radical claim indeed.
More information about the FOM