All Questions

For completeness of MathOverflow and for clarity of the question, I will first recall a few things, including the the definition of Kleene realizability: experts can jump directly to the question ...

There is a widely accepted opinion that the Axiom of Countable Choice (further, ACC) $$ \forall n\in \mathbb{N} . \exists x \in X . \varphi [n, x] \implies \exists f: \mathbb{N} \longrightarrow X . \...

(This is really long because I give a lot of context, but you can skip right to the end where the excerpt I'm trying to make sense of is copied and translated.) Background: I'm trying to understand ...

$\let\T\mathrm\def\kr{\mathrel{\mathbf r}}$This is a follow up to Kleene realizability in Peano arithmetic. We can summarize the results from Emil Jeřábek's answer as follows: \begin{gather*} T_1 = \{ ...