Skip to content

Instantly share code, notes, and snippets.

@jp-diegidio
Last active November 25, 2024 01:32
Show Gist options
  • Save jp-diegidio/f9a18bb0a8c87d585b1d56458cd082f6 to your computer and use it in GitHub Desktop.
Save jp-diegidio/f9a18bb0a8c87d585b1d56458cd082f6 to your computer and use it in GitHub Desktop.
Epimenides Paradox (in Coq)
(** 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
<< > 'Morning everybody,
> "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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment