[FOM] shipman's challenge: the best defense

[Vladimir Sazonov]

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

We always formalize something highly informal, intuitive, NOT YET 
MATHEMATICAL. (Mathematical is already formalised and may need only in 
further detalization.) Some mathematics appears only after and due to 
formalization. (As I wrote many times, I understand "form" in a wide 
sense of this word as the opposite to "content".) 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. 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). After and due to formalization the initial (vague) idea is 
usually radically CHANGED. As the result, we have a renewed intuition + 
formalization (content + form). The old intuition almost disappears. 
(Almost nothing to compare with the result.) Only by analysis of what 
happened we could somehow recall the old state of our mind, if possible 
at all - so strong influence has the process of formalization on our 
thought. As the result, we have a new mathematical concept or proof 
related with other (formerly invented) concepts and proofs in such a 
nice and fruitful way that we get a highest feeling of satisfaction, 
even euphoria. Asserting that we have got an "adequate formalization" 
is a only very modest and sober way to express such a feeling.

Let me repeat: 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.


Second,
> 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, even those who can only read and understand 
mathematical text, not being able to create something serious 
mathematical themselves, can have feeling like above. They were trained 
by reading good mathematical texts, by listening good teachers and by 
doing exercises under their supervision.


they should not assume that just because they do/don't have
> any doubts about adequacy/inadequacy today, they will/won't have any
> tomorrow.

Sorry, I do not understand this fragment at all.

>    Having said this, I invite Joe to think about the "adequacy" of
> a formalization of the informal statement, "The set of real numbers
> is uncountable."  The claim that it is a "faithful representation"
> of the informal statement might well make a mathematician (e.g., me)
> uncomfortable.  I believe this is a familiar point.

Good example. (Joe can say himself, but this is my view.) Before 
studying mathematics, in our childhood, we have had some intuition on 
discrete objects and continuous physical lines - looking as VERY 
different. It was hardly possible to say something more rational 
without any mathematics (even if we would be not children at that time).

This pre-intuition is formalized in mathematics at least in two ways, 
one of which is the concept of cardinality (bijection). I think, all of 
us experienced a very strong feeling of euphoria of the proof by Cantor 
that continuum is not countable. Not only we can feel that in some 
naive way, we can PROVE that!! And the manner of the proof was quite 
unexpected from the point of view of our original intuition. Then it 
unexpectedly appeared, against our intuition, that continuous lines and 
surfaces have the same cardinality. At this moment (after some internal 
struggle with ourselves) our intuition has changed even more strongly 
than by Cantor's diagonal method. Later we understood mathematical 
reasons why lines and surfaces are still strongly different (by the 
formal concept of dimensions). So, the intuition was even ramified.

I think, there is nothing wrong to call the two different 
formalizations arisen as highly adequate, although our original naive 
intuition was at least split.

If somebody would say that our original intuition was rather on 
dimensions than on cardinalities, I would hardly agree. Original 
intuition is something too vague (and even hardly possible to recall 
after the work of thought done) that it is difficult to assert what it 
was exactly about. Just some dim feeling. Mathematical crystallizing of 
our intuition is a hard, irreversible work (even if we are only 
"passive" readers). We are happy on the result of this work calling it 
"adequate".

Other examples:

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

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

Scott-Ershov domains are adequate class of specific partial ordered 
sets (which are also specific topological T-0 spaces) to define 
semantics of (lambda calculus and) programming languages.

Gurevich's Abstract State Machines are also (quite different) adequate 
tool to define semantics of programming languages.

What is "more adequate" and IN WHICH SENSE is an important, but 
different question. Each is adequate in its own sense!

Polynomial-time computability (and NP-completenes) is very adequate 
approach to feasible computability (however, there can be some doubts).

Everything this is so nice! I see nothing subjective in these 
assertions of adequateness. THIS IS MATHEMATICS! ANY mathematician is 
able to understand these examples and to get something reasonable from 
these assertions of adequateness. (Of course, somebody will suggest 
other examples.)

Etc.


Vladimir Sazonov

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