[FOM] Formalization Thesis
Timothy Y. Chow
tchow at alum.mit.edu
Thu Dec 27 15:55:02 EST 2007
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
More information about the FOM
mailing list