Editing Heyting algebra (section)

{{Short description|Algebraic structure used in logic}}
In [[mathematics]], a '''Heyting algebra''' (also known as '''pseudo-Boolean algebra'''<ref>{{Cite web|url=https://www.encyclopediaofmath.org/index.php/Pseudo-Boolean_algebra|title = Pseudo-Boolean algebra - Encyclopedia of Mathematics}}</ref>) is a [[Lattice (order)#Bounded lattice|bounded lattice]] (with join and meet operations written ∨ and ∧ and with least element 0 and greatest element 1) equipped with a binary operation ''a'' → ''b'' called ''implication'' such that (''c'' ∧ ''a'') ≤ ''b'' is equivalent to ''c'' ≤ (''a'' → ''b''). From a logical standpoint, ''A'' → ''B'' is by this definition the weakest proposition for which [[modus ponens]], the inference rule ''A'' → ''B'', ''A'' ⊢ ''B'', is [[Soundness#Logical systems|sound]].  Like [[Boolean algebra (structure)|Boolean algebras]], Heyting algebras form a [[Variety (universal algebra)|variety]] axiomatizable with finitely many equations. Heyting algebras were introduced in 1930 by [[Arend Heyting]] to formalize [[intuitionistic logic]]. <ref name="Heyting1930">{{citation|last=Heyting|first= A.
|title=Die formalen Regeln der intuitionistischen Logik. I, II, III|jfm= 56.0823.01
|journal=Sitzungsberichte Akad. Berlin |year=1930|pages= 42–56, 57–71, 158–169 }}</ref>

Heyting algebras are [[distributive lattice|distributive lattices]].  Every Boolean algebra is a Heyting algebra when ''a'' → ''b'' is defined as ¬''a'' ∨ ''b'', as is every [[Completeness (order theory)|complete]] [[distributive lattice]] satisfying a one-sided [[Distributivity (order theory)#Distributivity laws for complete lattices|infinite distributive law]] when ''a'' → ''b'' is taken to be the [[supremum]] of the set of all ''c'' for which ''c'' ∧ ''a'' ≤ ''b''.  In the finite case, every nonempty distributive lattice, in particular every nonempty finite [[Total order#Chains|chain]], is automatically complete and completely distributive, and hence a Heyting algebra.

It follows from the definition that 1 ≤ 0 → ''a'', corresponding to the intuition that any proposition ''a'' is implied by a contradiction 0.  Although the negation operation ¬''a'' is not part of the definition, it is definable as ''a'' → 0.  The intuitive content of ¬''a'' is the proposition that to assume ''a'' would lead to a contradiction. The definition implies that ''a'' ∧ ¬''a'' = 0.  It can further be shown that ''a'' ≤ ¬¬''a'', although the converse, ¬¬''a'' ≤ ''a'', is not true in general, that is, [[double negation elimination]] does not hold in general in a Heyting algebra.

Heyting algebras generalize Boolean algebras in the sense that Boolean algebras are precisely the Heyting algebras satisfying ''a'' ∨ ¬''a'' = 1 ([[excluded middle]]), equivalently ¬¬''a'' = ''a''. Those elements of a Heyting algebra ''H'' of the form ¬''a'' comprise a Boolean lattice, but in general this is not a [[subalgebra]] of ''H'' (see [[#Regular and complemented elements|below]]).

Heyting algebras serve as the algebraic models of propositional [[intuitionistic logic]] in the same way Boolean algebras model propositional [[classical logic]].<ref name="MacLane1994">{{cite book | vauthors=((Mac Lane, S.)), ((Moerdijk, I.)) | date= 1994 | title=Sheaves in Geometry and Logic | series= Universitext | publisher=Springer New York | url=http://dx.doi.org/10.1007/978-1-4612-0927-0 | pages=48 | doi=10.1007/978-1-4612-0927-0| isbn= 978-0-387-97710-2 }}</ref> The internal logic of an [[elementary topos]] is based on the Heyting algebra of [[subobject]]s of the [[terminal object]] 1 ordered by inclusion, equivalently the morphisms from 1 to the [[subobject classifier]] Ω.

The [[open set]]s of any [[topological space]] form a [[complete Heyting algebra]]. Complete Heyting algebras thus become a central object of study in [[pointless topology]].  

Every Heyting algebra whose set of non-greatest elements has a greatest element (and forms another Heyting algebra) is [[Subdirectly irreducible algebra|subdirectly irreducible]], whence every Heyting algebra can be made subdirectly irreducible by adjoining a new greatest element.  It follows that even among the finite Heyting algebras there exist infinitely many that are subdirectly irreducible, no two of which have the same [[equational theory]].  Hence no finite set of finite Heyting algebras can supply all the counterexamples to non-laws of Heyting algebra.  This is in sharp contrast to Boolean algebras, whose only subdirectly irreducible one is the two-element one, which on its own therefore suffices for all counterexamples to non-laws of Boolean algebra, the basis for the simple [[truth table]] decision method.  Nevertheless, it is [[Decidability (logic)|decidable]] whether an equation holds of all Heyting algebras.<ref name="Kripke63">Kripke, S. A.: 1965, 'Semantical analysis of intuitionistic logic I'. In: J. N. Crossley and M. A. E. Dummett (eds.): Formal Systems and Recursive Functions. Amsterdam: North-Holland, pp. 92–130.</ref>

Heyting algebras are less often called '''pseudo-Boolean algebras''',<ref name="Rasiowa-Sikorski">{{cite book|author1=Helena Rasiowa|author2=Roman Sikorski|title=The Mathematics of Metamathematics|year=1963 |publisher=Państwowe Wydawnictwo Naukowe (PWN)|pages=54–62, 93–95, 123–130}}</ref> or even '''Brouwer lattices''',<ref name="KusraevKutateladze1999">{{cite book|author1=A. G. Kusraev|author2=Samson Semenovich Kutateladze|title=Boolean valued analysis|url=https://books.google.com/books?id=MzVXq3LRHOYC&pg=PA12 |year=1999 |publisher=Springer|isbn=978-0-7923-5921-0|page=12}}</ref> although the latter term may denote the dual definition,<ref>{{springer | title=Brouwer lattice  | id= b/b017660  | last= Yankov  | first= V.A.}}</ref> or have a slightly more general meaning.<ref name="Blyth2005">{{cite book|author=Thomas Scott Blyth|title=Lattices and ordered algebraic structures|url=https://books.google.com/books?id=WgROkcmTxG4C&pg=PA151 |year=2005 |publisher=Springer |isbn=978-1-85233-905-0|page=151}}</ref>