Questions tagged [realizability]
Realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them.
16
questions
12
votes
1
answer
338
views
How exactly are realizability and the Curry-Howard correspondence related?
Consider, on the one hand:
the Curry-Howard correspondence between, on the one hand, types and terms (programs) in various flavors of typed $\lambda$-calculus, and on the other, propositions and ...
- 28.4k
3
votes
0
answers
86
views
Comparing computable structures via Kleene and Skolem
Below, by "structure" I mean "computable structure in a finite language with domain $\omega$," and by "sentence" I mean "finitary first-order sentence containing no ...
- 19.1k
6
votes
0
answers
117
views
An analogue of Scott sentences in the (mostly) computable realm?
Below, "structure" means "computable structure in a computable language." In particular, we do distinguish between isomorphic copies of the same structure.
Let $\mathcal{L}_{\...
- 19.1k
5
votes
1
answer
248
views
Which arithmetical sentences have no counterexamples in the sense of Kreisel?
It is a well-known fact that given a first-order sentence $\psi$ in prenex normal form $\forall x_1 \exists y_1 \forall x_2 \exists y_2 \dots \forall x_n \exists y_n \theta(x_1,\dots,x_n,y_1,\dots,y_n)...
- 10.1k
4
votes
1
answer
374
views
Homotopical realizability
After a long story of dancing around the effective topos $ \mathcal{Eff}$, I finally resolved to get to the bottom of it. To this effect, working as it were backward, I ended up revisiting Kleene's ...
- 7,487
6
votes
1
answer
432
views
Realizability for constructive Zermelo-Fraenkel set theory
$ \def \CZF {\mathbf {CZF}}
\def \IZF {\mathbf {IZF}}
\def \A {\mathcal A}
\def \then {\mathrel \rightarrow}
\def \r {\mathrel \Vdash}
\DeclareMathOperator \V V $
In "Realizability for ...
- 305
11
votes
0
answers
131
views
Stack completions in realizability toposes
An internal category $\mathbb A$ in an elementary topos $\mathcal E$ is called an (intrinsic) stack if the indexed category that it represents, $(X\in \mathcal E) \mapsto \mathcal{E}(X,\mathbb A) \in \...
- 64.1k
7
votes
1
answer
228
views
Are there simplicial spheres with "non-geometric symmetries"?
Let $\Delta$ be a simplicial sphere, that is, a finite (abstract) simplicial complex whose canonical geometric realization $|\Delta|$ is homeomorphic to a sphere $\mathbf S^d\subset\Bbb R^{d+1}$.
...
- 11.9k
5
votes
1
answer
218
views
Is there a polytope with an essentially unique shape?
More percisely:
Question: Is there a (convex) polytope that has a unique realization up to, say, projective transformations?
I suppose I have to assume that it has more than $d+2$ vertices/facets if ...
- 11.9k
19
votes
1
answer
844
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 ...
- 11.9k
10
votes
1
answer
419
views
Computability-theoretic results relevant to realizability
This may be a very naive question which only reflects my failure at literature search, but:
Although realizability (in its original form at least) is grounded in computability, the details of ...
- 19.1k
11
votes
1
answer
440
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 ...
- 28.4k
5
votes
1
answer
199
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, ...
- 163
5
votes
0
answers
374
views
Did Kleene constructively prove Brouwer's axioms?
Harvey Friedman's request on the FoM-forum for an overview of current intuitionistic foundations revived the following question, which I have been meaning to ask for five years. (I'm no expert on ...
- 1,616
5
votes
0
answers
322
views
A polytime feasible subuniverse of the Effective Topos
The effective topos is a well known universe of sets suitable for abstract computability, as it is build "from the ground up" via the classical notion of realisability by Kleene.
I have found a few ...
- 7,487
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 ...
- 8,993