All Questions
Tagged with computability-theory realizability
13 questions
4
votes
1
answer
192
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&...
- 21.2k
5
votes
0
answers
153
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 ...
- 32.5k
4
votes
1
answer
257
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 = \{ ...
- 6,353
6
votes
0
answers
297
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 ...
- 6,353
6
votes
1
answer
293
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 ...
- 32.5k
14
votes
1
answer
572
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 ...
- 32.5k
3
votes
0
answers
99
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 ...
- 21.2k
6
votes
0
answers
124
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}_{\...
- 21.2k
5
votes
1
answer
283
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)...
- 12.4k
13
votes
2
answers
522
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 ...
- 21.2k
13
votes
1
answer
648
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 ...
- 32.5k
6
votes
0
answers
345
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 ...
- 7,853
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,201