The Emil Jeřábek's comment in Can boolean algebra be expressed in simply typed lambda caclulus? 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.

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.

  • 5
    $\begingroup$ 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? $\endgroup$ – Emil Jeřábek Apr 27 '16 at 10:48
  • $\begingroup$ After the edit: yes, the 2-element Boplean algebra, which is also a Heyting algebra. $\endgroup$ – Emil Jeřábek Apr 27 '16 at 13:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.