Unification on subvarieties of pseudocomplemented distributive lattices (Q2374391)

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)\).