Many-Sorted Logic

Abstract

Classical logic is the appropriate formal language for describing mathematical structures containing a single universe or domain of discourse. By contrast, many-sorted logic (MSL) allows quantification over a variety of domains (called sorts). For this reason, it is a suitable vehicle for dealing with statements concerning different types of objects, which are ubiquitous in mathematics, philosophy, computer science, and formal semantics. Each sort groups a unique category of objects (for example, points and straight lines are different types of objects in a 2-sorted structure).

Despite the addition of this expressive resource, many-sorted logic “stays inside” first-order logic, so the main metatheorems (completeness, interpolation, and so on) can be proved. Many-sorted logic also serves as a unifying framework for translating various logical systems; for instance, some intensional and higher-order logics have natural translations into many-sorted logic. Many-sorted first-order logic can be reduced to one-sorted first-order logic, both syntactically and semantically. Many-sorted first-order logic can also be extended to a many-sorted second-order logic called “sort logic”.

An axiomatic calculus for many-sorted logic was introduced by Hao Wang in Wang (1952), where he made a comparison between one-sorted and many-sorted theories. In 1967, Solomon Feferman gave a sequent calculus for many-sorted logic, proving not only its completeness but also the cut elimination and interpolation theorems (Feferman 1968). Feferman (2008) summarizes some applications of the many-sorted interpolation theorems to model theory. (See the supplement on early history for more information.)

Section 1 lays out the basics of many-sorted logic, presenting some examples and explaining how the formal language, structures, and semantics differ or not from classical logic. Section 2 explains how to modify a one-sorted first-order calculus to obtain a many-sorted version; also, completeness is treated and some automated theorem provers are mentioned. Section 3 describes a plan on which many-sorted logic serves as a common framework for translating a variety of logical systems. Sections 4 and 5 apply this plan to second-order logic and non-classical logics (modal and dynamic logic), respectively. Finally, section 6 comments on further results in many-sorted logic.