Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

## Synopsis

- class BoundedLattice a => HeytingAlgebra a where
- implies :: HeytingAlgebra a => a -> a -> a
- (<=>) :: HeytingAlgebra a => a -> a -> a
- iff :: HeytingAlgebra a => a -> a -> a
- iff' :: (Eq a, HeytingAlgebra a) => a -> a -> Bool
- toBoolean :: HeytingAlgebra a => a -> a
- class HeytingAlgebra a => BooleanAlgebra a

# Heyting algebras

class BoundedLattice a => HeytingAlgebra a where Source #

Heyting algebra is a bounded semi-lattice with implication which should satisfy the following law:

x ∧ a ≤ b ⇔ x ≤ (a ⇒ b)

We also require that a Heyting algebra is a distributive lattice, which means any of the two equivalent conditions holds:

a ∧ (b ∨ c) = a ∧ b ∨ a ∧ c

a ∨ (b ∧ c) = (a ∨ b) ∧ (a ∨ c)

This means `a ⇒ b`

is an
exponential object,
which makes any Heyting algebra
a cartesian
closed category.
This means that Curry isomorphism holds (which takes a form of an actual
equality):

a ⇒ (b ⇒ c) = (a ∧ b) ⇒ c

Some other useful properties of Heyting algebras:

(a ⇒ b) ∧ a ≤ b

b ≤ a ⇒ a ∧ b

a ≤ b iff a ⇒ b = ⊤

b ≤ b' then a ⇒ b ≤ a ⇒ b'

a'≤ a then a' ⇒ b ≤ a ⇒ b

not (a ∧ b) = not (a ∨ b)

not (a ∨ b) = not a ∧ not b

(==>) :: a -> a -> a infixr 4 Source #

Default implementation: `a ==> b = not a / b`

, it requires `not`

to
satisfy Boolean axioms, which will make it into a Boolean algebra.

## Instances

(<=>) :: HeytingAlgebra a => a -> a -> a Source #

toBoolean :: HeytingAlgebra a => a -> a Source #

Every Heyting algebra contains a Boolean algebra.

maps onto it;
moreover it is a monad (Heyting algebra is a category as every poset is) which
preserves finite infima.`toBoolean`

# Boolean algebras

class HeytingAlgebra a => BooleanAlgebra a Source #

Boolean algebra is a Heyting algebra which negation satisfies the law of excluded middle, i.e. either of the following:

not . not == not

or

x ∨ not x == top

Another characterisation of Boolean algebras is as complemented distributive lattices where the complement satisfies the following three properties:

(not a) ∧ a == bottom and (not a) ∨ a == top -- excluded middle law

not (not a) == a -- involution law

a ≤ b ⇒ not b ≤ not a -- order-reversing