10
$\begingroup$

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

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

1 Answer 1

10
$\begingroup$

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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.