# Questions tagged [realizability]

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

24
questions

4
votes

1
answer

171
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&...

14
votes

1
answer

583
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 ...

3
votes

0
answers

90
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 ...

5
votes

0
answers

146
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 ...

4
votes

1
answer

248
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
votes

0
answers

154
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 ...

6
votes

0
answers

214
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 $\...

6
votes

1
answer

287
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 ...

14
votes

1
answer

534
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 ...

3
votes

0
answers

94
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 ...

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}_{\...

5
votes

1
answer

272
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)...

4
votes

1
answer

409
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
votes

1
answer

457
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 ...

11
votes

0
answers

145
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 \...

7
votes

1
answer

233
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}$.
...

5
votes

1
answer

230
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 ...

19
votes

1
answer

904
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 ...

12
votes

2
answers

504
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 ...

13
votes

1
answer

630
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 ...

6
votes

1
answer

225
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, ...

5
votes

0
answers

381
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 ...

5
votes

0
answers

338
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 ...

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 ...