# 简介多类逻辑（Many-Sorted Logic）

1，例子：欧几里德几何的第一公理

xy(x≠yX(Join(Xxy)∧∀Y(Join(Yxy)X=Y)))

Join是一个3元的谓词符号，与一条直线和两个点有关：

Join(Yxy):=Y joins x and y

2，基本概念

Σ=Sort,OperSym,Rank

https://en.wikipedia.org/wiki/Signature_(logic)

https://math.stackexchange.com/questions/1523458/categories-and-sorted-systems

https://plato.stanford.edu/entries/logic-many-sorted/

Many-Sorted Logic

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.)

1. Syntax and Semantics

1.1 Examples

We start with a few examples to illustrate how common statements concerning different types of data can be formalized in many-sorted first-order logic.

Example: Euclid’s first principle

Let us begin with geometry, by talking about straight lines and points. According to Euclid’s first principle:

A straight line can be drawn joining any two points.

In two sorted first-order logic one can use X, Y,… as variables for sort l (straight lines) and x,y,… as variables for sort p (points). To formulate Euclid’s principle we write:

xy(x≠yX(Join(Xxy)∧∀Y(Join(Yxy)X=Y)))

In this example, Join is a 3-place predicate symbol relating a straight line and two points,

Join(Yxy):=Y joins x and y

Literally our formalization reads: “For any two points there is a unique straight line joining them”.

1.2 Fundamental Ideas

To specify the syntax of a many-sorted language and associated structures we need first to say what our (countable) set of sorts is. We take

Sort={s1,…,sn} as the sorts of an n-sorted language.

Structures: A many-sorted structure has several non-empty domains, one for each sort, and variables of a given sort take values over the corresponding domain. An n-ary relation could be freely established between elements of different domains or only between certain ones. These two options are called liberal and strict. A liberal relation may relate objects of arbitrary domains and only the arity (a natural number) has to be stated. For a strict relation, the sorts involved have to be specified as well as the arity.

Alphabet: The alphabet of a many-sorted language L   includes all the relation, function, and constant symbols in a set called OperSym, as well as an infinite number of variables for each sort si Sort, and the corresponding sets of variables are disjoint. An n-ary relation symbol R could be strict or liberal and, in the first case, we must provide information about what are the involved sorts. To achieve this requirement, we define a function Rank having as domain the set OperSym and whose values are either natural numbers other than zero (liberal option) or finite strings of Sort {0} (strict option). For any strict fOperSym, its value Rank(f) always has the form i1,…,im,i0, with i0,i1,…,imSort{0}. When f is an m-ary predicate, i0=0, and i0≠0 for m-ary function symbols; individual constants are considered as zero-ary function symbols with

Rank(f)=i0, simplified as i0.

Signature: By a signature Σ we mean the ordered triple

Σ=Sort,OperSym,Rank

Equality is a binary symbol that  could be strict or liberal. In our language, the equality symbol ≈ with Rank(≈)=2 is liberal (having arity 2 and being allowed to work between terms of any sort). The quantifier xi is used for variables xi of any sort i.

In Euclid’s example we have two sorts, l (lines) and p (points) and a 3-place predicate Join with Rank(Join)=l,p,p,0.

Terms and Formulas

As we do in classical first-order logic, from the set of finite strings of elements of the alphabet we select the expressions of L: terms and formulas. The only difference is that in many-sorted logic terms have sorts and we have to specify it.

In consequence, the terms of many-sorted logic are defined recursively as follows: Each variable or individual constant of sort si is a term of the same sort si. If f

OperSym is such that Rank(f)=i1,…,im,i0 with i0≠0 and τ1,…,τm are terms of sorts i1,…,im, then f τ1…τm is a term of sort i0.

Atomic formulas are defined by means of predicates and terms: If ROperSym is such that Rank(R)=i1,…,im,0, and τ1,…,τm are terms of sorts i1,…, im, then Rτ1…τm is a formula (when R is a liberal predicate, we drop the sort requirement for terms). For any terms τ1 and τ2, the expression τ1≈τ2 is a formula. Notice that the sorts of τ1 and τ2 do not matter, because our choice of equality symbol is the liberal one.

Complex well-formed formulas (wffs) are defined as usual in first-order languages (see the entry on classical logic), except for quantified expressions. The new rule says: If φ is a formula and xi is a variable of sort i, then xiφ is a formula as well.

Free and bound variables

As in classical first-order logic, occurrences of variables in a formula can be free or bound; they are bound when they are under the scope of a quantifier, otherwise free. A variable is free in a formula if it has at least one free occurrence therein. A formula with no free variables is called a sentence. We use

Sent(L) to denote the set of sentences of language L.

Theory: Given a set of sentences Γ of a language L we say that Γ is a theory if and only if it is closed under consequence; that is, for every φSent(L): If Γφ

then φΓ.

https://blog.sciencenet.cn/blog-2322490-1378523.html

## 全部作者的其他最新博文

GMT+8, 2023-6-3 02:58