What does consistency mean for "computational theories" corresponding to inductive types?
With inductive types consistency is manifested as a termination property. Functions from inductive types are defined by structural recursion. How do we know they are well-defined, i.e., that they are total?

Here is an example:

Inductive nat :=
  | Z : nat
  | S : nat -&gt; nat.

Inductive omega1 :=
  | zero : omega1
  | succ : omega1 -&gt; omega1
  | sup  : (nat -&gt; omega1) -&gt; omega1.


Intuitively, omega1 consists of well-founded countable trees. Given a type A, an element a : A, a map f : A -&gt; A and a map g : (nat -&gt; A) -&gt; A we can define a map F : omega1 -&gt; A by recursion:

fix F (t : omega1) : A :=
  match t with
  | zero =&gt; a
  | succ x =&gt; f (F x)
  | sup s =&gt; g (fun n : nat =&gt; F (s n))
  end


The principle that every such F is well defined is equivalent to induction on well-founded countable trees. In terms of ordinal strength that's induction up to $\omega_1$. If you keep everything syntactic and/or computable so that you only use computable trees, you might get away with $\omega_1^{\mathrm{CK}}$, which isn't really better. Therefore, if $\omega_1$ does not exist we have a problem, and existence of $\omega_1$ is pretty strong in terms of consistency.

Concretely, suppose we came up with a new kind of inductive type I that were inhabited and it allowed us to write a non-terminating function. We could use it inhabit the empty type void by defining a non-terminating function f : I -&gt; void. This actually happened in history. Originallly Martin-Löf proposed a type theory with Type : Type and Girard proved it to be inconsistent by simulating the Burali-Forti paradox. This gives us an idea: suppose we define a type WellOrder of all well-orders. Because well-orders themselves are well-ordered, WellOrder has an induction principle -- it is a kind of inductive type, and in fact is itself a well-order. If we now also posit that WellOrder is an element of WellOrder (by which I mean that there is wt : WellOrder which encodes WellOrder) we will hit the Burali-Forty paradox, define a non-terminating function, and inhabit False. In fact, much less is needed and is included in the standard Coq library under Pardoxes.BuralliForti_ex, see theorem Burali_Forti : False.