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.