ClassicalEpsilon.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(************************************************************************)

This file provides classical logic and indefinite description under the form of Hilbert's epsilon operator

Hilbert's epsilon operator and classical logic implies excluded-middle in Set and leads to a classical world populated with non computable functions. It conflicts with the impredicativity of Set

Require Export Classical.
Require Import ChoiceFacts.

Set Implicit Arguments.

Axiom constructive_indefinite_description :
  forall (A : Type) (P : A->Prop),
    (exists x, P x) -> { x : A | P x }.

Lemma constructive_definite_description :
  forall (A : Type) (P : A->Prop),
    (exists! x, P x) -> { x : A | P x }.forall (A : Type) (P : A -> Prop),
(exists ! x : A, P x) -> {x : A | P x}
Proof.forall (A : Type) (P : A -> Prop),
(exists ! x : A, P x) -> {x : A | P x}
  intros; apply constructive_indefinite_description; firstorder.
Qed.

Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}.forall P : Prop, {P} + {~ P}
Proof.forall P : Prop, {P} + {~ P}
  apply
    (constructive_definite_descr_excluded_middle
      constructive_definite_description classic).
Qed.

Theorem classical_indefinite_description :
  forall (A : Type) (P : A->Prop), inhabited A ->
    { x : A | (exists x, P x) -> P x }.forall (A : Type) (P : A -> Prop),
inhabited A -> {x : A | (exists x0 : A, P x0) -> P x}
Proof.forall (A : Type) (P : A -> Prop),
inhabited A -> {x : A | (exists x0 : A, P x0) -> P x}
  intros A P i.A:Type
P:A -> Prop
i:inhabited A
{x : A | (exists x0 : A, P x0) -> P x}
  destruct (excluded_middle_informative (exists x, P x)) as [Hex|HnonP].A:Type
P:A -> Prop
i:inhabited A
Hex:exists x : A, P x
{x : A | (exists x0 : A, P x0) -> P x}
A:Type
P:A -> Prop
i:inhabited A
HnonP:~ (exists x : A, P x)
{x : A | (exists x0 : A, P x0) -> P x}
  apply constructive_indefinite_description
    with (P:= fun x => (exists x, P x) -> P x).A:Type
P:A -> Prop
i:inhabited A
Hex:exists x : A, P x
exists x : A, (exists x0 : A, P x0) -> P x
A:Type
P:A -> Prop
i:inhabited A
HnonP:~ (exists x : A, P x)
{x : A | (exists x0 : A, P x0) -> P x}
  destruct Hex as (x,Hx).A:Type
P:A -> Prop
i:inhabited A
x:A
Hx:P x
exists x0 : A, (exists x1 : A, P x1) -> P x0
A:Type
P:A -> Prop
i:inhabited A
HnonP:~ (exists x : A, P x)
{x : A | (exists x0 : A, P x0) -> P x}
    exists x; intros _; exact Hx.A:Type
P:A -> Prop
i:inhabited A
HnonP:~ (exists x : A, P x)
{x : A | (exists x0 : A, P x0) -> P x}
  assert {x : A | True} as (a,_).A:Type
P:A -> Prop
i:inhabited A
HnonP:~ (exists x : A, P x)
{_ : A | True}
A:Type
P:A -> Prop
i:inhabited A
HnonP:~ (exists x : A, P x)
a:A
{x : A | (exists x0 : A, P x0) -> P x}
    apply constructive_indefinite_description with (P := fun _ : A => True).A:Type
P:A -> Prop
i:inhabited A
HnonP:~ (exists x : A, P x)
exists _ : A, True
A:Type
P:A -> Prop
i:inhabited A
HnonP:~ (exists x : A, P x)
a:A
{x : A | (exists x0 : A, P x0) -> P x}
    destruct i as (a); firstorder.A:Type
P:A -> Prop
i:inhabited A
HnonP:~ (exists x : A, P x)
a:A
{x : A | (exists x0 : A, P x0) -> P x}
  firstorder.
Defined.

Hilbert's epsilon operator

Definition epsilon (A : Type) (i:inhabited A) (P : A->Prop) : A
  := proj1_sig (classical_indefinite_description P i).

Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) :
  (exists x, P x) -> P (epsilon i P)
  := proj2_sig (classical_indefinite_description P i).

Open question: is classical_indefinite_description constructively provable from relational_choice and constructive_definite_description (at least, using the fact that functional_choice is provable from relational_choice and unique_choice, we know that the double negation of classical_indefinite_description is provable (see relative_non_contradiction_of_indefinite_desc).

A proof that if P is inhabited, epsilon a P does not depend on the actual proof that the domain of P is inhabited (proof idea kindly provided by Pierre Castéran)

Lemma epsilon_inh_irrelevance :
   forall (A:Type) (i j : inhabited A) (P:A->Prop),
   (exists x, P x) -> epsilon i P = epsilon j P.forall (A : Type) (i j : inhabited A) (P : A -> Prop),
(exists x : A, P x) -> epsilon i P = epsilon j P
Proof.forall (A : Type) (i j : inhabited A) (P : A -> Prop),
(exists x : A, P x) -> epsilon i P = epsilon j P
 intros.A:Type
i, j:inhabited A
P:A -> Prop
H:exists x : A, P x
epsilon i P = epsilon j P
 unfold epsilon, classical_indefinite_description.A:Type
i, j:inhabited A
P:A -> Prop
H:exists x : A, P x
proj1_sig
  match
    excluded_middle_informative (exists x : A, P x)
  with
  | left Hex =>
      constructive_indefinite_description
        (fun x : A => (exists x0 : A, P x0) -> P x)
        match Hex with
        | ex_intro _ x Hx =>
            ex_intro
              (fun x0 : A =>
               (exists x1 : A, P x1) -> P x0) x
              (fun _ : exists x0 : A, P x0 => Hx)
        end
  | right HnonP =>
      let (a, _) :=
        constructive_indefinite_description
          (fun _ : A => True)
          match i with
          | inhabits a =>
              ex_intro (fun _ : A => True) a I
          end in
      exist
        (fun x : A => (exists x0 : A, P x0) -> P x) a
        (fun H0 : exists x : A, P x =>
         inhabited_ind
           (fun _ : A =>
            ex_ind
              (fun (x : A) (H1 : P x) =>
               False_ind (P a)
                 (HnonP
                    (ex_intro (fun x0 : A => P x0) x
                       H1))) H0) i)
  end =
proj1_sig
  match
    excluded_middle_informative (exists x : A, P x)
  with
  | left Hex =>
      constructive_indefinite_description
        (fun x : A => (exists x0 : A, P x0) -> P x)
        match Hex with
        | ex_intro _ x Hx =>
            ex_intro
              (fun x0 : A =>
               (exists x1 : A, P x1) -> P x0) x
              (fun _ : exists x0 : A, P x0 => Hx)
        end
  | right HnonP =>
      let (a, _) :=
        constructive_indefinite_description
          (fun _ : A => True)
          match j with
          | inhabits a =>
              ex_intro (fun _ : A => True) a I
          end in
      exist
        (fun x : A => (exists x0 : A, P x0) -> P x) a
        (fun H0 : exists x : A, P x =>
         inhabited_ind
           (fun _ : A =>
            ex_ind
              (fun (x : A) (H1 : P x) =>
               False_ind (P a)
                 (HnonP
                    (ex_intro (fun x0 : A => P x0) x
                       H1))) H0) j)
  end
 destruct (excluded_middle_informative (exists x : A, P x)) as [|[]]; trivial.
Qed.

Opaque epsilon.

Weaker lemmas (compatibility lemmas)

Theorem choice :
  forall (A B : Type) (R : A->B->Prop),
    (forall x : A, exists y : B, R x y) ->
    (exists f : A->B, forall x : A, R x (f x)).forall (A B : Type) (R : A -> B -> Prop),
(forall x : A, exists y : B, R x y) ->
exists f : A -> B, forall x : A, R x (f x)
Proof.forall (A B : Type) (R : A -> B -> Prop),
(forall x : A, exists y : B, R x y) ->
exists f : A -> B, forall x : A, R x (f x)
  intros A B R H.A, B:Type
R:A -> B -> Prop
H:forall x : A, exists y : B, R x y
exists f : A -> B, forall x : A, R x (f x)
  exists (fun x => proj1_sig (constructive_indefinite_description _ (H x))).A, B:Type
R:A -> B -> Prop
H:forall x : A, exists y : B, R x y
forall x : A,
R x
  (proj1_sig
     (constructive_indefinite_description (R x) (H x)))
  intro x.A, B:Type
R:A -> B -> Prop
H:forall x0 : A, exists y : B, R x0 y
x:A
R x
  (proj1_sig
     (constructive_indefinite_description (R x) (H x)))
  apply (proj2_sig (constructive_indefinite_description _ (H x))).
Qed.