First-order theories as many-sorted algebras.
Vincenzo Manca, Antonino Salibra · Notre Dame Journal of Formal Logic · 1984
introductionIn this paper, by developing a study of first-order logic through many-sorted algebras, we show that every first-order theory is a particular algebra verifying axioms in equational form (see Section 2); therefore we are able to apply Birkhoff s theorems concerning the varieties (see Section 1 and [7] and [8]) and to obtain the Henkin models algebraically, whence the completeness theorem of first-order logic (see Section 3).The many-sorted (or heterogeneous) algebras, systematized by Birkhoff and Lipson (see [4] and [10]), find a natural application in investigating programming languages: several approaches to the formal definition of semantics for such languages can be developed by means of morphisms between manysorted algebras (see [2] and [6]).This paper shows the analogous possibility of algebraizing linguistic features of logic, thus yielding a unique framework for the formal analysis of both programming and logical languages within universal algebra.The analysis here developed is strongly related to those of [1], [2], [11], and [12].Moreover, an approach to the topic of present paper is elaborated in the monographs [8] and [9].Knowledge of these works is not necessary to understand what follows, though it would better enable one to appreciate our results.