[FOM] Formalization Thesis

[Timothy Y. Chow]

On Fri, 28 Dec 2007, S. S. Kutateladze wrote:
> perhaps a more cautious formulation would say that there exists a
> category-theoretic proof a category-theoretic theorem T if and only if
> there exists a set-theoretic proof of a
> set-theoretic translation T' of T.
> __________________________________________
> 
> This is clearly wrong. Category theory can speak about all elementary
> toposes whereas ZFC cannot.  This is like standard poetry and poetry
> in Braille.

O.K., fine.  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.

> --------------------------
>  Timothy Y. Chow writes
>  Formalize  model theory *within* ZFC...
>  ----------------------------------------
>  This is impossible. ZFC is an instance of a first order theory,
>  that's  all. Model theory is much more.

Why is it impossible?  Model theory textbooks typically start off by 
defining what first-order languages are and what structures and 
interpretations are.  How do they define them?  Well, they start by saying 
that an alphabet is a *set* of symbols.  A structure is a *set* together 
with a bunch of functions and relations (which in turn can be thought of 
as *sets*).  An interpretation is a mapping, which also can be thought of 
as a *set*.  All these set-theoretic definitions and assertions can be 
formalized in the first-order language of set theory, with ZFC (or 
something similar) as the axiom set.

Tim