[FOM] Formalization Thesis

[Andre.Rodin@ens.fr]

William Messing wrote:

> With regard to the use of category theory concering the Formalization
> Thesis, I do not see what the advantage might be.  As I have previously
> written, a category is defined in terms of ZFC, as is the concept of a
> functor between two categories.  If "category" is not defined in this
> manner, I have previously asked for someone to give an explicit example
> of a statement concerning a category which can not be equivalently
> reformulated using the the notion a cateogry is a sextuble consisting of
> its objects, its morphisms and the source, target, identity and
> composition functions.


What kind of equivalence are you talking about here? My worry is that this
equivalence concept is completele *informal*, and non-rigorous. And my
suggestion is to use CT for replace such informal equivalences by something
more precise. In fact, I don't think one needs an equivalence here - some kind
of one-way (non-reversible) functor could be sufficient for the purpose.

The fact that CT *itself* is a subject of possible formalisation doesn't change
my argument. Once again: until one has some precise notion of equivalence at
hand (category-theretic or other) the claim that a given piece of maths is
equivalently reformulated into a given formal language cannot be precise
either.