[FOM] Formalization Thesis

[James Hirschorn]

Vladimir Sazanov:
>
> Let me repeat again, that I do not understand the originally presented
> in this discussion FT. However, the question of Joe seems to me
> appropriate.

My understanding is that Joe's challenge was to find a counterexample to FT, 
and thus by FT I meant a negative answer to Joe. (There was the 
word "ordinary" in the original version of FT, which I believe you suggested 
should mean something like "within classical logic".)

> on some kind of belief. I believe in nothing (I hope), but as any human
> being have some (vague) intuition and imagination. Thus, I do not
> understand your comments on compatibilioty with the Platonistic
> viewpoint.
>

Let FT(*) denote the Formalization Thesis that every specific mathematical 
statement can be faithfully expressed in some formal system. Your arguments 
convinced me that FT(*) is a tautology, although I now realize you were 
arguing for much more than this. It was this claim that "FT(*) is a tautology" 
which I felt was compatible with Platonism. My thinking is simply that a 
Platonist can (consistently) believe that it is possible to formalize any 
given specific mathematical statement, but that individual mathematical 
statements always fail to completely convey some deeper mathematical truth.  

I would consider myself to be an "instinctive Platonist" because I have never 
consciously worked out with any precision my own Platonistic views (let alone 
defended them). Obviously this is hardly a compelling position, considering 
e.g. the widely held misconceptions of the ancients that the Earth is flat, or 
that the Sun revolves around it and not visa versa, etc ...

>
> The point is that mathematics (according the FVM) is a science on such
> general formal systems as tools strengthening our thought. (Therefore -
> not just a meaningless game with symbols, contrary to the usual vulgar,
> scoffing understanding of FVM.)

OK, but what then about those core mathematicians who think that all of the 
interesting and necessary foundational work was already done a long time 
ago (and from what I've seen there are quite a few (perhaps even the 
majority?) judging for example from the prevalent condescending attitudes 
towards modern Set Theory in the department where I did my graduate work), 
some of whom consider any mathematics that cannot be handled in ZFC to be a 
priori uninteresting? If I understand the FVM stance correctly, then it 
states that these mathematicians who intentionally restrict their entire 
realm to ZFC deductions, are in fact doing nothing more meaningful than 
playing games with symbols.

>
> Timothy Y. Chow wrote:
> > I note that Sazonov argues for a
> > view of mathematics in which the Formalization Thesis is vacuously
> > true. Implicitly, Sazonov is focusing only on the part of the
> > Formalization
> > Thesis that talks about formal vs. informal, because even on Sazonov's
> > view, the notion that all (or most) branches of mathematics can be
> > "reduced" to set theory is not vacuously true.
>
> Virtually for all the contemporary mathematics it is vacuously true.
>
> Anything what is confirmed to be mathematical (by a classical
> mathematician) is THEREBY confirmed to be formalized in ZFC (or some
> its usual extension) according to the contemporary standard of
> mathematical rigour (which means: ALWAYS USE ZFC or the like, AND
> EVERYTHING WILL BE OK). The only concrete exceptions I see (based on a
> more general, also acceptable standard of formal rigour) are related
> with the concept of "feasible numbers" on which I wrote many times in
> FOM.

I see now (if I correctly understand you) that you are claiming that our 
present standards of rigour subsumes formalization in ZFC. Your view seems
very radical indeed, considering the ubiquitous comments in the literature on 
how remarkable it is that all of mathematics can be reduced to ZFC. In spite 
of some compelling arguments you have given in this thread, I remain 
unconvinced. I am personally not aware that I am translating into ZFC (or 
transmuting if you prefer) whenever I am verifying a proof. 

James Hirschorn