经典逻辑是描述包含单一域的数学结构的合适的形式语言。相比之下，多类逻辑（MSL）允许对各种域（称为sorts）进行量化，因此多类逻辑是处理有关不同类型对象的断言的合适载体，这些对象在数学、哲学、计算机科学和形式语义学中无处不在，每种类型都将一类独特的对象分组（例如，点和直线是2类结构中不同类型的对象）。

尽管增加了这种表达资源，多类逻辑还是“属于”一阶逻辑，所以主要的元定理（completeness, interpolation等）都可以被证明。多类逻辑还可以作为翻译各种逻辑系统的统一框架；例如，一些扩展逻辑和高阶逻辑都可以自然地翻译成多类逻辑。多类一阶逻辑在语法上和语义上都可以被还原为单类一阶逻辑。多类一阶逻辑也可以扩展为多类二阶逻辑，称为“类逻辑”。

王浩在Wang（1952）中介绍了多类逻辑的公理计算，他在其中对单类和多类的理论进行了比较。1967年，Solomon Feferman给出了多类逻辑的序列计算，不仅证明了其完备性，还证明了cut elimination和interpolation theorems（Feferman 1968）。Feferman（2008）总结了多类theorems 在模型理论中的一些应用。

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

经过任何两点可以画一条直线。

在有两个类的一阶逻辑中，人们可以用X,Y,...作为类l（直线）的变量， x,y,… 作为类p（点）的变量。为了表述欧几里德原理，我们写道：

∀x∀y(x≠y→∃X(Join(Xxy)∧∀Y(Join(Yxy)→X=Y)))

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

Join(Yxy):=Y joins x and y

2，基本概念

为了说明多类语言的语法和相关结构，我们把 Sort={s1,…,sn}作为一个n类语言的类集。

结构：一个多类结构有几个非空域，一个类一个域，一个给定类的变量在相应的域中取值。一个n元关系可以在不同域的元素之间自由建立，也可以只在某些域之间建立。这两种选择被称为自由和严格。自由关系可以把任意域的对象联系起来，而且只需要说明元数（一个自然数）。对于一个严格的关系，所涉及的类和元数都必须被指定。

字母表：多类语言L的字母表包括一个叫做OperSym的集合中的所有关系、函数和常数符号，以及每个类si∈Sort的无限多的变量，相应的变量集是不相交的。一个n元关系符号R可以是严格的，也可以是自由的，在第一种情下，我们必须提供有关什么是所涉及的类的信息。为了达到这个要求，我们定义一个函数Rank，其域是OperSym集，其值是0以外的自然数（自由选项）或Sort∪{0}的有限字符串（严格选项）。对于任何严格的f∈OperSym，其值Rank(f)总是具有⟨i1,…,im,i0⟩的形式，其中i0,i1,...,im∈Sort∪{0}。当f是m-ary谓词时，i0=0，i0≠0为m-ary函数符号；个别常数被认为是零元函数符号，有 Rank(f)=⟨i0⟩，简化为i0。

签名：我们所说的签名Σ是指有序的三要素

Σ=⟨Sort,OperSym,Rank⟩ 

等价是一个二元符号，可以是严格的，也可以是自由的。在我们的语言中，Rank(≈)=2的等价符号≈是自由的（有2的元数，允许在任何类型的项之间起作用）。量词∃xi用于任何种类i的变量xi。

在欧几里德的例子中，我们有两个类，l（线）和p（点），以及一个3元谓词Join，Rank(Join)=⟨l,p,p,0⟩。

术语和公式：正如我们在经典一阶逻辑中所做的那样，我们从字母表元素的有限字符串集合中选择L的表达式：术语和公式。唯一的区别是，在多类逻辑中，术语有类，我们必须指定它。

因此，多类逻辑的术语被递归地定义如下：每个变量或单个常数的类si都是同一类si的术语。如果f∈OperSym是这样的：Rank(f)=⟨i1,…,im,i0⟩，i0≠0，τ1,…,τm是类i1,...,im的术语，那么fτ1...τm是类i0的术语。

原子公式是通过谓词和术语来定义的。如果R∈OperSym是这样的：Rank(R)=⟨i1,…,im,0⟩，并且τ1,...,τm是类为i1,...,im的术语，那么Rτ1...τm就是一个公式（当R是一个自由谓词时，我们放弃对术语类的要求）。对于任何术语τ1和τ2，表达式τ1≈τ2是一个公式。注意，τ1和τ2的类并不重要，因为我们对等价符号的选择是自由的。

复合良好形式公式（wffs）的定义与一阶语言中的定义一样，但量化的表达式除外。新规则说：如果φ是一个公式，xi是一个i类的变量，那么∃xiφ也是一个公式。

自由变量和约束变量：与经典一阶逻辑一样，变量在公式中的出现可以是自由的，也可以是约束的；当它们处于量词的范围内时，它们是约束的，否则就是自由的。如果一个变量在公式中至少有一个自由出现，那么它就是自由的。

一个没有自由变量的公式被称为一个句子。我们用Sent(L)来表示语言L的句子集合。

理论：给定语言L的一组句子Γ，我们说Γ是一个理论，当且仅当它在推导下是封闭的；也就是说，对于每个φ∈Sent(L)，如果 Γ⊨φ 则φ∈Γ。

参考文献：

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:

∀x∀y(x≠y→∃X(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 f∈OperSym, its value Rank(f) always has the form ⟨i1,…,im,i0⟩, with i0,i1,…,im∈Sort∪{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 R∈OperSym 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[6] if and only if it is closed under consequence; that is, for every φ∈Sent(L): If Γ⊨φ

then φ∈Γ.