<p>The OP wrote above that the question is answered by <a href="http://math.andrej.com/2009/03/21/how-to-simulate-booleans-in-simply-typed-lambda-calculus/" rel="nofollow noreferrer">a post on @AndrejBauer's blog</a>.</p>

CC BY-SA 4.0
2018-09-24T06:03:29.860Z
2018-09-24T06:03:29.860Z
Bjørn Kjos-Hanssen
<p><a href="http://en.wikipedia.org/wiki/Church_encoding">Boolean algebra can be expressed in untyped lambda calculus</a> in (for example) this way.</p>

<pre><code>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;
</code></pre>

<p>Also boolean algebra can be encoded in System F in <a href="http://en.wikipedia.org/wiki/System_F#Logic_and_predicates">this way</a>:</p>

<pre><code>CBool = All X.X -&gt; X -&gt; 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;
</code></pre>

<p>Is there a way to express boolean algebra in simply typed lambda calculus? I assume that answer is NO. (<a href="http://okmij.org/ftp/Computation/lambda-calc.html#predecessor">For example, Predecessor and lists are not representable in simply typed lambda-calculus</a>.) If the answer is NO indeed, is there a simple intuitive explanation, why it is impossible to encode booleans in simply typed lambda calculus?</p>

<p>UPDATE: We assume that there are base types.</p>

<p>UPDATE: The negative answer with explanation was found <a href="http://math.andrej.com/2009/03/21/how-to-simulate-booleans-in-simply-typed-lambda-calculus/">here</a> (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.</p>

CC BY-SA 3.0
2012-02-06T12:30:10.887Z
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
CC BY-SA 3.0
2012-02-06T12:48:24.067Z
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
CC BY-SA 3.0
2012-02-06T13:41:08.790Z
Sorry that I was not pedantic. The answer was found here: http://math.andrej.com/2009/03/21/how-to-simulate-booleans-in-simply-typed-lambda-calculus/
Ilya Klyuchnikov
CC BY-SA 3.0
2012-02-06T13:51:46.510Z
I feel like I should get some credit for running such a nifty blog :-)
Andrej Bauer
CC BY-SA 3.0
2012-02-07T12:59:10.697Z
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
<lo.logic><type-theory><lambda-calculus>
Can boolean algebra be expressed in simply typed lambda caclulus?
Ilya Klyuchnikov
# Can boolean algebra be expressed in simply typed lambda caclulus?

(Asked by: username_0 on 2012-02-06)

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.

**Tags:** lo.logic, type-theory, lambda-calculus

> **Comments:**
> **username_1**: 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.  
> **username_2**: 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.  
> **username_0**: Sorry that I was not pedantic. The answer was found here: http://math.andrej.com/2009/03/21/how-to-simulate-booleans-in-simply-typed-lambda-calculus/  
> **username_3**: I feel like I should get some credit for running such a nifty blog :-)  
> **username_4**: 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)$.  

---

## 1 answers

### Answer by username_5 on 2018-09-24. Score: 3

The OP wrote above that the question is answered by [a post on @AndrejBauer's blog](http://math.andrej.com/2009/03/21/how-to-simulate-booleans-in-simply-typed-lambda-calculus/).


---

