Heyting algebra

From Example Problems
Jump to navigation Jump to search

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.

Formal definitions

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 Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a \wedge x \le b} . This element is called the relative pseudo-complement of a with respect to b, and is denoted Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a \Rightarrow b} (or Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a \rightarrow b} ).

An equivalent definition can be given by considering the mappings Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f_a: H \to H} defined by Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f_a(x)=a\wedge x} , for some fixed a in H. A bounded lattice H is a Heyting algebra iff all mappings Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f_a} are the lower adjoint of a monotone Galois connection. In this case the respective upper adjoints Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle g_a} are given by Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle g_a(x)= a \Rightarrow x} , where Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Rightarrow} 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 Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lnot x} of some element x by setting Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lnot x = x \Rightarrow 0} , where 0 is the least element of the Heyting algebra.

An element x of a Heyting algebra is called regular if Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x=\lnot\lnot x} . An element x is regular if and only if Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x=\lnot y} for some element y of the Heyting algebra.

Properties

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, Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \wedge} preserves all existing suprema. Distributivity in turn is just the preservation of binary suprema by Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \wedge} .

Furthermore, by a similar argument, the following infinite distributive law holds in any complete Heyting algebra:

Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x\wedge\bigvee Y = \bigvee \{x\wedge y : y \in Y\}}

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:

  1. H satisfies both De Morgan laws.
  2. Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lnot(x \wedge y)=\lnot x \vee \lnot y} , for all x, y in H.
  3. Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lnot x \vee \lnot\lnot x = 1} , for all x in H.
  4. Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lnot\lnot (x \vee y) = \lnot\lnot x \vee \lnot\lnot y} , for all x, y in H.

The pseudo-complement of an element x of H is the supremum of the set Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \{ y : y \wedge x = 0\}} and it belongs to this set (i.e. Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x \wedge \lnot x = 0} holds).

Boolean algebras are exactly those Heyting algebras in which Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x = \lnot\lnot x} for all x, or, equivalently, in which Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x\vee\lnot x=1} for all x. In this case, the element Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a \Rightarrow b} is equal to Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lnot a \vee b} .

In any Heyting algebra, the least and greatest elements 0 and 1 are regular.

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.

Examples

  • Every totally ordered set that is a bounded lattice is also a Heyting algebra, where Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lnot 0 = 1} and Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lnot a = 0} for all a other than 0.
  • Every topology provides a complete Heyting algebra in the form of its open set lattice. In this case, the element Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A \Rightarrow B} is the interior of the union of Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A_c} and B, where Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A_c} denotes the complement of the open set A. Not all complete Heyting algebras are of this form. These issues are studied in pointless topology, where complete Heyting algebras are also called frames or locales.
  • The Lindenbaum algebra of propositional intuitionistic logic is a Heyting algebra. It is defined to be the set of all propositional logic formulae, ordered via logical entailment: for any two formulae F and G we have Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle F \le G} iff Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle F \models G} . At this stage Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \le} is merely a preorder that induces a partial order which is the desired Heyting algebra.

Heyting algebras as applied to intuitionistic logic

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 Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \top} , 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 Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \top} (true) and Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \bot} (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 Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \top} 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 Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \top} in any Heyting algebra under any assignment of values to the formula's variables.

One can construct a Heyting algebra in which the value of Peirce's law is not always Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \top} . 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.

See also

References

  • F. Borceux, Handbook of Categorical Algebra 3, In Encyclopedia of Mathematics and its Applications, Vol. 53, Cambridge University Press, 1994.
  • G. Gierz, K.H. Hoffmann, K. Keinel, J. D. Lawson, M. Mislove and D. S. Scott, Continuous Lattices and Domains, In Encyclopedia of Mathematics and its Applications, Vol. 93, Cambridge University Press, 2003.

es:Álgebra de Heyting