[FOM] re sazanov's intuitive formalizations

[Gabriel Stolzenberg]

   In "Re shipman's challenge: the best defense," Jan 10, Vladimir
Sazonov begins by quoting me, in "shipman's challenge: the best
defense" Jan 8, commmenting on a remark by Joe Shipman.  [In what
follows, '>' is me quoting sazanov and '> >' is him quoting me.]

> Gabriel Stolzenberg wrote:

> >    On Thu 03 Jan 2008, in Re: Formalization Thesis (Vol 61 Issue 5),
> > Joe Shipman 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?
>
> >  I would expect that, at least initially, in just about every case,
> > a more responsible attitude for a mathematician (e.g., me) to take
> > would be to refrain from answering either in the affirmative or the
> > negative.  I say this for two related reasons.  First, the expression,
> > "adequately expressible," is radically vague and subjective.

> I think that the usage of "adequate formalization" is of such a
> specific character for which vagueness does not play essential role
> to doubt in "adequate".

   I strongly disagree.  For what I am talking about (but maybe you
are not), namely, formalization of ordinary math in a formal system,
this should be obvious.  Also, your claim is, I think, supposed to
apply to me (because I'm a mathematician).  But it doesn't.  My usage
of "adequate formalization" is not of "such a specific character."
Nothing like it.

>  "Adequate formalization" is not the same as "adequate translation"
> from one natural language to another (or from a natural language to
> formal) as it might be thought.

   Who said that it is?  The expression, "adequate translation" is
in far better shape.

> Such an act of formalization arises also each time when we read a
> good mathematical text which is, strictly speaking, only a way how
> to communicate ideas on such a formalization.

   Strictly speaking, what you say here is incorrect.  So far as I
can see, it bears no interesting relationship to what I (and others
I know) do when I am reading a text.  If you provide evidence that
it does, I'll do the same for my claim that it doesn't.

> With the help of the author of such a text the readers also do
> the work of formalization in their minds (working like co-authors).

   That's not what readers typically do.  Again, if you have evidence
to show that I'm mistaken, let's see it.

>   Asserting that we have got an "adequate formalization" is a only
> very modest and sober way to express such a feeling [of satisfaction,
> even eupohria].

   For "formalization" in a formal system, this is not how it goes.
And remember, we're talking here about assessments of formalizations
by mathematicians.

> saying that a formalization is adequate does not mean that there
> still exists what to compare the result with.  We are satisfied
> with the RESULT by a different reason - the result is mathematically
> excellent! That is the point.

  At least currently (and probably always), this doesn't work for
"formalization" of ordinary math in a formal system.  We don't
ask that a formalization in a formal system be, in any interesting
sense, "mathematically excellent."

> > because mathematicians are not trained to assess such matters
> > (there is no course of training because, as of now, there is
> > nothing to be taught),

> I think all mathematicians...can have feeling like above. They
> were trained by reading good mathematical texts, by listening good
> teachers and by doing exercises under their supervision.

   You make my point.  Here you're talking about ordinary mathematics.
But, as I've already explained, I'm talking only about assessing the
"adequacy" of "formalizations" of ordinary math in formal systems.
 And for this, your remark does not apply because, as we both know,
there currently is no such training.

> I think, all of us experienced a very strong feeling of euphoria
> of the proof by Cantor that continuum is not countable.

   I didn't.  Nor have I ever noticed my students (or anyone else
I know) feeling this way.  (I brought up this example in response
to Shipman's challenge for a wholly different reason: the experience
of discomfort at finding that the uncountable is sitting in a system
that is countable.)

  (By the way, some mathematicians experience such a feeling when
they convince themselves that, in ordinary mathematics, they can use
uncountability to prove that there exist "undefinable" real numbers.
This REALLY satisfies them.)

>  Then it unexpectedly appeared, against our intuition, that
> continuous lines and surfaces have the same cardinality.

   Apparently, you didn't consider it interesting enough to mention
that what allegedly "unexpectedly appeared, against our intuition"
here is a classical phenomenon not a constructive one.  Also, it
wasn't against my own intuition.  I was agnostic.)

> Church Thesis asserts that known (quivalent) formalization(s) of
> computability are adequate.

   And it suffers from the same problem.

> Epsilon-delta (or topological) definition of continuity is adequate.

   I think this shows the inadequacy of your idea of adequacy.  In
your sense, what you say here may be correct; but one of the original
"intuitions" of continuity is being able to "draw it" without taking
the pencil off the paper.  And, with respect to this, I can't imagine
even you saying that an epsilon-delta definition is adequate.

> Everything this is so nice! I see nothing subjective in these
> assertions of adequateness.

   When there is a consensus (as many people think there is about
Church's thesis) and we are part of it, we see nothing subjective.
When there isn't, we do.

   Gabriel Stolzenberg