# Can boolean algebra be expressed in simply typed lambda caclulus?

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.

• Try typing the definitions into Haskell and see what happens when you give types to various expressions. You'll see that the code relies heavily on polymorphism. – Dave Clarke Feb 6 '12 at 12:30
• Sorry to be pedantic, but questions about the expressivity of this or that calculus become meaninful only with a clear understanding of what you mean by "expressed", "encoded" and "represented", as there are multiple reasonable ways of understanding these terms. Moreover, since you stipulate the existence of base-types, you'd need to be specific about what those are, and what constructors/destructors they come with. – Martin Berger Feb 6 '12 at 12:48
• Sorry that I was not pedantic. The answer was found here: math.andrej.com/2009/03/21/… – Ilya Klyuchnikov Feb 6 '12 at 13:41
• I feel like I should get some credit for running such a nifty blog :-) – Andrej Bauer Feb 6 '12 at 13:51
• The definition of a Boolean type used on the blog is stronger than here. In fact, Jeremy’s answer shows that simply typed lambda calculus with at least one base type (call it $O$) can express Boolean algebra in the sense of the OP: define $B=O\to O\to O$, $\mathrm{true}=\lambda x:O.\lambda y:O.x$, $\mathrm{false}=\lambda x:O.\lambda y:O.y$, $\mathrm{not}=\lambda a:B.\lambda x:O.\lambda y:O.ayx$, $\mathrm{and}=\lambda a:B.\lambda b:B.\lambda x:O.\lambda y:O.a(bxy)y$, $\mathrm{or}=\lambda a:B.\lambda b:B.\lambda x:O.\lambda y:O.ax(bxy)$. – Emil Jeřábek Feb 7 '12 at 12:59