This paper studies the complexity of constant depth propositional proofs in the cedent and sequent calculus. We discuss the relationships between the size of tree-like proofs, the size of dag-like proofs, and the heights of proofs. The main result is to correct a proof construction in an earlier paper about transformations from proofs with polylogarithmic height and constantly many formulas per cedent.

We introduce a system of Hyper Natural Deduction for Gödel Logic as an extension of Gentzen’s system of Natural Deduction. A deduction in this system consists of a finite set of derivations which uses the typical rules of Natural Deduction, plus additional rules providing means for communication between derivations. We show that our system is sound and complete for infinite-valued propositional Gödel Logic, by giving translations to and from Avron’s Hypersequent Calculus. We provide conversions for normalization extending usual conversions for Natural Deduction and prove the existence of normal forms for Hyper Natural Deduction for Gödel Logic. We show that normal deductions satisfy the subformula property.

We study consistency search problems for Frege and extended Frege proofs, namely the NP search problems of finding syntactic errors in Frege and extended Frege proofs of contradictions. The input is a polynomial time function, or an oracle, describing a proof of a contradiction; the output is the location of a syntactic error in the proof. The consistency search problems for Frege and extended Frege systems are shown to be many-one complete for the provably total NP search problems of the second order bounded arithmetic theories U^1_2 and V^1_2 , respectively.

We show that logics based on linear Kripke frames – with or without constant domains – that have a scattered end piece are not recursively enumerable. This is done by reduction to validity in all finite classical models.

We consider intermediate predicate logics defined by fixed well-ordered (or dually well-ordered) linear Kripke frames with constant domains where the order-type of the well-order is strictly smaller than~$\omega^\omega$. We show that two such logics of different order-type are separated by a first-order sentence using only one monadic predicate symbol. Previous results by Minari, Takano and Ono, as well as the second author, obtained the same separation but relied on the use of predicate symbols of unbounded arity.

A propositional proof system is weakly automatizable if there is a polynomial time algorithm which separates satisfiable formulas from formulas which have a short refutation in the system, with respect to a given length bound. We show that if the resolution proof system is weakly automatizable, then parity games can be decided in polynomial time. We give simple proofs that the same holds for depth-1 propositional calculus (where resolution has depth 0) with respect to mean payoff and simple stochastic games. We define a new type of combinatorial game and prove that resolution is weakly automatizable if and only if one can separate, by a set decidable in polynomial time, the games in which the first player has a positional winning strategy from the games in which the second player has a positional winning strategy.
Our main technique is to show that a suitable weak bounded arithmetic theory proves that both players in a game cannot simultaneously have a winning strategy, and then to translate this proof into propositional form.

This paper concerns the second order systems U^1_2 and V^1_2 of bounded arithmetic, which have proof theoretic strengths corresponding to polynomial space and exponential time computation. We formulate improved witnessing theorems for these two theories by using S^1_2 as a base theory for proving the correctness of the polynomial space or exponential time witnessing functions. We develop the theory of nondeterministic polynomial space computation in U^1_2 . Kołodziejczyk, Nguyen, and Thapen have introduced local improvement properties to characterize the provably total NP functions of these second order theories. We show that the strengths of their local improvement principles over U^1_2 and V^1_2 depend primarily on the topology of the underlying graph, not the number of rounds in the local improvement games. The theory U^1_2 proves the local improvement principle for linear graphs even without restricting to logarithmically many rounds. The local improvement principle for grid graphs with only logarithmically rounds is complete for the provably total NP search problems of V^1_2 . Related results are obtained for local improvement principles with one improvement round, and for local improvement over rectangular grids.

The paper corrects earlier upper bounds on the size of free-cut elimination. Free-cut elimination allows cut elimination to be carried out in the presence of non-logical axioms. The correction requires that the notion of a free-cut be modified so that a cut formula is anchored provided that all of its introductions are anchored, instead of only requiring that one of its introductions is anchored. With the correction, the originally proved size upper bounds remain unchanged. These results also apply to partial cut elimination. We also apply these bounds to elimination of cuts in propositional logic.
If the non-logical inferences are closed under cut and infer only atomic formulas, then all cuts can be eliminated. This generalizes earlier results of Takeuti and of Negri and van Plato.

Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations, and explicit bounds can be given. Developing a suitable notation system for Bounded Arithmetic, and applying these bounds, all the known results on definable functions of certain such theories can be reobtained in a uniform way.

The complexity class of Π^p_k – Polynomial Local Search (PLS) problems with Π^p_l – goal is introduced, and is used to give new characterisations of definable search problems in fragments of Bounded Arithmetic. The characterisations are established via notations for propositional proofs obtained by translating Bounded Arithmetic proofs using the Paris-Wilkie-translation. For l ≤ i ≤ k , the Σ bi – definable search problems of T^k+1_2 are exactly characterised by Π^p_k – PLS problems with Π^p_l – goals. These Π^p_k – PLS problems can be defined in a weak base theory such as S^1_2 , and proved to be total in T^k+1_2 . Furthermore, the Π^p_k – PLS definitions can be Skolemised with simple polynomial time functions. The Skolemised Π^p_k – PLS definitions give rise to a new ∀Σ^b_1(α) – principle conjectured to separate T^k_2(α) and T^k+1_2(α).

The complexity class of Π^p_k – polynomial local search (PLS) problems is introduced and is used to give new witnessing theorems for fragments of bounded arithmetic. For 1 ≤ i ≤ k+1 , the Σ^b_i – definable functions of T^k+1_2 are characterized in terms of Π^p_k – PLS problems. These Π^p_k – PLS problems can be defined in a weak base theory such as S^1_2 , and proved to be total in T^k+1_2 . Furthermore, the Π^p_k – PLS definitions can be skolemized with simple polynomial time functions, and the witnessing theorem itself can be formalized, and skolemized, in a weak base theory. We introduce a new ∀Σ^b_1(α) – principle that is conjectured to separate T^k_2(α) and T^k+1_2(α) .

We investigate the relation of countable closed linear orderings with respect to continuous monotone embeddability and show that there are exactly ℵ1 many equivalence classes with respect to this embeddability relation. This is an extension of Laver’s result, who considered (plain) embeddability, which yields coarser equivalence classes. Using this result we show that there are only ℵ0 many different Gödel logics.

We investigate the relation between logics of countable linear Kripke frames with constant domains and Gödel logics. We show that for any such Kripke frame there is a Gödel logic which coincides with the logic of this Kripke frame and vice versa. This allows us to transfer several recent results on Gödel logics to the logics of countable linear Kripke frames with constant domains.

We extend the definition of dynamic ordinals to generalised dynamic ordinals. We compute generalised dynamic ordinals of all fragments of relativised bounded arithmetic by utilising methods from Boolean complexity theory, similar to [Krajicek1994]. We indicate the role of generalised dynamic ordinals as universal measures for implicit computational complexity. I.e., we describe the connections between generalised dynamic ordinals and witness oracle Turing machines for bounded arithmetic theories. In particular, through the determination of generalised dynamic ordinals we re-obtain well-known independence results for relativised bounded arithmetic theories.

We define the notion of the uniform reduct of a propositional proof system as the set of those bounded formulas in the language of Peano Arithmetic which have polynomial size proofs under the Paris-Wilkie-translation. With respect to the arithmetic complexity of uniform reducts, we show that uniform reducts are Π^0_1-hard and obviously in Σ^0_2. We also show under certain regularity conditions that each uniform reduct is closed under bounded generalisation; that in the case the language includes a symbol for exponentiation, a uniform reduct is closed under modus ponens if and only if it already contains all true bounded formulas; and that each uniform reduct contains all true Π^b_1(α)-formulas.

This paper proves exponential separations between depth d-LK and depth (d+1/2)-LK for every d in 0, 1/2, 1, 1 1/2,… utilizing the order induction principle. As a consequence, we obtain an exponential separation between depth d-LK and depth (d+1)-LK for d in 0,1,2,… . We investigate the relationship between the sequence-size, tree-size and height of depth d-LK-derivations for d in 0, 1/2, 1, 1 1/2,… and describe transformations between them.

We define a general method to lift principles requiring exponential tree-size (d+1/2)-LK-refutations for d in 0,1,2,… to principles requiring exponential sequence-size d-LK-refutations, which will be described for the Ramsey principle and d=0. From this we also deduce width lower bounds for resolution refutations of the Ramsey principle.

The theories S^i_1(α) and T^i_1(α) are the analogues of Buss’ relativized bounded arithmetic theories in the language where every term is bounded by a polynomial, and thus all definable functions grow linearly in length. For every i , a Σ^b_i+1(α) – formula TOP^i(α), which expresses a form of the total ordering principle, is exhibited that is provable in S^i+1_1(α) , but unprovable in T^i_1(α). This is in contrast with the classical situation, where S^i+1_2 is conservative over T^i_2 w.r.t. Σ^b_i+1-sentences. The independence results are proved by translations into propositional logic, and using lower bounds for corresponding propositional proof systems.

We define and study a new restricted consistency notion for bounded arithmetic theories T2j. It is the strongest ∀Π1b-statement over S21 provable in T2j, similar to Con(Gi) in Krajíček and Pudlák, (Z. Math. Logik Grundl. Math. 36 (1990) 29) or RCon(Ti1) in Krajı́ček and Takeuti (Ann. Math. Artificial Intelligence 6 (1992) 107). The advantage of our notion over the others is that can directly be used to construct models of T2j. We apply this by proving preservation theorems for theories of bounded arithmetic of the following well-known kind: The ∀Π1b-separation of bounded arithmetic theories S2i from T2j (1⩽i⩽j) is equivalent to the existence of a model of S2i which does not have a Δ0b-elementary extension to a model of T2j.

Ordinal notations and provability of well-foundedness have been a central tool in the study of the consistency strength and computational strength of formal theories of arithmetic. This development began with Gentzen’s consistency proof for Peano arithmetic based on the well-foundedness of ordinal notations up to ε_0 . Since the work of Gentzen, ordinal notations and provable well-foundedness have been studied extensively for many other formal systems, some stronger and some weaker than Peano arithmetic. In the present paper, we investigate the provability and non-provability of well-foundedness of ordinal notations in very weak theories of bounded arithmetic, notably the theories S^i_2 and T^i_2 with 1 ≤ i ≤ 2 . We prove several results about the provability of well-foundedness for ordinal notations; our main results state that for the usual ordinal notations for ordinals below ε_0 and Γ_0, the theories T^i2 and S^2_2 can prove the ordinal Σ^b_1 – minimization principle over a bounded domain. PLS is the class of functions computed by a polynomial local search to minimize a cost function. It is a corollary of our theorems that the cost function can be allowed to take on ordinal values below Γ_0 , without increasing the class PLS .

Dynamic ordinal analysis is ordinal analysis for weak arithmetics like fragments of bounded arithmetic. In this paper we will define dynamic ordinals – they will be sets of number theoretic functions measuring the amount of Π^b_1(α) order induction available in a theory. We will compare order induction to successor induction over weak theories. We will compute dynamic ordinals of the bounded arithmetic theories Σ^b_n(α)-L^mIND for m=n and m=n+1, n≥0 . Different dynamic ordinals lead to separation. Therefore, we will obtain several separation results between these relativized theories. We will generalize our results to arbitrary languages extending the language of Peano arithmetic.

We consider equational theories for functions defined via recursion involving equations between closed terms with natural rules based on recursive definition of the function symbols. We show that consistency of such equational theories can be proved in the weak fragment of arithmetic S^1_2 . In particular this solves an open problem formulated by Takeuti.