What is the role of predicativity in inductive definitions in type theory?

Question

We often want to define an object $A \in U$ according to some inference rules. Those rules denote a generating function $F$ which, when it is monotonic, yields a least fixed point $\mu F$. We take $A := \mu F$ to be the "inductive definition" of $A$. Moreover, monotonicity of $F$ allows us to reason with the "principle of induction" to determine when a set contains $A$ (i.e. when a property universally holds on $A$).

In Coq this corresponds to writing an $\mathtt{Inductive}$ definition of $A$ with explicit introduction terms. While this definition denotes a particular function $F$, that function is not necessarily monotonic. Coq therefore employs some syntactic checks to guarantee the "well-formedness" of the definition. To some approximation, it rejects occurrences of $A$ in negative positions in the types of the introduction terms.

(If my understanding up to this point is flawed, please correct me!)

First, some questions in the context of Coq:

1) Does the syntactic check in Coq merely serve to ensure that the definition of $A$ is predicative? (If so, is impredicativity the only way in which the definition would be ill-defined?) Or is it checking for monotonicity? (Correspondingly, is non-monotonicity what might kill it?)

2) Does such a negative occurrence of $A$ necessarily imply that $A$'s definition is impredicative/non-monotonic? Or is Coq simply unable to verify that it's well-defined in that case?

And more generally:

3) What is the relation between predicativity of an inductive definition and monotonicity of that definition's generating function? Are they two sides of the same coin? Are they unrelated? Informally, which one matters more?

Answer 1

No, in this case, predicativity and monotonicity are not closely related.

The positivity check in Coq/Adga serves to ensure that you are taking the least fixed point of a monotonic thing, roughly.

Here's how to think of inductive types in terms of lattices and monotone operators. Recall that the Knaster-Tarski theorem says that on a complete lattice $L$, every monotone operator $f : L \to L$ has a least fixed point $\mu(f)$. Next, we can think of the types in a type theory as forming a lattice under provability. That is, type $S$ is below $T$ if the truth of $S$ entails that of $T$. Now, what we would like to do is to take a monotone operator $F$ on types, and use Knaster-Tarski to get out an interpretation of the least fixed point of this operator $\mu(F)$.

However, types in type theory aren't just a lattice: they form a category. That is, given two types $S$ and $T$, there are potentially many ways for $S$ to be below $T$, with one way for each proof $e : S \to T$. So a type operator $F$ also has to do something sensible on these proofs. The appropriate generalization of monotonicity is functoriality. That is, we want $F$ to have an operator on types, and also to have an action on proofs, such that if $e : S \to T$, then $F(e) : F(S) \to F(T)$.

Now, functoriality is preserved by sums and products (ie., if $F$ and $G$ are endofunctors on types, then $F+G$ and $F\times G$ (acting pointwise) are also functors on types (assuming we have sums and products in our algebra of types). However, it is not preserved by the function space, since the exponential bifunctor $F \to G$ is contravariant in its left argument. So when you write an inductive type definition, you are defining a functor to take a least fixed point of. To ensure that it is indeed a functor, you need to rule out occurences of the recursive parameter on the left-hand-side of function spaces --- hence the positivity check.

Impredicativity (in the sense of System F) is generally avoided, because it is a principle that forces you to choose between classical logic and set-theoretic models. You can't interpret types as sets in classical set theory if you have F-style indexing. (See Reynolds' famous "Polymorphism is Not Set-Theoretic".)

Categorically, F-style impredicativity says that the category of types and terms forms a small complete category (that is, homs and objects are both sets, and limits of all small diagrams exist). Classically this forces a category to be a poset. Many constructivists are constructive because they want their theorems to hold in more systems than just classical logic, and so they don't want to prove anything that would be classically false. Hence they are leery of impredicative polymorphism.

However, polymorphism lets you say many conditions that are classically "large" internally to your type theory -- and positivity is one of them! A type operator $F$ is functorial, if you can produce a polymorphic term:

$$ \mathsf{Fmap} : \forall \alpha, \beta.\; (\alpha \to \beta) \to (F(\alpha) \to F(\beta)) $$

See how this corresponds to functoriality? IMO, this would be a very nice option to have in Coq, since it would let you do generic programming much more easily. The syntactic nature of the positivity check is a big hindrance to generic programming, and I would be happy to trade the possibility of classical axioms for more flexible functional programs.

EDIT: The question you are asking about the difference between Prop and Set arises from the fact that the Coq developers want to permit you think about Coq theorems in naive set-theoretic terms if you want, without forcing you to do so. Technically, they split Prop and Set, and then prohibit sets from depending on the computational content of Prop.

So you can interpret Prop as truth values in ZFC, which are the booleans true and false. In this world, all proofs of propositions are equal, and so obviously you should not be able to branch on the proof of a proposition. So the prohibition on sets depending on the computational content of proofs of Prop is totally sensible. Furthermore, the 2-element boolean lattice is obviously a complete lattice, so it should support impredicative indexing, since arbitrary set-valued meets exist. The predicativity restriction on Sets arises from the fact (mentioned above) that F-style indexing is degenerate in classical set-theoretic models.

Coq has other models (it's constructive logic!) but the point is that off the shelf it will never prove anything that a classical mathematician would be puzzled by.

Answer 2

There is a very deep connection between inductive definitions and impredicativity, but my understanding is that in the context of what you are talking about (im)predicativity is not particularly relevant and the test is purely to guarantee monotonicity, so that fixed point theory can be applied, namely, that the principle of induction is well-defined. (I'm willing to be corrected on this point.)

The relationship between impredicativity and inductive definitions is explored in this talk by Coquand. It goes back to some results from the 50s by G. Takeuti that impredicative definitions can be reduced to inductive definitions. The book

• Proof Theory of Impredicative Subsystems of Analysis - Monographs and Textbooks in Physical Science 2 by W. Buchholz, K. Schutte

gives a good analysis of the topic, if you can get your hands on it. These slides give an overview.

Answer 3

Just to complete the excellent explanation by Neil, impredicativity has a "soft" sense: the definition of sets or collections by using a reference to themselves. In that sense:

Inductive Lam : Set :=
| Var : Nat -> Lam
| App : Lam -> Lam -> Lam
| Abs : (Lam -> Lam) -> Lam

is an impredicative definition, as it defines an inductive type, Lam using a function space (Lam -> Lam) which refers to the collection itself. In this situation, impredicativity is harmful: it is possible to use Cantor's theorem to prove False. In fact this is the same brand of impredicativity which discounts naive Set Theory as a consistent foundation for mathematics. It is therefore disallowed in Coq. Another form of impredicativity is allowed, as you are aware:

Definition Unit : Prop := forall X:Prop, X -> X

The definition of Unit as a proposition makes reference to the collection of all Propositions of which it is a member. However, for reasons somewhat obscure to me, this impredicativity is not harmful as it is present in ZFC (in the form of unbounded comprehension) which is not known to be inconsistent.

In conclusion, negative occurences of inductive types in definitions is a form of impredicativity, but not the one usually referred to when speaking of CoC as an impredicative framework.