[FOM] Formalization Thesis vs Formal nature of mathematics

[Vladimir Sazonov]

S. S. Kutateladze [mailto:sskut at math.nsc.ru] wrote

 > Vladimir Sazonov    wrote :
> I do not know what is mathematical 'truth', except the truth in the
> real world...
> __________________________________________________
> Of course, you know a la Tarski; but I appreciate that
> you acknowledge something mathematical in the real
> informal world.

Mathematical formalisms, constructs and proofs are related
to our intuition in particular concerning the real world.

Tarski definition of truth is a mathematical toy as ANY other
mathematical definition. What is mathematical TRUTH, I do not
understand.

>
> Sazonov wrote:
> But please note "by way of proof". No other way to 'truth' is allowed.
> ________________________
> Proof may be informal like you statement above: you mentioned
> something informal and I understand you somehow.

Mathematical proofs are always sufficiently formal (just
to such degree to which it is necessary/essential).
Otherwise they are not mathematical.


> ____________________________
> My point is that calculus was mathematics at the time of invention,
> whereas there was no formalization in the modern sense at all.


It was mathematics (not just speculations) to that degree to
which it was formalized (in the wide sense of this word),
in fact, "fragmentary" . The process of finding satisfactory
formalization or proof from its DRAFT can take some time,
even ages. Of course a draft can also have high mathematical
value. Mathematicians of that time realized that something
was non-well. This was the lack of rigour (the lack of
mathematics in these considerations).


> Sazonov wrote:
> I know no particular exclusion from the formalist paradigm...

__________________________________________________________
> Invention, fantasy, semantics, etc. reside partly beyond
> formalization.

I explicitly related formalisms with intuition and thought
(the former as tools and as "rail ways" for the latter).
They complement one another (in a specific way). It is
this what I call formalist paradigm (or view) on mathematics.
I see nothing in mathematics what is not covered by this paradigm.


> Sazonov wrote:
> Because he [Euclid]was sufficiently formal, except some minor points.
> ____________________________________________________________
> So you consider  the absence of any definition of a notion used in
> in  a proof a minor point for formalization. I presume always that
> the formal paradigm is much stricter.

This probably was so trivial to him. We, nowadays, also
allow various such omissions which are usually easily
recovered by any qualified reader. The point is that even
ancient mathematicians developed instinctively (because of
the very nature of mathematical activity) such a formal style
of their proofs which did not allowed doing non-formalizable
(let in the future times) purely speculative steps. Probably
this could be explained in a better way, may be referring to
human psychology... I think this might be a good topic
of research.


> Sazonov wrote:
> I do not know what is greater. Assume so. And so what?
> _________________________________________________________
>
> So the modern standards of rigor are as incomplete and powerful as
> ever.

I am not sure what do you really mean.

As to me, I see further improvement in the standards of
rigour/formality by adding the requirement that all
proofs should be feasible. This would require extensions
of formal logic by some mechanisms which currently are
considered as conservative extensions. Some mechanisms
such as cut rule could probably be restricted. In the case
of feasible proofs this gives rise to (feasibly) non-equivalent
versions of logic which may lead to formalization of new,
more subtle mathematical concepts.

The linguistic (via languages in a finite alphabet) approach
to formality could be replaced or extended by using
pictorial diagrams like in category theory - also quite formal
objects.

Indeed, there is probably no end in extending or deepening
or ramifying the idea of formal system. But what we already
have now is a definite limit (the comparatively "highest"
standard of rigour) in comparison with the previous history
of mathematics. We have reached a kind of absolute rigour,
at least a "stable" point. Now some really new qualitative,
may be revolutionary changes are necessary to get considerably
new version of mathematical rigour. But at this moment I
consider this mainly as a fantasy.


> Sazonov wrote:

...

> And so what? Is this knowledge outside of the formal paradigm (or the
> paradigm of rigour) of mathematics?
> ____________________________________________________
> The quest for mathematical knowledge is mathematical but may be
> informal.

There is always the place for speculations on formal devices
for thought created and studied in mathematics. This does not
change its formal nature in the sense that it is an activity
by creating such formal "devices".


> Sazonov wrote:
> Yes, human enterprise of creating and studying formal side and formal
> tools of our thought. (Not a meaningless formal game!)
> What is misleading?
> _______________________________________________________
> The nature of math is human whereas the objects of math are formal.


Should I conclude that you actually agree with me?

>  Sazonov wrote;
> ... the goal is formal tools, not truths. Getting truth (in the real
> world) is only a side effect of mathematical activity. 'Truth' in
> mathematics is a kind of chess piece, a very important piece, sometimes
> having relation to the truth in the real world.
> ______________________________
>
> This reminds me of the mad tailor of Stanislaw Lem's  "Summa
> Technologiae."

Do you believe (or may be know???) that mathematical objects
and truths exist objectively and that they are not results
of interplay between our intuition/imagination and formalisms?

Inventing formal tools for thought (as I understand mathematics)
covers whatever RATIONAL you might want on "mathematical truth".


> In fact, I am in favor of Mac Lane's approach.

Mac Lane's formulation seems to me a special case and is
fully coherent with what I suggest. He says about provable
truth whereas I on intuition and thought supported by
formalisms. Or I do not know something essential on his
views? I think you overestimate the idea of mathematical truth.
For me this is only an interesting (let highly non-trivial)
"toy", an illusion and schematic ersatz of the real world truth.
Human thought, intuition and imagination - this is philosophically
more fundamental, and this is for which mathematics creates
formal systems (tools, engines of thought) and derivations
in them (rail ways of thought).


Vladimir Sazonov


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