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?
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.