2
$\begingroup$

Kleene introduced realizability as a practical semantical interpretation of Heyting Arithmetic (see link for definition). The key result he proved is that provability of $\varphi$ in HA implies the existence of a realizer $n \in \mathbb{N}$ for $\varphi$. Two questions:

  1. Is $n$ computable from the Gödel code of $\varphi$? Or otherwise, is it at least computable from the Gödel code of the proof of $\varphi$ in HA (assuming there is such a proof)?

  2. In what system is Kleene's result proved/can be proved (my interest is mostly in the weakest such system)?

$\endgroup$
2
  • 1
    $\begingroup$ (Merely commenting since uncertain:) I'm not sure about 2, but I believe the answer to 1 is yes. We can computably find a realizer $n_i$ for the $i$th axiom of $\mathsf{HA}$, and the deduction rules of intuitionistic logic "computably preserve realizability." Exactly what this clause means will depend on what version of deduction we use, but the basic idea is that if $\mathbb{X}$ is one of the "one-step" proof rules, then there is a computable function $\varphi_x$ such that $c_i$ realizes $A_i$ and $\mathbb{X}$ applies to $\{A_i:i<k\}$ to yield $B$ then $\varphi_x(c_1,...,c_k)$ realizes $B$. $\endgroup$ May 17 at 19:48
  • $\begingroup$ Like @NoahSchweber, I'm uncertain, but I would expect a realizer for $\phi$ to be primitive recursively computable from a proof of $\phi$ (as in Noah's comment), so if you're given a provable $\phi$ but not given a proof, you could find a realizer (non-primitive) recursively by searching for a proof. For Question 2, I'd expect that "provable implies realizable" can be proved in primitive recursive arithmetic. $\endgroup$ May 17 at 23:58

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.