Epimenides Paradox (in Coq)

EpimenidesParadox.v

(**
  Epimenides' Paradox (v1.3-draft)

  << 'Morning everybody,
     "Epimenides lies iff everybody lies!" which
     I am taking to be *the predicative version of*
     "the uncooperative rational player". >>

  Proposition:
    Epimenides the Cretan says
      "all Cretans are liars!"
  Question:
    Is it true (that "all Cretans are liars")?
  Answer:
    It is true if Epimenides says so!
    In fact, it is true iff any Cretan says so!!
  Notes:
  - Since "Cretan" is the one universe of discourse,
    we write it as the more generic "Person" in our
    formalization: persons who assert propositions
    and may be lying about what they are asserting.
  - Our definition of "asserting" is a specific one:
    we assume that asserting a proposition amounts
    to assuring that there exists evidence for the
    proposition, and that "liar" is one who gives
    false assurance.
  - *TODO*: In this "paradox", the rule of the game
    is that who speaks the truth *always* speaks the
    truth, and who lies *always* lies: and I have
    barely started exploring that part, "the intrinsic
    consequences of Epimenides' logic", anyway this
    seems immaterial to our main theorem...

  Initially presented at sci.logic here:
  https://groups.google.com/g/sci.logic/c/27ig6u97dgM/m/swXAFyDkAQAJ

  > "Epimenides lies iff everybody lies!" which

  << Eh, sorry, I have said that upside down: beware of bugs...
     The short answer is "if he says so!" though it turns out
     it works in both directions... >>
*)

Module Type EpimenidesSig.

  (* [Person] is "our universe of discourse". *)
  Parameter Person : Set.

End EpimenidesSig.

Module EpimenidesLogic (Sig : EpimenidesSig).

  Include Sig.

  (** [asserts who P] :=
      [who] "assures evidence for" [P]. *)
  Inductive asserts (who : Person) : Prop -> Prop :=
    asserted (P : Prop)
      (HP : P) : asserts who P.

  (** [denies who P] :=
      [who] "assures evidence for" [~ P]. *)
  Inductive denies (who : Person) : Prop -> Prop :=
    denied (P : Prop)
      (AN : asserts who (~ P)) : denies who P.

  (** [liar who] :=
      if [who] "asserts" [P] then [~ P]. *)
  Inductive liar (who : Person) : Prop :=
    lied (H : forall (P : Prop),
      asserts who P -> ~ P) : liar who.

  (** [assertion] :
      if "asserts" [P] then [P]. *)
  Lemma assertion :
    forall (who : Person) (P : Prop),
      asserts who P -> P.
  Proof.
    intros who P AP.
    destruct AP as [P HP].
    apply HP.
  Qed.

  (** [denial] :
      if "denies" [P] then [~ P]. *)
  Lemma denial :
    forall (who : Person) (P : Prop),
      denies who P -> ~ P.
  Proof.
    intros who P DP.
    destruct DP as [P AN].
    apply assertion in AN.
    apply AN.
  Qed.

  (** [asserting_consistent] :
      "not asserts and denies". *)
  Theorem asserting_consistent :
    forall (who : Person) (P : Prop),
      ~ (asserts who P /\ denies who P).
  Proof.
    intros who P [AP DP].
    apply assertion in AP as HP.
    apply denial in DP as HN.
    apply (HN HP).
  Qed.

  (** [asserts_to_denies_not] :
      "to assert is to deny~". *)
  Lemma asserts_to_denies_not :
    forall (who : Person) (P : Prop),
      asserts who P -> denies who (~ P).
  Proof.
    intros who P AP.
    apply (denied who).
    apply (asserted who).
    apply assertion in AP as HP.
    intros HN.
    apply (HN HP).
  Qed.

  (** [asserts_not_to_denies] :
      "to assert~ is to deny". *)
  Lemma asserts_not_to_denies :
    forall (who : Person) (P : Prop),
      asserts who (~ P) -> denies who P.
  Proof.
    intros who P AN.
    apply (denied who).
    apply AN.
  Qed.

  (** [denies_to_asserts_not] :
      "to deny is to assert~". *)
  Lemma denies_to_asserts_not :
    forall (who : Person) (P : Prop),
      denies who P -> asserts who (~ P).
  Proof.
    intros who P DN.
    apply (asserted who).
    apply denial in DN as HN.
    apply HN.
  Qed.

  (** [denies_not_to_asserts_AX] :
      "to deny~ is to assert".
    Note: requires classical logic! *)
  Lemma denies_not_to_asserts_AX :
    (forall (P : Prop), ~ ~ P -> P) -> (** DNE! *)
    forall (who : Person) (P : Prop),
      denies who (~ P) -> asserts who P.
  Proof.
    intros DNE who P DN.
    apply (asserted who).
    apply denial in DN as HNN.
    apply ((DNE P) HNN).
  Qed.

  (** [liar_incorrect] :
      "a liar denies what is". *)
  Theorem liar_incorrect :
    forall (who : Person),
      liar who <->
      forall (P : Prop),
        asserts who P -> ~ P.
  Proof.
    intros who.
    split.
    - (* liar who -> asserted opp. *)
      intros [L] P AP.
      apply ((L P) AP).
    - (* asserted opp. -> liar who *)
      intros H.
      apply (lied who).
      apply H.
  Qed.

  (** [liar_scorrect] :
      "a liar induces dishonesty". *)
  Theorem liar_scorrect :
    forall (who : Person),
      liar who <->
      forall (epi : Person) (P : Prop),
        asserts who P -> asserts epi (~ P).
  Proof.
    intros who.
    split.
    - (* liar who -> induces dishon. *)
      intros Lw epi P Aw.
      destruct Lw as [Hw].
      apply (asserted epi).
      apply ((Hw P) Aw).
    - (* induced dishon. -> liar who *)
      intros H.
      apply (lied who).
      intros P AP HP.
      assert (AN : asserts who (~ P))
        by apply ((H who P) AP).
      apply (assertion who) in AP.
      apply (assertion who) in AN.
      apply (AN AP).
  Qed.

End EpimenidesLogic.

Module EpimenidesParadox (Sig : EpimenidesSig).

  Module Export Logic := EpimenidesLogic Sig.

  (* [all_liars] :=
     "all persons are liars". *)
  Definition all_liars : Prop :=
    forall (who : Person),
      liar who.

  (* [epimenides_paradox] :
     "all liars iff asserted so". *)
  Theorem epimenides_paradox :
    forall (who : Person),
      asserts who all_liars <->
      all_liars.
  Proof.
    intros who.
    split.
    - (* asserts -> all liars *)
      intros AL.
      apply assertion in AL.
      apply AL.
    - (* all liars -> asserts *)
      intros HL.
      apply (asserted who).
      apply HL.
  Qed.

End EpimenidesParadox.