Questions tagged [realizability]
Realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them.
35 questions
9 votes
0 answers
248 views
Characterization theorems for lambda calculus realizability
There are theorems characterizing Kleene's realizability$\def\realize{\mathbin{\textbf{r}}}$ in various systems. For example, $$\textsf{HA} \vdash \exists n,n \realize \varphi \iff \exists n. \textsf{...
- 2,146
2 votes
0 answers
129 views
Logical differences between Effective and Kleene-Vesley topos
The Kleene-Vesley topos $RT(\mathcal{K}_2,\mathcal{K}_2^{rec})$ and Effective topos $RT(\mathcal{K_1})$ share quite a few properties. They're evidently both constructive and reject LPO, and both have ...
- 313
5 votes
3 answers
383 views
Regarding the realizability topos on the computable part of Kleene's second algebra
Let: $\mathcal{K}_1$ be the first Kleene algebra, meaning $\mathbb{N}$ endowed with the partial operation $(p,n) \mapsto p\bullet n := \varphi_p(n)$ where $\varphi$ is the $p$-th partial computable ...
- 38k
2 votes
0 answers
168 views
What is known about realizability model of the real analysis?
What do "Realizability of the axiom of choice in HOL" and "Realizability and the Axiom of Choice" mean when they claim they realize a non extensional version of $\sf AC$? Can they ...
- 1,391
12 votes
0 answers
314 views
Realizability ∞-topos
This is my first question on MathOverflow, so it is possible it is poorly composed. My interests lie in the field of the type theory and (higher) category theory, specifically I am interested in the ...
- 121
7 votes
1 answer
286 views
Non-equivalent PCA’s with equivalent realizability toposes?
This question was prompted by this recent answer by aws on a question by Gro-Tsen. As that answer recalls, two PCA’s (partial combinatory algebras) are equivalent via applicative morphisms precisely ...
8 votes
1 answer
497 views
What does “the” mean in “the first Kleene algebra”? (In what sense is it unique?)
Definition: “The” first Kleene algebra $\mathcal{K}_1$ is the set $\mathbb{N}$ of natural numbers endowed with the partial operation $(p,n) \mapsto p\bullet n := \varphi_p(n)$ where $\varphi_p$ is the ...
- 38k
7 votes
1 answer
332 views
A topos for realizability under a variable oracle
I am looking for a topos that describes realizability by Turing machines with access to a “variable oracle”. I think the construction I want is this. Start with Baire space $\mathcal{N} := \mathbb{N}^...
- 38k
3 votes
0 answers
173 views
Realizability model of the core models/inner models
Background According to A program for the full axiom of choice, forcing has a computational interpretation and a realizability models. However, this paper also mentions that it is not possible to ...
- 1,391
3 votes
1 answer
127 views
Do $\mathcal{U}$-small partitioned assemblies densely generate realizability toposes?
Given a partial combinatory algebra $A$, the realizability topos $\mathrm{RT}(A)$ is the ex/lex completion of the category of partitioned assemblies $\mathrm{PA}(A)$. This implies that $\mathrm{PA}(A)$...
- 171
4 votes
0 answers
311 views
Läuchli's "intermediate thing"
On page 230 of An abstract notion of realizability ..., Läuchli writes the following: If we drop the restrictions put on $\Theta$, then we get classical logic in one case and an intermediate thing in ...
- 19.6k
4 votes
1 answer
245 views
Further research on relevant realizability etc
I just read Dunn's 1979 paper Relevant Robinson's Arithmetic, and the end especially caught my interest. Following the surprising role of constant functions in collapsing "relevant Q with zero&...
- 19.6k
15 votes
2 answers
895 views
Ordinal realizability vs the constructible universe
Koepke's paper Turing Computations on Ordinals defines a notion of "ordinal computability" using Turing machines with a tape the length of Ord and that can run for Ord-many steps, and shows ...
- 68.7k
3 votes
0 answers
129 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 ...
- 7,130
5 votes
0 answers
213 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 ...
- 38k
4 votes
1 answer
330 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 = \{ ...
- 7,130
9 votes
0 answers
217 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 ...
- 38k
7 votes
0 answers
355 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 particular, an answer as specific as Emil Jeřábek's answer would be great!) In the context of ...
- 7,130
6 votes
1 answer
355 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 ...
- 38k
14 votes
1 answer
780 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 ...
- 38k
3 votes
0 answers
133 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.6k
6 votes
0 answers
148 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.6k
5 votes
1 answer
347 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)...
- 19k
4 votes
1 answer
523 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 ...
- 8,008
7 votes
1 answer
612 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 ...
- 488
11 votes
0 answers
169 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 \...
- 68.7k
7 votes
1 answer
294 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}$. ...
- 14.5k
5 votes
1 answer
341 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 ...
- 14.5k
19 votes
1 answer
1k 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 ...
- 14.5k
14 votes
2 answers
661 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.6k
14 votes
1 answer
838 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 ...
- 38k
6 votes
1 answer
304 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, ...
- 173
5 votes
0 answers
424 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,711
6 votes
0 answers
388 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 ...
- 8,008
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 ...
- 9,349