[FOM] ZFC and the Formalisation Thesis

[Timothy Y. Chow]

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.  
Objection answered.

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