Heyting algebra Guide, Meaning , Facts, Information and Description
In mathematics, Heyting algebras are special partially ordered sets that constitute a generalization of Boolean algebras. Heyting algebras arise as models of intuitionistic logic, a logic in which the law of excluded middle does not in general hold. Complete Heyting algebras are a central object of study in pointless topology.
| Table of contents |
|
2 Properties 3 Examples 4 Heyting algebras as applied to intuitionistic logic 5 See also 6 References |
A Heyting algebra H is a bounded lattice such that for all a and b in H there is a greatest element x of H such that
.
This element is called the relative pseudo-complement of a with respect to b, and is denoted (or ).
An equivalent definition can be given by considering the mappings
Formal definitions
defined by , for some fixed a in H. A bounded lattice H is a Heyting algebra iff all mappings are the lower adjoint of a monotone Galois connection. In this case the respective upper adjoints are given by , where is defined as above.
A complete Heyting algebra is a Heyting algebra that is a complete lattice.
In any Heyting algebra, one can define the pseudo-complement of some element x by setting , where 0 is the least element of the Heyting algebra.
An element x of a Heyting algebra is called regular if . An element x is regular if and only if for some element y of the Heyting algebra.
Heyting algebras are always distributive. This is sometimes stated as an axiom, but in fact it follows from the existence of relative pseudo-complements. The reason is that, being the lower adjoint of a Galois connection, preserves all existing suprema. Distributivity in turn is just the preservation of binary suprema by .
Furthermore, by a similar argument, the following infinite distributive law holds in any complete Heyting algebra:
for any element x in H and any subset Y of H.
Not every Heyting algebra satisfies the two De Morgan laws. However, the following statements are equivalent for all Heyting algebras H:
The regular elements of any Heyting algebra constitute a Boolean algebra.
Unless all elements of the Heyting algebra are regular, this Boolean algebra will not be a sublattice of the Heyting algebra, because its join operation will be different.
Arend Heyting (1898-1980) was himself interested in clarifying the foundational status of intuitionistic logic, in introducing this type of structures. The case of Peirce's law illustrates the semantic role of Heyting algebras. No simple proof is known that Peirce's law cannot be deduced from the basic laws of intuitionistic logic.
A Heyting algebra, from the logical standpoint, is essentially a
generalization of the usual system of truth values. Amongst other
properties, the largest element, called in logic
, is analogous to 'true'. The usual two-valued
logic system is the simplest example of a Heyting algebra, one in
which the elements of the algebra are (true) and
One can construct a Heyting algebra in which the value of Pierce's law
is not always . From what has just been said, this does show that it cannot be derived. See Curry-Howard isomorphism for the general context, of what this implies in type theory.
This is an Article on Heyting algebra. Page Contains Information, Facts Details or Explanation Guide About Heyting algebra Properties
The pseudo-complement of an element x of H is the supremum of the set
and it belongs to this set (i.e.
holds).
Boolean algebras are exactly those Heyting algebras in which
for all x, or, equivalently, in which
for all x. In this case, the element
is equal to .
In any Heyting algebra, the least and greatest elements 0 and 1 are regular.Examples
Heyting algebras as applied to intuitionistic logic
(false). That is, in abstract terms, the two-element Boolean algebra is also a Heyting algebra.
Classically valid formulas are those formulas that have a value of
in this Boolean algebra under any
possible assignment of true and false to the formula's
variables — that is, they are formulas which are tautologies in the
usual truth-table sense. Intuitionistically valid formulas are those
formulas that have a value of in any Heyting
algebra under any assignment of values to the formula's variables.See also
References