FOM: Length of proofs and consistency of formal systems by Prikh

[Vladimir Sazonov]

Harvey Friedman 13 Sep 1998 10:11:50 +0100 wrote:
>
> Sazonov 5:32PM 8/31/98 writes:
>
> >The resulting formal system proves to be
> >*feasibly consistent* in the sense that there exists no formal
> >proof of feasible length (say, proof written in a book) which
> >leads to a contradiction. It is Rohit Parikh who introduced (in
> >his paper in JSL, 1971) this, still rather NEW AND UNFORTUNATELY
> >COMPLETELY UNEXPLORED IN F.O.M.  UNDERSTANDING OF CONSISTENCY OF
> >A FORMAL SYSTEM.
>
> The FOM may be interested in the new Handbook of Proof Theory, editor Sam
> Buss, that has just come out from North-Holland. There is an extensive
> article there by Pudlak on the lengths of proofs, including my early result
> which I called "finite Godel's theorem" concerning how many steps are
> needed to prove in T that T has no inconsistency of size <= n.

Yes, there is (very important!) complexity theoretic aspect in 
the traditional technical sense of estimating the length of 
proofs (either of a contradiction in a theory or of some its 
restricted Consis statement, etc.).

However, the paper of Parikh contains *additionally* new and 
very simple idea that we could restrict ourselves only to those 
formal proofs which are physically existing. Proofs which exist 
only in our imagination because of their unrealistic length (say 
10^{10^10}) are not considered as proper proofs at all. (What 
would we think about a mathematician which asserts that he has 
an imaginary proof of imaginary length on imaginary paper sheets 
resolving a difficult mathematical problem? We will ask him to 
present a *real* proof with all the necessary details!) This may 
serve as a realistic and reasonable approach to f.o.m.  Note, 
that there exists no precise borderline between physically 
existing (in principle) and imaginary proofs. Of course this 
approach changes the notion of consistency of a formal system 
and is not reducible to (however is essentially based on) the 
complexity theoretic length-of-proof aspect.

If we admit Goedel completeness theorem as a plausible *informal 
postulate* saying that any (even feasibly/physically) consistent 
formal theory has a meaning (model, interpretation) then 
considering this new class of theories may extend mathematics 
radically by new concepts which have no direct counterparts in 
ZFC universe.

For example, it may be obtained in this way a very unusual 
version of the concept of continuum satisfying unexpected 
(but reasonbable) properties. I wrote about this in some my 
postings to FOM. It is the task of f.o.m. to construct 
formalisms for any kind of fundamental concepts which pretend 
to be mathematical. In some cases only feasibly consistent 
(but potentially, say, in 10^{10^10} number of steps 
inconsistent) formalisms may work. 


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/