We introduce the notion of τ-like partial order, where τ is one of the linear order types ω, ω*, ω + ω*, and ζ. For example, being ω-like means that every element has finitely many predecessors, while being ζ-like means that every interval is finite. We consider statements of the form “any τ-like partial order has a τ-like linear extension” and “any τ-like partial order is embeddable into τ” . Working in the framework of reverse mathematics, we show that these (...) statements are equivalent either to equation image or to equation image over the usual base system equation image. (shrink)

Goodman’s theorem states that HAω+AC+RDC is conservative over HA. The same result applies to the extensional case, that is, E-HAω+AC+RDC is also conservative over HA. This is due to Beeson. In this article, we modified the Goodman realizability and provide a new proof of the extensional case.

In this paper we study the reverse mathematics of two theorems by Bonnet about partial orders. These results concern the structure and cardinality of the collection of initial intervals. The first theorem states that a partial order has no infinite antichains if and only if its initial intervals are finite unions of ideals. The second one asserts that a countable partial order is scattered and does not contain infinite antichains if and only if it has countably many initial intervals. We (...) show that the left to right directions of these theorems are equivalent to ACA0 and ATR0, respectively. On the other hand, the opposite directions are both provable in WKL0, but not in RCA0. We also prove the equivalence with ACA0 of the following result of Erdös and Tarski: a partial order with no infinite strong antichains has no arbitrarily large finite strong antichains. (shrink)

A quasi-order Q induces two natural quasi-orders on $${\mathcal{P}(Q)}$$, but if Q is a well-quasi-order, then these quasi-orders need not necessarily be well-quasi-orders. Nevertheless, Goubault-Larrecq (Proceedings of the 22nd Annual IEEE Symposium 4 on Logic in Computer Science (LICS’07), pp. 453–462, 2007) showed that moving from a well-quasi-order Q to the quasi-orders on $${\mathcal{P}(Q)}$$ preserves well-quasi-orderedness in a topological sense. Specifically, Goubault-Larrecq proved that the upper topologies of the induced quasi-orders on $${\mathcal{P}(Q)}$$ are Noetherian, which means that they contain no (...) infinite strictly descending sequences of closed sets. We analyze various theorems of the form “if Q is a well-quasi-order then a certain topology on (a subset of) $${\mathcal{P}(Q)}$$ is Noetherian” in the style of reverse mathematics, proving that these theorems are equivalent to ACA 0 over RCA 0. To state these theorems in RCA 0 we introduce a new framework for dealing with second-countable topological spaces. (shrink)

In [17], we introduced an extensional variant of generic realizability [22], where realizers act extensionally on realizers, and showed that this form of realizability provides inner models of $\mathsf {CZF}$ (constructive Zermelo–Fraenkel set theory) and $\mathsf {IZF}$ (intuitionistic Zermelo–Fraenkel set theory), that further validate $\mathsf {AC}_{\mathsf {FT}}$ (the axiom of choice in all finite types). In this paper, we show that extensional generic realizability validates several choice principles for dependent types, all exceeding $\mathsf {AC}_{\mathsf {FT}}$. We then show that adding (...) such choice principles does not change the arithmetic part of either $\mathsf {CZF}$ or $\mathsf {IZF}$. (shrink)

We consider fragments of uniform reflection for formulas in the analytic hierarchy over theories of second order arithmetic. The main result is that for any second order arithmetic theory $T_0$ extending $\mathsf {RCA}_0$ and axiomatizable by a $\Pi ^1_{k+2}$ sentence, and for any $n\geq k+1$, $$\begin{align*}T_0+ \mathrm{RFN}_{\varPi^1_{n+2}} \ = \ T_0 + \mathrm{TI}_{\varPi^1_n}, \end{align*}$$ $$\begin{align*}T_0+ \mathrm{RFN}_{\varSigma^1_{n+1}} \ = \ T_0+ \mathrm{TI}_{\varPi^1_n}^{-}, \end{align*}$$ where T is $T_0$ augmented with full induction, and $\mathrm {TI}_{\varPi ^1_n}^{-}$ denotes the schema of transfinite induction up (...) to $\varepsilon _0$ for $\varPi ^1_n$ formulas without set parameters. (shrink)

Shoenfield’s completeness theorem states that every true first order arithmetical sentence has a recursive \-proof encodable by using recursive applications of the \-rule. For a suitable encoding of Gentzen style \-proofs, we show that Shoenfield’s completeness theorem applies to cut free \-proofs encodable by using primitive recursive applications of the \-rule. We also show that the set of codes of \-proofs, whether it is based on recursive or primitive recursive applications of the \-rule, is \ complete. The same \ completeness (...) results apply to codes of cut free \-proofs. (shrink)