[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: FOM <fom@math.psu.edu>*Subject*: Re: FOM: certainty*From*: Vladimir Sazonov <sazonov@logic.botik.ru>*Date*: Fri, 18 Dec 1998 17:53:32 +0300*CC*: "Sazonov, Vladimir" <sazonov@logic.botik.ru>*Organization*: Program Systems Institute, RAS*References*: <199812151746.RAA08507@hawaii.dcs.gla.ac.uk>*Reply-To*: sazonov@logic.botik.ru*Sender*: owner-fom@math.psu.edu

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@logic.botik.ru 152140, RUSSIA | http://www.botik.ru/~logic/SAZONOV/

**Follow-Ups**:**Andrzej Trybulec**- Re: FOM: certainty

**References**:**Randy Pollack**- FOM: certainty

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]