FOM: What is mathematics?

[Vladimir Sazonov]

Gordon Fisher wrote:
> 
> Vladimir Sazonov wrote:
> 
> [deletion]
> 
> >
> > 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  
waving hands. 


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