liar_paradox : THEORY

BEGIN

Person : TYPE

Says : [Person,bool -> bool]

Liar : [Person -> bool] =
       (LAMBDA (a:Person):
               (FORALL (x:bool):(Says(a,x) IMPLIES (NOT x))))

TruthTeller : [Person -> bool] =
              (LAMBDA (a:Person):
                      (FORALL (x:bool):(Says(a,x) IMPLIES x)))

LoT : AXIOM
      (FORALL (a:Person):Liar(a) OR TruthTeller(a))

l:Person

lie : AXIOM
      (Says(l,Liar(l)))

contradiction : THEOREM
                FALSE

END liar_paradox