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
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
14 votes
1 answer
481 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 ...
Gro-Tsen's user avatar
  • 29.8k
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.8k
11 votes
1 answer
441 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 ...
Noah Schweber's user avatar
11 votes
0 answers
137 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 \...
Mike Shulman's user avatar
7 votes
1 answer
448 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 ...
Mohsen Shahriari's user avatar
7 votes
1 answer
230 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}$. ...
M. Winter's user avatar
  • 12.5k
7 votes
0 answers
129 views

Logical properties of realizability (topoi or McCarty models) defined by alpha-recursion on admissible ordinals

Setup: Let $\alpha$ be an admissible ordinal (viꝫ., one such that $L_\alpha$ is a model of Kripke-Platek set theory), identified as usual with the set of ordinals $<\alpha$. Then there is a ...
Gro-Tsen's user avatar
  • 29.8k
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
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.8k
6 votes
0 answers
205 views

What are these non-classical versions of ZFC defined by realizability?

See Kleene realizability in Peano arithmetic for a similar question, but about PA instead of ZFC. In the context of constructive set theory, consider two ways of defining realizability. The first is $\...
Christopher King's user avatar
6 votes
0 answers
121 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}_{\...
Noah Schweber's user avatar
5 votes
1 answer
259 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)...
James Hanson's user avatar
  • 10.3k
5 votes
1 answer
223 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 ...
M. Winter's user avatar
  • 12.5k
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.8k
5 votes
0 answers
379 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 ...
Franka Waaldijk's user avatar
5 votes
0 answers
323 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 ...
Mirco A. Mannucci's user avatar
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
4 votes
1 answer
387 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 ...
Mirco A. Mannucci's user avatar
3 votes
0 answers
74 views

What does the computation of irrationality and transcendentality via a fancy implementation of analytic Markov's property look like?

Proofs that various real numbers are not rational or not algebraic tend to be constructively valid as is. Examples include the proofs that $\sqrt 2$ and $\log_2(3)$ are not rational and that $e$ is ...
Christopher King's user avatar
3 votes
0 answers
91 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 ...
Noah Schweber's user avatar