sazonov at logic.botik.ru
Fri Dec 18 09:53:32 EST 1998
Randy Pollack wrote:
> Vladimir Sazonov said he is "a permanent opponent of those who assert
> existence of absolute mathematical truth." I don't know what
> "absolute truth" means.
I too! Does anybody know?
> Issues of evidence and belief are more
> interesting. What follows is not a final answer to mathematical
> meaning, but some sample thoughts meant to widen the FOM discussion.
> I suggest seperating belief in a formal system from belief in proofs
> in that formal system. Belief in ZFC is informal in the sense that if
> we disagree (say Steve Cook believes ZFC but I do not) there is no
> formal argument to attain agreement. We must talk about mathematical
> principles and other philosophical stuff.
I agree that it is much better to replace here the term "truth"
by something more flexible and *relativistic*. I prefer to tell,
instead, on "adequateness" to such and such reality or
intuition or on "applicability" somewhere.
But it is strange to me that we can speak about a formal system,
like ZFC, that it is believable or not. This seems somewhat
religious. However, I agree that it may be believable or not
that a system has no formal contradiction. The latter has some
more real meaning. On the other hand, probably each
mathematician, even intuitionist or any other "...ist", is able
to have *some* kind of intuition which allows him to make
*meaningful* deductions in ZFC. And vice versa, each classical
mathematician is able to understand or create his own version of
intuition for any other kind of non-classical logic. There is
nothing here with beliefs. The question is only what is the
inclination of that or other mathematician. Something like
choosing algebra or geometry for active research. The majority
of mathematicians are inclined to use classical logic. But this
does not mean that other "minorities" are not mathematicians.
Thus, my view on mathematics is very simple: Any formal system
based on any kind of logic with any reasonable intuition behind
it may be considered as mathematical. Some formal systems (like
ZFC) and corresponding intuitions prove to be sufficiently
universal. Let it be! But I see no reason to believe in absolute
character of such universality (say to believe that all, *even
future* mathematics will be reduced to ZFC or its extensions by
stronger axioms and that out goal is to find "the only true"
intuition for ZFC). Such a belief is also a kind of belief in
> Belief in a formal proof in a given formal system, S, (here I'm vague
> about what is a formal system; I'll return to that later) is attained
> formally, not philosophically. If A doesn't accept a proof in S, s/he
> must say which step s/he doesn't accept. Then B, who believes the
> proof in S, can add more detail to the explanation of why the side
> conditions and premises of Rule xxx are satisfied; or possibly A can
> convince B the formal rule does not actually apply. Under reasonable
> meanings of "formal system", A and B can resolve the point purely
> The distinction is not quite as simple as I just suggested. We need
> some base notion of representation of a formal system; i.e. we somehow
> have to bridge the informal-formal gap. We cannot have a formal
> presentation of a formal system until we have, at bottom, some
> informally presented formal system. This is usually where we appeal
> to PRA (informally presented), or to Fefermans FS0, or to some weak
> dependent types system (Martin-Lof's or Plotkin's Logical Frameworks).
> So it is possible to find disagreement about the encoding of our
> object formal system in the meta-system PRA or FS0 or .... The
> "informal" framework may actually be a computer program in a
> completely formal notation, but it ultimately is executed on a
> physical device.
> We haven't yet addressed the formal system itself; we must look, not
> at extension (the judgements derived), but at presentation. Cut-free
> FOL is different from FOL with cut in terms of both feasible checking
> and mathematical principles. The admissibility of cut is
> meta-theoretic, outside of FOL, depending on induction in the
> meta-theory. So if we want to use cut, and other admissible rules,
> they should be explicitly part of the formal system.
Yes, of course! We also should be more explicit on using other
kinds of rules such as abbreviations (of terms, of formulas and
even of (sub)proofs).
> In this way, we might have a formal proof of the 4CT in a formal
> system that has rules explaining the computational behavior of the
> computer programs that check the cases. Those rules are shown to be
> admissible by meta-theoretic proof, just as the cut rule is for FOL.
> Accepting the meta-theoretic program correctness proof as a
> mathematical principle is the main difficulty to calling this a proof,
> but how is it different from accepting cut?
Yes, cut rule w.r.t. cut-free formal system behaves as a long
computation (cut elimination procedure). You seems to suggest
analogy with "rules explaining the computational behavior of the
computer programs that check the cases". One difference consists
in the fact that cut elimination theorem have been proved (in a
meta-theory), but there is no "elimination theorem" for the
computations involved in the proof of 4CT. That is there were no
(sufficiently short) meta-proof that those computations will
halt with such and such results. We should wait sufficiently
long time until the computation stops.
If, by some reason, we did not postulate cut rule in FOL then we
have no right to use it, except eventually to eliminate it from
any preliminary version of a proof. Even cut elimination
(meta-)theorem does not allow to use it in this case because
there is no hope that the elimination procedure will be always
feasible. Thus, the situation with cut rule is even worse than
that with the computations involved in 4CT. The latter are
known to *really* halt (without any meta-theorem). This is
-- | Tel. +7-08535-98945 (Inst.),
Computer Logic Lab., | Tel. +7-08535-98953 (Inst.),
Program Systems Institute, | Tel. +7-08535-98365 (home),
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