Related papers: The Veblen functions for computability theorists
Several theorems about the equivalence of familiar theories of reverse mathematics with certain well-ordering principles have been proved by recursion-theoretic and combinatorial methods (Friedman, Marcone, Montalban et al.) and with…
A well-ordering principle is a principle of the form: If $X$ is well-ordered then $F(X)$ is well-ordered, where $F$ is some natural operator transforming linear orders into linear orders. Many important subsystems of Second-order Arithmetic…
We conclude from Goedel's Theorem VII of his seminal 1931 paper that every recursive function f(x_{1}, x_{2}) is representable in the first-order Peano Arithmetic PA by a formula [F(x_{1}, x_{2}, x_{3})] which is algorithmically verifiable,…
We use forcing over admissible sets to show that, for every ordinal $\alpha$ in a club $C\subset\omega_1$, there are copies of $\alpha$ such that the isomorphism between them is not computable in the join of the complete $\Pi^1_1$ set…
We investigate the complexity of isomorphisms of computable structures on cones in the Turing degrees. We show that, on a cone, every structure has a strong degree of categoricity, and that degree of categoricity is $\bf{0^{(\alpha)}}$ for…
The notion of computability closure has been introduced for proving the termination of the combination of higher-order rewriting and beta-reduction. It is also used for strengthening the higher-order recursive path ordering. In the present…
Selman's Theorem in classical Computability Theory gives a characterization of the enumeration reducibility for arbitrary sets in terms of the enumeration reducibility on the total sets: $A \le_e B \iff \forall X [X \equiv_{e} X \oplus…
In this paper we consider transfinite provability logics where for each ordinal in some recursive well-order we have a corresponding modal provability operator. The modality [xi] will be interpreted as "provable in ACA_0 together with at…
We examine the computable part of the differentiability hierarchy defined by Kechris and Woodin. In that hierarchy, the rank of a differentiable function is an ordinal less than omega_1 which measures how complex it is to verify…
It is well-known that natural axiomatic theories are well-ordered by consistency strength. However, it is possible to construct descending chains of artificial theories with respect to consistency strength. We provide an explanation of this…
In mathematical logic there are two seemingly distinct kinds of principles called "reflection principles." Semantic reflection principles assert that if a formula holds in the whole universe, then it holds in a set-sized model. Syntactic…
Computability relative to a partial function $f$ on the natural numbers can be formalized using the notion of an oracle for this function $f$. This can be generalized to arbitrary partial combinatory algebras, yielding a notion of…
In this paper we give an ordinal analysis of the theory of second order arithmetic. We do this by working with proof trees -- that is, "deductions" which may not be well-founded. Working in a suitable theory, we are able to represent…
A type-2 computable real function is necessarily continuous; and this remains true for relative, i.e. oracle-based computations. Conversely, by the Weierstrass Approximation Theorem, every continuous f:[0,1]->R is computable relative to…
Let \alpha be a countable ordinal and \P(\alpha) the collection of its subsets isomorphic to \alpha. We show that the separative quotient of the set \P (\alpha) ordered by the inclusion is isomorphic to a forcing product of iterated reduced…
We reevaluate the claim that predicative reasoning (given the natural numbers) is limited by the Feferman-Schutte ordinal Gamma_0. First we comprehensively criticize the arguments that have been offered in support of this position. Then we…
This paper aims at carrying out termination proofs for simply typed higher-order calculi automatically by using ordering comparisons. To this end, we introduce the computability path ordering (CPO), a recursive relation on terms obtained by…
We recently described a formalism for reasoning with if-then rules that re expressed with different levels of firmness [18]. The formalism interprets these rules as extreme conditional probability statements, specifying orders of magnitude…
Inspired by Leivant's work on absolute predicativism, Bellantoni and Cook in 1992 introduced a structurally restricted form of recursion called predicative recursion. Using this recursion scheme on the inductive structures of natural…
It is well-known that natural axiomatic theories are pre-well-ordered by logical strength, according to various characterizations of logical strength such as consistency strength and inclusion of $\Pi^0_1$ theorems. Though these notions of…