The Cretan Liar Paradox: A Formal Resolution in First-Order Logic

-----------------------------------------------------------------

 

An original proof by Dan Christensen

 

This proof written with the aid of DC Proof 2.0 software.

Download it at http://www.dcproof.com

 

 

Informal Introduction

---------------------

 

(Note: Informal commentary is shown here in a blue font.)

 

The famous Cretan poet, Epimenides (circa 600 BC), wrote that Cretans are "always liars"  Paradoxically, if he was telling the truth, then, as a Cretan himself, everything he said would be a lie. If he was lying, he would only be confirming that he was telling the truth in the first place! Not exactly.

 

Here we will show, using only first-order logic, that if this narrative is to be logically consistent (i.e. free of any contradictions) then Epimenides must have been lying and, contrary to his claim, at least one Cretan once spoke the truth.

 

It is, of course, possible to construct an inconsistent narrative (e.g. one in which Epimenides' claim is supposed to be true), but then absolutely anything would go. It would logically follow, for example, that the moon is made of green cheese! It isn't, but that is another story.

 

Here, we define the following logical predicates:

 

C(a) means 'a' is a Cretan 

S(a) means 'a' is a statement           

T(a) means statement 'a' is true   

R(a,b) means person 'a' reports statement 'b'  

 

We define the following constants:

 

e  stands for Epimenides

x  stands for Epimenides' claim (as formally defined in Axiom 4)

 

Outline

-------

 

We list 4 axioms.

 

Part 1: From these axioms, we formally prove that Epimenides' claim was false:

 

        ~T(x)

 

Part 2: We then formally prove that at least one Cretan, on at least one occasion, spoke the truth:

 

        EXIST(a):EXIST(b):[C(a) & S(b) & ~b=x & R(a,b) & T(b)]

 

 

Axiom 1: Epimenides is a Cretan

 

1     C(e)

      Axiom

 

Axiom 2: x is a statement

 

2     S(x)

      Axiom

 

Axiom 3: Epimenides reported statement x

 

3     R(e,x)

      Axiom

 

Axiom 4: Statement x is true iff Cretans are always liars

 

Informally, we can say that x represents the statement "Cretans are always liars." The two expressions are not strictly interchangeable, however. Here, we use the predicate T to formally associate the constant x (on the LHS of the biconditional) with the logical expression on the RHS.

 

4     T(x) <=> ALL(a):[C(a) => ALL(b):[S(b) => [R(a,b) => ~T(b)]]]

      Axiom

 

Splitting up this biconditional...

 

5     [T(x) => ALL(a):[C(a) => ALL(b):[S(b) => [R(a,b) => ~T(b)]]]]

     & [ALL(a):[C(a) => ALL(b):[S(b) => [R(a,b) => ~T(b)]]] => T(x)]

      Iff-And, 4

 

6     T(x) => ALL(a):[C(a) => ALL(b):[S(b) => [R(a,b) => ~T(b)]]]

      Split, 5

 

7     ALL(a):[C(a) => ALL(b):[S(b) => [R(a,b) => ~T(b)]]] => T(x)

      Split, 5

 

    

     Proof: Part 1

     -------------    

 

     Show that Epimenides' claim was false.

 

     Prove: ~T(x)

    

     Suppose to contrary...

 

      8     T(x)

            Premise

 

     Apply Axiom 4

 

      9     ALL(a):[C(a) => ALL(b):[S(b) => [R(a,b) => ~T(b)]]]

            Detach, 6, 8

 

      10    C(e) => ALL(b):[S(b) => [R(e,b) => ~T(b)]]

            U Spec, 9

 

     Apply Axiom 1

 

      11    ALL(b):[S(b) => [R(e,b) => ~T(b)]]

            Detach, 10, 1

 

      12    S(x) => [R(e,x) => ~T(x)]

            U Spec, 11

 

     Apply Axiom 2

 

      13    R(e,x) => ~T(x)

            Detach, 12, 2

 

     Apply Axiom 3

 

      14    ~T(x)

            Detach, 13, 3

 

     Obtain the contradiction...

 

      15    T(x) & ~T(x)

            Join, 8, 14

 

 

Epimenides' claim was false.

 

As Required:

 

16    ~T(x)

      4 Conclusion, 8

 

 

Proof: Part 2

-------------

 

Show that at least one Cretan once spoke the truth.

 

Prove: EXIST(a):EXIST(b):[C(a) & S(b) & ~b=x & R(a,b) & T(b)]

 

Apply Axiom 4

 

17    ~T(x) => ~ALL(a):[C(a) => ALL(b):[S(b) => [R(a,b) => ~T(b)]]]

      Contra, 7

 

Apply previous result

 

18    ~ALL(a):[C(a) => ALL(b):[S(b) => [R(a,b) => ~T(b)]]]

      Detach, 17, 16

 

Change quantifiers, change => to & and remove ~~

 

19    ~~EXIST(a):~[C(a) => ALL(b):[S(b) => [R(a,b) => ~T(b)]]]

      Quant, 18

 

20    EXIST(a):~[C(a) => ALL(b):[S(b) => [R(a,b) => ~T(b)]]]

      Rem DNeg, 19

 

21    EXIST(a):~~[C(a) & ~ALL(b):[S(b) => [R(a,b) => ~T(b)]]]

      Imply-And, 20

 

22    EXIST(a):[C(a) & ~ALL(b):[S(b) => [R(a,b) => ~T(b)]]]

      Rem DNeg, 21

 

23    EXIST(a):[C(a) & ~~EXIST(b):~[S(b) => [R(a,b) => ~T(b)]]]

      Quant, 22

 

24    EXIST(a):[C(a) & EXIST(b):~[S(b) => [R(a,b) => ~T(b)]]]

      Rem DNeg, 23

 

25    EXIST(a):[C(a) & EXIST(b):~~[S(b) & ~[R(a,b) => ~T(b)]]]

      Imply-And, 24

 

26    EXIST(a):[C(a) & EXIST(b):[S(b) & ~[R(a,b) => ~T(b)]]]

      Rem DNeg, 25

 

27    EXIST(a):[C(a) & EXIST(b):[S(b) & ~~[R(a,b) & ~~T(b)]]]

      Imply-And, 26

 

28    EXIST(a):[C(a) & EXIST(b):[S(b) & [R(a,b) & ~~T(b)]]]

      Rem DNeg, 27

 

29    EXIST(a):[C(a) & EXIST(b):[S(b) & [R(a,b) & T(b)]]]

      Rem DNeg, 28

 

Apply Existential Specification (introduce y and z)

 

30    C(y) & EXIST(b):[S(b) & [R(y,b) & T(b)]]

      E Spec, 29

 

31    C(y)

      Split, 30

 

32    EXIST(b):[S(b) & [R(y,b) & T(b)]]

      Split, 30

 

33    S(z) & [R(y,z) & T(z)]

      E Spec, 32

 

34    S(z)

      Split, 33

 

35    R(y,z) & T(z)

      Split, 33

 

36    R(y,z)

      Split, 35

 

37    T(z)

      Split, 35

 

    

     Prove: ~z=x

    

     Suppose to the contrary...

 

      38    z=x

            Premise

 

     Apply premise

 

      39    T(x)

            Substitute, 38, 37

 

     Obtain the contradiction...

 

      40    T(x) & ~T(x)

            Join, 39, 16

 

As Required:

 

41    ~z=x

      4 Conclusion, 38

 

Join results

 

42    C(y) & S(z)

      Join, 31, 34

 

43    C(y) & S(z) & ~z=x

      Join, 42, 41

 

44    C(y) & S(z) & ~z=x & R(y,z)

      Join, 43, 36

 

45    C(y) & S(z) & ~z=x & R(y,z) & T(z)

      Join, 44, 37

 

Apply Existential Generalization

 

46    EXIST(b):[C(y) & S(b) & ~b=x & R(y,b) & T(b)]

      E Gen, 45

 

 

At least one Cretan once spoke the truth.

 

As Required:

 

47    EXIST(a):EXIST(b):[C(a) & S(b) & ~b=x & R(a,b) & T(b)]

      E Gen, 46