3
$\begingroup$

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 obtain realizability models for V = L by the same route.

In particular, L inhabited at the bottom of the inner model theory. According to $K$ without the measurable, we can generate many core models K such that the axioms $V = K$ and ZFC are relatively consistent, as long as there is no Woodin cardinals and $j: K \to K$.

In the other hand, inner model for KP/Z/... has a lot to study. e.g.

Question

  • What are the main obstacles to constructing a realizability model/computational interpretation for an core models/inner models?
  • Or, Are there known constructive ideas?
Improve this question
$\endgroup$
4
  • 3
    $\begingroup$ I must confess I still don't entirely 'get' the content of Krivine's classical realizability for $\mathsf{ZF}$, but why doesn't the fact that $\mathsf{L}$ is definable give us a realizability interpretation immediately? $\endgroup$ Commented Jan 16 at 0:31
  • $\begingroup$ Also you probably know about this already, but there has been some work on defining $\mathsf{L}$ in the context of constructive set theories. $\endgroup$ Commented Jan 16 at 0:31
  • $\begingroup$ I don't understand what you meant by that forcing has a computational interpretation. Krivine's classical realizability should rather be seen as a generalization of forcing, and forcing is a trivial subcase of classical realizability (I do not precisely remember, but should fall into the case when the application operator is trivial.) If I recall correctly, it means Krivine's classical realizability says forcing has a few computational meanings, right? $\endgroup$ Commented Jan 19 at 9:54
  • $\begingroup$ @HanulJeon According to here, forcing has these other computational explanations. $\endgroup$ Commented Mar 10 at 6:38

0

Reset to default

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.