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 12

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 13

Since False implies anything, including True, ...

Pablito: Is that right?

The fourth wall (rushing in): Just a sec.

Interlude

Pablito: Thanks, Fourth Wall.

The fourth wall: You are welcome, Pablito. Now you were saying?

Pablito: I was saying “Is that right?”, not very fast. It’s a common idiom in the American MidWest.

The fourth wall: Thanks, I get that. But what did you mean?

Pablito: Ah, right. I was wondering about the opening line of the exercise, namely “Since False implies anything, including True”.

The fourth wall: Er... OK?

Pablito: Just a sec:

Property False_implies_anything :
  forall A : Prop,
    False -> A.

The fourth wall: Yes?

Pablito: Let me see:

Proof.
  intros A F.

The fourth wall: Yes?

Pablito: Ah, right, we have False among our assumptions, and so we can use the contradiction tactic to complete the proof:

  contradiction F.
Qed.

The fourth wall: Yes. That is about the simplest illustration of the contradiction tactic.

Pablito: Indeed it is. Hum, just a sec.

The fourth wall: Sure.

Pablito <clickety clickety click>: Well, I just solved Exercise 07 in Week 07. Blush. Please proceed, Fourth Wall, please proceed.

Exercise 13

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 14

Prove the equivalence above.

Revisiting the proposition that does not hold

Thanks to the equivalence proved in Exercise 14, 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 15

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 16

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: 07 Mar 2025).

Version

Added the interlude nearby Exercise 13 [06 Jun 2025]

Created [07 Mar 2025]