不确定性的困惑与NP理论分享 http://blog.sciencenet.cn/u/liuyu2205 平常心是道

博文

简介多类逻辑(Many-Sorted Logic)

已有 581 次阅读 2023-3-2 00:50 |个人分类:解读哥德尔不完全性定理|系统分类:科研笔记

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


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


王浩在Wang1952)中介绍了多类逻辑的公理计算,他在其中对单类和多类的理论进行了比较。1967年,Solomon Feferman给出了多类逻辑的序列计算,不仅证明了其完备性,还证明了cut eliminationinterpolation theoremsFeferman 1968)。Feferman2008)总结了多类theorems 在模型理论中的一些应用。


1,例子:欧几里德几何的第一公理


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


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

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


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

Join(Yxy):=Y joins x and y


2,基本概念


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


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


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


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


Σ=Sort,OperSym,Rank 


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


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


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


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


原子公式是通过谓词和术语来定义的。如果ROperSym是这样的: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:

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[6] 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

上一篇:柏拉图学院
下一篇:简介Hilbert and Ackermann’s Principles of Theoretical Logic
收藏 IP: 194.57.109.*| 热度|

1 杨正瓴

该博文允许注册用户评论 请点击登录 评论 (0 个评论)

数据加载中...
扫一扫,分享此博文

Archiver|手机版|科学网 ( 京ICP备07017567号-12 )

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

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部