# Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic

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 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”.

• To clarify, when you say propositions-as-types, do you intend to interpret $\exists$ as $\Sigma$? Dec 17, 2023 at 20:43
• 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? Dec 18, 2023 at 9:40
• x.com/gro_tsen/status/1736401134598660096?s=20 Dec 18, 2023 at 10:21
• @AndrejBauer Here is a scan 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.] Dec 18, 2023 at 13:02
• @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. Dec 18, 2023 at 13:22

## 1 Answer

I do not know if this answers your question, but in Propositions as [Types] 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.

• 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. Dec 18, 2023 at 9:32
• 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.) Dec 18, 2023 at 9:38
• But it can be proved with exists in the hypothesis, right ? Dec 18, 2023 at 10:16
• Does this statement have a particular name in the literature? Dec 18, 2023 at 17:43
• @AndrejBauer sorry I meant "can't be proved", of course Dec 19, 2023 at 9:03