Хейтинг алгебралары: интуиционистік логика мен топологиядағы қолданыстары

In mathematics, a Heyting algebra (also known as pseudo Boolean algebra) is a 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 of 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 sound. Like Boolean algebras, Heyting algebras form a variety axiomatizable with finitely many equations. Heyting algebras were introduced by to formalize intuitionistic logic. Heyting algebras are distributive lattices. Every Boolean algebra is a Heyting algebra when a → b is defined as ¬a ∨ b, as is every complete distributive lattice satisfying a one sided 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 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 below). Heyting algebras serve as the algebraic models of propositional intuitionistic logic in the same way Boolean algebras model propositional classical logic. The internal logic of an elementary topos is based on the Heyting algebra of subobjects of the terminal object 1 ordered by inclusion, equivalently the morphisms from 1 to the subobject classifier Ω. The open sets 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, 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 decidable whether an equation holds of all Heyting algebras. Heyting algebras are less often called pseudo Boolean algebras, or even Brouwer lattices, although the latter term may denote the dual definition, or have a slightly more general meaning.

The ordering on a Heyting algebra H can be recovered from the operation → as follows: for any elements a, b of H, if and only if a→b = 1. In contrast to some many valued logics, Heyting algebras share the following property with Boolean algebras: if negation has a fixed point (i. e. ¬a = a for some a), then the Heyting algebra is the trivial one element Heyting algebra.

The identity map 1=f(x) = x from any Heyting algebra to itself is a morphism, and the composite 1=g ∘ f of any two morphisms f and g is a morphism. Hence Heyting algebras form a category.

Given a Heyting algebra H and any subalgebra H1, the inclusion mapping 1=i : H1 → H is a morphism. For any Heyting algebra H, the map 1=x ↦ ¬¬x defines a morphism from H onto the Boolean algebra of its regular elements Hreg. This is not in general a morphism from H to itself, since the join operation of Hreg may be different from that of H.

Let H be a Heyting algebra, and let 1=F ⊆ H. We call F a filter on H if it satisfies the following properties:

The intersection of any set of filters on H is again a filter. Therefore, given any subset S of H there is a smallest filter containing S. We call it the filter generated by S. If S is empty, 1=F = {1}. Otherwise, F is equal to the set of x in H such that there exist 1=y1, y2, , yn ∈ S with 1=y1 ∧ y2 ∧ ∧ yn ≤ x. If H is a Heyting algebra and F is a filter on H, we define a relation ~ on H as follows: we write 1=x ~ y whenever 1=x → y and 1=y → x both belong to F. Then ~ is an equivalence relation; we write 1=H/F for the quotient set. There is a unique Heyting algebra structure on 1=H/F such that the canonical surjection 1=pF : H → H/F becomes a Heyting algebra morphism. We call the Heyting algebra 1=H/F the quotient of H by F.

Let S be a subset of a Heyting algebra H and let F be the filter generated by S. Then H/F satisfies the following universal property:
Given any morphism of Heyting algebras satisfying 1=f(y) = 1 for every 1=y ∈ S, f factors uniquely through the canonical surjection 1=pF : H → H/F. That is, there is a unique morphism satisfying The morphism is said to be induced by f.

Let 1=f : H1 → H2 be a morphism of Heyting algebras. The kernel of f, written ker f, is the set 1=f−1[{1}]. It is a filter on H1. (Care should be taken because this definition, if applied to a morphism of Boolean algebras, is dual to what would be called the kernel of the morphism viewed as a morphism of rings.) By the foregoing, f induces a morphism It is an isomorphism of 1=H1/(ker f) onto the subalgebra f[H1] of H2.

In fact, the preceding construction can be carried out for any set of variables {Ai : i∈I} (possibly infinite). One obtains in this way the free Heyting algebra on the variables {Ai}, which we will again denote by H0. It is free in the sense that given any Heyting algebra H given together with a family of its elements 〈ai: i∈I 〉, there is a unique morphism f:H0→H satisfying f([Ai])=ai. The uniqueness of f is not difficult to see, and its existence results essentially from the metaimplication 1 ⇒ 2 of the section "Provable identities" above, in the form of its corollary that whenever F and G are provably equivalent formulas, F(〈ai〉)=G(〈ai〉) for any family of elements 〈ai〉in H.

Given a set of formulas T in the variables {Ai}, viewed as axioms, the same construction could have been carried out with respect to a relation F≼G defined on L to mean that G is a provable consequence of F and the set of axioms T. Let us denote by HT the Heyting algebra so obtained. Then HT satisfies the same universal property as H0 above, but with respect to Heyting algebras H and families of elements 〈ai〉 satisfying the property that J(〈ai〉)=1 for any axiom J(〈Ai〉) in T. (Let us note that HT, taken with the family of its elements 〈[Ai]〉, itself satisfies this property.) The existence and uniqueness of the morphism is proved the same way as for H0, except that one must modify the metaimplication 1 ⇒ 2 in "Provable identities" so that 1 reads "provably true from T," and 2 reads "any elements a1, a2, , an in H satisfying the formulas of T."

The Heyting algebra HT that we have just defined can be viewed as a quotient of the free Heyting algebra H0 on the same set of variables, by applying the universal property of H0 with respect to HT, and the family of its elements 〈[Ai]〉. Every Heyting algebra is isomorphic to one of the form HT. To see this, let H be any Heyting algebra, and let 〈ai: i∈I〉 be a family of elements generating H (for example, any surjective family). Now consider the set T of formulas J(〈Ai〉) in the variables 〈Ai: i∈I〉 such that J(〈ai〉)=1. Then we obtain a morphism f:HT→H by the universal property of HT, which is clearly surjective. It is not difficult to show that f is injective.

The constructions we have just given play an entirely analogous role with respect to Heyting algebras to that of Lindenbaum algebras with respect to Boolean algebras. In fact, The Lindenbaum algebra BT in the variables {Ai} with respect to the axioms T is just our HT∪T1, where T1 is the set of all formulas of the form ¬¬F→F, since the additional axioms of T1 are the only ones that need to be added in order to make all classical tautologies provable.

If one interprets the axioms of the intuitionistic propositional logic as terms of a Heyting algebra, then they will evaluate to the largest element, 1, in any Heyting algebra under any assignment of values to the formula's variables. For instance, (P∧Q)→P is, by definition of the pseudo complement, the largest element x such that This inequation is satisfied for any x, so the largest such x is 1. Furthermore, the rule of modus ponens allows us to derive the formula Q from the formulas P and P→Q. But in any Heyting algebra, if P has the value 1, and P→Q has the value 1, then it means that , and so ; it can only be that Q has the value 1. This means that if a formula is deducible from the laws of intuitionistic logic, being derived from its axioms by way of the rule of modus ponens, then it will always have the value 1 in all Heyting algebras under any assignment of values to the formula's variables. However one can construct a Heyting algebra in which the value of Peirce's law is not always 1. Consider the 3 element algebra {0,,1} as given above. If we assign to P and 0 to Q, then the value of Peirce's law ((P→Q)→P)→P is It follows that Peirce's law cannot be intuitionistically derived. See Curry–Howard isomorphism for the general context of what this implies in type theory. The converse can be proven as well: if a formula always has the value 1, then it is deducible from the laws of intuitionistic logic, so the intuitionistically valid formulas are exactly those that always have a value of 1. This is similar to the notion that classically valid formulas are those formulas that have a value of 1 in the two element Boolean algebra under any possible assignment of true and false to the formula's variables—that is, they are formulas that are tautologies in the usual truth table sense. A Heyting algebra, from the logical standpoint, is then a generalization of the usual system of truth values, and its largest element 1 is analogous to 'true'. The usual two valued logic system is a special case of a Heyting algebra, and the smallest non trivial one, in which the only elements of the algebra are 1 (true) and 0 (false).

The problem of whether a given equation holds in every Heyting algebra was shown to be decidable by Saul Kripke in 1965. and hence at least as hard as deciding equations of Boolean algebra (shown coNP complete in 1971 by Stephen Cook) and conjectured to be considerably harder. The elementary or first order theory of Heyting algebras is undecidable. It remains open whether the universal Horn theory of Heyting algebras, or word problem, is decidable. Regarding the word problem it is known that Heyting algebras are not locally finite (no Heyting algebra generated by a finite nonempty set is finite), in contrast to Boolean algebras, which are locally finite and whose word problem is decidable. It is unknown whether free complete Heyting algebras exist except in the case of a single generator where the free Heyting algebra on one generator is trivially completable by adjoining a new top.