Heyting algebra

A bounded distributive lattice with an implication operation that assigns the greatest element whose meet with a given element lies below another. Heyting algebras provide algebraic semantics for intuitionistic logic.

Partially ordered set: A set equipped with a reflexive, antisymmetric, transitive relation. The lattice order supplies the comparison used to define Heyting implication.
Heyting implication: The greatest element x such that x meet a is below b, for fixed elements a and b. This operation is the distinctive addition to a bounded distributive lattice.
Intuitionistic logic: A logic that does not assume the law of excluded middle for every proposition. Heyting algebras interpret its connectives while preserving intuitionistic validity.
Pseudo-Boolean algebra: A Boolean algebra equipped with operations for finite-valued logical reasoning. Despite its name, it is not the general lattice semantics of intuitionistic logic.
Arend Heyting: A Dutch mathematician and logician who formalized intuitionistic logic in the early twentieth century. His name became attached to the algebraic structures that model intuitionistic logic.
Lattice (order): A partially ordered set in which every pair of elements has a meet and a join. A Heyting algebra adds bounds, distributivity, and implication to this structure.
Adjunction (order theory): A pair of order-preserving maps related by an equivalence between their order inequalities. Heyting implication is right adjoint to meeting with a fixed element.
Propositional calculus: A formal system whose formulas are built from propositional variables and logical connectives. Heyting algebra semantics gives an algebraic account of intuitionistic propositional formulas.
Orthomodular lattice: A lattice structure used to model propositions in quantum logic. It replaces distributive lattice behavior with a structure suited to quantum propositions.
Intuitionism: A philosophy of mathematics holding that mathematical truth depends on constructive proof. Its rejection of unrestricted excluded middle motivated the logic represented by Heyting algebras.

Linked from 8 pages