# On the number of steps in proofs

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

 Abstract In this paper we prove some results about the complexity of proofs. We consider proofs in Hilbert-style formal systems such as in . 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  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 Logic and Philosophy of Logic (categorize this paper) DOI 10.1016/0168-0072(89)90012-2 Options Edit this record Mark as duplicate Export citation  Find it on Scholar Request removal from index Revision history

PhilArchive copy

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

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)

## References found in this work BETA

Existence and Feasibility in Arithmetic.Rohit Parikh - 1971 - Journal of Symbolic Logic 36 (3):494-508.
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.

## 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.

## Similar books and articles

On Me Number of Steps in Proofs.Jan Krajíè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.
Probabilistic Proofs and Transferability.Kenny Easwaran - 2009 - Philosophia Mathematica 17 (3):341-362.
Proofs of the Compactness Theorem.Alexander Paseau - 2010 - History and Philosophy of Logic 31 (1):73-98.
Kreisel's Conjecture with Minimality Principle.Pavel Hrubeš - 2009 - Journal of Symbolic Logic 74 (3):976-988.

## Analytics

Added to PP index
2014-01-16

Total views
4 ( #1,286,556 of 2,533,478 )