<p>I do not know if this answers your question, but in <a href="https://doi.org/10.1093/logcom/14.4.447" rel="noreferrer">Propositions as [Types]</a> we communicate in Remark 6.6 an observation by Thierry Coquand, namely that the statement
<span class="math-container">$$
(\forall x .\, \exists y .\, R(x,y))
\Rightarrow
\forall x, x' .\, \exists y, y' .\, R(x,y) \land R(x',y') \land (x = x' \Rightarrow y = y'))
$$</span>
is not provable in intuitionistic first-order logic, but is inhabited under propositions-as-types. Apparently this goes back to an unpublished note by Mints.</p>

CC BY-SA 4.0
2023-12-18T09:32:18.933Z
Thanks for the example, here is the proof in Coq: 
```Lemma foo: forall (A B: Type) (R:A->B->Prop) (H:forall x, {y | R x y}),
forall x x', exists y y', (R x y /\ R x' y' /\ (x=x' -> y=y')).
Proof.
intros.
exists (proj1_sig (H x)).
exists (proj1_sig (H x')).
repeat split.
apply (proj2_sig (H x)).
apply (proj2_sig (H x')).
intro;subst; auto.
Qed.```
Julien Narboux
CC BY-SA 4.0
2023-12-18T09:38:50.627Z
Thanks. Minor quibble: you're mixing `{... | ...}` and `exists`, the Curry-Howard version should use `{... | ...}` everywhere. And the "real" Curry-Howard would use `Type` instead of `Prop`. (Your proof woudl still work, of course.)
Andrej Bauer
CC BY-SA 4.0
2023-12-18T10:16:57.720Z
But it can be proved with ```exists``` in the hypothesis, right ?
Julien Narboux
CC BY-SA 4.0
2023-12-18T10:23:09.040Z
No, that's the whole point of the example.
Andrej Bauer
CC BY-SA 4.0
2023-12-18T13:12:29.900Z
Is this related to the axiom of choice in some way? Is it correct to say that in first-order intuitionistic logic we can't extract a choice function from `forall a, exists b, ...` but we can do so (in `Type`) in proposition-as-types?
chi
CC BY-SA 4.0
2023-12-18T14:40:19.730Z
@chi: That indeed explains why we can inhabit the type-theoretic version, although it says little about why th logical version is not provable (perhaps there is a proof that avoids choice).
Andrej Bauer
CC BY-SA 4.0
2023-12-18T17:43:43.600Z
Does this statement have a particular name in the literature?
user76284
CC BY-SA 4.0
2023-12-18T20:30:52.813Z
I'll ask Thierry Coquand tomorrow, as I happen to be in the same city as he is.
Andrej Bauer
CC BY-SA 4.0
2023-12-19T09:03:59.250Z
@AndrejBauer sorry I meant "can't be proved", of course
Julien Narboux
CC BY-SA 4.0
2023-12-17T20:52:26.763Z
2023-12-17T21:02:54.977Z
2023-12-17T21:02:54.977Z
Andrej Bauer
<p>Reading Barendregt's chapter “Lambda Calculi with Types” in the <em>Handbook of Logic in Computer Science (vol. 2: Computational Structures)</em> (Abramsky, Gabbay &amp; Maibaum eds., 1992) I learned (<em>op. cit.</em> theorem 5.4.21) that Berardi and Geuvers proved in 1989 that the Calculus of Constructions is not conservative over Higher-Order Predicate Logic, i.e., there is a sentence which is not provable in the latter but is (under the propositions-as-types interpretation) the type of a term of the former.</p>
<p>Barendregt gives an account of both proofs by Berardi and Geuvers (I was unable to get my hands on the original works; in fact, Berardi's is cited as “personal communication” by Barendregt): this account isn't too hard too follow, but I feel like I'm kind of missing the whole point, because I don't “see” where the typing rules of the CoC differ from the derivation rules of HOL in a way that makes the constructed term invalid as a proof.</p>
<p>So, <strong>questions</strong>:</p>
<ul>
<li><p>Can someone give an informal/intuitive explanation of <em>what is going on</em> here?  As in: what went wrong?  At what point exactly did the typing system and the logical system diverge?</p>
</li>
<li><p>Specifically, if we try to interpret the term constructed by Berardi or by Geuvers as a proof, <em>where exactly does it go wrong?</em>  I'd like to put my finger on the exact logical rule which isn't allowed in Higher-Order Predicate Logic but which is permitted as a typing rule in the Calculus of Construction (and trying to extract this from Barendregt's account leaves me lost in a maze of twisty little notations all alike).</p>
</li>
<li><p>In practice, what does this mean for a proof assistant like Coq which is based on the Calculus of Constructions?  Will Coq accept the term in question as a valid proof?</p>
</li>
</ul>
<hr />
<p><strong>Edit</strong> (2023-12-18): For completeness of CSTheorySE, here is a paraphrase of the account Barendregt gives of Geuvers's proof:</p>
<p>Consider the context <span class="math-container">$\Gamma$</span> and type <span class="math-container">$B$</span> defined by:
<span class="math-container">$$
\begin{aligned}
\Gamma &amp;:= A:*^s,\;c:A \\
B &amp;:= \Pi Q:(*^p\to *^p).\, \Pi q:*^p.\,
(Q(\Pi x:A.q) \to \exists q':*^p. Q(q'\to q))
\end{aligned}
$$</span>
This is in the <a href="https://en.wikipedia.org/wiki/Pure_type_system" rel="nofollow noreferrer">pure type system</a> which Barendregt calls “<span class="math-container">$\lambda\mathrm{PRED}\omega$</span>”, defined by:
<span class="math-container">$$
\begin{array}{ll}
\textrm{sorts}&amp;*^p,*^s,*^f,\square^p,\square^s\\
\textrm{axioms}&amp;*^p:\square^p,\,*^s:\square^s\\
\textrm{rules}&amp;(*^p,*^p),\,(*^s,*^p),\,(\square^p,*^p),\\
&amp;(*^s,*^s,*^f),\,(*^s,*^f,*^f),\,(*^s,\square^p),\,(\square^p,\square^p)
\end{array}
$$</span>
(Barendregt comments that <span class="math-container">$*^s$</span> is the sort of “sets”, <span class="math-container">$*^p$</span> is the sort of “propositions” and <span class="math-container">$*^f$</span> is the sort of first-order functions between sets),
and we define “<span class="math-container">$\exists x:S.A$</span>” for <span class="math-container">$A:*^p$</span> and <span class="math-container">$S:*^s$</span> by
<span class="math-container">$$
\exists x:S.A \;:=\; \Pi\gamma:*^p.\,(\Pi x:S.(A\to\gamma))\to\gamma
$$</span></p>
<p>Then <strong>(1)</strong> the translation <span class="math-container">$|B|$</span> of <span class="math-container">$B$</span> into <span class="math-container">$\lambda C$</span>, obtained by removing all superscripts on <span class="math-container">$*$</span> and <span class="math-container">$\square$</span>, is inhabited, but <strong>(2)</strong> <span class="math-container">$B$</span> considered as a formula is not derivable in <span class="math-container">$\lambda\mathrm{PRED}\omega$</span>.</p>
<p>To justify <strong>(1)</strong>, it is enough to construct <span class="math-container">$C_0$</span> of type <span class="math-container">$(Q(\Pi x:A.q) \to \exists q':*. Q(q'\to q))$</span> in context <span class="math-container">$A:*,\;c:A,\;Q:(*\to *),\;q:*$</span>.  Now note that <span class="math-container">$Q(\Pi x:A.q) = Q(A\to q)$</span> and the type
<span class="math-container">$$
\begin{aligned}
&amp; Q(\Pi x:A.q) \to \exists q':*. Q(q'\to q)\\
=\;&amp; Q(A\to q) \to (\Pi \alpha:*. (\Pi q':*. (Q(q'\to q)\to\alpha))\to\alpha)
\end{aligned}
$$</span>
is inhabited by
<span class="math-container">$$
\lambda y:Q(A\to q).\,
\lambda \alpha:*.\,
\lambda f:(\Pi q':*. (Q(q'\to q)\to\alpha)).\,
f A y
$$</span></p>
<p>As for <strong>(2)</strong>, Barendregt doesn't say much: if <span class="math-container">$C$</span> has type <span class="math-container">$B$</span> in <span class="math-container">$\lambda\mathrm{PRED}\omega$</span> then <span class="math-container">$CQqr\alpha t$</span> has type <span class="math-container">$\alpha$</span> in context
<span class="math-container">$$
\begin{array}{c}
A:*^s,\;c:A,\;Q:(*^p\to *^p),\;q:*^p,\\
r:(Q(\Pi x:A.q)),\;\alpha:\alpha^p,\\
t:(\Pi q':*^p. (Q(q'\to q)\to\alpha))
\end{array}
$$</span>
and Barendregt just writes “by considering the possible normal forms of <span class="math-container">$CQqr\alpha t$</span> it can be shown that this is impossible”.</p>

CC BY-SA 4.0
2023-12-17T20:43:52.507Z
To clarify, when you say propositions-as-types, do you intend to interpret $\exists$ as $\Sigma$?
Andrej Bauer
CC BY-SA 4.0
2023-12-18T09:40:17.573Z
It seems difficult to access the literature you cite on-line. Would you be so kind as to quickly outline the arguments you're talking about?
Andrej Bauer
CC BY-SA 4.0
2023-12-18T10:21:17.887Z
https://x.com/gro_tsen/status/1736401134598660096?s=20
Julien Narboux
CC BY-SA 4.0
2023-12-18T13:02:10.790Z
@AndrejBauer [Here is a scan](http://www.madore.org/~david/.misc/barendregt1992.pdf) of Barendregt's paper. Relevant section is the pages numbered 264–265, which are 148–149 in this PDF. \[This comment will self-desctruct in a few days.\]
Gro-Tsen
CC BY-SA 4.0
2023-12-18T13:22:33.950Z
@AndrejBauer I could cop out by saying that “propositions-as-types” is something Barendregt writes, not I. But since neither the Calculus of Construction nor the logical systems he compares it with have $\Sigma$ or $\exists$ in his paper (the systems are impredicative so he defines them $\Sigma$ or $\exists$ impredicatively), the question of how to interpret them doesn't arise. ❧ I'll edit the question soon to include Geuvers's term, but I can't really summarize the argument since its essence escapes me.
Gro-Tsen
<lo.logic><type-theory><proof-assistants><calculus-of-constructions>
Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic
Gro-Tsen
# Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic

(Asked by: username_0 on 2023-12-17)

Reading Barendregt's chapter “Lambda Calculi with Types” in the *Handbook of Logic in Computer Science (vol. 2: Computational Structures)* (Abramsky, Gabbay & Maibaum eds., 1992) I learned (*op. cit.* theorem 5.4.21) that Berardi and Geuvers proved in 1989 that the Calculus of Constructions is not conservative over Higher-Order Predicate Logic, i.e., there is a sentence which is not provable in the latter but is (under the propositions-as-types interpretation) the type of a term of the former.

Barendregt gives an account of both proofs by Berardi and Geuvers (I was unable to get my hands on the original works; in fact, Berardi's is cited as “personal communication” by Barendregt): this account isn't too hard too follow, but I feel like I'm kind of missing the whole point, because I don't “see” where the typing rules of the CoC differ from the derivation rules of HOL in a way that makes the constructed term invalid as a proof.

So, **questions**:

* Can someone give an informal/intuitive explanation of *what is going on* here? As in: what went wrong? At what point exactly did the typing system and the logical system diverge?
* Specifically, if we try to interpret the term constructed by Berardi or by Geuvers as a proof, *where exactly does it go wrong?* I'd like to put my finger on the exact logical rule which isn't allowed in Higher-Order Predicate Logic but which is permitted as a typing rule in the Calculus of Construction (and trying to extract this from Barendregt's account leaves me lost in a maze of twisty little notations all alike).
* In practice, what does this mean for a proof assistant like Coq which is based on the Calculus of Constructions? Will Coq accept the term in question as a valid proof?

---

**Edit** (2023-12-18): For completeness of CSTheorySE, here is a paraphrase of the account Barendregt gives of Geuvers's proof:

Consider the context $\Gamma$ and type $B$ defined by:
$$
\begin{aligned}
\Gamma &:= A:\*^s,\;c:A \\
B &:= \Pi Q:(\*^p\to \*^p).\, \Pi q:\*^p.\,
(Q(\Pi x:A.q) \to \exists q':\*^p. Q(q'\to q))
\end{aligned}
$$
This is in the [pure type system](https://en.wikipedia.org/wiki/Pure_type_system) which Barendregt calls “$\lambda\mathrm{PRED}\omega$”, defined by:
$$
\begin{array}{ll}
\textrm{sorts}&\*^p,\*^s,\*^f,\square^p,\square^s\\
\textrm{axioms}&\*^p:\square^p,\,\*^s:\square^s\\
\textrm{rules}&(\*^p,\*^p),\,(\*^s,\*^p),\,(\square^p,\*^p),\\
&(\*^s,\*^s,\*^f),\,(\*^s,\*^f,\*^f),\,(\*^s,\square^p),\,(\square^p,\square^p)
\end{array}
$$
(Barendregt comments that $\*^s$ is the sort of “sets”, $\*^p$ is the sort of “propositions” and $\*^f$ is the sort of first-order functions between sets),
and we define “$\exists x:S.A$” for $A:\*^p$ and $S:\*^s$ by
$$
\exists x:S.A \;:=\; \Pi\gamma:\*^p.\,(\Pi x:S.(A\to\gamma))\to\gamma
$$

Then **(1)** the translation $|B|$ of $B$ into $\lambda C$, obtained by removing all superscripts on $\*$ and $\square$, is inhabited, but **(2)** $B$ considered as a formula is not derivable in $\lambda\mathrm{PRED}\omega$.

To justify **(1)**, it is enough to construct $C\_0$ of type $(Q(\Pi x:A.q) \to \exists q':\*. Q(q'\to q))$ in context $A:\*,\;c:A,\;Q:(\*\to \*),\;q:\*$. Now note that $Q(\Pi x:A.q) = Q(A\to q)$ and the type
$$
\begin{aligned}
& Q(\Pi x:A.q) \to \exists q':\*. Q(q'\to q)\\
=\;& Q(A\to q) \to (\Pi \alpha:\*. (\Pi q':\*. (Q(q'\to q)\to\alpha))\to\alpha)
\end{aligned}
$$
is inhabited by
$$
\lambda y:Q(A\to q).\,
\lambda \alpha:\*.\,
\lambda f:(\Pi q':\*. (Q(q'\to q)\to\alpha)).\,
f A y
$$

As for **(2)**, Barendregt doesn't say much: if $C$ has type $B$ in $\lambda\mathrm{PRED}\omega$ then $CQqr\alpha t$ has type $\alpha$ in context
$$
\begin{array}{c}
A:\*^s,\;c:A,\;Q:(\*^p\to \*^p),\;q:\*^p,\\
r:(Q(\Pi x:A.q)),\;\alpha:\alpha^p,\\
t:(\Pi q':\*^p. (Q(q'\to q)\to\alpha))
\end{array}
$$
and Barendregt just writes “by considering the possible normal forms of $CQqr\alpha t$ it can be shown that this is impossible”.

**Tags:** lo.logic, type-theory, proof-assistants, calculus-of-constructions

> **Comments:**
> **username_1**: To clarify, when you say propositions-as-types, do you intend to interpret $\exists$ as $\Sigma$?  
> **username_1**: It seems difficult to access the literature you cite on-line. Would you be so kind as to quickly outline the arguments you're talking about?  
> **username_2**: https://x.com/gro_tsen/status/1736401134598660096?s=20  
> **username_0**: @AndrejBauer [Here is a scan](http://www.madore.org/~david/.misc/barendregt1992.pdf) of Barendregt's paper. Relevant section is the pages numbered 264–265, which are 148–149 in this PDF. \[This comment will self-desctruct in a few days.\]  
> **username_0**: @AndrejBauer I could cop out by saying that “propositions-as-types” is something Barendregt writes, not I. But since neither the Calculus of Construction nor the logical systems he compares it with have $\Sigma$ or $\exists$ in his paper (the systems are impredicative so he defines them $\Sigma$ or $\exists$ impredicatively), the question of how to interpret them doesn't arise. ❧ I'll edit the question soon to include Geuvers's term, but I can't really summarize the argument since its essence escapes me.  

---

## 1 answers

### Answer by username_1 on 2023-12-17. Score: 10

I do not know if this answers your question, but in [Propositions as [Types]](https://doi.org/10.1093/logcom/14.4.447) we communicate in Remark 6.6 an observation by Thierry Coquand, namely that the statement
$$
(\forall x .\, \exists y .\, R(x,y))
\Rightarrow
\forall x, x' .\, \exists y, y' .\, R(x,y) \land R(x',y') \land (x = x' \Rightarrow y = y'))
$$
is not provable in intuitionistic first-order logic, but is inhabited under propositions-as-types. Apparently this goes back to an unpublished note by Mints.

> **Comments:**
> **username_2**: Thanks for the example, here is the proof in Coq:  ```Lemma foo: forall (A B: Type) (R:A->B->Prop) (H:forall x, {y | R x y}), forall x x', exists y y', (R x y /\ R x' y' /\ (x=x' -> y=y')). Proof. intros. exists (proj1_sig (H x)). exists (proj1_sig (H x')). repeat split. apply (proj2_sig (H x)). apply (proj2_sig (H x')). intro;subst; auto. Qed.```  
> **username_1**: Thanks. Minor quibble: you're mixing `{... | ...}` and `exists`, the Curry-Howard version should use `{... | ...}` everywhere. And the "real" Curry-Howard would use `Type` instead of `Prop`. (Your proof woudl still work, of course.)  
> **username_2**: But it can be proved with ```exists``` in the hypothesis, right ?  
> **username_1**: No, that's the whole point of the example.  
> **username_3**: Is this related to the axiom of choice in some way? Is it correct to say that in first-order intuitionistic logic we can't extract a choice function from `forall a, exists b, ...` but we can do so (in `Type`) in proposition-as-types?  
> **username_1**: @username_3: That indeed explains why we can inhabit the type-theoretic version, although it says little about why th logical version is not provable (perhaps there is a proof that avoids choice).  
> **username_4**: Does this statement have a particular name in the literature?  
> **username_1**: I'll ask Thierry Coquand tomorrow, as I happen to be in the same city as he is.  
> **username_2**: @AndrejBauer sorry I meant "can't be proved", of course  

---

