Questions tagged [realizability]
Realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them.
9
questions
3
votes
1answer
77 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
1answer
141 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 ...
16
votes
1answer
593 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 ...
9
votes
1answer
300 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 ...
8
votes
1answer
303 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 ...
5
votes
1answer
149 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
0answers
341 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 ...
4
votes
0answers
296 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 ...
13
votes
2answers
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 ...
