We present a list of open questions in reverse mathematics, including some relevant background information for each question. We also mention some of the areas of reverse mathematics that are starting to be developed and where interesting open question may be found.

A statement of hyperarithmetic analysis is a sentence of second order arithmetic S such that for every Y⊆ω, the minimum ω-model containing Y of RCA0 + S is HYP, the ω-model consisting of the sets hyperarithmetic in Y. We provide an example of a mathematical theorem which is a statement of hyperarithmetic analysis. This statement, that we call INDEC, is due to Jullien [13]. To the author's knowledge, no other already published, purely mathematical statement has been found with this property (...) until now. We also prove that, over RCA0, INDEC is implied by [Formula: see text] and implies ACA0, but of course, neither ACA0, nor ACA 0+ imply it. We introduce five other statements of hyperarithmetic analysis and study the relations among them. Four of them are related to finitely-terminating games. The fifth one, related to iterations of the Turing jump, is strictly weaker than all the other statements that we study in this paper, as we prove using Steel's method of forcing with tagged trees. (shrink)

We study the complexity of the isomorphism relation on classes of computable structures. We use the notion of FF-reducibility introduced in [9] to show completeness of the isomorphism relation on many familiar classes in the context of all ${\mathrm{\Sigma }}_{1}^{1}$ equivalence relations on hyperarithmetical subsets of ω.

We prove that the maximal order type of the wqo of linear orders of finite Hausdorff rank under embeddability is φ2, the first fixed point of the ε-function. We then show that Fraïssé’s conjecture restricted to linear orders of finite Hausdorff rank is provable in +“φ2 is well-ordered” and, over , implies +“φ2 is well-ordered”.

Two linear orderings are equimorphic if each can be embedded into the other. We prove that every hyperarithmetic linear ordering is equimorphic to a recursive one. On the way to our main result we prove that a linear ordering has Hausdorff rank less than $\omega _{1}^{\mathit{CK}}$ if and only if it is equimorphic to a recursive one. As a corollary of our proof we prove that, given a recursive ordinal α, the partial ordering of equimorphism types of linear orderings of (...) Hausdorff rank at most α ordered by embeddablity is recursively presentable. (shrink)

We say that a linear ordering is extendible if every partial ordering that does not embed can be extended to a linear ordering which does not embed either. Jullien’s theorem is a complete classification of the countable extendible linear orderings. Fraïssé’s conjecture, which is actually a theorem, is the statement that says that the class of countable linear ordering, quasiordered by the relation of embeddability, contains no infinite descending chain and no infinite antichain. In this paper we study the strength (...) of these two theorems from the viewpoint of Reverse Mathematics and Effective Mathematics. As a result of our analysis we get that they are equivalent over the basic system of .We also prove that Fraïssé’s conjecture is equivalent, over , to two other interesting statements. One that says that the class of well founded labeled trees, with labels from {+,−}, and with a very natural order relation, is well quasiordered. The other statement says that every linear ordering which does not contain a copy of the rationals is equimorphic to a finite sum of indecomposable linear orderings.While studying the proof theoretic strength of Jullien’s theorem, we prove the extendibility of many linear orderings, including ω2 and η, using just . Moreover, for all these linear orderings, , we prove that any partial ordering, , which does not embed has a linearization, hyperarithmetic in , which does not embed. (shrink)

We study the computability-theoretic complexity and proof-theoretic strength of the following statements: (1) "If X is a well-ordering, then so is ε X ", and (2) "If X is a well-ordering, then so is φ(α, X)", where α is a fixed computable ordinal and φ represents the two-placed Veblen function. For the former statement, we show that ω iterations of the Turing jump are necessary in the proof and that the statement is equivalent to ${\mathrm{A}\mathrm{C}\mathrm{A}}_{0}^{+}$ over RCA₀. To prove the (...) latter statement we need to use ω α iterations of the Turing jump, and we show that the statement is equivalent to ${\mathrm{\Pi }}_{{\mathrm{\omega }}^{\mathrm{\alpha }}}^{0}{-\mathrm{C}\mathrm{A}}_{0}$ . Our proofs are purely computability-theoretic. We also give a new proof of a result of Friedman: the statement "if x is a well-ordering, then so is φ(x, 0)" is equivalent to ATR₀ over RCA₀. (shrink)

These are the lecture notes from a 10-hour course that the author gave at the University of Notre Dame in September 2010. The objective of the course was to introduce some basic concepts in computable structure theory and develop the background needed to understand the author’s research on back-and-forth relations.

We study the proof-theoretic strength of the Π11-separation axiom scheme, and we show that Π11-separation lies strictly in between the Δ11-comprehension and Σ11-choice axiom schemes over RCA0.

We prove that the existential theory of the Turing degrees, in the language with Turing reduction, 0, and unary relations for the classes in the generalized high/low hierarchy, is decidable. We also show that every finite poset labeled with elements of (where is the partition of induced by the generalized high/low hierarchy) can be embedded in preserving the labels. Note that no condition is imposed on the labels.

Tarski defined a way of assigning to each Boolean algebra, B, an invariant inv(B) ∈ In, where In is a set of triples from ℕ, such that two Boolean algebras have the same invariant if and only if they are elementarily equivalent. Moreover, given the invariant of a Boolean algebra, there is a computable procedure that decides its elementary theory. If we restrict our attention to dense Boolean algebras, these invariants determine the algebra up to isomorphism. In this paper we (...) analyze the complexity of the question "Does B have invariant x?" For each x ∈ In we define a complexity class Γx that could be either Σⁿ, Πⁿ, Σⁿ ∧ Πⁿ, or Πω+1 depending on x, and we prove that the set of indices for computable Boolean algebras with invariant x is complete for the class Γx. Analogs of many of these results for computably enumerable Boolean algebras were proven in earlier works by Selivanov. In a more recent work, he showed that similar methods can be used to obtain the results for computable ones. Our methods are quite different and give new results as well. As the algebras we construct to witness hardness are all dense, we establish new similar results for the complexity of various isomorphism problems for dense Boolean algebras. (shrink)

We prove Fraïssé’s conjecture within the system of Π11-comprehension. Furthermore, we prove that Fraïssé’s conjecture follows from the Δ20-bqo-ness of 3 over the system of Arithmetic Transfinite Recursion, and that the Δ20-bqo-ness of 3 is a Π21-statement strictly weaker than Π11-comprehension.

We prove that there is a structure, indeed a linear ordering, whose degree spectrum is the set of all non-hyperarithmetic degrees. We also show that degree spectra can distinguish measure from category.

Fraïssé studied countable structures S through analysis of the age of S i.e., the set of all finitely generated substructures of S. We investigate the effectiveness of his analysis, considering effectively presented lists of finitely generated structures and asking when such a list is the age of a computable structure. We focus particularly on the Fraïssé limit. We also show that degree spectra of relations on a sufficiently nice Fraïssé limit are always upward closed unless the relation is definable by (...) a quantifier-free formula. We give some sufficient or necessary conditions for a Fraïssé limit to be spectrally universal. As an application, we prove that the computable atomless Boolean algebra is spectrally universal. (shrink)

In (Fund Math 60:175–186 1967), Wolk proved that every well partial order (wpo) has a maximal chain; that is a chain of maximal order type. (Note that all chains in a wpo are well-ordered.) We prove that such maximal chain cannot be found computably, not even hyperarithmetically: No hyperarithmetic set can compute maximal chains in all computable wpos. However, we prove that almost every set, in the sense of category, can compute maximal chains in all computable wpos. Wolk’s original result (...) actually shows that every wpo has a strongly maximal chain, which we define below. We show that a set computes strongly maximal chains in all computable wpo if and only if it computes all hyperarithmetic sets. (shrink)

We construct a computable ℵ0-categorical structure whose first order theory is computably equivalent to the true first order theory of arithmetic.

Assuming that $0^\#$ exists, we prove that there is a structure that can effectively interpret its own jump. In particular, we get a structure $\mathcal A$ such that \[ \textit{Sp}({\mathcal A}) = \{{\bf x}'\colon {\bf x}\in \textit{Sp}({\mathcal A})\}, \] where $\textit{Sp}({\mathcal A})$ is the set of Turing degrees which compute a copy of $\mathcal A$. More interesting than the result itself is its unexpected complexity. We prove that higher-order arithmetic, which is the union of full $n$th-order arithmetic for all $n$, (...) cannot prove the existence of such a structure. (shrink)