[FOM] on the formal nature of mathematics

[Vladimir Sazonov]

Catarina Dutilh wrote

... So please feel free to re-send your message to the list.

CD:

You are saying that what is distinguishable about mathematics is that
it is formal, by which you understand rigorous. As I think I already
mentioned, I am working on the very notion of 'formal' at the moment,
and it turns out that it is not at all obvious how to give a unified
definition of this notion. If you are going to use it to demarcate
mathematics, then obviously you cannot use the notion of mathematical
to define what is formal, on pain of circularity.


VS:

I think, sometimes circularity is unavoidable, even in mathematics.
When we ask ourselves what is a set, intuitively (not just
axiomatically, implicitly defined), we explain this in terms, say, of
collection.

What is mathematical rigour? I explain this by equating

rigourous = formal,

i.e. when the form of our reasoning determines whether it is correct.
In mathematics we should abstract of the content of reasoning as much
as possible. A kind of asceticism. But the content also exists as our
intuition. Once we abstract of it, we still have it in our reasoning
(and should not lose sight of it, however such danger exists in
principle).

You say that it is not at all obvious how to give a unified definition
of 'formal'. In general, it is philosophical concept (form vs content).

In mathematics the form of reasoning is highly important for its
correctness. So, here is the mathematical specifics of this concept. On 
the other hand, contemporary concept of a formal system may be very
complex, but, in principle, is reducible to a language whose syntax is
well (algorithmically) described, say, by using a kind of grammar (BNF
or the like) + a finite system of derivation rules of the form P/C
where the premise is P and conclusion C consist of strings of symbols,
may be containing meta variables for well formed expression of the
language. Anyway, there are several examples which illustrate what it
is.

Do you need anything more unified or more precise? I think that for
this level of consideration the above description is quite sufficient.
The point is that we are able to understand such examples of formal
systems essentially without and before any mathematics as a lot of
people (knowing no mathematics) understand the grammar of any natural
language.

By the way, I do not see here too much of circularity you mentioned.

CD:

If I understood you correctly, something can be counted as a
mathematical argument if it is potentially formal, i.e. if it can be
transformed into a formalized proof. By formalized proof I think you
mean 'computable', 'machine-checkable', is that correct?

VS:

For contemporary mathematics, I consider this as taken for granted,
even if not all mathematicians realize this well. But I am sure any
mathematician listened somewhere that everything in mathematics can be
formalized in set theory and realizes that any his result can, in
principle be checked for correctness according to this perspective. To
reject this is to reject the real progress made in f.o.m. in the
previous century and its role for mathematics. It is like some
physicist would insist that relativity theory or quantum mechanics are
non-essential and would ignore them in his work. There is the
mathematical community who eventually checks the formal correctness of
proofs. There are even such projects as Mizar.

CD:

But then, aren't we back to the original issue, i.e. the Formalization
Thesis? How are we to evaluate the correctness of this transformation,
say for example of Euclid's geometrical proofs? Again, I am not saying
that this is not possible (I would be entirely happy with a
'sociological arguments', i.e. there is significant agreement in the
mathematical community to the effect that T* is a correct formalization 
of Euclid's geometry), but once again this seems to be the real 
conceptual problem. Let me add, however, that I have defended this very 
view at some point, that what is to count as formal is what is 
potentially formalizable, so I am very sympathetic to the view; but
precisely for this reason I deem it important to discuss it thoroughly, 
including its tricky aspects.

VS:

I usually do not consider 'sociological arguments' in f.o.m. as
something important. The 'rational reasons' can be given instead, based 
on our mathematical experience. As to Euclid, the structure of his 
reasoning can be fully preserved under formalization, say, in ZFC (with 
filling some minor gaps like using Pasch's axiom). The rest is rather 
only some encoding of points, lines, planes, etc. by sets. The encoding 
is quite faithful and the axioms used by Euclid are provable under this 
encoding - the witness and guarantee of faithfulness. Our intuitive 
understanding of set theory is quite good (if we avoid some subtler 
questions, moreover, even if ZFC will be found to be contradictory!) 
and adequately described by axioms and proof rules of ZFC. Therefore 
the encoding in question is well understood both intuitively and 
formally. I do not see what is the problem.

The questions whether some separate statements like "2 + 2 = 4" are
adequately represented by sets (finite ordinals) do not seem to me
essential. First, we should consider encoding of "ALL" natural numbers
by sets, and it serves well for all our purposes. Second, even in Peano 
Arithmetic which deals "immediately" with natural numbers we also need 
to use encodings of finite sequences or sets of (of sets, etc. of) 
natural numbers. And so what? We CAN do this, and this is the point. 
Take any program in a high level programming language such as Java 
involving high level (programming) concepts. We can imitate this in 
Turing Machine adequately by using some encoding, likewise we can
(typically) imitate whatever mathematical we want in ZFC. Some encoding 
is inevitable as soon as we use some FIXED formal system. Moreover, it 
is the GOAL of ZFC to ENCODE various mathematics. Anyway, I see no 
reason to regret that some encodings should be used. Once we are using 
some tool (hammer, lever, car, ZFC - the tool of thought - or whatever 
else), we should be ready to adopt to and to take full advantage from 
its innate features.

Recall that mathematics deals with various FORMAL TOOLS OF THOUGHT. Its 
EXTRAORDINARY POWER is related just with formality of these tools - 
when we can do things AUTOMATICALLY (like multiplication of decimal
numbers or working with integrals) without thinking on each separate
step. (Recall again opening a planet by calculations! And a lot of
similar things...)


Best wishes

Vladimir

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