Equations, Dependent Equations and Quasi-Dependent Equations - on their unification

Sun, Yong

Abstract: This paper concentrates on many-sorted calculi for equations, equational implications and conditional equations (or quasi-equations). It attempts to unify the three of them not only on their names, say dependent equations and quasi-dependent equations for the equational implications and conditional equations (or quasi-equations) respectively, but also on their semantical results which will be totally presented in Birkhoff's approach. Their deduction systems are written as D^{~}, D^{~d} and D^{~q} respectively. The completeness of D^{~} is not new, but a proof of it (to be presented) is very unique and deserves special attention. A new concept of cross-fully invariant congruences is introduced to capture the completeness by Birkhoff's method, which does not have its place in single-sorted case. The calculi for D^{~d} and D^{~q} presented in [14] and in [11] respectively will be shown unsound. The right one for D^{~d} is found, and its completeness of D^{~d} is achieved with a pay-off on total derivability. Although the calculus in [11] can be served as an alternative for the right one, a sound and complete D^{~q} is remained open. Nevertheless, the results, especially the ones related to D^{~q}, suggest us to look for a universal equational form to unite the three equational forms. One candidate is briefly proposed.


Previous | Index | Next