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.

conference

In: Bradfield J. (eds) Computer Science Logic. CSL 2002. Lecture Notes in Computer Science, vol 2471. Springer, Berlin, Heidelberg, Pages 599 - 612.

Publication year: 2002

Height restricted resolution (proofs or refutations) is a natural restriction of resolution where the height of the corresponding proof tree is bounded. Height restricted resolution does not distinguish between tree- and sequence-like proofs. We show that polylogarithmic-height resolution is strongly connected to the bounded arithmetic theory S^1_2(\alpha) . We separate polylogarithmic-height resolution from quasi-polynomial size tree-like resolution. Inspired by this we will study infinitely many sub-linear-height restrictions given by functions n → 2_i((log^(i+1) n)^O(1)) for i ≥ 0 . We show that the resulting resolution systems are connected to certain bounded arithmetic theories, and that they form a strict hierarchy of resolution proof systems. To this end we will develop some proof theory for height restricted proofs.

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.

We define a coding of natural numbers — which we will call the exponential notations — and interpretations of the less-than-relation, the successor function, addition and exponentiation on the exponential notations. We prove that all these interpretations are polynomial time computable. As an application we show that we can interpret terms over a certain restricted language — including exponentiation — in polynomial time on exponential notations.

conference

9th International Conference, LPAR 2002, Tbilisi, Georgia, October 14-18, 2002, Pages: 53 - 67

Publication year: 2002

This note is a case study for finding universal measures for weak implicit complexity. We will instanciate “universal measures” by “dynamic ordinals”, and “weak implicit complexity” by “bounded arithmetic”. Concretely, we will describe the connection between dynamic ordinals and witness oracle Turing machines for bounded arithmetic theories.

We show that there is a primitive recursive tree which is not well-founded, but which is well-founded for co-r.e. sets, provable in Σ_1-Ind. It follows that the supremum of order-types of primitive recursive well-orderings, whose well-foundedness on co-r.e. sets is provable in Σ_1-Ind, equals the limit of all recursive ordinals.

We determine the exact bounds for the length of an arbitrary reduction sequence of a term in the typed λ – calculus with β -, ξ – and η – conversion. There will be two essentially different classifications, one depending on the height and the degree of the term and the other depending on the length and the degree of the term.

We use a modified Howard-Schütte-function [ ]_0 which assigns finite ordinals to each term from Tpred and which witnesses the strong normalization for T^pred . Furthermore the derivation lengths function for T^pred is elementary recursive, hence representable functions in T^pred are computable in elementary time, hence are elementary recursive. On the other hand it is shown that random-access machine transitions can be simulated in simple typed combinatorial calculus with combinators for the case distinction function and for the predecessor function, hence T^pred represents any elementary recursive function.

Inspired from Buchholz’ ordinal analysis of ID_1 and Beckmann’s analysis of the simple typed λ – calculus we classify the derivation lengths for Gödel’s system T in the λ – formulation (where the η – rule is included).

In this paper we introduce an infinitary proof system for a language of second order arithmetic which is complete for Pi^1_1 – sentences. The main observation there is the Boundedness Theorem telling that the order-type of a Sigma^1_1 – definable well-ordering < is less than or equal to the truth complexity of TI(<) . The commonly known Boundedness Principle of Generalized Recursion Theory will be obtained as a consequence of our proof theoretical Boundedness Theorem which in turn is a consequence of cut-freeness. This yields a proof of the Boundedness Principle which does not use the Analytical Hierarchy Theorem.

The aim of this work is to investigate proof-theoretically formal theories of bounded arithmetic. For this purpose the subsystems IΣ_n of first order arithmetic and subsystems of bounded predicative arithmetic will be investigated, too.

A natural term rewriting framework for the Bellantoni Cook schemata of predicative recursion, which yields a canonical definition of the polynomial time computable functions, is introduced. In terms of an exponential function both, an upper bound and a lower bound are proved for the resulting derivation lengths of the functions in question. It is proved that any natural reduction strategy yields an algorithm which runs in exponential time. We give an example in which this estimate is tight. It is proved that the resulting derivation lengths become polynomially bounded in the lengths of the inputs if the rewrite rules are only applied to terms in which the safe arguments – no restrictions are assumed for the normal arguments – consist of values, i.e. numerals, and not of names, i.e. non numeral terms. It is proved that in the latter situation any inside first reduction strategy and any head reduction strategy yield algorithms, for the function under consideration, for which the running time is bounded by an appropriate polynomial in the lengths of the input. A feasible rewrite system for predicative recursion with predicative parameter substitution is defined. It is proved that the derivation lengths of this rewrite system are polynomially bounded in the lengths of the inputs. As a corollary we reobtain Bellantoni´s result stating that predicative recursion is closed under predicative parameter recursion.

This master thesis gives a detailed workout of Takeuti’s article *A Second Order Version of S^i_2 and U^1_2* including some improvements.