23
votes
Accepted
Can every simple polytope be inscribed in a sphere?
Not all simple polytopes are incribable, e.g. the dual of the cyclic polytope $C_4(8)$ is simple and not inscribable, as shown recently in Combinatorial Inscribability Obstructions for Higher-...
- 10.7k
17
votes
Accepted
Kleene realizability in Peano arithmetic
$\let\T\mathrm\def\kr{\mathrel{\mathbf r}}$Let me first answer a slightly modified question:
Proposition: For any sentence $\phi$, the following are equivalent:
There exists $n\in\mathbb N$ such ...
- 47.1k
13
votes
Computability-theoretic results relevant to realizability
Many results of computability theory can be stated synthetically in the effective topos. I have dubbed this idea "synthetic computability" and have tried to develop as much computability ...
- 48.8k
11
votes
How exactly are realizability and the Curry-Howard correspondence related?
I am sure more than one exact correspondence can be made, but here's at least one that is technically precise. We shall employ categorical logic.
Executive summary: realizability is the ...
- 48.8k
9
votes
Accepted
Realizability for constructive Zermelo-Fraenkel set theory
For your first question, the definition of $e\Vdash x\in y$ and $e\Vdash x=y$ seems circular, but $\mathsf{CZF}$ provides a way to avoid the circularity, called inductive definition.
Definition. An ...
- 3,042
8
votes
Accepted
Are there simplicial spheres with "non-geometric symmetries"?
The answer is negative. Already in dimension 4 there are fake real-projective spaces, which are smooth 4-manifolds homotopy-equivalent but not homeomorphic to $RP^4$. These correspond to smooth free ...
- 12.2k
7
votes
Accepted
What is the theory of statements with a provably *bounded* realizer (according to PA)?
$\let\T\mathrm\def\kr{\mathrel{\mathbf r}}\let\LOR\bigvee$The same argument as in my linked answer shows that
$$T_2=\T{HA+ECT_0+MP+SWLEM},$$
where
$$\T{SWLEM}=\{\neg\phi\lor\neg\neg\phi:\text{$\phi$ ...
- 47.1k
5
votes
Ordinal realizability vs the constructible universe
As pointed out by Noah and Hanul in the comments, there are known models of set theory making use of class sized pcas. The earliest relevant to this question is probably Tharp, A quasi-intuitionistic ...
- 4,378
4
votes
How is this HA unprovable formula recursive realizable?
Let us first have a look at the core obstace for $$\neg (A \wedge B) \rightarrow (\neg A \vee \neg B)$$
Negated formulas do not have computational content, so $\neg (A \wedge B)$ is only a promise ...
- 4,667
4
votes
Accepted
Homotopical realizability
The reference to "truth in $\mathbb{N}$" is a mirage. As Andreas Blass points out, there is a computable procedure that determines whether $s = t$ holds for closed term $s$ and $t$ of HA. ...
- 48.8k
4
votes
Accepted
Further research on relevant realizability etc
I thought this was an interesting question and so I asked some relevant logicians on Mastodon. Here's a quick summary of the answers, although the short version seems to be "No", with Shawn ...
- 1,084
3
votes
Accepted
Which arithmetical sentences have no counterexamples in the sense of Kreisel?
In fact all true arithmetical sentences have weak classical realizers. Namely, a true arithmetical sentence $\psi$ $$\forall x_1\exists y_1 \ldots \forall x_n\exists y_n \theta(x_1,\ldots,x_n,y_1,\...
- 5,821
2
votes
Accepted
Is there a polytope with an essentially unique shape?
What you are after seems to be projectively unique polytopes. And so the paper of Adiprasito and Ziegler may answer your question. Perhaps two papers in the references of that paper will give you many ...
2
votes
Do $\mathcal{U}$-small partitioned assemblies densely generate realizability toposes?
I don't know if this is what the authors of the paper had in mind, but here's one way to do it. Also, I'm not sure if there's a constructive way to do this, so I'll give an answer assuming the axiom ...
- 4,378
1
vote
Need help in trying to understand an argument by V. A. Yankov on the nonrealizability of Scott's axiom
So, I didn't understand the exact details of what Yankov was trying to do with his $K$ and $Q,P,R$ (the definition of $K$ probably depends on the details of the coding he uses for realizability, which ...
- 32.5k
1
vote
Computability-theoretic results relevant to realizability
This wasn't exactly what I had in mind when I first asked this question, but I don't think it's unrelated either: combining realizability (in a very naive way) with classical computability-theoretic ...
- 21.2k
Only top scored, non community-wiki answers of a minimum length are eligible