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
5 votes
1 answer
211 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)...
user avatar
  • 6,364
3 votes
1 answer
314 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 ...
user avatar
6 votes
1 answer
361 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 ...
user avatar
11 votes
0 answers
119 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 \...
user avatar
  • 58.9k
7 votes
1 answer
213 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}$. ...
user avatar
  • 9,513
5 votes
1 answer
194 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 ...
user avatar
  • 9,513
17 votes
1 answer
701 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 ...
user avatar
  • 9,513
10 votes
1 answer
384 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 ...
user avatar
9 votes
1 answer
355 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 ...
user avatar
  • 21.7k
5 votes
1 answer
159 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, ...
user avatar
5 votes
0 answers
352 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 ...
user avatar
4 votes
0 answers
305 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 ...
user avatar
14 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 ...
user avatar