FOM: certainty

[Vladimir Sazonov]

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 
absolute truth.

> 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
> formally.
>
> 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 
another difference. 


Vladimir Sazonov
-- 			   | 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/