This paper is intended to give for a general mathematical audience a survey of intriguing connections between analytic combinatorics and logic. We define the ordinals below ε0 in non-logical terms and we survey a selection of recent results about the analytic combinatorics of these ordinals. Using a versatile and flexible compression technique we give applications to phase transitions for independence results, Hilbert’s basis theorem, local number theory, Ramsey theory, Hydra games, and Goodstein sequences. We discuss briefly universality and renormalization issues (...) in this context. Finally, we indicate how regularity properties of ordinal count functions can be used to prove logical limit laws. (shrink)

We study, from a classical point of view, how the truth of a statement about higher type functionals depends on the underlying model. The models considered are the classical set-theoretic finite type hierarchy and the constructively more meaningful models of continuous functionals, hereditarily effective operations, as well as the closed term model of Gödel's system T. The main results are characterisations of prenex classes for which truth in the full set-theoretic model transfers to truth in the other models. As a (...) corollary we obtain that the axiom of choice is not conservative over Gödel's system T with classical logic for closed ∃2-formulas. We hope that this study will contribute to a clearer delineation and perception of constructive mathematics from a classical perspective. (shrink)

This paper proves exponential separations between depth d-LK and depth -LK for every utilizing the order induction principle. As a consequence, we obtain an exponential separation between depth d-LK and depth -LK for . We investigate the relationship between the sequence-size, tree-size and height of depth d-LK-derivations for , and describe transformations between them. We define a general method to lift principles requiring exponential tree-size -LK-refutations for 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. (shrink)

We define and study a new restricted consistency notion RCon ∗ for bounded arithmetic theories T 2 j . It is the strongest ∀ Π 1 b -statement over S 2 1 provable in T 2 j , similar to Con in Krajíček and Pudlák, 29) or RCon in Krajı́ček and Takeuti 107). The advantage of our notion over the others is that RCon ∗ can directly be used to construct models of T 2 j . We apply this by (...) proving preservation theorems for theories of bounded arithmetic of the following well-known kind: The ∀ Π 1 b -separation of bounded arithmetic theories S 2 i from T 2 j is equivalent to the existence of a model of S 2 i which does not have a Δ 0 b -elementary extension to a model of T 2 j . More specific, let M ⊨ Ω 1 nst denote that there is a nonstandard element c in M such that the function n ↦ 2 log c is total in M . Let BLΣ 1 b be the bounded collection schema for Σ 1 b -formulas. We obtain the following preservation results: the ∀ Π 1 b -separation of S 2 i from T 2 j is equivalent to the existence of 1. a model of S 2 i +Ω 1 nst which is 1 b -closed w.r.t. T 2 j , 2. a countable model of S 2 i + BLΣ 1 b without weak end extensions to models of T 2 j. (shrink)

The theories Si1 and Ti1 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 Σbi+1-formula TOPi, which expresses a form of the total ordering principle, is exhibited that is provable in Si+11 , but unprovable in Ti1. This is in contrast with the classical situation, where Si+12 is conservative over Ti2 w. r. t. Σbi+1-sentences. The independence (...) results are proved by translations into propositional logic, and using lower bounds for corresponding propositional proof systems. (shrink)

Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations. 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.