Annals of Pure and Applied Logic 41 (2):153-178 (1989)

In this paper we prove some results about the complexity of proofs. We consider proofs in Hilbert-style formal systems such as in [17]. Thus a proof is a sequence offormulas satisfying certain conditions. We can view the formulas as being strings of symbols; hence the whole proof is a string too. We consider the following measures of complexity of proofs: length , depth and number of steps For a particular formal system and a given formula A we consider the shortest length of a proof of A , the minimal depth of a proof of A and the minimal number of steps in a proof of A . The main results are the following: a bound on the depth in terms of the number of steps: Theorem 2.2, a bound on the depth in terms of the length: Theorem 2.3, a bound on the length in terms of the number of steps for restricted systems: Theorem 3.1. These results are applied to obtain several corollaries. In particular we show: a bound on the number of steps in a cut-free proof, some speed-up results, bounds on the number of steps in proofs of Paris-Harrington sentences. Some papers related to our research are listed in the references. We were especially influenced by Parikh's paper [17] on the famous conjecture of Kreisel . Many important problems in this field remain open. We hope that our paper will contribute to progress in this area. It should be noted that some results of this paper can be equally well obtained using unification theory , by translating a complexity-of-proof problem into a unification problem. A unification algorithm solving the unification problem can then be constructed and the complexity of the unification algorithm analyzed. As pointed out by the referee this method can be used to solve the problem stated in Section 3 for some non-simple schematic systems
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/0168-0072(89)90012-2
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 72,564
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

A Mathematical Incompleteness in Peano Arithmetic.Jeff Paris & Leo Harrington - 1977 - In Jon Barwise & H. Jerome Keisler (eds.), Handbook of Mathematical Logic. North-Holland Pub. Co.. pp. 90--1133.
One Hundred and Two Problems in Mathematical Logic.Harvey Friedman - 1975 - Journal of Symbolic Logic 40 (2):113-129.
Cuts, Consistency Statements and Interpretations.Pavel Pudlák - 1985 - Journal of Symbolic Logic 50 (2):423-441.

View all 8 references / Add more references

Citations of this work BETA

Proof Lengths for Instances of the Paris–Harrington Principle.Anton Freund - 2017 - Annals of Pure and Applied Logic 168 (7):1361-1382.
Some Remarks on Lengths of Propositional Proofs.Samuel R. Buss - 1995 - Archive for Mathematical Logic 34 (6):377-394.
Von Neumann, Gödel and Complexity Theory.Alasdair Urquhart - 2010 - Bulletin of Symbolic Logic 16 (4):516-530.

View all 11 citations / Add more citations

Similar books and articles

On the Number of Steps in Proofs.Jan Kraj\mIček - 1989 - Annals of Pure and Applied Logic 41 (2):153-178.
Cutting Planes, Connectivity, and Threshold Logic.Samuel R. Buss & Peter Clote - 1996 - Archive for Mathematical Logic 35 (1):33-62.
Some Remarks on Lengths of Propositional Proofs.Samuel R. Buss - 1995 - Archive for Mathematical Logic 34 (6):377-394.
Counting Proofs in Propositional Logic.René David & Marek Zaionc - 2009 - Archive for Mathematical Logic 48 (2):185-199.
The Role of Diagrams in Mathematical Arguments.David Sherry - 2008 - Foundations of Science 14 (1-2):59-74.
Proofs of the Compactness Theorem.Alexander Paseau - 2010 - History and Philosophy of Logic 31 (1):73-98.
Probabilistic Proofs and Transferability.Kenny Easwaran - 2009 - Philosophia Mathematica 17 (3):341-362.
The Depth of Resolution Proofs.Alasdair Urquhart - 2011 - Studia Logica 99 (1-3):349-364.


Added to PP index

Total views
34 ( #339,421 of 2,533,479 )

Recent downloads (6 months)
1 ( #391,480 of 2,533,479 )

How can I increase my downloads?


My notes