t

# Heyting 

### Companion object Heyting

#### trait Heyting[A] extends BoundedDistributiveLattice[A]

Heyting algebras are bounded lattices that are also equipped with an additional binary operation `imp` (for implication, also written as →).

Implication obeys the following laws:

• a → a = 1
• a ∧ (a → b) = a ∧ b
• b ∧ (a → b) = b
• a → (b ∧ c) = (a → b) ∧ (a → c)

In heyting algebras, `and` is equivalent to `meet` and `or` is equivalent to `join`; both methods are available.

Heyting algebra also define `complement` operation (sometimes written as ¬a). The complement of `a` is equivalent to `(a → 0)`, and the following laws hold:

• a ∧ ¬a = 0

However, in Heyting algebras this operation is only a pseudo-complement, since Heyting algebras do not necessarily provide the law of the excluded middle. This means that there is no guarantee that (a ∨ ¬a) = 1.

Heyting algebras model intuitionistic logic. For a model of classical logic, see the boolean algebra type class implemented as `Bool`.

Self Type
Heyting[A]
Source
Heyting.scala
Known Subclasses
Ordering
1. Alphabetic
2. By Inheritance
Inherited
1. Heyting
2. BoundedDistributiveLattice
3. DistributiveLattice
4. BoundedLattice
5. BoundedJoinSemilattice
6. BoundedMeetSemilattice
7. Lattice
8. MeetSemilattice
9. JoinSemilattice
10. Serializable
11. Serializable
12. Any
1. Hide All
2. Show All
Visibility
1. Public
2. All

### Abstract Value Members

1. abstract def and(a: A, b: A): A
2. abstract def complement(a: A): A
3. abstract def getClass(): Class[_]
Definition Classes
Any
4. abstract def imp(a: A, b: A): A
5. abstract def one: A
Definition Classes
BoundedMeetSemilattice
6. abstract def or(a: A, b: A): A
7. abstract def zero: A
Definition Classes
BoundedJoinSemilattice

### Concrete Value Members

1. final def !=(arg0: Any)
Definition Classes
Any
2. final def ##(): Int
Definition Classes
Any
3. final def ==(arg0: Any)
Definition Classes
Any
4. def asCommutativeRig: CommutativeRig[A]

Return a CommutativeRig using join and meet.

Return a CommutativeRig using join and meet. Note this must obey the commutative rig laws since meet(a, one) = a, and meet and join are associative, commutative and distributive.

Definition Classes
BoundedDistributiveLattice
5. final def asInstanceOf[T0]: T0
Definition Classes
Any
6. def dual

This is the lattice with meet and join swapped

This is the lattice with meet and join swapped

Definition Classes
BoundedDistributiveLatticeBoundedLatticeLattice
7. def equals(arg0: Any)
Definition Classes
Any
8. def hashCode(): Int
Definition Classes
Any
9. final def isInstanceOf[T0]
Definition Classes
Any
10. def isOne(a: A)(implicit ev: Eq[A])
Definition Classes
BoundedMeetSemilattice
11. def isZero(a: A)(implicit ev: Eq[A])
Definition Classes
BoundedJoinSemilattice
12. def join(a: A, b: A): A
Definition Classes
HeytingJoinSemilattice
13. def joinPartialOrder(implicit ev: Eq[A]): PartialOrder[A]
Definition Classes
JoinSemilattice
14. def joinSemilattice
15. def meet(a: A, b: A): A
Definition Classes
HeytingMeetSemilattice
16. def meetPartialOrder(implicit ev: Eq[A]): PartialOrder[A]
Definition Classes
MeetSemilattice
17. def meetSemilattice
18. def nand(a: A, b: A): A
19. def nor(a: A, b: A): A
20. def nxor(a: A, b: A): A
21. def toString(): String
Definition Classes
Any
22. def xor(a: A, b: A): A