<p>The Emil Jeřábek's comment in <a href="https://cstheory.stackexchange.com/q/10085">Can boolean algebra be expressed in simply typed lambda caclulus?</a> give rise to the following question:</p>

<p>Can some non-trivial Heyting algebra be expressed in simply typed lambda calculus?</p>

<p>Consider, for example, the simplest Heyting algebra that is not already a Boolean algebra, that's the totally ordered set $\{0, \frac 12, 1\}$ described <a href="https://en.wikipedia.org/wiki/Heyting_algebra" rel="nofollow noreferrer">here</a>.</p>

<p>More generally, I ask if is possible to build a type $H$ togheter with two terms $\mathrm{true},\mathrm{false}:H$ and functions $\wedge, \vee, \Rightarrow, \neg:H\to H$ satisfying the inference usual rules for intuitionistic logic, exception for the excluded middle.</p>

CC BY-SA 3.0
2016-04-27T10:48:38.537Z
The previous question was about representation of the *specific* 2-element Boolean algebra, not the variety of Boolean algebras. So: *which* Heyting algebra? And what are the conditions that you want the expression to satisfy?
Emil Jeřábek
CC BY-SA 3.0
2016-04-27T13:35:37.620Z
After the edit: yes, the 2-element Boplean algebra, which is also a Heyting algebra.
Emil Jeřábek
<typed-lambda-calculus>
Heyting algebra in simply typed lambda calculus
Fabio Lucchini
# Heyting algebra in simply typed lambda calculus

(Asked by: username_0 on 2016-04-26)

The username_1's comment in [Can boolean algebra be expressed in simply typed lambda caclulus?](https://cstheory.stackexchange.com/q/10085) give rise to the following question:

Can some non-trivial Heyting algebra be expressed in simply typed lambda calculus?

Consider, for example, the simplest Heyting algebra that is not already a Boolean algebra, that's the totally ordered set $\{0, \frac 12, 1\}$ described [here](https://en.wikipedia.org/wiki/Heyting_algebra).

More generally, I ask if is possible to build a type $H$ togheter with two terms $\mathrm{true},\mathrm{false}:H$ and functions $\wedge, \vee, \Rightarrow, \neg:H\to H$ satisfying the inference usual rules for intuitionistic logic, exception for the excluded middle.

**Tags:** typed-lambda-calculus

> **Comments:**
> **username_1**: The previous question was about representation of the *specific* 2-element Boolean algebra, not the variety of Boolean algebras. So: *which* Heyting algebra? And what are the conditions that you want the expression to satisfy?  
> **username_1**: After the edit: yes, the 2-element Boplean algebra, which is also a Heyting algebra.  

---

## 0 answers

