7
$\begingroup$

I've heard some claims that the calculus of constructions without inductive types isn't powerful enough to express proofs by induction. Is that correct? If so, why isn't the Church-encoding sufficient for that?

$\endgroup$
5
$\begingroup$

How would you prove inside the pure CoC that the induction principle holds of the Church numerals? See Thomas Streicher's, Independence of the induction principle and the axiom of choice in the pure calculus of constructions.

$\endgroup$
  • 1
    $\begingroup$ Herman Geuvers has also proven (here) that no possible encoding of the natural numbers can work. $\endgroup$ – cody Jan 16 '17 at 20:20
  • $\begingroup$ @cody Geuvers' result is for second-order dependent types. Is it obvious that it generalises to higher-order dependent types? $\endgroup$ – Martin Berger Jan 17 '17 at 12:58
  • 1
    $\begingroup$ It's not obvious, no. I do think the model construction outlined in the paper generalizes though, as it's based on a model originally developed for the full calculus. $\endgroup$ – cody Jan 17 '17 at 15:28
1
$\begingroup$

There is a result recently published within Annals of Pure and Applied Logic in which church encoded data are realizers of their own induction principle. In this system, the induction principle for natural numbers, trees, lists... are derivable. The core calculus doesn't have any datatype constructors packaged in. It starts at an extrinsic (curry style) System F adding 3 typing constructs: implicit product, heterogeneous equality, and dependent intersection.

Geuvers result does not apply to this calculus and is mentioned in the paper.

paper: "From Realizability to Induction via Dependent Intersection", by Aaron Stump

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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