[FOM] Formalization Thesis

[Vladimir Sazonov]

James Hirschorn wrote:
> 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).

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.


I prefer and defend a more general version than FT of (non-vulgar) 
Farmalist View on Mathematics (FVM), and also consider Platonistic View 
as something awfully meaningless. Of course, I myself have some 
imagination concerning "the" universe of a first-order theory such as 
ZFC. (Even irreconcilable intuitionists and constructivists have some 
kind of intuition on ZFC.) But I consider that having SOME intuition on 
ZFC does not necessarily mean accepting Platonistic view which is based 
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.

As I wrote, the ordinary ("classical") mathematics TYPICALLY reduces to 
ZFC or some its extension. Even intuitionistic math reduces to ZFC ( + 
?) by means of Kleene realizability (or the like) or Kripke models (not 
a direct translation, but the most appropriate for a classical 
mathematician who does not want to warp brains (I am not sure whether 
it sounds well in English). Thus, practically everything in the 
contemporary mathematics reduces to ZFC, (although there are some 
non-traditional mathematical considerations
- e.g. on the vague feasibility concept - which are non-reducible to 
ZFC or its usual extensions by large cardinals or the like). Thus, to 
not restrict mathematics unnecessarily, I suggested to consider "any 
formal system", not just the ordinary extensions of ZFC. This means 
formal systems in so general form that even they are not necessarily 
based on First Order Logic (FOL). (ANY formal language + a system of 
formal rules of inference. E.g. multiplication rules of decimal natural 
numbers or formal rules for integration in Analysis are examples of 
such formal systems.)

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.)


> 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.

This sufficiently agrees with my comments above concerning the usual 
mathematics.

>
> 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?

I have not read that yet, but I can imagine that it is equivalent.


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.

(Intuitionistic mathematics is sufficiently adequately reducible to ZFC 
in the sense as I described above. Somebody may not like this sense, 
but it, anyway, works for non-intuitionists who want to understand 
intuitionistic mathematics. I am not an intuitionist and, except one my 
paper (on Markov's Principle, Formal Church Thesis and P=?NP in a weak 
arithmetic), did and studied not so much on constructive mathematics, 
and cannot judge what essential from the pint of view of intuitionists 
is lost under Kleene-like Realizability or Kripke Semantics, but it 
seems to me that for the classical mathematician who does not want to 
change his mind so radically to forget classical mathematics completely 
or temporarily - what is not impossible, of course - this is the best 
or easiest and appropriate way.)


Vladimir Sazonov


----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.