Proving False with negative inductive types in Coq

Question

The third chapter of CPDT briefly discusses why negative inductive types are forbidden in Coq. If we had

Inductive term : Set :=
| App : term -> term -> term
| Abs : (term -> term) -> term.
Non strictly positive occurrence of "term" in
 "(term -> term) -> term".

then we could easily define a function

Definition uhoh (t : term) : term :=
  match t with
  | Abs f => f t
  | _ => t
  end.

so that the term uhoh (Abs uhoh) would be non-terminating, with which "we would be able to prove every theorem".

I understand the non-termination part, but I don't get how we can prove anything with it. How would one prove False using term as defined above?

Answer

Reading your question made me realize that I didn't quite understand Adam's argument either. But inconsistency in this case results quite easily from Cantor's usual diagonal argument (a never-ending source of paradoxes and puzzles in logic). Consider the following assumptions:

Section Diag.

  Variable T : Type.
  Variable test : T -> bool.
  Variables x y : T.

  Hypothesis xT : test x = true.
  Hypothesis yF : test y = false.

  Variable g : (T -> T) -> T.
  Variable g_inv : T -> (T -> T).

  Hypothesis gK : forall f, g_inv (g f) = f.

  Definition kaboom (t : T) : T :=
    if test (g_inv t t) then y else x.

  Lemma kaboom1 : forall t, kaboom t <> g_inv t t.
T: Type
test: T -> bool
x, y: T
xT: test x = true
yF: test y = false
g: (T -> T) -> T
g_inv: T -> T -> T
gK: forall f : T -> T, g_inv (g f) = f
forall t : T, kaboom t <> g_inv t t
  Proof using T test x y xT yF g_inv.
T: Type
test: T -> bool
x, y: T
xT: test x = true
yF: test y = false
g: (T -> T) -> T
g_inv: T -> T -> T
gK: forall f : T -> T, g_inv (g f) = f
forall t : T, kaboom t <> g_inv t t
    intros t H.
T: Type
test: T -> bool
x, y: T
xT: test x = true
yF: test y = false
g: (T -> T) -> T
g_inv: T -> T -> T
gK: forall f : T -> T, g_inv (g f) = f
t: T
H: kaboom t = g_inv t t
False
    unfold kaboom in H.
T: Type
test: T -> bool
x, y: T
xT: test x = true
yF: test y = false
g: (T -> T) -> T
g_inv: T -> T -> T
gK: forall f : T -> T, g_inv (g f) = f
t: T
H: (if test (g_inv t t) then y else x) = g_inv t t
False
    destruct (test (g_inv t t)) eqn:E; congruence.
  Qed.

  Lemma kaboom2 : False.
T: Type
test: T -> bool
x, y: T
xT: test x = true
yF: test y = false
g: (T -> T) -> T
g_inv: T -> T -> T
gK: forall f : T -> T, g_inv (g f) = f
False
  Proof using T test x y xT yF g g_inv gK.
T: Type
test: T -> bool
x, y: T
xT: test x = true
yF: test y = false
g: (T -> T) -> T
g_inv: T -> T -> T
gK: forall f : T -> T, g_inv (g f) = f
False
    assert (H := @kaboom1 (g kaboom)).
T: Type
test: T -> bool
x, y: T
xT: test x = true
yF: test y = false
g: (T -> T) -> T
g_inv: T -> T -> T
gK: forall f : T -> T, g_inv (g f) = f
H: kaboom (g kaboom) <> g_inv (g kaboom) (g kaboom)
False
    rewrite -> gK in H.
T: Type
test: T -> bool
x, y: T
xT: test x = true
yF: test y = false
g: (T -> T) -> T
g_inv: T -> T -> T
gK: forall f : T -> T, g_inv (g f) = f
H: kaboom (g kaboom) <> kaboom (g kaboom)
False
    congruence.
  Qed.

End Diag.

This is a generic development that could be instantiated with the term type defined in CPDT: T would be term, x and y would be two elements of term that we can test discriminate between (e.g. App (Abs id) (Abs id) and Abs id). The key point is the last assumption: we assume that we have an invertible function g : (T -> T) -> T which, in your example, would be Abs. Using that function, we play the usual diagonalization trick: we define a function kaboom that is by construction different from every function T -> T, including itself. The contradiction results from that.