We analyse the structure of propositional proofs in the sequent calculus focusing on the well-known procedures of Interpolation and Cut Elimination. We are motivated in part by the desire to understand why a tautology might be ‘hard to prove’. Given a proof we associate to it a logical graph tracing the flow of formulas in it . We show some general facts about logical graphs such as acyclicity of cut-free proofs and acyclicity of contraction-free proofs , and we give a (...) proof of a strengthened version of the Craig Interpolation Theorem based on flows of formulas. We show that tautologies having minimal interpolants of non-linear size must have proofs with certain precise structural properties. We then show that given a proof Π and a cut-free form Π′ associated to it , certain subgraphs of Π′ which are logical graphs correspond to subgraphs of Π which are logical graphs for the same sequent. This locality property of cut elimination leads to new results on the complexity of interpolants, which cannot follow from the known constructions proving the Craig Interpolation Theorem. (shrink)

We study cut-elimination in first-order classical logic. We construct a sequence of polynomial-length proofs having a non-elementary number of different cut-free normal forms. These normal forms are different in a strong sense: they not only represent different Herbrand-disjunctions but also differ in their propositional structure. This result illustrates that the constructive content of a proof in classical logic is not uniquely determined but rather depends on the chosen method for extracting it.

The essential structure of proofs is proposed as the basis for a measure of complexity of formulas in FOL. The motivating idea was the recognition that distinct theorems can have the same derivation modulo some non essential details. Hence the difficulty in proving them is identical and so their complexity should be the same. We propose a notion of complexity of formulas capturing this property. With this purpose, we introduce the notions of schema calculus, schema derivation and description complexity of (...) a schema formula. Based on these concepts we prove general robustness results that relate the complexity of introducing a logical constructor with the complexity of the component schema formulas as well as the complexity of a schema formula across different schema calculi. (shrink)

Buss, S.R., The undecidability of k-provability, Annals of Pure and Applied Logic 53 75-102. The k-provability problem is, given a first-order formula ø and an integer k, to determine if ø has a proof consisting of k or fewer lines . This paper shows that the k-provability problem for the sequent calculus is undecidable. Indeed, for every r.e. set X there is a formula ø and an integer k such that for all n,ø has a proof of k sequents if (...) and only if n ε X. (shrink)

We prove that Kreisel's Conjecture is true, if Peano arithmetic is axiomatised using minimality principle and axioms of identity (theory $PA_M $ )-The result is independent on the choice of language of $PA_M $ . We also show that if infinitely many instances of A(x) are provable in a bounded number of steps in $PA_M $ then there existe k ∈ ω s. t. $PA_M $ ┤ ∀x > k̄ A(x). The results imply that $PA_M $ does not prove scheme (...) of induction or identity schemes in a bounded number of steps. (shrink)

The $$\varepsilon $$ -elimination method of Hilbert’s $$\varepsilon $$ -calculus yields the up-to-date most direct algorithm for computing the Herbrand disjunction of an extensional formula. A central advantage is that the upper bound on the Herbrand complexity obtained is independent of the propositional structure of the proof. Prior (modern) work on Hilbert’s $$\varepsilon $$ -calculus focused mainly on the pure calculus, without equality. We clarify that this independence also holds for first-order logic with equality. Further, we provide upper bounds analyses (...) of the extended first $$\varepsilon $$ -theorem, even if the formalisation incorporates so-called $$\varepsilon $$ -equality axioms. (shrink)

In this paper we first give a survey of reductive cut-elimination methods in classical logic. In particular we describe the methods of Gentzen and Schütte-Tait from the abstract point of view of proof reduction. We also present the method CERES which we classify as a semi-semantic method. In a further section we describe the so-called semantic methods. In the second part of the paper we carry the proof analysis further by generalizing the CERES method to CERESD . In the generalized (...) version CERESD we admit general elimination rules which are based on the mere semantical truth of sentences. We construct complete cut-free LK-derivations originating from derivations potentially containing unproven lemmas. Finally we give a comparison of reductive methods and CERESD by presenting a general simulation result. (shrink)

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. (shrink)

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. (shrink)

Jan Krajíček posed the following problem: Is there is a generalization result in the theory of real closed fields of the form: If A is provable in length k for all n ϵ ω , then A is provable? It is argued that the answer to this question depends on the particular formulation of the “theory of real closed fields.” Four distinct formulations are investigated with respect to their generalization behavior. It is shown that there is a positive answer to (...) Krajíček's question for 1. the axiom system RCF of Artin-Schreier with Gentzen's LK as underlying logical calculus, 2. RCF with the variant LK B of LK allowing introduction of several quantifiers of the same type in one step, 3. LK B and the first-order schemata corresponding to Dedekind cuts and the supremum principle. A negative answer is given for 4. any system containing the schema of extensionality. (shrink)

Buss, S.R., The undecidability of k-provability, Annals of Pure and Applied Logic 53 75-102. The k-provability problem is, given a first-order formula ø and an integer k, to determine if ø has a proof consisting of k or fewer lines. This paper shows that the k-provability problem for the sequent calculus is undecidable. Indeed, for every r.e. set X there is a formula ø and an integer k such that for all n,ø has a proof of k sequents if and (...) only if n ε X. (shrink)

In this programmatic paper we renew the well-known question “What is a proof?”. Starting from the challenge of the mathematical community by computer assisted theorem provers we discuss in the first part how the experiences from examinations of proofs can help to sharpen the question. In the second part we have a look to the new challenge given by “big proofs”.

This paper presents a translation which allows one to describe constructive provability within classical first-order logic.

We study the formal first order system TIND in the standard language of Gentzen's LK . TIND extends LK by the purely logical rule of term-induction, that is a restricted induction principle, deriving numerals instead of arbitrary terms. This rule may be conceived as the logical image of full induction.

This paper develops a proof theory for logical forms of proofs in the case of monadic languages. Among the consequences are different kinds of generalization of proofs in various schematic proof systems. The results use suitable relations between logical properties of partial proof data and algebraic properties of corresponding sets of linear diophantine equations.