In this paper we calibrate the exact proof-theoretic strength of Kruskal's theorem, thereby giving, in some sense, the most elementary proof of Kruskal's theorem. Furthermore, these investigations give rise to ordinal analyses of restricted bar induction.

Guessing the outcome of iterations of even most simple arithmetical functions could be an extremely hazardous experience. Not less harder, if at all possible, might be to prove the veracity of even a "sure" guess concerning iterations : this is the case of the famous 3x+1 conjecture. Our purpose here is to study and conceptualize some intuitive insights related to the ultimate (un)solvability of this conjecture.

"The definitive clarification of the nature of the infinite has become necessary, not merely for the special interests of the individual sciences, but rather for the honour of the human understanding itself. The infinite has always stirred the emotions of mankind more deeply than any other question; the infinite has stimulated and fertilized reason as few other ideas have ; but also the infinite, more than other notion, is in need of clarification." (David Hilbert 1925).

This paper proves the finite axiomatizability of transitive modal logics of finite depth and finite width w.r.t. proper-successor-equivalence. The frame condition of the latter requires, in a rooted transitive frame, a finite upper bound of cardinality for antichains of points with different sets of proper successors. The result generalizes Rybakov’s result of the finite axiomatizability of extensions of$\mathbf {S4}$of finite depth and finite width.

We consider total well-founded orderings on monadic terms satisfying the replacement and full invariance properties. We show that any such ordering on monadic terms in one variable and two unary function symbols must have order type $\omega, \omega^2$ or $\omega^\omega$. We show that a familiar construction gives rise to continuum many such orderings of order type $\omega$. We construct a new family of such orderings of order type $\omega^2$, and show that there are continuum many of these. We show that (...) there are only four such orderings of order type $\omega^\omega$, the two familiar recursive path orderings and two closely related orderings. We consider also total well-founded orderings on $\mathbf{N}^n$ which are preserved under vector addition. We show that any such ordering must have order type $\omega^k$ for some $1 \leq k \leq n$. We show that if $k < n$ there are continuum many such orderings, and if $k = n$ there are only $n$!, the $n$! lexicographic orderings. (shrink)

We consider total well-founded orderings on monadic terms satisfying the replacement and full invariance properties. We show that any such ordering on monadic terms in one variable and two unary function symbols must have order typeω,ω2orωω. We show that a familiar construction gives rise to continuum many such orderings of order typeω. We construct a new family of such orderings of order typeω2, and show that there are continuum many of these. We show that there are only four such orderings (...) of order typeωω, the two familiar recursive path orderings and two closely related orderings. We consider also total well-founded orderings onNnwhich are preserved under vector addition. We show that any such ordering must have order typeωkfor some 1 ≤k≤n. We show that ifkshrink)

A poset is well‐partially ordered (WPO) if all its linear extensions are well orders; the supremum of ordered types of these linear extensions is the length, of p. We prove that if the vertex set X is infinite, of cardinality κ, and the ordering ⩽ is the intersection of finitely many well partial orderings of X,, then, letting, with, denote the euclidian division by κ (seen as an initial ordinal) of the length of each corresponding poset: where denotes the least (...) initial ordinal greater than the ordinal. This inequality is optimal. This result answers questions of Forster. (shrink)

Subrecursive hierarchy classifications are used to compare the complexities of recursive functions according to their derivations in a version of Kleene's equation calculus, and their computations by term-rewriting. In each case ordinal bounds are assigned, and it turns out that the respective complexity measures are given by a version of the Fast Growing Hierarchy, and the Slow Growing Hierarchy. Known comparisons between the two hierarchies then provide ordinal trade-offs between derivation and computation. Characteristics of some well-known subrecursive classes are also (...) read off. (shrink)