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.

We investigate the strength of the existence of a non-principal ultrafilter over fragments of higher-order arithmetic. Let [Formula: see text] be the statement that a non-principal ultrafilter on ℕ exists and let [Formula: see text] be the higher-order extension of ACA0. We show that [Formula: see text] is [Formula: see text]-conservative over [Formula: see text] and thus that [Formula: see text] is conservative over PA. Moreover, we provide a program extraction method and show that from a proof of a strictly (...) [Formula: see text] statement ∀ f ∃ g A qf in [Formula: see text] a realizing term in Gödel's system T can be extracted. This means that one can extract a term t ∈ T, such that ∀ f A qf). (shrink)

ZusammenfassungP. Bernays hat darauf hingewiesen, dass man, um die Widerspruchs freiheit der klassischen Zahlentheorie zu beweisen, den Hilbertschen flniter Standpunkt dadurch erweitern muss, dass man neben den auf Symbole sich beziehenden kombinatorischen Begriffen gewisse abstrakte Begriffe zulässt, Die abstrakten Begriffe, die bisher für diesen Zweck verwendet wurden, sinc die der konstruktiven Ordinalzahltheorie und die der intuitionistischer. Logik. Es wird gezeigt, dass man statt deesen den Begriff einer berechenbaren Funktion endlichen einfachen Typs über den natürlichen Zahler benutzen kann, wobei keine anderen (...) Konstruktionsverfahren für solche Funktionen nötig sind, als einfache Rekursion nach einer Zahlvariablen und Einsetzung von Funktionen ineinander .P. Bernays has pointed out that, in order to prove the consistency of classical number theory, it is necessary to extend Hilbert's finitary stand‐point by admitting certain abstract concepts in addition to the combinatorial concepts referring to symbols. The abstract concepts that so far have been used for this purpose are those of the constructive theory of ordinals and those of intuitionistic logic. It is shown that the concept of a computable function of finite simple type over the integers can be used instead, where no other procedures of constructing such functions are necessary except simple recursion by an integral variable and substitution of functions in each other. (shrink)