n -Rational Algebras II. Varieties and Logic of inequalities
Jean H. Gallier · SIAM Journal on Computing · 1984
This work is a continuation of the study of n-rational algebras initiated in the first part of this paper [SIAM J. Comput.,13 (1984), pp.750–775.]. In this second part, varieties of n-rational algebras satisfying a set of inequalities and the corresponding logic are investigated. It is shown that there is a bijective Galois connection between such varieties, called semi-varieties, and “fully invariant” n-rational precongruences. A deductive system for proving inequalities in which a proof is represented as a well-founded tree is shown to be sound and complete. This proof system uses one infinitary inference rule, the “lub rule”. A “Birkhoff variety theorem” is also proved for semi-varieties. The relationship between this approach in which classes of interpretations are semi-varieties of n-rational algebras, and the approach in which $\omega $-continuous algebras are used (Courcelle, Nivat, Guessarian) is also briefly explored.