[FOM] Formalization Thesis

[Vaughan Pratt]

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