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.

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

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

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