Heyting algebra

English Etymology After Dutch mathematician Arend Heyting, who developed the theory as a way of modelling his intuitionistic logic. Noun en algebra order theory A bounded lattice, L, modified to serve as a model for a logical calculus by being equipped with a binary operation called "implies", denoted → (sometimes ⊃ or ⇒), defined such that (a→b)∧a ≤ b and, moreover, that x = a→b is the greatest element such that x∧a ≤ b (in the sense that if c∧a ≤ b then c ≤ a→b). en 1984 Robert Goldblatt Topoi, the categorial analysis of logic xii The laws of Heyting algebra embody a rich and profound mathematical structure that is manifest in a variety of contexts. It arises from the epistemological deliberations of Brouwer, the topologisation (localisation) of set-theoretic notions, and the categorial formulation of set theory, all of which, although interrelated, are independently motivated. The ubiquity lends weight, not to the suggestion that the correct logic is in fact intuitionistic instead of classical, but rather to the recognition that thinking in such terms is simply inappropriate — in the same way that it is inappropriate to speak without qualification about the correct geometry. 1994, Francis Borceux, Handbook of Categorical Algebra 3: Categories of Sheaves, Cambridge University Press, page 13, Proposition 1.2.14 should certainly be completed by the observation that the modus ponens holds as well in every Heyting algebra. Since, in the intuitionistic propositional calculus, being a true formula is being a terminal object (see proof of 1.1.3), the modus ponens of a Heyting algebra reduces to   and    imply   which is just obvious. 1997, J. G. Stell, M. W. Worboys, The Algebraic Structure of Sets and Regions, Stephen C. Hirtle, Andrew U. Frank (editors), Spatial Information Theory A Theoretical Basis for GIS: International Conference, Proceedings, Springer, LNCS 1329, page 163, The main contention of this paper is that Heyting algebras, and related structures, provide elegant and natural theories of parthood and boundary which have close connections to the above three ontologies. Usage notes The symbols for the lattice operations join (∨) and meet (∧) and for the partial order relation (≤) are reinterpreted as logical connectives: ∨ becomes or, ∧ becomes and and ≤ becomes proves (⊢). Thus, (a→b)∧a ≤ b (the defining condition for →) becomes (a→b), a ⊢ b, which is modus ponens. The qualifying condition c∧a ≤ b ⇒ c ≤ a→b becomes c, a ⊢ b ⇒ c ⊢ a→b, which is the deduction theorem. The en pseudo-complement of a, denoted ¬a, is defined as a→0, and a→b is called the en relative pseudo-complement of a with respect to b A Heyting algebra in which a∨¬a = 1 (the law of excluded middle) is a Boolean algebra. In this sense, Heyting algebras generalise Boolean algebras, which model (propositional) classical logic. Synonyms bounded lattice en pseudo-Boolean algebra Hypernyms bounded lattice en distributive lattice, en residuated lattice, en bicartesian closed category Hyponyms bounded lattice en Boolean algebra, en complete Heyting algebra, finite distributive lattice Derived terms en bi-Heyting algebra, en biHeyting algebra en co-Heyting algebra, en coHeyting algebra en complete Heyting algebra Related terms en Heyting prealgebra Translations bounded lattice equipped with operation called implies Italian: it algebra di Heyting f See also en pseudo-complement en relative pseudo-complement en residuated lattice Further reading Intuitionistic logic Boolean algebra (structure) Complemented lattice Distributive lattice Lindenbaum–Tarski algebra Heyting algebra on NLab nLab Pseudo-Boolean algebra on Encyclopedia of Mathematics en eponyms