[FOM] Formalization Thesis

[Timothy Y. Chow]

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 
set-theoretic statements?

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.

Tim