Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
Epimenides' Paradox (in Coq)
163 views
Skip to first unread message
Julio Di Egidio
Mar 29, 2023, 5:45:27 AM3/29/23
to
'Morning everybody,
"Epimenides lies iff everybody lies!" which
I am taking to be *the predicative version of*
"the uncooperative rational player".
I won't challenge you for conciseness on this
one, in fact it's not even finished...
Feedback welcome.
```coq
(**
Epimenides' Paradox. (v1.1-draft)
Proposition:
Epimenides the Cretan says
"all Cretans are liars!"
Question:
Is it true (that "all Cretans are liars")?
Answer:
It is true *iff* 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 the original "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...
*)
Module EpimenidesLogic.
(* [Person] is "our universe of discourse". *)
Parameter Person : Set.
(** [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 "asserted" [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_self_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 asserts the opposite of 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.
Import EpimenidesLogic.
(* [all_are_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.
```
Julio
"Epimenides lies iff everybody lies!" which
I am taking to be *the predicative version of*
"the uncooperative rational player".
I won't challenge you for conciseness on this
one, in fact it's not even finished...
Feedback welcome.
```coq
(**
Epimenides' Paradox. (v1.1-draft)
Proposition:
Epimenides the Cretan says
"all Cretans are liars!"
Question:
Is it true (that "all Cretans are liars")?
Answer:
It is true *iff* 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 the original "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...
*)
Module EpimenidesLogic.
(* [Person] is "our universe of discourse". *)
Parameter Person : Set.
(** [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 "asserted" [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_self_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 asserts the opposite of 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.
Import EpimenidesLogic.
(* [all_are_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.
```
Julio
Julio Di Egidio
Mar 29, 2023, 5:51:20 AM3/29/23
to
On Wednesday, 29 March 2023 at 11:45:27 UTC+2, Julio Di Egidio wrote:
> 'Morning everybody,
>
> "Epimenides lies iff everybody lies!" which
Eh, sorry, I have said that upside down: beware of bugs...
> 'Morning everybody,
>
> "Epimenides lies iff everybody lies!" which
The short answer is "if he says so!" though it turns out it
works in both directions...
Julio
Message has been deleted
olcott
Mar 29, 2023, 1:47:56 PM3/29/23
to
On 3/29/2023 9:41 AM, Dan Christensen wrote:
> Legend has it that the Cretan poet, Epimenides, once said that Cretans are "always liars." This narrative is often cited as an ancient paradox of logic. In fact, there is nothing "paradoxical" about it. It simply must be case that Epimenides himself was lying when he said this, and that at least one Cretan once told the truth.
>
> FORMAL PROOF: http://dcproof.com/LiarParadox2.htm (47 lines n DC Proof)
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
This version of the Liar Paradox seems to be an isomorphism to Russell's
Barber Paradox. ZFC was able to prove that any barber that claims to
shave everyone that does not shave themselves must be a liar.
This version of the Liar Paradox essentially has one barber making this
same sort of claim for all barbers, thus ZFC should refute this version
of the Liar Paradox.
--
Copyright 2023 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
> Legend has it that the Cretan poet, Epimenides, once said that Cretans are "always liars." This narrative is often cited as an ancient paradox of logic. In fact, there is nothing "paradoxical" about it. It simply must be case that Epimenides himself was lying when he said this, and that at least one Cretan once told the truth.
>
> FORMAL PROOF: http://dcproof.com/LiarParadox2.htm (47 lines n DC Proof)
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
This version of the Liar Paradox seems to be an isomorphism to Russell's
Barber Paradox. ZFC was able to prove that any barber that claims to
shave everyone that does not shave themselves must be a liar.
This version of the Liar Paradox essentially has one barber making this
same sort of claim for all barbers, thus ZFC should refute this version
of the Liar Paradox.
--
Copyright 2023 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
Mostowski Collapse
Mar 29, 2023, 5:03:00 PM3/29/23
to
Thank you for sharing. A little test case for my new prover.
And woa, it works. This is the input, not yet very comfortable,
just copy paste it into the dialog box:
?- gentzen((c(e) -> (s(x) -> (r(e,x) -> (
(t(x) ->
all(a:A,(c(A) ->
all(b:B, (s(B) -> (r(A,B) -> (t(B)->f))))
)
) -> (t(x)->f)))))), N), !.
https://www.dogelog.ch/littab/doclet/docs/05_supplement/07_unicorn/example54/package.html
And this is the output, generated in a blink! I am currently
experimenting with a proof shortener. But I guess it cannot
be made shorter? Not sure. If I find something will post again.
I do not yet have a axiom mechanism. So the last 4 conclusions
are just premis collection. So I would say with axioms it would have
14 steps. DC Poop needs 16 steps, because of <=> unpacking.
18 c(e) ⊃ s(x) ⊃ r(e, x) ⊃ t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b))) ⊃ ¬t(x)
▶ Conclusion 1,17
If I unfold the proof I get:
1 c(e)
Premise
2 s(x)
Premise
3 r(e, x)
Premise
4 t(x)
Premise
5 ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b)))
Premise
6 t(x)
Premise
7 c(e) ⊃ ∀b:(s(b) ⊃ r(e, b) ⊃ ¬t(b))
U Spec 5
8 ∀b:(s(b) ⊃ r(e, b) ⊃ ¬t(b))
Detach 7,1
9 s(x) ⊃ r(e, x) ⊃ ¬t(x)
U Spec 8
10 r(e, x) ⊃ ¬t(x)
Detach 9,2
11 ¬t(x)
Detach 10,3
12 ⊥
Detach 11,6
13 ¬t(x)
▲ Conclusion 6,12
14 ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b))) ⊃ ¬t(x)
▲ Conclusion 5,13
15 t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b))) ⊃ ¬t(x)
▲ Conclusion 4,14
16 r(e, x) ⊃ t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b))) ⊃ ¬t(x)
▲ Conclusion 3,15
17 s(x) ⊃ r(e, x) ⊃ t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b))) ⊃ ¬t(x)
▲ Conclusion 2,16
18 c(e) ⊃ s(x) ⊃ r(e, x) ⊃ t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b))) ⊃ ¬t(x)
▲ Conclusion 1,17
And woa, it works. This is the input, not yet very comfortable,
just copy paste it into the dialog box:
?- gentzen((c(e) -> (s(x) -> (r(e,x) -> (
(t(x) ->
all(a:A,(c(A) ->
all(b:B, (s(B) -> (r(A,B) -> (t(B)->f))))
)
) -> (t(x)->f)))))), N), !.
https://www.dogelog.ch/littab/doclet/docs/05_supplement/07_unicorn/example54/package.html
And this is the output, generated in a blink! I am currently
experimenting with a proof shortener. But I guess it cannot
be made shorter? Not sure. If I find something will post again.
I do not yet have a axiom mechanism. So the last 4 conclusions
are just premis collection. So I would say with axioms it would have
14 steps. DC Poop needs 16 steps, because of <=> unpacking.
18 c(e) ⊃ s(x) ⊃ r(e, x) ⊃ t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b))) ⊃ ¬t(x)
▶ Conclusion 1,17
If I unfold the proof I get:
1 c(e)
Premise
2 s(x)
Premise
3 r(e, x)
Premise
4 t(x)
Premise
5 ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b)))
Premise
6 t(x)
Premise
7 c(e) ⊃ ∀b:(s(b) ⊃ r(e, b) ⊃ ¬t(b))
U Spec 5
8 ∀b:(s(b) ⊃ r(e, b) ⊃ ¬t(b))
Detach 7,1
9 s(x) ⊃ r(e, x) ⊃ ¬t(x)
U Spec 8
10 r(e, x) ⊃ ¬t(x)
Detach 9,2
11 ¬t(x)
Detach 10,3
12 ⊥
Detach 11,6
13 ¬t(x)
▲ Conclusion 6,12
14 ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b))) ⊃ ¬t(x)
▲ Conclusion 5,13
15 t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b))) ⊃ ¬t(x)
▲ Conclusion 4,14
16 r(e, x) ⊃ t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b))) ⊃ ¬t(x)
▲ Conclusion 3,15
17 s(x) ⊃ r(e, x) ⊃ t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b))) ⊃ ¬t(x)
▲ Conclusion 2,16
18 c(e) ⊃ s(x) ⊃ r(e, x) ⊃ t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b))) ⊃ ¬t(x)
▲ Conclusion 1,17
Mostowski Collapse
Mar 29, 2023, 5:24:13 PM3/29/23
to
But there is something fishy with the output, it should place
parenthesis ( ... ) around t(x) ⊃ ... . Whats going wrong?
Ok, wrong input, this is the better input:
?- gentzen((c(e) -> (s(x) -> (r(e,x) -> (
(t(x) ->
all(a:A,(c(A) ->
all(b:B, (s(B) -> (r(A,B) -> (t(B)->f))))
)
)
) -> (t(x)->f))))), N), !.
And now an itch shorter proof, subtract 4 axioms, and its 13 lines!
But I have the feeling it can be shortened. Line 11 and line 13 show
the same thing? Nope, possibly no way to make it shorter, otherwise,
the premise on line 5 doesn't disappear.
17 c(e) ⊃ s(x) ⊃ r(e, x) ⊃ (t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b)))) ⊃ ¬t(x)
▶ Conclusion 1,16
-------------------------- begin proof ---------------------------------
1 c(e)
Premise
2 s(x)
Premise
3 r(e, x)
Premise
4 t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b)))
Premise
5 t(x)
Premise
6 ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b)))
Detach 4,5
7 c(e) ⊃ ∀b:(s(b) ⊃ r(e, b) ⊃ ¬t(b))
U Spec 6
8 ∀b:(s(b) ⊃ r(e, b) ⊃ ¬t(b))
Detach 7,1
9 s(x) ⊃ r(e, x) ⊃ ¬t(x)
U Spec 8
10 r(e, x) ⊃ ¬t(x)
Detach 9,2
11 ¬t(x)
Detach 10,3
12 ⊥
Detach 11,5
13 ¬t(x)
▲ Conclusion 5,12
14 (t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b)))) ⊃ ¬t(x)
▲ Conclusion 4,13
15 r(e, x) ⊃ (t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b)))) ⊃ ¬t(x)
▲ Conclusion 3,14
16 s(x) ⊃ r(e, x) ⊃ (t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b)))) ⊃ ¬t(x)
▲ Conclusion 2,15
17 c(e) ⊃ s(x) ⊃ r(e, x) ⊃ (t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b)))) ⊃ ¬t(x)
▲ Conclusion 1,16
-------------------------------------- end proof --------------------------------------------
parenthesis ( ... ) around t(x) ⊃ ... . Whats going wrong?
Ok, wrong input, this is the better input:
?- gentzen((c(e) -> (s(x) -> (r(e,x) -> (
(t(x) ->
all(a:A,(c(A) ->
all(b:B, (s(B) -> (r(A,B) -> (t(B)->f))))
)
)
And now an itch shorter proof, subtract 4 axioms, and its 13 lines!
But I have the feeling it can be shortened. Line 11 and line 13 show
the same thing? Nope, possibly no way to make it shorter, otherwise,
the premise on line 5 doesn't disappear.
17 c(e) ⊃ s(x) ⊃ r(e, x) ⊃ (t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b)))) ⊃ ¬t(x)
▶ Conclusion 1,16
-------------------------- begin proof ---------------------------------
1 c(e)
Premise
2 s(x)
Premise
3 r(e, x)
Premise
Premise
5 t(x)
Premise
6 ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b)))
Detach 4,5
7 c(e) ⊃ ∀b:(s(b) ⊃ r(e, b) ⊃ ¬t(b))
8 ∀b:(s(b) ⊃ r(e, b) ⊃ ¬t(b))
Detach 7,1
9 s(x) ⊃ r(e, x) ⊃ ¬t(x)
U Spec 8
10 r(e, x) ⊃ ¬t(x)
Detach 9,2
11 ¬t(x)
Detach 10,3
12 ⊥
13 ¬t(x)
▲ Conclusion 5,12
14 (t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b)))) ⊃ ¬t(x)
▲ Conclusion 4,13
15 r(e, x) ⊃ (t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b)))) ⊃ ¬t(x)
▲ Conclusion 3,14
16 s(x) ⊃ r(e, x) ⊃ (t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b)))) ⊃ ¬t(x)
▲ Conclusion 2,15
17 c(e) ⊃ s(x) ⊃ r(e, x) ⊃ (t(x) ⊃ ∀a:(c(a) ⊃ ∀b:(s(b) ⊃ r(a, b) ⊃ ¬t(b)))) ⊃ ¬t(x)
▲ Conclusion 1,16
-------------------------------------- end proof --------------------------------------------
Dan Christensen
Mar 30, 2023, 12:41:51 PM3/30/23
to
Taking another stab at it...
Epidmenides is a Cretan
1. Cretan(epi)
Axiom
Define: Statement x
2. Statement(x)
Axiom
3. True(x) <=> ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Axiom
Epimenides said statement x
4. Said(epi,x)
Axiom
Prove: ~True(x) (Statement x is not true)
Suppose to the contrary...
5. True(x)
Premise
Apply definition of statement x
6. [True(x) => ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]]
& [ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)] => True(x)]
Iff-And, 3
7. True(x) => ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Split, 6
8. ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Detach, 7, 5
9. ALL(b):[Cretan(epi) & Statement(b) & Said(epi,b) => ~True(b)]
U Spec, 8
10. Cretan(epi) & Statement(x) & Said(epi,x) => ~True(x)
U Spec, 9
11. Cretan(epi) & Statement(x)
Join, 1, 2
12. Cretan(epi) & Statement(x) & Said(epi,x)
Join, 11, 4
13. ~True(x)
Detach, 10, 12
14. True(x) & ~True(x)
Join, 5, 13
As Required: (By contradiction)
15. ~True(x)
4 Conclusion, 5
Apply definition of statement x
16. [True(x) => ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]]
& [ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)] => True(x)]
Iff-And, 3
17. True(x) => ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Split, 16
18. ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)] => True(x)
Split, 16
19. ~True(x) => ~ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Contra, 18
20. ~ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Detach, 19, 15
Changing quantifiers, etc....
21. ~~EXIST(a):~ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Quant, 20
22. EXIST(a):~ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Rem DNeg, 21
23. EXIST(a):~~EXIST(b):~[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Quant, 22
24. EXIST(a):EXIST(b):~[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Rem DNeg, 23
25. EXIST(a):EXIST(b):~~[Cretan(a) & Statement(b) & Said(a,b) & ~~True(b)]
Imply-And, 24
26. EXIST(a):EXIST(b):[Cretan(a) & Statement(b) & Said(a,b) & ~~True(b)]
Rem DNeg, 25
At least on Cretan once said a true statement.
27. EXIST(a):EXIST(b):[Cretan(a) & Statement(b) & Said(a,b) & True(b)]
Rem DNeg, 26
Joining results: Statement x must be false, and some Cretan once said a true statement.
28. ~True(x)
& EXIST(a):EXIST(b):[Cretan(a) & Statement(b) & Said(a,b) & True(b)]
Join, 15, 27
Epidmenides is a Cretan
1. Cretan(epi)
Axiom
Define: Statement x
2. Statement(x)
Axiom
3. True(x) <=> ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Axiom
Epimenides said statement x
4. Said(epi,x)
Axiom
Prove: ~True(x) (Statement x is not true)
Suppose to the contrary...
5. True(x)
Premise
Apply definition of statement x
6. [True(x) => ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]]
& [ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)] => True(x)]
Iff-And, 3
7. True(x) => ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Split, 6
8. ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Detach, 7, 5
9. ALL(b):[Cretan(epi) & Statement(b) & Said(epi,b) => ~True(b)]
U Spec, 8
10. Cretan(epi) & Statement(x) & Said(epi,x) => ~True(x)
U Spec, 9
11. Cretan(epi) & Statement(x)
Join, 1, 2
12. Cretan(epi) & Statement(x) & Said(epi,x)
Join, 11, 4
13. ~True(x)
Detach, 10, 12
14. True(x) & ~True(x)
Join, 5, 13
As Required: (By contradiction)
15. ~True(x)
4 Conclusion, 5
Apply definition of statement x
16. [True(x) => ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]]
& [ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)] => True(x)]
Iff-And, 3
17. True(x) => ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Split, 16
18. ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)] => True(x)
Split, 16
19. ~True(x) => ~ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Contra, 18
20. ~ALL(a):ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Detach, 19, 15
Changing quantifiers, etc....
21. ~~EXIST(a):~ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Quant, 20
22. EXIST(a):~ALL(b):[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Rem DNeg, 21
23. EXIST(a):~~EXIST(b):~[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Quant, 22
24. EXIST(a):EXIST(b):~[Cretan(a) & Statement(b) & Said(a,b) => ~True(b)]
Rem DNeg, 23
25. EXIST(a):EXIST(b):~~[Cretan(a) & Statement(b) & Said(a,b) & ~~True(b)]
Imply-And, 24
26. EXIST(a):EXIST(b):[Cretan(a) & Statement(b) & Said(a,b) & ~~True(b)]
Rem DNeg, 25
At least on Cretan once said a true statement.
27. EXIST(a):EXIST(b):[Cretan(a) & Statement(b) & Said(a,b) & True(b)]
Rem DNeg, 26
Joining results: Statement x must be false, and some Cretan once said a true statement.
28. ~True(x)
& EXIST(a):EXIST(b):[Cretan(a) & Statement(b) & Said(a,b) & True(b)]
Join, 15, 27
Mostowski Collapse
Mar 30, 2023, 4:31:48 PM3/30/23
to
Thanks again. Now you helped me spot a bug in my
prover. I saw this bug already before, but now I have a
better test case. Not sure whether its the proof search
or the proof display, but line 7 is abnormal. Lets see
whether Ι can analyse the problem better and deploy
a fix to the problem soon:
Input:
?- gentzen((cretan(epi) -> (statement(x) -> (said(epi,x) -> (
(true(x) ->
all(a:A,
all(b:B, (cretan(A) -> (statement(B) -> (said(A,B) -> (true(B)->f))))
)
)
) -> (true(x)->f))))), N), !.
https://www.dogelog.ch/littab/doclet/docs/05_supplement/07_unicorn/example54/package.html
Output:
1 cretan(epi)
Premise
2 statement(x)
Premise
3 said(epi, x)
Premise
4 true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))
Premise
5 true(x)
Premise
6 ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))
Detach 4,5
7 ∀b:(cretan(_28067) ⊃ statement(b) ⊃ said(_28067, b) ⊃ ¬true(b))
U Spec 6
8 cretan(epi) ⊃ statement(x) ⊃ said(epi, x) ⊃ ¬true(x)
U Spec 7
9 statement(x) ⊃ said(epi, x) ⊃ ¬true(x)
Detach 8,1
10 said(epi, x) ⊃ ¬true(x)
Detach 9,2
11 ¬true(x)
▲ Conclusion 5,12
14 (true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))) ⊃ ¬true(x)
▲ Conclusion 4,13
15 said(epi, x) ⊃ (true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))) ⊃ ¬true(x)
▲ Conclusion 3,14
16 statement(x) ⊃ said(epi, x) ⊃ (true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))) ⊃ ¬true(x)
▲ Conclusion 2,15
17 cretan(epi) ⊃ statement(x) ⊃ said(epi, x) ⊃ (true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))) ⊃ ¬true(x)
▲ Conclusion 1,16
prover. I saw this bug already before, but now I have a
better test case. Not sure whether its the proof search
or the proof display, but line 7 is abnormal. Lets see
whether Ι can analyse the problem better and deploy
a fix to the problem soon:
Input:
?- gentzen((cretan(epi) -> (statement(x) -> (said(epi,x) -> (
(true(x) ->
all(a:A,
all(b:B, (cretan(A) -> (statement(B) -> (said(A,B) -> (true(B)->f))))
)
)
) -> (true(x)->f))))), N), !.
https://www.dogelog.ch/littab/doclet/docs/05_supplement/07_unicorn/example54/package.html
Output:
1 cretan(epi)
Premise
2 statement(x)
Premise
3 said(epi, x)
Premise
4 true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))
Premise
5 true(x)
Premise
6 ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))
Detach 4,5
7 ∀b:(cretan(_28067) ⊃ statement(b) ⊃ said(_28067, b) ⊃ ¬true(b))
U Spec 6
8 cretan(epi) ⊃ statement(x) ⊃ said(epi, x) ⊃ ¬true(x)
U Spec 7
9 statement(x) ⊃ said(epi, x) ⊃ ¬true(x)
Detach 8,1
10 said(epi, x) ⊃ ¬true(x)
Detach 9,2
11 ¬true(x)
Detach 10,3
12 ⊥
Detach 11,5
13 ¬true(x)
12 ⊥
Detach 11,5
▲ Conclusion 5,12
14 (true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))) ⊃ ¬true(x)
▲ Conclusion 4,13
15 said(epi, x) ⊃ (true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))) ⊃ ¬true(x)
▲ Conclusion 3,14
16 statement(x) ⊃ said(epi, x) ⊃ (true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))) ⊃ ¬true(x)
▲ Conclusion 2,15
17 cretan(epi) ⊃ statement(x) ⊃ said(epi, x) ⊃ (true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))) ⊃ ¬true(x)
▲ Conclusion 1,16
Mostowski Collapse
Mar 30, 2023, 5:54:26 PM3/30/23
to
Ok the bug is gone! And the input is more comfy now,
might need browser reload, to get the new version:
Input:
?- gentzen(cretan(epi) ⊃ statement(x) ⊃ said(epi, x) ⊃
might need browser reload, to get the new version:
Input:
?- gentzen(cretan(epi) ⊃ statement(x) ⊃ said(epi, x) ⊃
(true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b)))
⊃ ¬true(x), N), !.
https://www.dogelog.ch/littab/doclet/docs/05_supplement/07_unicorn/example54/package.html
Output:
1 cretan(epi)
Premise
2 statement(x)
Premise
3 said(epi, x)
Premise
4 true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))
Premise
5 true(x)
Premise
6 ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))
Detach 4,5
7 ∀b:(cretan(epi) ⊃ statement(b) ⊃ said(epi, b) ⊃ ¬true(b))
Output:
1 cretan(epi)
Premise
2 statement(x)
Premise
3 said(epi, x)
Premise
4 true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))
Premise
5 true(x)
Premise
6 ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))
Detach 4,5
U Spec 6
8 cretan(epi) ⊃ statement(x) ⊃ said(epi, x) ⊃ ¬true(x)
U Spec 7
9 statement(x) ⊃ said(epi, x) ⊃ ¬true(x)
Detach 8,1
10 said(epi, x) ⊃ ¬true(x)
Detach 9,2
11 ¬true(x)
Detach 10,3
12 ⊥
Detach 11,5
13 ¬true(x)
▲ Conclusion 5,12
14 (true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))) ⊃ ¬true(x)
▲ Conclusion 4,13
15 said(epi, x) ⊃ (true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))) ⊃ ¬true(x)
▲ Conclusion 3,14
16 statement(x) ⊃ said(epi, x) ⊃ (true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))) ⊃ ¬true(x)
▲ Conclusion 2,15
17 cretan(epi) ⊃ statement(x) ⊃ said(epi, x) ⊃ (true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))) ⊃ ¬true(x)
▲ Conclusion 1,16
8 cretan(epi) ⊃ statement(x) ⊃ said(epi, x) ⊃ ¬true(x)
U Spec 7
9 statement(x) ⊃ said(epi, x) ⊃ ¬true(x)
Detach 8,1
10 said(epi, x) ⊃ ¬true(x)
Detach 9,2
11 ¬true(x)
Detach 10,3
12 ⊥
Detach 11,5
13 ¬true(x)
▲ Conclusion 5,12
14 (true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))) ⊃ ¬true(x)
▲ Conclusion 4,13
15 said(epi, x) ⊃ (true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))) ⊃ ¬true(x)
▲ Conclusion 3,14
16 statement(x) ⊃ said(epi, x) ⊃ (true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))) ⊃ ¬true(x)
▲ Conclusion 2,15
17 cretan(epi) ⊃ statement(x) ⊃ said(epi, x) ⊃ (true(x) ⊃ ∀a: ∀b:(cretan(a) ⊃ statement(b) ⊃ said(a, b) ⊃ ¬true(b))) ⊃ ¬true(x)
▲ Conclusion 1,16
olcott
Apr 24, 2023, 11:05:38 PM4/24/23
to
On 3/29/2023 9:41 AM, Dan Christensen wrote:
> Legend has it that the Cretan poet, Epimenides, once said that Cretans are "always liars." This narrative is often cited as an ancient paradox of logic. In fact, there is nothing "paradoxical" about it. It simply must be case that Epimenides himself was lying when he said this, and that at least one Cretan once told the truth.
>
> FORMAL PROOF: http://dcproof.com/LiarParadox2.htm (47 lines n DC Proof)
>
>
> FORMAL PROOF: http://dcproof.com/LiarParadox2.htm (47 lines n DC Proof)
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>
Epimenides [a Cretan] says that all Cretans are Liars.
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>
A barber [member of a town] says he shaves all [in this town] that do
not shave themselves.
E ∈ C asserts a property of C that negates the assertion
B ∈ T asserts a property of B that negates the assertion
Mild Shock
Aug 31, 2023, 6:12:00 PM8/31/23
to
There are serious doubts, it could be that an Olcott Fallacy is
involved. Of the form that one thinks that "if pigs can fly then
the moon is made of green cheese" implies that
"the moon s made of green cheese". But I could not yet produce
a proof that the axioms used by for example Dan Christensen
are inconsistent, and therefore its not really the case that
there is a cretan that says the truth. But the sketch is now:
I think Dan Christensen used something like:
(Pb ↔ ∀x¬Px) → ¬Pb is valid.
https://www.umsu.de/trees/#(Pb~4~6x~3Px)~5~3Pb
We can also write it like this, there is now a collection of b's
that satisfies Pb, and this collection is non-empty, this is what ∃xPx says.
(∃xPx ↔ ∀x¬Px) → ¬∃xPx is valid.
https://www.umsu.de/trees/#(~7xPx~4~6x~3Px)~5~3~7xPx
But the above is a vacous truth, since ∃xPx ↔ ∀x¬Px is
logically equivalent to ∃xPx ↔ ¬∃xPx which is an antinomy,
its just like the liar paradox Q ↔ ¬Q, namely we have:
¬(∃xPx ↔ ¬∃xPx) is valid.
https://www.umsu.de/trees/#~3(~7xPx~4~3~7xPx)
involved. Of the form that one thinks that "if pigs can fly then
the moon is made of green cheese" implies that
"the moon s made of green cheese". But I could not yet produce
a proof that the axioms used by for example Dan Christensen
are inconsistent, and therefore its not really the case that
there is a cretan that says the truth. But the sketch is now:
I think Dan Christensen used something like:
(Pb ↔ ∀x¬Px) → ¬Pb is valid.
https://www.umsu.de/trees/#(Pb~4~6x~3Px)~5~3Pb
We can also write it like this, there is now a collection of b's
that satisfies Pb, and this collection is non-empty, this is what ∃xPx says.
(∃xPx ↔ ∀x¬Px) → ¬∃xPx is valid.
https://www.umsu.de/trees/#(~7xPx~4~6x~3Px)~5~3~7xPx
But the above is a vacous truth, since ∃xPx ↔ ∀x¬Px is
logically equivalent to ∃xPx ↔ ¬∃xPx which is an antinomy,
its just like the liar paradox Q ↔ ¬Q, namely we have:
¬(∃xPx ↔ ¬∃xPx) is valid.
https://www.umsu.de/trees/#~3(~7xPx~4~3~7xPx)
Mild Shock
Sep 4, 2023, 3:31:21 PM9/4/23
to
Isn't Epimenides' Paradox the same as Yablos Paradox?
Possibly no, since in Yablos Paradox, there is a relationship
between many sentences x, and the negated sentences.
∀x(Q(x) ↔ ∀y(R(x,y) → ¬Q(y)))
https://en.wikipedia.org/wiki/Stephen_Yablo#Yablo's_paradox
Where in Epimenides' Paradox there is one sentence x
contra all of the other sentences. Can you do Yablos
Paradox in Coq? Like prove a contradiction from it,
or even refute it, show that it is an Antinomy? What domain
and relation R do we need to consider for an Antinomy?
Is this even possible, show it paradoxical resp. Antinomy?
Possibly no, since in Yablos Paradox, there is a relationship
between many sentences x, and the negated sentences.
∀x(Q(x) ↔ ∀y(R(x,y) → ¬Q(y)))
https://en.wikipedia.org/wiki/Stephen_Yablo#Yablo's_paradox
Where in Epimenides' Paradox there is one sentence x
contra all of the other sentences. Can you do Yablos
Paradox in Coq? Like prove a contradiction from it,
or even refute it, show that it is an Antinomy? What domain
and relation R do we need to consider for an Antinomy?
Is this even possible, show it paradoxical resp. Antinomy?
0 new messages