one of our basic combinators: T = K Kxy = x The second is also fairly simple: F = SK SKxy = Ky(xy) = y Once true and false are defined, all Boolean logic can be implemented in terms of if-then-else structures. Boolean NOT (which returns the opposite of a given Boolean) works the same as the if-then-else structure, with F and T as the second and third values, so it can be implemented as a postfix operation: NOT = (F)(T) = (SK)(K) If this is put in an if-then-else structure, it can be shown that this has the expected result (T)NOT = T(F)(T) = F (F)NOT = F(F)(T) = T Boolean OR (which returns T if either of the two Boolean values surrounding it is T) works the same as an if-then-else structure with T as the second value, so it can be implemented as an infix operation: OR = T = K If this is put in an if-then-else structure, it can be shown that this has the expected result: (T)OR(T) = T(T)(T) = T (T)OR(F) = T(T)(F) = T (F)OR(T) = F(T)(T) = T (F)OR(F) = F(T)(F) = F Boolean AND (which returns T if both of the two Boolean values surrounding it are T) works the same as an if-then-else structure with F as the third value, so it can be implemented as a postfix operation: AND = F = SK If this is put in an if-then-else structure, it can be shown that this has the expected result: (T)(T)AND = T(T)(F) = T (T)(F)AND = T(F)(F) = F (F)(T)AND = F(T)(F) = F (F)(F)AND = F(F)(F) = F Because this defines T, F, NOT (as a postfix operator), OR (as an infix operator), and AND (as a postfix operator) in terms of SKI notation, this proves that the SKI system can fully express Boolean logic. As the SKI calculus is complete, it is also possible to express NOT, OR and AND as prefix operators: NOT = S(SI(KF))(KT) (as S(SI(KF))(KT)x = SI(KF)x(KTx) = Ix(KFx)T = xFT) OR = SI(KT) (as SI(KT)xy = Ix(KTx)y = xTy) AND = SS(K(KF)) (as SS(K(KF))xy = Sx(K(KF)x)y = xy(KFy) = xyF) Connection to intuitionistic logic The combinators K and S correspond to two well-known axioms of sentential logic: , . Function application corresponds to the rule modus ponens: : from and , infer . The axioms AK and AS, and the