Boolean algebra can be expressed in untyped lambda calculus in (for example) this way.true  = \t. \f. t;false = \t. \f. t;not   = \x. x false true;and   = \x. \y. x y false;or    = \x. \y. x true y;Also boolean algebra can be encoded in System F in this way:CBool = All X.X -> X -> X;true  = \X. \t:X. \f:X. t;false = \X. \t:X. \f:X. f;not   = \x:CBool. x [CBool] false true;and   = \x:CBool. \y:CBool. x [CBool] y false;or    = \x:CBool. \y:CBool. x [CBool] true y;Is there a way to express boolean algebra in simply typed lambda calculus? I assume that answer is NO. (For example, Predecessor and lists are not representable in simply typed lambda-calculus.) If the answer is NO indeed, is there a simple intuitive explanation, why it is impossible to encode booleans in simply typed lambda calculus?UPDATE: We assume that there are base types.UPDATE: The negative answer with explanation was found here (Comment Here's a proof sketch to show that simply-typed lambda calculus with products and infinitely many base types does not have booleans.) This is what I was looking for.
Can boolean algebra be expressed in simply typed lambda caclulus?
lo.logic;type theory;lambda calculus