What does consistency mean for "computational theories" corresponding to inductive types? I am currently reading the book by Luo on computation and reasoning. In the book he contrasts inductive types considered as computational theories with axiomatic theories widespread in "standard" mathematics. 

However, if we have axiomatic theories, then they can be inconsistent. It seems to be impossible with inductive types. But why this is so?

P.S. As far as I understand from an answer to my previous question &quot;Correctness&quot; of type theory we can create an inductively defined set and consistency of the type theory + inductive type will be equivalent to the consistency of set theory. Am I right?
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.