FOM: What is mathematics?
V.Sazonov at csc.liv.ac.uk
Thu Feb 21 08:32:48 EST 2002
Gordon Fisher wrote:
> Vladimir Sazonov wrote:
> > This is absolutely unnecessary. We have a very good standard
> > of mathematical rigor without complete formalization. Only
> > potential formalizability (whatever it means) plays the role
> > in contemporary mathematics. Also partial formalization usually
> > suffices.
> I think you have introduced here a crucial idea in connection
> with our conversation, namely that of "potential formalizability,"
> together with the modifier "whatever it means". What does it
> mean? Has anyone ever tried to deal with idea in a precise
> way. Of course, observation and experience show that many
> mathematicians who don't use much formal logic in their work
> have a feeling, or a faith, that what they present as proofs in
> fairly ordinary language could be put into some formal
> language based, for example, on a traditional predicate calculus
> of some sort. But is this actually possible? That is, can all
> that is communicated by way of ordinary language in the way
> of rigorous proofs actually be so translated? This is related
> to the idea of making proofs with computer programs, which
> I take it has so far had only limited success.
Yes, "potential formalizability" is a crucial issue. A lot
of questions arize!
First, it should be understood as possibility to present
a FEASIBLE proof or construction (physically presented, say,
in a computer). Proofs of nonfeasible length, if it makes
a sense to speak on them at all, are imaginary objects
and therefore cannot be considered as mathematical proofs.
(However, they are the subject of METAmathematics - quite
different story! In particular, Goedel's completeness
and incompleteness theorems should not be understood
absolutely literally! Let me ask, for example, are Predicate
and even Propositional Calculi REALLY complete? And what
completeness REALLY mean, taking into account that only
feasible proofs are REAL proofs?)
Second, we should extend the first order logic (FOL) by
abbreviation mechanisms (a formally fixed ability
to give definitions). But abbreviation may be of various
character - of formulas, of terms, of proofs. Imagine an
iterative proof - therefore recursive abbreviations are
possible. Of course, all of this makes FOL something vague.
Even with abbreviations it is not so easy to write formal
proofs, however, there are some known projects. I believe,
that in principle it is possible, as is really possible
the art of programming for computers. For computers,
programming is inevitable. But for mathematics writing
absolutely formal proofs like computer programs is still
questionable. Why do we need this if the ORDINARY level
of mathematical rigor seems quite reliable and sufficient?
On the other hand, to be MORE RIGOROUS (once we discuss
this subject in the context of f.o.m.), mathematicians
could try to CONVINCE one another that their proofs
really can be written in all details in some specific
version of FOL (or any other logic), but
in WHICH EXACTLY VERSION??
(is there a complete in any sense, system of abbreviations,
or an incompleteness result like Goedel theorem could be
stated?), instead of writing the formal proof explicitly.
Note, that here complexity of proofs comes into scene.
Mathematicians should have a serious reason to start
counting symbols they use. Of course, instead of counting
we could just write explicitly formal proofs as a most
direct evidence. But then also a proof checker system will
be necessary. It is hardly possible to write formal proofs
without mistakes and also humans hardly could read and check
absolutely formal proofs.
Actually, for the contemporary (actually, 20th Century)
mathematics this question on what potential formalizability
means plays no essential role. But let us note a new issue
arising from considering absolutely formal FEASIBLE proofs.
What does it mean that a formal theory is (feasibly!)
consistent/contradictory? What if only nonfeasible
contradiction (is proved in a metamathematical theory to)
exist? Should we consider such a formal system contradictory?
Or semiconsistent, almost consistent? I think, we should
not hesitate to consider such theories as consistent.
Otherwise, I see no solid ground for the concept of formal
consistency. Moreover, such a theory can formalize some
reasonable intuitive concept. For example, the very concept
of feasibility could be formalized. This concept is as foreign
for contemporary mathematics as it was, at the beginning,
Cantorian set theory. But it seems that at least for complexity
theory (if not for the whole mathematics) the concept of
feasibility may be crucial.
Here we should return to the discussion on extensions of
FOL by abbreviation rules. It is evident, that (in a very
weak arithmetical system) abbreviation of terms may lead to
proofs of existence of non-feasible numbers. (Having only
addition, the abbreviation 2*n \bydef n+n would easily lead
to proving existence of very large, nonfeasible numbers.)
Thus, to formalize Feasible Arithmetic we should be very
careful with allowing abbreviation mechanisms. They may play
the role of non-logical principles if they change the intended
concept to be formalized. Therefore, some abbreviations
(say, of formulas) may be allowed, and others (say, of terms)
may be forbidden.
Moreover, it could be argued that even pure FOL without
any added abbreviations ALREADY HAS THEM when E-introduction
rule (in natural deduction version of FOL) is followed by
corresponding E-elimination rule. The first introduces
abbreviation for a term and the second uses it. Can we
restrict FOL (say, by considering only normalized deductions
or by forbidding the cut rule and therefore restricting
even modus ponense rule)? If we want to formalize
feasibility, something such is probably inevitable.
I would also note that mathematical rigor is heavily based
on feasibility concept and therefore this concept should be
formalized to be understood mathematically, not just via
Vladimir Sazonov V.Sazonov at csc.liv.ac.uk
Department of Computer Science tel: (+44) 0151 794-6792
University of Liverpool fax: (+44) 0151 794 3715
Liverpool L69 7ZF, U.K. http://www.csc.liv.ac.uk/~sazonov
More information about the FOM