本页使用了标题或全文手工转换

一阶逻辑

维基百科,自由的百科全书
跳到导航 跳到搜索

一阶逻辑是使用于数学哲学语言学计算机科学中的一种形式系统

过去一百多年,一阶逻辑出现过许多种名称,包括:一阶断言演算低端断言演算量化理论谓词逻辑。一阶逻辑和命题逻辑的不同之处在于,一阶逻辑有使用量化变量。一个一阶逻辑,若具有由一系列量化变量、一个以上有意义的断言字母及包含了有意义的断言字母的纯公理所组成的特定论域,即是一个一阶理论

一阶逻辑和其他高端逻辑不同之处在于,高端逻辑的断言可以有断言或函数当做引数,且允许断言量词或函数量词的(同时或不同时)存在[1]。在一阶逻辑中,断言通常和集合相关连。在有意义的高端逻辑中,断言则会被解释为集合的集合。

存在许多对一阶逻辑是可靠(所有可证的叙述皆为真)且完备(所有为真的叙述皆可证)的演绎系统。虽然一阶逻辑的逻辑归结只是半可判定性的,但还是有许多用于一阶逻辑上的自动定理证明。一阶逻辑也符合一些使其能通过证明论分析的元逻辑定理,如勒文海姆–斯科伦定理紧致性定理

一阶逻辑是数学基础中很重要的一部分,因为它是公理系统的标准形式逻辑。许多常见的公理系统,如一阶皮亚诺公理和包含策梅洛-弗兰克尔集合论公理化集合论等,都可以形式化成一阶理论。然而,一阶定理并没有能力去完整描述及范畴性地建构如自然数实数之类无限的概念。这些结构的公理系统可以由如二阶逻辑之类更强的逻辑来获取。

简介[编辑]

不像命题逻辑只处理简单的陈述命题,一阶逻辑还额外包含了断言和量化

断言像是一个会传回真或伪的函数。考虑下列句子:“苏格拉底是哲学家”、“柏拉图是哲学家”。在命题逻辑里,上述两句被视为两个不相关的命题,简单标记为pq。然而,在一阶逻辑里,上述两句可以使用断言以更相似的方法来表示。其断言为Phil(a),表示a是哲学家。因此,若a代表苏格拉底,则Phil(a)为第一个命题-p;若a代表柏拉图,则Phil(a)为第二个命题-q。一阶逻辑的一个关键要点在此可见:字符串“Phil”为一个语法实体,以当a为哲学家时陈述Phil(a)为真来赋与其语义。一个语义的赋与称为解释

一阶逻辑允许以使用变量的方法推论被许多组件共享的性质。例如,令Phil(a)表示a为哲学家,且令Schol(a)表示a为学者。则公式

表示若a为哲学家,则a为学者。符号被用来标记一个条件叙述。箭号的左边为假设,右边则为结论。此一公式的真值取决于标记成a的组件,及“Phil”和“Schol”的解释之上。

“对于每个a,若a为哲学家,则a为学者”之类形式的断言,需要同时使用变量及量化。再次,令Phil(a)表示a为哲学家,且令Schol(a)表示a为一学者,则一阶叙述

表示不论a代表什么,若a为哲学家,则a为学者。此处的全称量化)代表宣称对“所有”a的选择,括弧内的叙述皆为真的想法。

为了表明,声称“如果是一个哲学家然后是一个学者”是假的,一会显示有一些人是不是一个学者的哲学家。这与存在量词可以表示反诉 : 若想证明“若a为哲学家,则a为学者”此一宣称是错的,有些人会证明存在有些不是学者的哲学家。此一反论可以用存在量化来表示:

其中,

  • 是否定算符:为真当且仅当为假;换句话说,当且仅当a不是学者。
  • 是合取算符:表示a是哲学家且不是学者。

断言Phil(a)和Schol(a)都各只有一个参数。但一阶逻辑其实也可以表示具有一个以上参数的断言。例如,“存在一些人可以在任何时间被愚弄”可表示成

这里,Person(x)解释为x是人,Time(y)为y是某段时间,且Canfool(x,y)则为(人)x可在(时)y被愚弄。清楚地说,上述叙述表示至少存在一个人可以在任何时间被愚弄,这比“在任何时间,至少存在一个人可以被愚弄”的叙述要强。后者并不意味着,被愚弄的人在任何时间时上总是要是同一位。

量化的范围是由可以用来满足量化的对象所组成的集合(在本节中的一些非正式的例子里,量化的范围并没有被指定)。除了指定Person和Time等断言符号的意义,解释也必须指定一个非空集合,称为论域,做为量化的范围。因此,之类形式的叙述在一特定解释下称之为真,若在可用来赋予断言中符号Phil意义的解释所指定的论域里存在着对象。

语法[编辑]

一阶逻辑可分成两个主要的部分:语法决定哪些符号的组合是一阶逻辑内的合法表示式,而语义则决定这些表示式之前的意思。

词汇表[编辑]

和英语之类的自然语言不同,一阶逻辑的语言是完全角式的,因为可以机械式地判断一个给定的表示式是否合法。存在两种合法的表示式:“项”(直观上代表对象)和“公式”(直观上代表可真或伪的断言)。一阶逻辑的项与公式是一串符号,这些符号一起形成了这个语言的词汇表。如同所有的形式语言一般,符号本身的性质不在形式逻辑讨论的范围之内;它们通常只被当成字母及标点符号。

一般会将词汇表中的符号分成“逻辑符号”(总有相同的意思)及“非逻辑符号”(意思依解释不同而变动)。例如,逻辑符号总是解释成“且”,而绝不会解释成“或”。另一方面,一个非逻辑断言符号,如Phil(x),可以解释成“x是哲学家”、“x的个名为Philip 的人”或任何其他的1元断言,单看其解释为何。

逻辑符号[编辑]

词汇表中存在若干个逻辑符号,虽然会因作者而异,但通常包括:

  • 量化符号
  • 逻辑联结词条件双条件否定。偶尔还会包括一些其他的逻辑联结词。某些作家会使用或Cpq来表示,用或Epq来表示,特别是文中被拿去做其他用途之时。更多地,也有用来表示,用来表示,用(~)、Np或Fpq来表示,用||或Apq来表示,以及用&或Kpq来表示,尤其是这些符号因技术上的原因无法输入时。
  • 括号、方括号及其他标点符号。此类符号的选择依文章不同而有所不同。
  • 无限集的变量,通常标记为英文字母末端的小写字母xyz、…,也常会使用下标来区别不同的变量:x0x1x2、…。
  • 一个等式符号= 。详见下面的“等式”一节。

需注意,并不是所有的符号都需要,只要有量化符号的其中一个、否定及且、变量、括号及等式就足够了。还存在许多定义了额外逻辑符号的变体:

  • 有时也会包括真值常数,用T、Vpq来表示“真”,并用F、Opq来表示“假”。若没有此类零参数的逻辑算符,这两个常数就只能用量化来表示。
  • 有时也会包括额外的逻辑联结词,如谢费尔竖线、NAND及异或

非逻辑符号[编辑]

非逻辑符号用来表示论域上的断言(关系)、函数及常数。以前标准上会对所有不同的用途使用相同的无限集的非逻辑符号,而最近则会根据应用的不同而使用不同的非逻辑符号。因此变得需要枚举出使用于一特定应用中的所有非逻辑符号。其选择是经由标识来形成的。

传统的做法是对所有的应用都只有单一个无限集的非逻辑符号。因此,根据传统的做法只会存在一种一阶逻辑的语言。这种做法现在依然很常见,尤其是在哲学方面的书籍。

  1. 对每个整数n ≥ 0,皆存在一组n断言符号。因为这些断言符号表示n个元素间的关系,因此也称为关系符号。对每个参数量n,皆能有无限多个断言符号:#:Pn0, Pn1, Pn2, Pn3,…
  2. 对每个整数n ≥ 0,皆存在无限多个n函数符号
    f n0, f n1, f n2, f n3,…

在当代的数理逻辑里,标识会因应用的不同而不同。数学里的典型标识,在里为{1, ×},或只为{×};在有序域里为{0, 1, +, ×, <}。并没有限制非逻辑符号的数量,标识可以是的、有限、无限,甚至是不可数的。例如,在勒文海姆–斯科伦定理的证明之中即会出现不可数的标识。

根据最近的做法,每个非逻辑符号皆为下列两种类型的其中一种。

  1. 具有0个或0个以上参数的断言符号(或关系符号)。通常标记为大写字母PQR、…。
    • 0参数的关系可以视同为命题变量。例如可以代表任何叙述的P
    • P(x)为具有1个参数的断言变量,其中一个可能的解释为“x是个人”。
    • Q(x,y)为具有2个参数的由词变量,其中一些可能的解释有“x大于y”或“xy的父亲”。
  2. 具有0个或0个以上参数的函数符号。标常标记为小写字母fgh、…。
    • 举例来说,f(x)可以解释成“x的父亲”;在算术里,可代表“-x”;在集合论里,可代表“x幂集”。gx,y)在算术里可代表“x+y”;在集合论里,可代表“xy的并集”。
    • 0参数的函数符号也称为常数符号,常标记成英文字母前端的字母abc、…。a可代表“苏格拉底”;在算术里,可代表0;在集合论里,可代表空集。

如何分辨断言符号与函数符号?

  • 断言符号将定义域D映射到值域{0,1}或{True,False}。
  • 函数符号将定义域D映射到D,没有维度的变化。

形成规则[编辑]

形成规则定义一阶逻辑的项及公式。因为项及公式被表示为一串符号,这些规则可被用来写成项及公式的形式文法。这些规则通常是上下文无关的(规则的每个结果在其左侧都会有单一个符号),除非允许有无限多符号,且有许多开始符号,如中的变量。

[编辑]

可依如下规则递归地定义:

  1. 变量。每个变量皆是项。
  2. 函数。每个具有n个参数的表示式ft1,...,tn,其中每个参数ti是项,且f是具有n个参数的函数符号)是项。另外,常数符号是0参数的函数符号,因此也是项。

只有可经由有限次地应用上述规则来得到的表示式才是项。举例来说,不存在包含断言符号的项。

公式[编辑]

公式(或称合式公式)可依如下规则递归地定义:

  1. 断言符号。若P是一个n元断言符号,且t1, ..., tn是项,则P(t1,...,tn)是公式。
  2. 等式。若等式符号算是逻辑的一部分,且t1t2是项,则t1 = t2是公式。
  3. 否定。若φ是公式,则φ是公式。
  4. 二元联结词。若φ及ψ是公式,则(φ ψ)是公式。其他的二元逻辑联结词也可相似的规则。
  5. 量化。若φ是公式,且x是变量,则都是公式。

只有可经由有限次地应用上述规则来得到的表示式才是公式。由头两个规则得到的公式称为原子公式

举例来说,

是公式,若f是1元函数符号,P是1元断言符号,且Q是3元断言符号。另一方面,则不是公式,虽然这也是由词汇表中的符号组成的字符串。

定义中的括号,其用途是为了确保任何公式都只能依递归定义以单一种方法得到(换句话说,每一个公式都只存在唯一的剖析树)。这个性质被称为公式的唯一可读性。对于括号要用在公式中的哪里存在有许多的惯例。例如,有些作者会使用冒号或句号来代替括号,或变更括号插入的地方。但每个作家个人的定义都必须证明会满足唯一可读性。

定义公式的规则无法定义“若-则-否则”函数ite(c,a,b),其中的c是个以公式表示的条件,当c为真时传回a,为假时传回b。这是因为断言和函数都只能接受项当做其参数,但上述函数的第一个参数为公式。某些建构在一阶逻辑上的语言,如SMT-LIB 2.0,会增加此一定义。[2]

标示惯例[编辑]

为了方便起见,会约定逻辑算符的优先性,来减少括号使用的情况。这些规则和算术中的运算顺序很像,一个常见的惯例为:

  • 最先赋值;
  • 下一个为先赋值;
  • 再下一个为量化先赋值;
  • 则最后赋值。

此外,定义中不需要的额外标点符号也许会插入公式中,使公式更容易阅读。因此,公式

可写成

在某些领域里,常见使用中缀表示法来代表二元关系及函数,而非上面定义的前缀表示法。例如,在算术中,一般会写成“2+2=4”,而非“=(+(2,2),4)”。一般会将以中缀表示法表示的公式当做是以前缀表示法表示的对应公式的缩写。

上面定义中的二元联结词,如,是使用中缀表示法。一个较少见的惯例为波兰表示法,它将等放在参数的前面而非之间。这个表示法允许舍弃所有的标点符号。波兰表示法是简洁且优雅的,但因为对人类很难阅读,所以实务上不常使用。使用波兰表示法,公式

会变成"∀x∀y→Pfx¬→ PxQfyxz"

自由变量和约束变量[编辑]

在一个公式里,变量可能是自由的或约束的。直观上来看,一个变量在公式里若没有被量化则是自由的:在里,变量x是自由的,而y则是约束的。自由变量和约束变量可依如下规则递归地定义:

  1. 原子公式。若φ是原子公式,则x在φ里是自由的,当且仅当x出现在φ里。更甚之,在原子公式中不存在约束变量。
  2. 否定xφ里是自由的,当且仅当x在φ里是自由的。xφ里是约束的,当且仅当x在φ里是约束的。
  3. 二元联结词x在(φ ψ)里是自由的,当且仅当x在φ或ψ里是自由的。x在(φ ψ)里是约束的,当且仅当x在φ或ψ里是约束的。相同的规则也适用于其他的二元联结词之上。
  4. 量化xy φ里是自由的,当且仅当x在φ里是自由的,且x是个和y相异的符号。而且,xy φ里是约束的,当且仅当xyx在φ里是约束的。相同的规则也适用于之上。

举例来说,在x y (P(x) Q(x,f(x),z))里,xy是约束变量,z是自由变量,而w则两者皆不是,因为它没有出现在公式之中。

自由和约束也可以用来专指在公式里特定地方出现的变量。如在里,第一个x是自由的,而第二个则是约束的。换句话说,x里是自由的,而在里则是约束的。

在一阶逻辑中,一个没有自由变量的公式称为一阶句子。此类公式在特定解释之下即会有良好定义的真值。例如,公式Phil(x)是否为真需看x代表什么,而句子在一特定解释下则必为真或必为假。

例子[编辑]

有序阿贝尔群的语言有一个常量0,一个一元函数−,一个二元函数 +,和一个二元关系≤。所以

  • 0, x, y原子项
  • +(x, y), +(x, +(y, −(z)))是,通常写为x + y, x + yz
  • =(+(x, y), 0),≤(+(x, +(y, −(z))), +(x, y))是原子公式,通常写为x + y = 0, x + y - zx + y
  • (∀xy ≤( +(x, y), z))∧(∃x =(+(x, y), 0))是公式,通常写为 (∀xy x + yz)∧(∃x x + y = 0)

语义[编辑]

一阶语言的解释会对语言内的所有非逻辑常数赋予上意义,同时也决定能指明量化范围的论域。其结果为,每个项都会被赋予其代表的组件,每个句子也都会被赋予上一个真值。这样,解释即对语言内的项及公式提供了语义。研究形式语言的解释的学科称为形式语义学

论域D是由某种类型的“对象”所组成的非空集合。直观上来看,一阶公式是有关这些对象的叙述。例如,叙述存在一个对象x,能使得指涉此对象的断言P为真。论域即是此类考量的对象的集合,例如可取D为整数的集合。

函数符号的解释是函数。举例来说,若论域由整数所组成,则一个2元的函数符号f能解释为给出其参数之和的函数。换句话说,符号f和在此解释下为加法的函数I(f)是相关连的。

常数符号的解释是一个从单元素集合D0映射至D的函数,也可简单视为是D内的一个对象。例如,一个解释可将值赋予常数符号

n元断言符号的解释是由论域中的元素所组成的n对有序集。这意味着,给定一个解释、一个断言符号及论域中的n个元素,则可依给定的解释判断这些元素的断言是否为真。例如,一个2元断言符号P的解释I(P)可以是一对整数,能使得第一个整数小于第二个整数。依据这个解释,断言P在其第一个参数小于第二个参数时为真。

一阶结构[编辑]

指定一个解释的最常见方法是指定一个结构(或称做模型,见下文)。结构包括一个由论域及标识内的非逻辑项的解释I所组成的非空集合。这个解释自身是个函数:

  • 每个n元函数符号f都会赋予一个从映射至的函数I(f)。特别地是,每个标识内的常数符号都会被赋予论域中的一个个体。
  • 每个n元断言符号P都会赋予一个在上的关系I(P)(或等价地说,一个从映射至的函数)。因此,每个断言符号都被D上的布尔值函数所解释。

真值的赋值[编辑]

一个公式由给定的解释及将论域中的元素与每个变量相关连的变量赋值μ来决定为真或为假。需要变量赋值的原因是为了给予具自由变量的公式(如)意义。上述公式的真值为何要看xy是否标记着相同的个体。

首先,变量赋值μ可以扩展到语言内的所有项,使每个项都能映射至论域中的单一元素。下列的规则被用来得到赋值:

  1. 变量。每个变量x皆可得到μ(x)。
  2. 函数。给定一组项(这些项皆已得到论域中的元素)及一个n元函数符号f,则项可得到

再来,每个公式皆可赋予一个真值。用来得到赋值的递归性定义称为T-模式

  1. 原子公式(1)。公式是依靠(其中为项的赋值,且的解释)来决定其值是真是假。
  2. 原子公式(2)。公式为真,若得到论域中的相同对象(见下面等式一节)。
  3. 逻辑联结词 及等形式的公式是依据联结词的真值表(如命题逻辑一般)来赋值的。
  4. 存在量化。公式根据解释M和变量赋值μ为真,若存在一个只和μ在对x的赋值上有所不同的变量赋值μ',能使得φ根据解释M和变量赋值μ'为真。此一形式定义是由“为真,当且仅当存在一种选择x的方法,使得φ(x)为真”的这个概念来的。
  5. 全称量化。公式根据解释M和变量赋值μ为真,若φ(x)根据每个只和μ在对x的赋值上有所不同的变量赋值μ'及解释M为真。此一形式定义是由“为真,当且仅当每一种选择x的方法,皆能使φ(x)为真”的这个概念来的。

若一个公式不包含自由变量,即为一个句子,则一开始的变量赋值不会影响其真值。换句话说,一个句子根据M为真,当且仅当这个句子根据M及其他的变量赋值为真。

还有第二种常见的做法可以定义真值,而且不需要依靠变量赋值函数。给定一个解释M,首先将一组常数符号加至标识之中,每一个在M中的论域的元素对应一个常数符号:称对每个域论中的元素d,都会固定有一个常数符号cd。如此,解释就会被扩展至能使每一新的常数符号被赋予至其对应的论域元素上。现在可语法性地定义量化公式的真值如下:

  1. 存在量化。公式根据M为真,若存在某些在论域中的d,使得为真。这里,是用cd取代每个φ内以自由变量出现的x所得到的公式。
  2. 全称量化。公式根据M为真,若对每个论域中的d,根据M皆为真。

这个做法对所有的句子会给出和使用变量赋值的做法一样的真值。

有效性、可满足性及逻辑结论[编辑]

若句子φ在一给定解释M下为真,则称M 满足φ,标记为。一个句子称为可满足的,若存在某个解释使其为真。

具自由变量的公式的可满足性就较为复杂了,因为只用解释并无法决定此类公式的真值。一个常见的惯例是称一个具自由变量的公式在一个解释下为可满足的,若不论如何将论域中的个体赋予其自由变量,这个公式皆为真。这等价于称公式为可从足的,当且仅当其全称闭包为可满足的。

一个公式是逻辑有效的(或简单称为有效的),若在每一个解释之下皆为真。此类的公式和命题逻辑中的重言式扮演着相似的角色。

一个公式φ是公式ψ的逻辑结论,若每个使得ψ为真的解释皆会使得φ为真。在此一状况下,称φ被ψ逻辑蕴涵着。

代数化[编辑]

另一种赋予一阶逻辑语义的方法可经由抽象代数处理。这种方法是将命题逻辑的林登鲍姆-塔斯基代数扩展而成。有如下几种类型:

这些代数都是纯粹扩展两元素布尔代数而成的

塔斯基和葛范德于1987年证明,没有超过包在三个以上的量化内的原子句子的部分一阶逻辑,其表示力和关系代数相同。上述部分一阶逻辑令人十分地感到有兴趣,因为它已足够表示皮亚诺算术公理化集合论,包括典型的ZFC。他们亦证明了,具有简单有序对的一阶逻辑和具有两个有序的投影函数的关系代数等价。

一阶理论、模型及基本类[编辑]

一阶理论是由在一特定一阶标识内的一组公理所组成的。公理所组成的集合通常是有限的或递归可枚举的,此类的理论称为是有效的。有些作者要求理论也要包括所有由公理导出的逻辑结论。

满足给定理论内的所有句子的一阶结构称为此理论的模型基本类是由所有满足特定理论的结构所组成的集合。这些类是类型论里的研究主题。

许多理论都有一个预期解释,即一个在研究理论时会在意的某种模型。例如,皮亚诺公理预期解释是由一般的自然数和其一般的运算所组成的。不过,勒文海姆–斯科伦定理证明,大多数的一阶理论也都会有其他的非标准模型

一个理论是兼容的,若不可能由这个理论的公理中证明出矛盾来。一个理论是完备的,若对每个其标识内的公式,此公式或公式的否定会是个由理论公理导出的逻辑结论。哥德尔不完备定理证明,有效的一阶理论只要它强到足以蕴涵自然数的理论,即无法同时是兼容且完备的。

空论域[编辑]

上述定义需要任何一个解释的论域均为非空集合。但在如自由逻辑之中,设置空论域是被允许的。更甚之,若代数结构的类包含一个空结构(如空偏序集),当允许空论域时,这个类只能是一阶逻辑中的一个基本类,不然就要将空结构由类中移除。

不过,空论域存在着一些难点:

  • 许多常见的推理规则只在论域被要求是非空时才为有效的。一个例子为,当x不是内的自由变量时,会蕰涵。这个用来将公式写成前束范式的规则在非空论域中是可靠的,但在允许空论域时则是不可靠的。
  • 在使用变量赋值函数的解释中,真值的定义不能和空论域一起运作,因为不存在范围为空的变量赋值函数。(相似地,也无法将解释赋予上常数符号。)在甚至是原子公式的真值可被定义之前,都必须选定一个变量赋值函数。然后一个句子的真值即可在任一个变量赋值之下定义出其真值,且可证明其真值不依选定的赋值而变。这个做法在赋值函数不存在时不能运作;除非将其改成配上空论域。

因此,若空论域是被允许的,通常也必须被视成特例。不过,大多数的作家会简单地将空论域由定义中排除。

代换[编辑]

t是项。φ(x)是可能包含x作为自由变量的公式。

φ(t)可定义为把自由变量x替代为t的结果,但前提是必须没有任何t在φ(x)中是约束的

若非如此,则x替代成t之前,必须先把φ中的约束变量,改为不同于t的符号。

例如把公式φ(x)假定为∀y:yx("x是极大的")。

若用t代换x,则φ(t)即∀y:yt就表示t是极大的。

这里举个错误的例子,若在φ(x)中含有约束变量y的状况下,不去修改φ(x)中含有约束变量y,直接把x代换成y,代换结果如下

y:yy

如此一来即成为跟φ(x)意义完全不同的公式。

正确的演算方法为先把φ(x)中的约束变量用到y的地方改成不同于y的符号,好比z

即把∀y:yx改成∀z:zx,这两命题的意义一致。

再把x代换成y,即为∀z:zy

所以φ(y)表示∀z:zy,而不是∀y:yy

忘记这个条件是声名狼籍的犯错误原因。

推理规则[编辑]

肯定前件充当推理的唯一规则。

叫做全称普遍化的推理规则是断言演算的特征。它可以陈述为

如果

这里的Z(x)假定表示断言演算的一个已证明的定理,而∀xZ(x)是它针对于变量x的闭包。断言字母Z可以被任何断言字母所替代。

公理[编辑]

下面描述一阶逻辑的公理。如上所述,一个给定的一阶理论有进一步的非逻辑公理。下列逻辑公理刻画了本文的样例一阶逻辑的一种演算[3]

对于任何理论,知道公理的集合是否可用算法生成,或是否存在算法确定合式公式为公理,是很有价值的。

如果存在生成所有公理的算法,则公理的集合被称为递归可枚举的。

如果存在算法在有限步骤后确定一个公式是否是公理,则公理的集合被称为递归的或“可判定的”。在这种情况下,你还可以构造一个算法来生成所有的公理:这个算法简单的(随着长度增长)一个接一个的生成所有可能的公式,而算法对每个公式确定它是否是个公理。

一阶逻辑的公理总是可判定的。但是在一阶理论中非逻辑公式就不必需如此。

量词公理[编辑]

下列四个公理是断言演算的特征:

  • PRED-1:
  • PRED-2:
  • PRED-3:
  • PRED-4:

它们实际上是公理模式:表达式W表示对于其中任何wff,x不是自由的;而表达式Z(x)表示对于任何wff带有额外的约定,即Z(t)表示把Z(x)中的所有x替代为项t的结果。

等式和它的公理[编辑]

在一阶逻辑中对使用等式(或恒等式)有多种不同的约定。本节总结其中主要的。不同的约定对同样的工作给出本质上相同的结果,区别主要在术语上。

  • 对等式的最常见的约定是把等号包括为基本逻辑符号,并向一阶逻辑增加等式的公理。等式公理是
x = x
x = yf(...,x,...) = f(...,y,...)对于任何函数f
x = y →(P(...,x,...) → P(...,y,...))对于任何关系P(包括 = 自身)
  • 其次常见的约定是把等号包括为理论的关系之一,并向这个理论的公理增加等式的公理。在实际中这是同前面约定最难分辨的,除了在没有等式概念的不常见情况下。公理是一样的,唯一的区别是把它叫做逻辑公理还是这个理论的公理。
  • 在没有函数和有有限数目个关系的理论中,有可能以关系的方式定义等式,通过定义两个项st是相等的,如果任何关系通过把s改变为t 在任何讨论下都没有改变。例如,在带有一个关系∈的集合论中,我们可以定义s = t为∀x (sxtx) ∧ ∀xxsxt)的缩写。这个等式定义接着自动的满足了关于等式的公理。
  • 在某些理论中有可能给出特别的等式定义。例如,在带有一个关系 ≤的偏序的理论中,我们可以定义s = tstts的缩写。

断言演算[编辑]

断言演算是命题演算的扩展,它定义了哪些一阶逻辑的陈述是可证明的。它是用来描述数学理论的形式系统。如果命题演算用一组合适的公理和一个单一的推理规则肯定前件来定义(可以有很多不同的方式),则断言演算可以通过增加一些补充的公理和补充的推理规则"全称普遍化"来定义。更精确地说,断言演算采用的公理有:

  • 来自命题演算的所有重言式(命题变量被替代为公式)。
  • 上面给出的量词公理。
  • 上面给出的等式公理,如果等式被认为是逻辑概念的话。

一个句子被定义为是在一阶逻辑中可证明的,如果可以通过从断言演算的公理开始并重复应用推理规则"肯定前件"和"全称普遍化"来得出它。

如果我们有一个理论T(在某些语言中叫做公理的陈述的集合),则一个句子φ被定义为是在理论T中可证明的,如果

ab ∧ ... → φ

在一阶逻辑中对于理论T的某个公理a, b,...的有限集合是可证明的。

可证明性的一个明显问题是它好像非常特别:我们采用了显然随机的公理和推理规则的搜集,不清楚是否意外的漏掉了某个关键的公理或规则。哥德尔完备性定理确保这实际上不是问题:这个定理声称在所有模型中为真的任何陈述在一阶逻辑中都是可证明的。特别是,在一阶逻辑中"可证明性"的任何合理定义都必须等价于上述定义(尽管在不同的可证明性的定义下证明的长度可能有巨大差别)。

有很多不同(但等价)的方式来定义可证明性。前面的演算是"希尔伯特风格"演算的一个典型例子,它有许多不同的公理但只有非常少的推理规则。"根岑风格"断言演算有非常少的公理但有许多推理规则。

文法上说断言演算在现存的命题演算上增加了“断言-主词结构”和量词。主词是给定的个体群组(集合)的一个成员的名字,而断言是在这个群组上的关系,一元断言在哲学中称为性质,在数学中称为指示函数,在数理逻辑中称为布尔值函数

可证明的恒等式[编辑]

可能增加的推理规则[编辑]

一阶逻辑的元逻辑定理[编辑]

下面列出了一些重要的元逻辑定理。

  1. 不像命题演算,一阶逻辑是不可判定性的。对于任意的公式P,可以证实没有判定过程,判定P是否有效,(参见停机问题)。(结论独立的来自于邱奇图灵。)
  2. 有效性的判定问题是半可判定的。按哥德尔完备性定理所展示的,对于任何有效的公式P, P是可证明的。
  3. 一元断言逻辑(就是说,断言只有一个参数的断言逻辑)是可判定的。

转换自然语言到一阶逻辑[编辑]

用自然语言表达的概念必须在一阶逻辑(FOL)可以为为其效力之前必须被转换到FOL,而在这种转换中可能有一些潜在的缺陷。在FOL中,意味着“要么p要么q要么二者”,就是说它是“包容性”的。在英语中,单词“or”有时是包容性的(比如,“加牛奶或糖?”),有时是排斥性的(比如,“喝咖啡或茶?”,通常意味着取其中一个或另一个但非二者)。类似的,英语单词“some”可以意味着“至少一个,可能全部”,有时意味着“不是全部,可能没有”。英语单词“and”有时要按“or”转换(比如,“男人和女人可以申请”)。 [4]

一阶逻辑的限制[编辑]

所有数学概念都有它的强项和弱点;下面列出一阶逻辑的一些问题。

难于表达if-then-else[编辑]

带有等式的FOL不包含或允许定义if-then-else断言或函数if(c,a,b),这里的c是表达为公式的条件,而a和b是要么都是项要么都是公式,并且它的结果是a如果c为真,或者b如果它为假。问题在于FOL中,断言和函数二者只接受(“非布尔类型”)项作为参数,而条件的明确表达是(“布尔类型”)公式。这是不幸的,因为很多数学函数是依据if-then-else而方便的表达的,而if-then-else是描述大多数计算机程序的基础。

在数学上,有可能重定义匹配公式算子的新函数的完备集合,但是这是非常笨拙的。[5] 断言if(c,a,b)如果重写为就可以在FOL中表达,但是如果条件c是复杂的这就是笨拙的。很多人扩展FOL增加特殊情况断言叫做“if(条件,a, b)”(这里a和b是公式)和/或函数“ite(条件,a, b)”(这里的a和b是项),它们都接受一个公式作为条件,并且等于a如果条件为真,或b如果条件为假。这些扩展使FOL易于用于某些问题,并使某类自动定理证明更容易。[6] 其他人进一步扩展FOL使得函数和断言可以在任何位置接受项和公式二者。

类型(种类)[编辑]

除了在公式(“布尔类型”)和项(“非布尔类型”)之间的区别之外,FOL不包括类型(种类)到自身的概念中。 某些人争辩说缺乏类型是巨大优点 [7],而很多其他人发觉了定义和使用类型(种类)的优点,比如帮助拒绝某些错误或不想要的规定 [8]。 想要指示类型的那些人必须使用在FOL中可获得的符号来提供这种信息。这么做使得这种表达更加复杂,并也容易导致错误。

单一参数断言可以用来在合适的地方实现类型的概念。例如:

断言Man(x)可以被认为是一类“类型断言”(就是说,x必须是男人)。 断言还可以同指示类型的“存在”量词一起使用,但这通常应当转而与逻辑合取算子一起来做,比如:

(“存在既是男人又是人类的事物”)。

容易写成,但这将等价与(“存在不是男人的事物或者存在是人类的事物”),这通常不是想要的。类似的,可以做一个类型是另一个类型的子类型的断言,比如:

(“对于所有x,如果x是男人,则x是哺乳动物)。

难于刻画有限性或可数性[编辑]

Löwenheim–Skolem定理得出在一阶逻辑中不可能刻画有限性或可数性。例如,在一阶逻辑中你不能断言实数的集合的上确界性质,它声称实数的所有有界的、非空集合都有上确界;这就需要二阶逻辑了。

图可及性不能表达[编辑]

很多情况可以被建模为节点和有向连接(边)的。例如,效验很多系统要求展示不能从“好”状态触及到“坏”状态,而状态的相互连接经常可以建模为图。但是,可以证明这种可及性不能用断言逻辑完全表达。换句话说,没有断言逻辑公式f,带有u和v作为它的唯一自由变量,而R作为它唯一的(2元)断言符号,使得f在一个有向图中成立,如果在这个图中存在从关联于u的节点到关联于v的节点的路径。[9]

参考文献[编辑]

引用[编辑]

  1. ^ Mendelson, Elliott. Introduction to Mathematical Logic. Van Nostrand Reinhold. 1964: 56. 
  2. ^ The SMT-LIB Standard: Version 2.0, by Clark Barrett, Aaron Stump, and Cesare Tinelli. 存档副本. [2012-04-07]. (原始内容存档于2012-03-14). 
  3. ^ For another well-worked example, see Metamath proof explorer
  4. ^ Suber, Peter, Translation Tips, [2007-09-20] 
  5. ^ Otter Example if.in, [2007-09-21] 
  6. ^ Manna, Zohar, Mathematical Theory of Computation, McGraw-Hill Computer Science Series, New York, New York: McGraw-Hill Book Company: 77–147, 1974, ISBN 0-07-039910-7 
  7. ^ Leslie Lamport, Lawrence C. Paulson. Should Your Specification Language Be Typed? ACM Transactions on Programming Languages and Systems. 1998. http://citeseer.ist.psu.edu/71125.html
  8. ^ Rushby, John. Subtypes for Specification. 1997. Proceedings of the Sixth European Software Engineering Conference (ESEC/FSE 97). http://citeseer.ist.psu.edu/328947.html
  9. ^ Huth, Michael; Ryan, Mark, Logic in Computer Science, 2nd edition: 138–139, 2004, ISBN 0-521-54310-X 

来源[编辑]

外部链接[编辑]

参见[编辑]