Many-sorted logic

Many-sorted logic can reflect formally our intention not to handle the universe as a homogeneous collection of objects, but to partition it in a way that is similar to types in typeful programming. Both functional and assertive "" in the language of the logic reflect this typeful partitioning of the universe, even on the syntax level: substitution and argument passing can be done only accordingly, respecting the "sorts". There are various ways to formalize the intention mentioned above; a many-sorted logic is any package of information which fulfils it. In most cases, the following are given: a set of sorts, S an appropriate generalization of the notion of signature to be able to handle the additional information that comes with the sorts. The domain of discourse of any structure of that signature is then fragmented into disjoint subsets, one for every sort. When reasoning about biological organisms, it is useful to distinguish two sorts: and . While a function makes sense, a similar function usually does not. Many-sorted logic allows one to have terms like , but to discard terms like as syntactically ill-formed. The algebraization of many-sorted logic is explained in an article by Caleiro and Gonçalves, which generalizes abstract algebraic logic to the many-sorted case, but can also be used as introductory material. While many-sorted logic requires two distinct sorts to have disjoint universe sets, order-sorted logic allows one sort to be declared a subsort of another sort , usually by writing or similar syntax. In the above biology example, it is desirable to declare and so on; cf. picture. Wherever a term of some sort is required, a term of any subsort of may be supplied instead (Liskov substitution principle). For example, assuming a function declaration , and a constant declaration , the term is perfectly valid and has the sort . In order to supply the information that the mother of a dog is a dog in turn, another declaration may be issued; this is called function overloading, similar to overloading in programming languages.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related concepts (2)

Related lectures (2)

LISA proof assistant: Formalisation and Verification

Covers the LISA proof assistant's codebase organization, kernel package, FOL formalization, and proof package.

Boolean Algebra: Properties and Theorems

Covers the properties and theorems of Boolean algebra in logic systems.

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable.