13
$\begingroup$

Question

Is CiC stronger than CoC, in terms of proof strength?

Context

To illustrate the kind of confusion I am in, and what I'd like to learn from the answer, here is part of my inner monologue:

If I have understood correctly, CiC is CoC plus inductive definitions. An inductive definition places one or more types into the context, plus some constants and a recursor function. So is it just syntactic sugar to formulate assumptions or is it kind of an axiom, that recursors exist for every possible inductive definition? Can you do inductive definitions within a proof and if so, how would this look like in coq or lean?

Example: Let FTT be a rephrasing of the Feit–Thompson theorem, that does't refer to the integers or any other infinite structure, e.g. "Every (Tarski-)finite non abelian simple group has a non trivial involution". Thanks to Gonthier et alt. FTT is clearly provable in coq/CiC. I assume the proof uses the integers. Is FTT still provable if we did not define the integers before? If yes, can we create the integers on the fly when we need them in the proof? Or is there a procedure to eliminate the use of the integers from the proof?

$\endgroup$
5
  • 1
    $\begingroup$ I think you need to clarify. CoC and CIC may also differ on universe structures, depending on your terminology. Coq has an infinite hierarchy of universes, while CoC only has two. So CIC is a little bit awkward and ambiguous here. $\endgroup$
    – Trebor
    May 2 at 5:38
  • 3
    $\begingroup$ Cross-posted at mathoverflow.net/questions/421509/… Please don't do that, it wastes people's energy. $\endgroup$ May 2 at 8:01
  • $\begingroup$ @AndrejBauer Sorry, first posted on mathoverflow, because I was not aware of the proofassistants site, until I got a hint in a comment. $\endgroup$ May 2 at 20:37
  • $\begingroup$ You're asking a lot of questions at once, making it hard to answer. It might be a good idea to break up the latter parts of your question into a new more focused question. $\endgroup$
    – Couchy
    May 2 at 21:11
  • $\begingroup$ I assume you mean the fully bevy of structures: inductive types, coinductive types, nested inductive types and nested inductive coinductive types. IIRC there's a way to encode inductive-inductive types in Coq. I know coinductive types can be encoded impredicatively with inductive types but I'm not sure of the limitations there. $\endgroup$ May 2 at 21:47

3 Answers 3

8
$\begingroup$

Meven's answer explains that without inductive types, you cannot hope to recover a natural number object with proper induction principles. You can interpret this as saying that you lose some mathematical expressiveness.

However, in the Calculus of Constructions (CC) you can still define the Church integers

$N := \forall (X : \mathrm{Prop}) , X \to (X \to X) \to X$,

and even though they don't come with an induction principle, you can still define exactly the same functions as terms $N \to N$ as in CC + Inductives. So, in a way, you do not get any proof-theoretic strength out of inductives in an impredicative system.

Note that it is not true at all for predicative systems, such as MLTT, where inductive types are the main source of proof-theoretical strength.


Let's make this claim more precise: by CC, I mean the original system of Coquand, which can be expressed as a PTS with two sorts $\mathrm{Prop}$ and $\mathrm{Type}$, the first being impredicative.

For simplicity, I will only consider one inductive type, the integers. I use CC+Nat to mean CC extended with an inductive type $\mathbb{N} : \mathrm{Prop}$ with large elimination (and adequate computation rules):

$$ \frac{P : \mathbb{N} \to \mathrm{Prop} \quad t_0 : P\ 0 \quad P_S : \Pi\ n. P\ n\to P\ (S\ n) \quad n : \mathbb{N}}{\mathrm{natrec}(P, t_0, t_S, n) : P\ n} $$ $$ \frac{K : \mathrm{Type} \quad P_0 : K \quad P_S : K\to K \quad n : \mathbb{N}}{\mathrm{Natrec}(K, P_0, P_S, n) : K} $$

One can show that any term of type $N \to N$ (where $N$ still means the Church integers, not $\mathbb{N}$!) in CC+Nat corresponds to an integer function using the normalization theorem. I will first explain that any such function is provably recursive in higher-order Peano arithmetic without choice (PAω), and then I will explain that any function that is provably recursive in PAω can be expressed as a term in CC. Thus, CC+Nat and CC can define exactly the same functions on the Church integers.


From CC+Nat to PAω

This direction requires analyzing a normalization proof (this one doesn't treat large elimination, but we can follow Werner on this). Given any typing derivation in CC+Nat, our goal is to prove that the term is normalizing within PAω (we cannot do it uniformly for all derivations, as the proof strength of PAω is not sufficient).

First, we can show through simple syntactic consideration that in CC+Nat, terms can be stratified into kinds (inhabitants of $\mathrm{Type}$), predicates (inhabitants of a kind), and objects (inhabitants of a predicate of kind $\mathrm{Prop}$), and that nothing complex happens at the level of kinds — they can't be abstracted over, and they can be described by the following syntax:

$$ K ::= \mathrm{Prop}\ |\ \Pi (\alpha : K) . K\ |\ \Pi (x : T) . K\qquad \text{where $T$ has type Prop} $$

The standard reducibility proof assigns a set-theoretic interpretation to each kind:

$$ \begin{split} \mathcal{V}(\mathrm{Prop}) & = SAT \quad \text{The set of saturated sets of terms} \\ \mathcal{V}(\Pi (\alpha : K_1) . K_2) & = \mathcal{V}(K_1) \to \mathcal{V}(K_2)\\ \mathcal{V}(\Pi (\alpha : T) . K) & = \mathcal{V}(K_2) \end{split} $$

Unfortunately, we cannot reproduce this definition in PAω, because it "lives in kind ω+1". But we are only interested in proving normalization for a specific derivation, and only finitely many kinds appear in that derivation — so we can restrict ourselves to a subtheory with bounded kinds, in which case the interpretation is definable in PAn for some n.

Then one proceeds to assign an element $[P]$ of $\mathcal{V}(K)$ to every predicate $P$ of kind $K$ by induction on the syntax, in the usual fashion (see this summary for instance. Integers and predicates defined by recursion are treated in Werner's thesis). Finally, one shows by induction on the typing derivations that if $\vdash t : A$, then $t \in [P]$ and thus $t$ is normalizing.

We have that if $\vdash f : N \to N$ in CC+Nat, then PAω proves that for any Church integer $\overline{n}$, $f\ \overline{n}$ is normalizing (since it does not involve more kinds than $f$). After some simple considerations on normal forms, we can show that it normalizes to an integer $\overline{m}$, and thus we showed that the function coded by $f$ is recursive.


From PAω to CC

Girard's representation theorem shows that any function that is provably recursive in PAω can be expressed as a term in System Fω. The idea is to first use a double negation translation and "Friedman's trick" to reduce the problem to higher-order Heyting arithmetic HAω, and then translate HAω into Fω by erasing integers.

Finally, there is an obvious embedding of System Fω in CC.


Extensions

This proves that CC+Nat and CC can define the same functions on the Church integers. What about stronger systems?

Werner actually treats a full scheme of inductives with large elimination for small constructors (also known as "Impredicative-Set"). I would expect that the same technique carries through for the full scheme, but inductives are somewhat messy.

What about a universe hierarchy? We could hope that the full CIC (CC with a universe hierarchy and inductives) has the same proof-theoretic strength as CCω (CC with a universe hierarchy). However, I don't know any normalization proof for CIC — we cannot do the stratification by kind anymore, so it is not clear whether a similar technique works.

$\endgroup$
5
$\begingroup$

There is a paper by Geuvers constructing a model showing that Induction is not derivable in second order logic. The name is pretty explicit, but to reformulate, the main result is that while you can use impredicative encodings to construct types equipped with recursors corresponding to the usual ones for inductive types, you cannot construct a type in λP2 (second order logic) that satisfies the induction principle of natural numbers. While λP2 is not CoC, from what I understand this extends quite straightforwardly to CoC. On the higher level, I think this means that your impredicative encoding gives you a weakly initial object, but no initial object.

In the case of natural numbers, this implies you can construct some type $N$ and terms $z : N$, $S : N \to N$ and $\mathrm{rec}_N : \Pi T : \star. P \to (P \to P) \to N \to P$ that have the behaviour you expect. But given any type $N'$ with $z' : N'$ and $S' : N' \to N'$, you cannot inhabit $\mathrm{ind}_{N'} : \Pi P : N' \to \star. P\ z' \to (\Pi\ n : N'. P\ n \to P\ (S'\ n)) \to \Pi n : N'. P\ n'$ (where $\star$ is your sort of propositions).

Thus, at least some things you can do with inductive types you cannot do without, in terms of usability. But I am not sure how this fares in term of "logical power", eg if there are cardinals you can prove to be well-founded with inductive types but not without, or theories you can prove terminating… And I don’t know either what this say in the case of FTT.

$\endgroup$
5
$\begingroup$

In complement to Meven Lennon-Bertrand's answer, it is shown in From realizability to induction via dependent intersection by Aaron Stump that by extending $\lambda P2$ (or CoC) with dependent intersection types, and adopting extrinsic (Curry-style) typing, it is possible to define inductive types, and hence you can inhabit

$$\text{ind}:\forall P:N\to \star.P z\to(\forall n:N.P n\to P (S n))\to \forall n:N.P n.$$

Extrinsic (Curry-style) typing means that lambda terms are unannotated, thus we can type $$\lambda x.x : (\text{Nat}\to\text{Nat})\cap(\text{Bool}\to\text{Bool})$$ The dependent intersection type $\iota x : A. B$ has introduction and elimination rules $$\frac{\Gamma\vdash t : A\quad \Gamma\vdash t : [t/x]B}{\Gamma\vdash t : \iota (x:A).B}\qquad\frac{\Gamma\vdash t : \iota(x:A).B}{\Gamma\vdash t : [t/x]B}$$ so we may define $$N := \iota (n : \forall X : \star. X \to (X \to X) \to X). \text{Ind}(n)$$

where $\text{Ind}(n)$ is the predicate saying that $n$ is an inductive natural: $$\text{Ind}(n) := \forall P : N\to\star.P z \to (\forall m:N.P m\to P(Sm))\to P n$$ which is in fact the example given in Geuvers' paper.

$\endgroup$
4
  • $\begingroup$ I am then curious to know whether CoC with dependent intersection types is equivalent in proof strength to CiC. $\endgroup$
    – Couchy
    May 2 at 16:18
  • $\begingroup$ I don't think your characterization of dependent intersection is correct. At least to me, $\bigcap_{x:A} B(x)$ suggests the intersection of the family $B(x)$, I.E. it is intersecting all the $B$s, similar to how $Σ$ takes the disjoint union of a family. However, if I understand correctly, dependent intersection is meant to relate to binary intersection in the way that $Σ$ can be imagined to relate to binary products. So, $ιx:A.B$ is intersecting $A$ with $B$, but $B$ somehow depends on values of $A$. $\endgroup$
    – Dan Doel
    May 2 at 18:08
  • $\begingroup$ @DanDoel Thanks, relating dependent intersection to dependent sums seems like a more appropriate analogy $\endgroup$
    – Couchy
    May 2 at 18:24
  • 2
    $\begingroup$ Note that critically you have internal erasure, erased products, and a very liberal equality in this work too. Also, for a an introduction of the term, [a, b] you also critically need that |a| = |b| which justifies the simpler projections from both components. $\endgroup$ May 3 at 1:27

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.