patternMinor
Why Church-encoded types aren't sufficient to express inductive proofs?
Viewed 0 times
whyexpressencodedarentypesinductivechurchsufficientproofs
Problem
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?
Solution
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.
principle and the axiom of
choice in the pure calculus
of constructions.
Context
StackExchange Computer Science Q#68808, answer score: 5
Revisions (0)
No revisions yet.