[FOM] Formalization Thesis

[James Hirschorn]

It has been pointed out in this thread that the FT is highly dependent on the 
choice of formal system(s). For example,

Vladimir Sazonov wrote:
> joeshipman at aol.com wrote:
> > I repeat my earlier challenge: can anyone who disputes Chow's
> > Formalization Thesis respond with a SPECIFIC MATHEMATICAL STATEMENT
> > which they are willing to claim is not, despite its expressiblity in
> > English text on the FOM discussion forum, "faithfully representable"
> > or "adequately expressible" as a sentence in the formal system ZFC?
>
> Let me replace "in the formal system ZFC" by "in a formal system".

And went on to give a compelling argument that if we allow "any formal system" 
in FT then it becomes a tautology. I find this very feasible, and it seems to 
be compatible with the Platonistic viewpoint (although I initially got the 
impression that it was not). 

I would suggest (perhaps this has already been suggested) FT(ZFC+LC) stating 
that every mathematical statement can be faithfully expressed in ZFC+A for 
some large cardinal axiom A that is believed to be consistent with ZFC. 

There is another possibly relevant issue which apparently has not been 
discussed in this thread. This is the duality between "set theoretic 
foundations" based on membership and "categorical foundations" based on form. 
The duality goes back to Cantor versus Zermelo, with Cantor expounding the 
latter. See for example the following paper by Lawvere including the 
commentary by McLarty:

http://tac.mta.ca/tac/reprints/articles/11/tr11abs.html

Thus we could consider the dual thesis FT(CAT) stating that all mathematical 
statements can be faithfully formalized in category theory, i.e. a formal 
category theoretic system. Or perhaps this approach is known to be 
equivalent?

James Hirschorn