2026-06-28T20:10:00Zhttps://docta.ucm.es/rest/oai/request

oai:docta.ucm.es:20.500.14352/984542025-02-03T16:25:40Zcom_20.500.14352_14col_20.500.14352_15

Many-Sorted Logic Manzano Arjona, María Gracia Aranda Utrero, Víctor Zalta, Edward Nodelman, Uri 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. 2024-02-02T17:10:32Z 2024-02-02T17:10:32Z 2024-02-02T17:10:32Z 2022 book part https://hdl.handle.net/20.500.14352/98454 1095-5054 eng Manzano, María and Víctor Aranda, "Many-Sorted Logic", The Stanford Encyclopedia of Philosophy (Winter 2022 Edition), Edward N. Zalta & Uri Nodelman (eds.), URL = <https://plato.stanford.edu/archives/win2022/entries/logic-many-sorted/>. http://creativecommons.org/licenses/by-nc-nd/4.0/ metadata only access Attribution-NonCommercial-NoDerivatives 4.0 International