Questions tagged [realizability]

Realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them.

Filter by
Sorted by
Tagged with
13 votes
1 answer
599 views

Kleene realizability in Peano arithmetic

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 ...
Gro-Tsen's user avatar
  • 29.9k
6 votes
1 answer
222 views

How is this HA unprovable formula recursive realizable?

In Realizability: A Historical Essay [Jaap van Oosten, 2002], it is said that recursive realizability and HA provability do not concur, because although every HA provable closed formula is realizable, ...
Kelley van Evert's user avatar
19 votes
1 answer
873 views

Can every simple polytope be inscribed in a sphere?

It is known that not every convex polytope (even polyhedron, e.g. this one) can be made inscribed, that is, we cannot always move its vertices so that all vertices end up on a common sphere, and the ...
M. Winter's user avatar
  • 12.5k
17 votes
2 answers
2k views

Why is Kleene's notion of computability better than Banach-Mazur's?

In this post about the difference between the recursive and effective topos, Andrej Bauer said: If you are looking for a deeper explanation, then perhaps it is fair to say that the Recursive Topos ...
Neel Krishnaswami's user avatar
6 votes
1 answer
276 views

Need help in trying to understand an argument by V. A. Yankov on the nonrealizability of Scott's axiom

(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 ...
Gro-Tsen's user avatar
  • 29.9k
5 votes
0 answers
130 views

What is known about propositional realizability for the second Kleene algebra and related PCAs?

Short version: Various things are known about realizability of propositional formulas for Kleene's “first algebra” (i.e., $\mathbb{N}$), like examples of realizable but unprovable formulas, and some ...
Gro-Tsen's user avatar
  • 29.9k
4 votes
1 answer
230 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 = \{ ...
Christopher King's user avatar