The parameterized local deduction theorem for quasivarieties of algebras and its application (Q1918964)

For any class \({\mathbf K}\) of algebras of a given type \(\tau\), there is a natural consequence relation \(\models_{\mathbf K}\) on the set of all equations (in the first-order language \(L_\tau\) corresponding to \(\tau)\), defined as follows: Let \(\Sigma\) be a set of such equations, and \(p \doteq q\) be a single equation; then \(\Sigma \models_{\mathbf K} p \doteq q\) iff for every algebra \(A\in {\mathbf K}\) and every valuation \(h\) of the variables of \(L_\tau\) in \(A\) we have \(A\vdash p \doteq q[h]\) whenever \(A\vdash \sigma [h]\) for every \(\sigma\in \Sigma\). The paper under review is devoted to an in-depth study of \(\models_{\mathbf K}\) for quasivarieties \({\mathbf K}\) of algebras. The key property investigated for such \({\mathbf K}\) is the so-called Parametrized Local Deduction Theorem -- (PLDT), for short. Let \({\mathcal P}\) be a family of finite sets \(P\) of pairs of terms (of \(L_\tau)\) such that some fixed variables \(x,y,z,w\) occur in all terms of all \(P\in {\mathcal P}\). Then \({\mathbf K}\) is said to satisfy (PLDT) with respect to \({\mathcal P}\) iff for any set \(\Xi\) of \(L_\tau\)-equations and pairs \(p \doteq q\), \(r \doteq s\) of such equations, one has that \(\Xi\cup \{p \doteq q\} \models_{\mathbf K} r \doteq s\) if there exist a \(P\in {\mathcal P}\) and a finite sequence \({\mathbf t}\) of \(L_\tau\)-terms such that \(\Xi \models_{\mathbf K} \alpha (p,q, r,s, {\mathbf t}) \doteq \beta (p,q,r,s, {\mathbf t})\) for all \(\langle \alpha,\beta \rangle \in P\). The existence of a family \({\mathcal P}\) making (PLDT) true for \({\mathbf K}\) is intimately connected with the possibility of defining, by \(L_\tau\)-formulae, the principal congruence \(\theta\) on algebras \(A\in {\mathbf K}\) such that \(A/ \theta\in {\mathbf K}\). Among the main results of the paper are theorems expressing ``\({\mathbf K}\) satisfies (PLDT) with respect to some special type of \({\mathcal P}\)'' in terms of definability of such congruences, and of the presence of a generalized congruence extension property. Also, a generalization -- to quasivarieties -- of McKenzies Finite Basis Theorem is proved, and applications to various classes of algebras such as Lukasiewicz, Heyting and interior algebras are provided.