RESOLUTION OF EPIMENIDES' PARADOX

*********************************

 

The Cretan poet Epimenidies, once wrote, "Cretans (are) always liars."

 

Assuming this claim is true leads to a contradiction (lines 6-16). Therefore, it cannot be true.

 

We make use the following predicates:

 

Stmt(x) = x is a statement

True(x) = x is true

Cretan(x) = x is a Cretan

Said(x,y) = x said statement y

 

Constants:

 

epi = Epimenides

x = the statement that "Cretans always lie"

 

 

Dan Christensen

http://www.dcproof.com

2023-04-17

 

 

AXIOMS

******

 

Define: x  (Epimenides' claim)

 

1     Stmt(x)

      Axiom

 

2     ALL(a):[True(a) => Stmt(a)]

      Axiom

 

3     True(x) <=> ALL(a):ALL(b):[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)]

      Axiom

 

 

Define: epi  (Epimenides)

 

4     Cretan(epi)

      Axiom

 

5     Said(epi,x)

      Axiom

 

   

    Prove: ~True(x) (i.e. that x is not true)

   

    Suppose to the contrary...

 

      6     True(x)

            Premise

 

    Apply the definition of x to obtain a contradiction

 

      7     [True(x) => ALL(a):ALL(b):[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)]]

         & [ALL(a):ALL(b):[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)] => True(x)]

            Iff-And, 3

 

      8     True(x) => ALL(a):ALL(b):[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)]

            Split, 7

 

      9     ALL(a):ALL(b):[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)]

            Detach, 8, 6

 

      10   ALL(b):[Cretan(epi) & Stmt(b) & Said(epi,b) => ~True(b)]

            U Spec, 9

 

      11   Cretan(epi) & Stmt(x) & Said(epi,x) => ~True(x)

            U Spec, 10

 

      12   Cretan(epi) & Stmt(x)

            Join, 4, 1

 

      13   Cretan(epi) & Stmt(x) & Said(epi,x)

            Join, 12, 5

 

      14   ~True(x)

            Detach, 11, 13

 

      15   True(x) & ~True(x)

            Join, 6, 14

 

By contradiction, Epimenides's claim (x) is not true.

 

As Required:

 

16   ~True(x)

      4 Conclusion, 6

 

 

Apply definition of True(x)

 

17   [True(x) => ALL(a):ALL(b):[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)]]

    & [ALL(a):ALL(b):[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)] => True(x)]

      Iff-And, 3

 

18   ALL(a):ALL(b):[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)] => True(x)

      Split, 17

 

19   ~True(x) => ~ALL(a):ALL(b):[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)]

      Contra, 18

 

20   ~ALL(a):ALL(b):[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)]

      Detach, 19, 16

 

21   ~~EXIST(a):~ALL(b):[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)]

      Quant, 20

 

22   EXIST(a):~ALL(b):[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)]

      Rem DNeg, 21

 

23   EXIST(a):~~EXIST(b):~[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)]

      Quant, 22

 

24   EXIST(a):EXIST(b):~[Cretan(a) & Stmt(b) & Said(a,b) => ~True(b)]

      Rem DNeg, 23

 

25   EXIST(a):EXIST(b):~~[Cretan(a) & Stmt(b) & Said(a,b) & ~~True(b)]

      Imply-And, 24

 

26   EXIST(a):EXIST(b):[Cretan(a) & Stmt(b) & Said(a,b) & ~~True(b)]

      Rem DNeg, 25

 

 

Contrary to Epimenides' claim, at least one Cretan must have once said the truth.

 

As Required:

 

27   EXIST(a):EXIST(b):[Cretan(a) & Stmt(b) & Said(a,b) & True(b)]

      Rem DNeg, 26