All Questions
1 question
4
votes
1
answer
258
views
What is the theory of statements with a provably *bounded* realizer (according to PA)?
$\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 = \{ ...