<p>In <a href="https://cs.stackexchange.com/a/82891/988">this answer</a> I mention a paper by Geuvers in which he describes a class of models for a type theory $\lambda P_2$ which is a sub-system of the CoC and roughly corresponds to 2nd order predicate logic.</p>

<p>He goes on to describe a class of realizability models, which are based on Weakly Extensional Combinatory Algebras (WECAs). In a couple of lines, the model involves a WECA $\cal A$ and a set ${\cal P}\subset {\mathscr P}({\cal A})$, closed under arbitrary intersections and closed under the <em>realizability product</em>:
$$\prod_{t\in X}F(t):= \{a\in{\cal A}\mid \forall t\in X,\ a\cdot t\in F(t)\} $$
where $F:X\rightarrow {\cal A}$ is an arbitrary function. One can then define the interpretation $[\![\_]\!]$ from types in $\lambda P_2$ to elements of $\cal P$:</p>

<p>$$[\![\alpha]\!]_{\xi\rho}:= \xi(\alpha)$$
$$[\![\Pi\alpha.\tau]\!]_{\xi\rho}:=\bigcap_{A\in{\cal P}}[\![\tau]\!]_{\xi[\alpha:=A]\rho} $$
$$[\![\Pi x:\sigma.\tau]\!]_{\xi\rho}:= \prod_{a\in[\![\sigma]\!]}[\![\tau]\!]_{\xi\rho[x:=a]}$$
$$[\![P\ t]\!]_{\xi\rho}:= [\![P]\!]_{\xi\rho}((\!|t|\!)_{\xi\rho})$$
$$[\![\lambda x:\sigma. P]\!]_{\xi\rho}:= a\in[\![\sigma]\!] \mapsto [\![P]\!]_{\xi\rho[x:=a]}$$</p>

<p>Where $\xi$ and $\rho$ are appropriate valuations, and $(\!|\_|\!)$ is the interpretation of terms into elements of the WECA $\cal A$. I'm omitting a fair number of details, e.g. the interpretation is actually over type <em>constructors</em> and not only types.</p>

<p>My question is pretty straightforward: is this class of models complete for $\lambda P_2$? Is the "obvious" generalization complete for CoC? For CIC? Are there any references for this?</p>

<p>The interpretation of the "large" product is restricted to be intersections, which may make it too weak a notion of models to be complete, but the choice of WECAs seems to make it a powerful notion of models.</p>

<p>In Pitts' paper <a href="https://www.irif.fr/~mellies/mpri/mpri-ens/articles/pitts-polymorphism-is-set-theoretic-constructively.pdf" rel="nofollow noreferrer">Polymorphism is Set-Theoretic, Constructively</a>, it is shown that every model of system $F$ can be embedded in a topos, and so a rather general notion of topos models is indeed complete for system $F$.</p>

<p>So my follow up questions are:
Do these topos models generalize the class of realizability models described above? Does the theorem generalize to $\lambda P_2$? I suspect the answer is yes, but I'd kind of like to see the details worked out.</p>

<hr>

<p><strong>Edit:</strong> I've asked both Herman and Andrew for insights, and they were kind enough to both reply. I'll summarize their response.</p>

<p>Herman notes that there is completeness for 2nd order predicate logic, in which it is crucial to allow subsets of the full powerset for the interpretation of 2nd order quantifiers. It is an open question about whether $\lambda P_2$ is conservative over 2nd order predicate logic, and this seems to be a related question. He also refers to Geuvers - <em>Extending Models of Second Order Predicate Logic to Models of Second Order Dependent Type Theory</em>, CSL 1996.</p>

<p>Andrew notes that the completeness results involving topos models seem very close to the syntax as opposed to the set theoretic ones, and so is skeptical that the results can be extended to this setting without significant effort (he is agnostic about the result itself though!).</p>

CC BY-SA 3.0
2017-10-24T22:52:55.943Z
And you asked Herman and Andy?
Andrej Bauer
CC BY-SA 3.0
2017-10-25T19:32:26.113Z
@AndrejBauer I'm afraid I haven't, good suggestion!
cody
CC BY-SA 3.0
2017-11-02T19:44:50.630Z
@AndrejBauer I've now e-mailed both Herman and Andrew, and I'll summarize their comments in an edit.
cody
<type-theory><dependent-type><polymorphism>
Completeness of realizability semantics for higher-order type theory
cody
# Completeness of realizability semantics for higher-order type theory

(Asked by: username_0 on 2017-10-24)

In [this answer](https://cs.stackexchange.com/a/82891/988) I mention a paper by Geuvers in which he describes a class of models for a type theory $\lambda P\_2$ which is a sub-system of the CoC and roughly corresponds to 2nd order predicate logic.

He goes on to describe a class of realizability models, which are based on Weakly Extensional Combinatory Algebras (WECAs). In a couple of lines, the model involves a WECA $\cal A$ and a set ${\cal P}\subset {\mathscr P}({\cal A})$, closed under arbitrary intersections and closed under the *realizability product*:
$$\prod\_{t\in X}F(t):= \{a\in{\cal A}\mid \forall t\in X,\ a\cdot t\in F(t)\} $$
where $F:X\rightarrow {\cal A}$ is an arbitrary function. One can then define the interpretation $[\![\\_]\!]$ from types in $\lambda P\_2$ to elements of $\cal P$:

$$[\![\alpha]\!]\_{\xi\rho}:= \xi(\alpha)$$
$$[\![\Pi\alpha.\tau]\!]\_{\xi\rho}:=\bigcap\_{A\in{\cal P}}[\![\tau]\!]\_{\xi[\alpha:=A]\rho} $$
$$[\![\Pi x:\sigma.\tau]\!]\_{\xi\rho}:= \prod\_{a\in[\![\sigma]\!]}[\![\tau]\!]\_{\xi\rho[x:=a]}$$
$$[\![P\ t]\!]\_{\xi\rho}:= [\![P]\!]\_{\xi\rho}((\!|t|\!)\_{\xi\rho})$$
$$[\![\lambda x:\sigma. P]\!]\_{\xi\rho}:= a\in[\![\sigma]\!] \mapsto [\![P]\!]\_{\xi\rho[x:=a]}$$

Where $\xi$ and $\rho$ are appropriate valuations, and $(\!|\\_|\!)$ is the interpretation of terms into elements of the WECA $\cal A$. I'm omitting a fair number of details, e.g. the interpretation is actually over type *constructors* and not only types.

My question is pretty straightforward: is this class of models complete for $\lambda P\_2$? Is the "obvious" generalization complete for CoC? For CIC? Are there any references for this?

The interpretation of the "large" product is restricted to be intersections, which may make it too weak a notion of models to be complete, but the choice of WECAs seems to make it a powerful notion of models.

In Pitts' paper [Polymorphism is Set-Theoretic, Constructively](https://www.irif.fr/~mellies/mpri/mpri-ens/articles/pitts-polymorphism-is-set-theoretic-constructively.pdf), it is shown that every model of system $F$ can be embedded in a topos, and so a rather general notion of topos models is indeed complete for system $F$.

So my follow up questions are:
Do these topos models generalize the class of realizability models described above? Does the theorem generalize to $\lambda P\_2$? I suspect the answer is yes, but I'd kind of like to see the details worked out.

---

**Edit:** I've asked both Herman and Andrew for insights, and they were kind enough to both reply. I'll summarize their response.

Herman notes that there is completeness for 2nd order predicate logic, in which it is crucial to allow subsets of the full powerset for the interpretation of 2nd order quantifiers. It is an open question about whether $\lambda P\_2$ is conservative over 2nd order predicate logic, and this seems to be a related question. He also refers to Geuvers - *Extending Models of Second Order Predicate Logic to Models of Second Order Dependent Type Theory*, CSL 1996.

Andrew notes that the completeness results involving topos models seem very close to the syntax as opposed to the set theoretic ones, and so is skeptical that the results can be extended to this setting without significant effort (he is agnostic about the result itself though!).

**Tags:** type-theory, dependent-type, polymorphism
> **Comments:**
> **username_1**: And you asked Herman and Andy?  
> **username_0**: @AndrejBauer I'm afraid I haven't, good suggestion!  
> **username_0**: @AndrejBauer I've now e-mailed both Herman and Andrew, and I'll summarize their comments in an edit.  

---

## 0 answers

