# [FOM] ZFC and the Formalisation Thesis

Timothy Y. Chow tchow at alum.mit.edu
Mon May 31 00:55:02 EDT 2010

```F.A. Muller wrote:

> Category Theory works with lots of 'sets' that do not exist
> according to ZFC. The body of theorems proved in Category
> Theory surely cannot be neglected, right?
>
> (*) So the thesis that all mathematical knowledge can be founded
> on ZFC is refuted.

No.  I already blocked these trivial attempts at counterexamples in my
article, but I'll spell it out for your benefit.  The simplest refutation
is that I explicitly said that I'm not wedded to ZFC in particular.  So
let's just take your own "modest extension of ZFC" in place of ZFC.

Alternatively, in my new formulation of the Formalization Thesis, I took
pains not to say that the formal sentence of ZFC must "faithfully express"
the original statement.  It just has to have the property that any proof
of the original statement can be mirrored by a proof of the formal
sentence in ZFC.  Thus for most of the theorems of category theory, we can
encode everything in ZFC by using standard dodges.  We're not obligated to
"call a set a set" so to speak.

> The 'higher infinite'

Ditto here; just throw in a large-cardinal axiom if you need it.
Alternatively, I think that a plausible case can be made that for any
theorem T that uses a large-cardinal axiom A, virtually all the
mathematical content of T is captured in the theorem "A implies T".  And
"A implies T" is virtually always a theorem of ZFC.  So by using "A
implies T" as a surrogate for T itself, we don't even have to go beyond
ZFC.

By the way, I don't know what you mean when you say that forcing cannot be
founded upon ZFC.  Basic forcing arguments themselves are logically very
weak; I'm sure PA suffices if not PRA.  Though it's common to think about
forcing arguments model-theoretically, the essence of the argument can
be expressed purely syntactically.

Tim
```