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