What are inductive predicates?

Question

How would you explain inductive predicates? What are they used for? What's the theory behind them? Are they only present in dependent type systems, or in other systems as well? Are they related to GADT's in some way? Why are they true by default in Coq?

This is an example from Coq:

Inductive even : nat -> Prop :=
| even0 : even 0
| evens : forall p:nat, even p -> even (S (S P))

How would you use this definition? Is it a datatype or a proposition?

Answer 1

I think we call inductive predicates objects that are defined inductively and sorted in Prop.

They are used for defining properties inductively (duh). The theory behind can probably be found in the literature for inductive constructions. Search papers about CIC (the Calculus of Inductive Constructions) for instance.

They are somewhat related to GADTs, though with dependent types they can express more things. If I am not mistaken, with GADTs each constructor lives in one particular family, whereas the addition of dependent types allows constructors to inhabit different families based on their arguments.

I do not know what you mean by "true by default in Coq".

even as you define it is an inductive datatype. It is not a proposition yet, as the type nat -> Prop indicates. A proposition would be even 0 or even 1. It can be inhabited (provable) as in even 0, or not as in even 1.

Answer 2

To answer another part of the question. Inductive predicates/definitions are not only present in dependent type systems (e.g., Isabelle/HOL also has them). In principle they are much older and just describe the least predicate (or set) that is closed under some given inference rules. Whether this is well-defined or not depends on the rules. There are sufficient conditions which are easy to check (e.g., that the defined predicate itself only occurs positively in premises of rules). Then the Knaster-Tarski theorem yields the desired result.

If I remember correctly the book The Formal Semantics of Programming Languages: An Introduction by Glynn Winskel gives an introduction to the mathematical foundations.