<p>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?</p>

<p>Here is an example:</p>

<pre><code>Inductive nat :=
  | Z : nat
  | S : nat -&gt; nat.

Inductive omega1 :=
  | zero : omega1
  | succ : omega1 -&gt; omega1
  | sup  : (nat -&gt; omega1) -&gt; omega1.
</code></pre>

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

<pre><code>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
</code></pre>

<p>The principle that every such <code>F</code> 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.</p>

<p>Concretely, suppose we came up with a new kind of inductive type <code>I</code> that were inhabited and it allowed us to write a non-terminating function. We could use it inhabit the empty type <code>void</code> by defining a non-terminating function <code>f : I -&gt; void</code>. This actually happened in history. Originallly Martin-Löf proposed a type theory with <code>Type : Type</code> and Girard proved it to be inconsistent by simulating the Burali-Forti paradox. This gives us an idea: suppose we define a type <code>WellOrder</code> of all well-orders. Because well-orders themselves are well-ordered, <code>WellOrder</code> 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 <code>WellOrder</code> is an element of <code>WellOrder</code> (by which I mean that there is <code>wt : WellOrder</code> which encodes <code>WellOrder</code>) we will hit the Burali-Forty paradox, define a non-terminating function, and inhabit <code>False</code>. In fact, much less is needed and is included in the standard Coq library under <a href="http://coq.inria.fr/V8.2pl1/contribs/Paradoxes.BuraliForti_ex.html" rel="nofollow"><code>Pardoxes.BuralliForti_ex</code></a>, see theorem <a href="http://coq.inria.fr/V8.2pl1/contribs/Paradoxes.BuraliForti_ex.html#Burali_Forti" rel="nofollow"><code>Burali_Forti : False</code></a>.</p>

CC BY-SA 3.0
2014-04-17T18:59:25.507Z
> With inductive types consistency is manifested as a termination property 

But why is this so? I.e. what is the most basic notion of consistency?
Konstantin Solomatov
CC BY-SA 3.0
2014-04-17T19:14:23.373Z
@KonstantinSolomatov Non-terminating functions can he used to inhabit every type, including types representing falsity.
Martin Berger
CC BY-SA 3.0
2014-04-17T19:16:45.067Z
@MartinBerger Yes, I understand this. What I don't understand is why other kinds of inconsistencies are impossible or at least why they aren't considered.
Konstantin Solomatov
CC BY-SA 3.0
2014-04-17T19:22:35.133Z
@KonstantinSolomatov What do you mean by other kinds of inconsistencies?
Martin Berger
CC BY-SA 3.0
2014-04-17T19:32:16.503Z
@KonstantinSolomatov Typically, consistency comes from soundness (which establishes that if $M \to N$ then $N$ has all of $M$'s types), normalization (which establishes that if $M : T$ then there exists a value (normal form) $V$ such that $M \to^* V$), and syntactic analysis on values (there's no way to infer $3 : \mathsf{Bool}$). Putting them all together, there is no way to collapse the type system: every term's types are also the type of a value and no value has all the types.
Gilles 'SO- stop being evil'
CC BY-SA 3.0
2014-04-17T20:09:05.877Z
@MartinBerger I mean other types of consistency than just termination property.
Konstantin Solomatov
CC BY-SA 3.0
2014-04-17T20:10:06.770Z
@Giles What you described is progress and preservation of type system. What I am interested in, is consistency of a logic.
Konstantin Solomatov
CC BY-SA 3.0
2014-04-17T20:30:05.433Z
@Gilles I disagree with this. Consistency of a foundational system always means the same: you can't prove something false. For different approaches to foundations, different obstacles must be overcome towards consistency. Showing type-soundness and the indefinability of non-total functions are but proof techniques towards showing falsity cannot be derived. For type-theoretic  foundations, type-soundness and the indefinability of
non-terminating functions are the key obstacles to be overcome,
that's why there is so much focus on them. But they are not
conceptually equal to consistency.
Martin Berger
CC BY-SA 3.0
2014-04-17T20:44:01.030Z
@MartinBerger I view “prove something false” as a kind of special case — the point of proving something false is that it lets you prove everything, which collapses the logic to an utterly boring one. What do you do if “false” is a derived notion in the system (as it is in the calculus of constructions, for instance)? But I don't understand how this would mean that we disagree: we seem to be approaching the same definition from different angles.
Gilles 'SO- stop being evil'
CC BY-SA 3.0
2014-04-17T21:00:14.497Z
There are various ways of expressing inconsistency, but they all amount to "the system is trival". In type theory one kind of inconsistency is "every type is inhabited", which in the presence of an empty type (primitive or derived) is the same as "the empty type is inhabited". Note however that there are perfectly interesting type theories with inhabited types, e.g., programming languages with recursion. Konstantin, you speak of other kinds of inconsistencies, and we keep asking you what they might be. Can you please be concrete? What more do you want than to inhabit every type?
Andrej Bauer
CC BY-SA 3.0
2014-04-17T22:25:10.463Z
@AndrejBauer I think philosophically the essence of consistency is the
inability to derive something false. In most systems we typically
consider this inability coincides with non-triviality (i.e. not
everything can be derived). But I can imagine a three-valued
foundation that is non-trivial but allows me to derive 0 = 1.

Anyway, I think we all agree that in the systems Konstantin cares
about, both notions coincide.
Martin Berger
CC BY-SA 3.0
2014-04-18T03:43:03.590Z
@AndrejBauer Basically I found what I wanted in your answer and comments. Thank you.

Consistency and what to consider as such seems to be a philosophical question in many respects, but reading the long list of comments helped me a lot. Thank you.
Konstantin Solomatov
CC BY-SA 3.0
2014-04-17T18:20:25.550Z
2014-04-17T21:00:39.837Z
2014-04-17T21:00:39.837Z
Andrej Bauer
<p>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. </p>

<p>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>

<p>P.S. As far as I understand from an answer to my previous question <a href="https://cstheory.stackexchange.com/questions/21938/correctness-of-type-theory">&quot;Correctness&quot; of type theory</a> 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?</p>

<lo.logic><dependent-type>
What does consistency mean for "computational theories" corresponding to inductive types?
Konstantin Solomatov
# What does consistency mean for "computational theories" corresponding to inductive types?

(Asked by: username_0 on 2014-04-17)

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 ["Correctness" of type theory](https://cstheory.stackexchange.com/questions/21938/correctness-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?

**Tags:** lo.logic, dependent-type

---

## 1 answers

### Answer by username_1 on 2014-04-17. Score: 7 | Accepted answer

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

Inductive omega1 :=
  | zero : omega1
  | succ : omega1 -> omega1
  | sup  : (nat -> omega1) -> omega1.

Intuitively, omega1 consists of well-founded countable trees. Given a type A, an element a : A, a map f : A -> A and a map g : (nat -> A) -> A we can define a map F : omega1 -> A by recursion:
fix F (t : omega1) : A :=
  match t with
  | zero => a
  | succ x => f (F x)
  | sup s => g (fun n : nat => 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 -> 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.

> **Comments:**
> **username_0**: > With inductive types consistency is manifested as a termination property   But why is this so? I.e. what is the most basic notion of consistency?  
> **username_2**: @KonstantinSolomatov Non-terminating functions can he used to inhabit every type, including types representing falsity.  
> **username_0**: @MartinBerger Yes, I understand this. What I don't understand is why other kinds of inconsistencies are impossible or at least why they aren't considered.  
> **username_2**: @KonstantinSolomatov What do you mean by other kinds of inconsistencies?  
> **username_3**: @KonstantinSolomatov Typically, consistency comes from soundness (which establishes that if $M \to N$ then $N$ has all of $M$'s types), normalization (which establishes that if $M : T$ then there exists a value (normal form) $V$ such that $M \to^* V$), and syntactic analysis on values (there's no way to infer $3 : \mathsf{Bool}$). Putting them all together, there is no way to collapse the type system: every term's types are also the type of a value and no value has all the types.  
> **username_0**: @MartinBerger I mean other types of consistency than just termination property.  
> **username_0**: @Giles What you described is progress and preservation of type system. What I am interested in, is consistency of a logic.  
> **username_2**: @Gilles I disagree with this. Consistency of a foundational system always means the same: you can't prove something false. For different approaches to foundations, different obstacles must be overcome towards consistency. Showing type-soundness and the indefinability of non-total functions are but proof techniques towards showing falsity cannot be derived. For type-theoretic  foundations, type-soundness and the indefinability of non-terminating functions are the key obstacles to be overcome, that's why there is so much focus on them. But they are not conceptually equal to consistency.  
> **username_3**: @MartinBerger I view “prove something false” as a kind of special case — the point of proving something false is that it lets you prove everything, which collapses the logic to an utterly boring one. What do you do if “false” is a derived notion in the system (as it is in the calculus of constructions, for instance)? But I don't understand how this would mean that we disagree: we seem to be approaching the same definition from different angles.  
> **username_1**: There are various ways of expressing inconsistency, but they all amount to "the system is trival". In type theory one kind of inconsistency is "every type is inhabited", which in the presence of an empty type (primitive or derived) is the same as "the empty type is inhabited". Note however that there are perfectly interesting type theories with inhabited types, e.g., programming languages with recursion. Konstantin, you speak of other kinds of inconsistencies, and we keep asking you what they might be. Can you please be concrete? What more do you want than to inhabit every type?  
> **username_2**: @AndrejBauer I think philosophically the essence of consistency is the inability to derive something false. In most systems we typically consider this inability coincides with non-triviality (i.e. not everything can be derived). But I can imagine a three-valued foundation that is non-trivial but allows me to derive 0 = 1.  Anyway, I think we all agree that in the systems Konstantin cares about, both notions coincide.  
> **username_0**: @AndrejBauer Basically I found what I wanted in your answer and comments. Thank you.  Consistency and what to consider as such seems to be a philosophical question in many respects, but reading the long list of comments helped me a lot. Thank you.  

---

