# zbMATH — the first resource for mathematics

Unification on subvarieties of pseudocomplemented distributive lattices. (English) Zbl 1375.06009
The author studies unification in the implication-free fragment of intuitionistic logic, that is, the equational theory of pseudo-complemented distributive lattices ($$p$$-lattices) and its extensions. He proved the following two important results.
The first is that Boolean algebras form the only nontrivial subvariety of $$p$$-lattices that has type 1, while the others have nullary type in
Theorem 4.2: Let $$\mathfrak{V}$$ be a non-trivial subvariety of $$\mathfrak{B}_{\omega}$$. Then the following holds: $(\mathfrak{V}) = \begin{cases} 1 & \text{if }\mathfrak{V}=\mathfrak{B}_0\\ 0 & \text{otherwise,} \end{cases}$ where $$\mathfrak{B}_0$$ is the class of Boolean algebras.
The second result is about the type of each unification problem in every extension of the equational theory of $$p$$-lattices, Theorem 7.5 and Theorem 8.8, that is,
Theorem 7.5: Let $$X$$ be a nonempty poset in $$\mathcal{P}^f$$. Then $\text{Type} (U_{\mathcal{P}^f}(X)) = \begin{cases}|\max (\mathcal{C}(X))| & \text{if each }Y\in\max (\mathcal{C}(X))\text{ satisfies (*)}\\ 0 & \text{otherwise}. \end{cases}$ and
Theorem 8.8: Let $$X$$ be a nonempty poset in $$\mathcal{P}_{n}^{f}$$. Then $\text{Type} (U_{\mathcal{P}_n^f}(X)) = \begin{cases} |\max (\mathcal{C}_n(X))| & \text{if each }Y\in\max (\mathcal{C}(X))\text{ satisfies }(*_n)\\ 0 & \text{otherwise}. \end{cases}$ In the statements above, the symbols represent the following.
1. $$\mathfrak{B}_{\omega}$$ is the variety of $$p$$-lattices and also means the category of $$p$$-lattices as objects and homomorphisms as arrows.
2. For a finite poset $$(X,\leq)$$, the condition (*) is that if for each $$x,y \in X$$ the least upper bound $$x\vee y$$ exists in $$X$$ and it is such that $$\min_X (x\vee y) = \min_X(x) \cup \min_Y(y)$$, where $$\min_X(x)$$ is the set of minimal elements of $$X$$ below $$x$$.
3. $$\mathcal{P}^f$$ is the category whose objects are finite posets and whose arrows are $$p$$-morphisms. Moreover, $$\mathcal{P}_n^f$$ denotes the full subcategory of $$\mathcal{P}^f$$ whose objects $$X$$ satisfy $$|\min_X(x)| \leq n$$ for all $$x\in X$$.
4. $$U_{\mathcal{P}^f}(X)$$ is the class of morphisms $$v: Y\to X$$ with $$Y\in \mathcal{P}^f$$ satisfying (*).
5. $$\mathcal{C}(X)$$ is the posets of connected subsets of $$X$$ ordered by set inclusion, where a subset $$Y\subseteq X$$ is called connected if $$Y$$ satisfies
(i) $$\min_X(Y) \subseteq Y$$;
(ii) for each $$x,y\in Y$$ there exists $$z\in Y$$ such that $$x,y\leq z$$ and $$\displaystyle \min_X(x) \cup \min_X(y) = \min_X(z)$$.
##### MSC:
 06D15 Pseudocomplemented lattices 08B30 Injectives, projectives 06D50 Lattices and duality 03G10 Logical aspects of lattices and related structures
Full Text: