6
$\begingroup$

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

Improve this question
$\endgroup$

1 Answer 1

Reset to default
7
$\begingroup$

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.

Improve this answer
$\endgroup$
12
  • 2
    $\begingroup$ @KonstantinSolomatov Non-terminating functions can he used to inhabit every type, including types representing falsity. $\endgroup$
    – Martin Berger
    Apr 17, 2014 at 19:14
  • 2
    $\begingroup$ @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. $\endgroup$
    – Gilles 'SO- stop being evil'
    Apr 17, 2014 at 19:32
  • 1
    $\begingroup$ @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. $\endgroup$
    – Martin Berger
    Apr 17, 2014 at 20:30
  • 1
    $\begingroup$ @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. $\endgroup$
    – Gilles 'SO- stop being evil'
    Apr 17, 2014 at 20:44
  • 3
    $\begingroup$ 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? $\endgroup$
    – Andrej Bauer
    Apr 17, 2014 at 21:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.