val TRUE = fn x => fn y => x; val FALSE = fn x => fn y => y; val IF = fn c => fn e1 => fn e2 => ((c e1) e2); val AND = fn x => fn y => (((IF x) y) FALSE); val OR = fn x => fn y => (((IF x) TRUE) y); val NOT = fn x => (((IF x) FALSE) TRUE); (* (not true) => (Lx.(((IF x) false) true) true) => (((IF true) false) true) => (((Lc.Le1.Le2.((c e1) e2) true) false) true) => ((Le1.Le2.((true e1) e2) false) true) => (Le2.((true false) e2) true) => ((true false) true) => ((Lx.Ly.x false) true) => (Ly.false true) => false => Lx.Ly.y *) (* Implication is defined as follows: X Y X implies Y ----- ----- ----------- false false true false true true true false false true true true Write a lambda function implies = Lx.Ly. *) val implies = fn x => fn y => (NOT ((AND x) (NOT y))); (* The above is possible given the definitions of TRUE, FALSE, AND, OR, NOT, and IF. This allows all of propositional logic. *)