FOM: Platonism and social constructivism
sazonov at logic.botik.ru
Thu Mar 26 16:38:12 EST 1998
Martin Davis wrote:
> At 06:30 PM 3/25/98 +0300, sazonov at logic.botik.ru wrote:
> >Thus, I would say that mathematical objects exist *only*
> >together with and via some *formal* axioms, rules and
> How do you reconcile this with G"odel's incompleteness theorem which I
> understand to tell us that there are arithmetic truths transcending any
> given formal system?
I do not feel any need of having as "real" or even "quasi-real" the
intended model of the axioms of a formal system like PA which would
be considerably more serious than the ordinary informal intuition or
even illusion I really need to have an orientation or psychological
support when working with axioms and proof rules of underlying
classical logic. (Of course, I am also able to invoke temporarily
in my consciousness the *illusion* of "true" or "standard model"
of PA and even of ZFC. Also I think I realize the relation
between an abstract formal theory and the real world which it is
intendend to describe such as the pebbles interpretation of LT.)
Do I loose anything essential by staying on this position? It seems
I rather got a little bit more freedom. For example, this allows me
to "reconcile" myself with somewhat unusual character of the
formalization of feasibility concept I have. I consider my position
rather as realistic one.
As to the traditional considerations with statements like Consis(PA),
I understand them simply as yet another witness that the process of
formalization and creation of an abstract mathematical concept is
indeed a *process*. Say, first we have ZF and then see some necessity
to extend it to ZFC and to ZFC + something else, etc. making more
and more definite (in some respects) our concept of the cumulative
hierarchy of sets. (It is *not* discovering more and more truth on
the intended universe!) The case of Consis(T) is only some more
*regular* process of extension of any T which reflects some
important low of *dynamics* of our mathematical thought.
Let me note also that there may be some doubts that Consis(PA)
faithfully expresses consistency of PA. I consider that *real*
consistency of PA which we "observe" in our mathematical practice
is rather its *feasible* consistency. We really use only proofs
of feasible length. Who knows what will happen if somebody would
be able to write infeasible proofs? But who is this "somebody"
and what are really these "infeasible proofs"?
Program Systems Institute, | Tel. +7-08535-98945 (Inst.),
Russian Acad. of Sci. | Fax. +7-08535-20566
Pereslavl-Zalessky, | e-mail: sazonov at logic.botik.ru
152140, RUSSIA | http://www.botik.ru/~logic/SAZONOV/
More information about the FOM