On the number of steps in proofs
type: Item
instance of: scholarly article
title: On the number of steps in proofs
zbMATH Open document ID: 0672.03042
DOI: 10.1016/0168-0072(89)90012-2
author: Jan Krajíček
published in: Annals of Pure and Applied Logic
publication date: 1989-01-01T00:00:00Z
review text: The paper considers the following measures of complexity of proofs: length \((=the\) number of symbols in the proof), depth \((=the\) maximal depth of a formula in the proof) and number of steps \((=the\) number of formulas in the proof). Some upper bound results for first-order logics are obtained: A bound on the depth in terms of the number of steps, a bound on the depth in terms of the length, a bound on the length in terms of the number of steps (for restricted systems). Some interesting applications are given: A bound on the number of steps in a cut-free proof, bounds on the number of steps in proofs of Paris-Harrington sentences.
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F07
zbMATH DE Number: 4099292
zbMATH Keywords: cut-elimination
zbMATH Keywords: complexity of proofs
zbMATH Keywords: length
zbMATH Keywords: depth
zbMATH Keywords: number of steps
zbMATH Keywords: upper bound
zbMATH Keywords: cut-free proof
zbMATH Keywords: Paris-Harrington sentences
reviewed by: Sergei Artemov
MaRDI profile type: Publication
full work available at URL: 0168-0072(89)90012-2
OpenAlex ID: W2112754349
cites work: Q3691675
cites work: Abbreviating proofs by adding new axioms
cites work: One hundred and two problems in mathematical logic
cites work: Q3968902
cites work: Q5812175
cites work: Construction of Satisfaction Classes for Nonstandard Models
cites work: The number of proof lines and the size of proofs in first order logic
cites work: Q3786479
cites work: Some applications of formalized consistency proofs
cites work: On the length of proofs in formal systems
cites work: Sentences undecidable in formalized arithmetic. An exposition of the theory of Kurt Gödel
cites work: Existence and feasibility in arithmetic
cites work: Some Results on the Length of Proofs
cites work: Q3893931
cites work: Q4739657
cites work: Cuts, consistency statements and interpretations
cites work: Q3755452
cites work: Q3773878
cites work: Q4143279
cites work: Q5537599
cites work: Speed-Up by Theories with Infinite Models
cites work: Bounds for proof-search and speed-up in the predicate calculus
cites work: Proof theory
cites work: Undecidable theories
cites work: A theorem on the formalized arithmetic with function symbols ' and +
cites work: A note on a formalized arithmetic with function symbols ' and +
cites work: Some results on speed-up
Recommended article: A Note on the Length of Proofs
Recommended article: Q4215637
Recommended article: Bounded Proofs and Step Frames
Recommended article: On calculational proofs
Recommended article: Counting proofs in propositional logic
Recommended article: Proofs, Proofs, Proofs, and Proofs
Recommended article: Some remarks on lengths of propositional proofs
Recommended article: Reflections on Proof Complexity and Counting Principles
Recommended article: Length and structure of proofs
Recommended article: Q5149136
description: scientific article; zbMATH DE number 4099292