Ex falso quodlibet

Ostensibly, the goal of this lecture note is to illustrate that False implies anything. In passing, we also show how to construct a universal statement (i.e., forall ..., ...) as well as an existential statement (i.e., exists ..., ...).

A property that does not hold

The following property very much does not hold:

Property foo :
  forall P : nat -> Prop,
    (exists i : nat,
        P i) ->
    forall j : nat,
      P j.

Indeed if one assumes that it holds, one can conclude an absurdity:

Theorem ex_falso_quodlibet_eg_False :
  (forall P : nat -> Prop,
      (exists i : nat,
          P i) ->
      forall j : nat,
        P j) ->
  0 = 1.

To prove this theorem, we need to construct an existential statement, which is done using ex_intro as illustrated below, picking the proposition that all natural numbers are equal to 0 as a token proposition that does not hold:

Proof.
  intro H_absurd.
  Check (H_absurd
           (fun n : nat => 0 = n)).
  (* : (exists i : nat, 0 = i) -> forall j : nat, 0 = j *)

So we need to construct an expression of type exists i : nat, 0 = i:

Check (ex_intro
         (fun i : nat => 0 = i)).
(* : forall x : nat, 0 = x -> exists i : nat, 0 = i *)

We can further instantiate ex_intro with 0 and the fact that 0 is equal to itself:

Check (ex_intro
         (fun i : nat => 0 = i)
         0
         (eq_refl 0)).
(* : exists i : nat, 0 = i *)

We now have an expression of type exists i : nat, 0 = i, so let’s further instantiate H_absurd:

Check (H_absurd
         (fun n : nat => 0 = n)
         (ex_intro
            (fun i : nat => 0 = i)
            0
            (eq_refl 0))).
(* : forall j : nat, 0 = j *)

Let us pick 1, for example:

Check (H_absurd
         (fun n : nat => 0 = n)
         (ex_intro
            (fun i : nat => 0 = i)
            0
            (eq_refl 0))
         1).
(* : 0 = 1 *)

Which is what we wanted to prove:

  exact (H_absurd
           (fun n : nat => 0 = n)
           (ex_intro
              (fun i : nat => 0 = i)
              0
              (eq_refl 0))
           1).
Qed.

Exercise 08

Prove the following alternative theorem:

Theorem ex_falso_quodlibet_indeed :
  (forall (P : nat -> Prop),
      (exists i : nat,
          P i) ->
      forall j : nat,
        P j) -> False.

Exercise 09

Since False implies anything, including True, prove the following theorem as a corollary of Property foo, assuming that it was admitted:

Theorem ex_falso_quodlibet_eg_True :
  forall m : nat,
    exists n : nat,
      m < n.

An equivalence

As it happens, an existential quantification, when it is in the premise of an implication, can be restated as a universal quantification based on the following equivalence:

Proposition an_equivalence :
  (forall P : nat -> Prop,
      (exists i : nat,
          P i) ->
      forall j : nat,
        P j)
  <->
  (forall (P : nat -> Prop)
          (i : nat),
      P i ->
      forall j : nat,
        P j).

Exercise 10

Prove the equivalence above.

Revisiting the proposition that does not hold

Thanks to the equivalence proved in Exercise 10, the property that very much does not hold can be restated as follows:

Property bar :
  forall (P : nat -> Prop)
         (i : nat),
    P i ->
    forall j : nat,
      P j.

Exercise 11

Prove that if Property bar is assumed to hold, an absurdity can be concluded:

Theorem ex_falso_quodlibet_eg_False_revisited :
  (forall (P : nat -> Prop)
          (i : nat),
      P i ->
      forall j : nat,
        P j) ->
  0 = 1.

Exercise 12

Since False implies anything, including True, prove the following theorem as a corollary of Property bar, assuming that it was admitted:

Theorem ex_falso_quodlibet_eg_True_revisited :
  forall m : nat,
    exists n : nat,
      m < n.

Resources

• The .v file for the present lecture note (latest version: 22 Feb 2024).

Version

Created [22 Feb 2024]