# [FOM] Formalization Thesis

Vaughan Pratt pratt at cs.stanford.edu
Tue Jan 15 03:46:32 EST 2008

Larry Stout wrote:
> Here's a candidate:
>
> Every category has a skeleton; that is, given any category C there is
> a category Skel(C) in which the only isomorphisms are the identities
> and a functor F:C\to Skel(C) which preserves and reflects isomorphism.

"The identities" should read "the automorphisms."  Also your functor
condition if I've understood it is satisfiable by a non-skeleton, e.g.
C = 0=>1 consisting of two objects 0,1 and two nonidentity morphisms,
both from 0 to 1; the functor F that identifies the two morphisms meets
your condition but its image although skeletal is not equivalent to C.

A category is *skeletal* when all of its isomorphisms are automorphisms.
A *skeleton* of C is any skeletal category equivalent to C;
equivalently, (any category isomorphic to) a full subcategory A of C
such that every object of C is isomorphic (in C) to exactly one object
of A (Mac Lane CTWM p.91).

> If you start with the category of finite sets this would give the
> natural numbers with a category structure somewhat richer than the
> order.  The obvious construction of Skel(C) in ZFC would be to make
> objects equivalence classes of objects in C under isomorphism.

While this is a nicely canonical way of constructing the objects of a
skeleton of C, there is no equally canonical way of constructing its
morphisms.  Locally, for every pair of isomorphic objects to be thus
identified one of the witnessing isomorphisms must be chosen to become
the identity.  And globally, these choices must be coherent.  Absent a
concrete specification of such choices I don't see how this can be
understood as a construction.

Doing
> that in the case of C=FiniteSets would make each of the objects a
> Frege number.  But Roy Cook showed at the PHILMATH conference at
> Notre Dame last October that the existence of Frege numbers (in
> particular 1 and 2) as sets is inconsistent with ZFC.

Ok, so what is your candidate exactly, i.e. what is the mathematical
statement serving as a counterexample to the Formalization Thesis?  And
what role do morphisms play in this counterexample?

This isn't to imply that your approach is unlikely to produce such a
counterexample but only that it needs work.  It's also likely to turn
out to be overkill.

The map x |-> {x} being an injection, there are as many singletons in a
model of ZFC as there are sets.  So it should not come as a great
surprise that there is no set of all singletons (the Frege number 1),
any more than there is no set of all sets.  But in that case it should
be possible to strip your counterexample down to its essence, namely
that ZFC only caters for small objects whereas mathematicians don't seem
to mind considering large objects such as the class of all groups or all
sets as being within their purview.

Von Neumann-Bernays-Goedel (NBG) set theory as a conservative extension
of ZFC purportedly caters for this sort of short-coming of ZFC.  In that
respect NBG can provide counterexamples to the Formalization Thesis in
much the same way as Blum-Shub-Smale (BSS) complexity theory can provide
counterexamples to the Church-Turing thesis by harboring individual
reals such as Chaitin's Omega.

The existence of such counterexamples establishes the status of the
proposition, whether Church's or Chow's, as a thesis rather than a
theorem.  On the other hand the reasonably well understood fringe nature
of the counterexamples does little to undermine the general import of
the thesis in either case.

Vaughan Pratt