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

一阶逻辑

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

一阶逻辑是使用于数学哲学语言学计算机科学中的一种形式系统,也可以称为:一阶断言演算低端断言演算量化理论谓词逻辑。一阶逻辑和命题逻辑的不同之处在于,一阶逻辑包含量词

高端逻辑和一阶逻辑不同之处在于,高端逻辑的断言符号可以有断言符号或函数符号当做引数,且容许断言量词或函数量词[1]。在一阶逻辑的语义中,断言被解释为关系。而高端逻辑的语义里,断言则会被解释为集合的集合。

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

一阶逻辑是数学基础中很重要的一部分。许多常见的公理系统,如一阶皮亚诺公理冯诺伊曼-博内斯-哥德尔集合论策梅洛-弗兰克尔集合论都是一阶理论。然而一阶逻辑不能控制其无穷模型的基数大小,因根据勒文海姆–斯科伦定理康托尔定理,可以构造出一种"病态"集合论模型,使整个模型可数,但模型内却会觉得自己有“不可数集”。类似地,可以证明实数系的普通一阶理论既有可数模型又有不可数模型。这类的悖论被称为斯科伦悖论。但一阶的直觉主义逻辑里,勒文海姆–斯科伦定理不可证明[2],故不会有以上之现象。

简介[编辑]

在命题逻辑里,“苏格拉底是哲学家”、“帕雷托是哲学家”只能简单标记为

而一阶逻辑先将符号 解释为 “ 是哲学家”,然后以 代表苏格拉底; 代表帕雷托,则 对应到 对应到 。也就是赋予断言符号语义的解释,而这个解释默认一个“所有人类的群体”(也就是语义解释的论域),将变量 解释为自群体取出来的某人。

其实断言符号可以包含一个以上的变量,像是把 解释为“xy是夫妻”,这样

就解释成“苏格拉底和y是夫妻”。

一阶逻辑和命题逻辑相同,断言符号和变量还能与逻辑符号组成更复杂的叙述:如将断言符号 解释为 为学者。则“若x为哲学家,则x为学者”可表示为

而“对所有x,若x为哲学家,则x为学者”则记为

也就是自左方开始阅读,以 代表“对所有x”;将之理解为“对所有的x 右方的叙述为真。”而 这个符号称为 全称量词

直观上还会有“若所有x是哲学家,那x的长子也会是哲学家”这样"合理"的叙述,为此将 解释为 “x的长子”,那这段"合理"叙述可记为

这种解释为成与 有唯一对应的那个对象的符号,称为函数符号。而事实上这段直观为真的叙述,经过适当的扩展以后就是一阶逻辑其中的一条公理

而对于“有x是哲学家”,则引入另一种量词表记为:

自左方开始阅读,以 代表“存在x”;也就是解释为“有x使 右方的叙述为真”。而 被称为 存在量词。全称量词和存在量词一起被简称为量词

而直观上,“并非所有x不是哲学家”,和“有x是哲学家”是等价的;且“不存在x不是学者”也跟“所有的x是学者”在直观上也是等价的。所以只要有“否定”这个逻辑概念,那一阶逻辑就能以全称量词为基础,作以下的符号定义( 解释为 “否定”, 而 代表一段"叙述"):

而将存在量词定义为全称量词的衍伸。

形式理论[编辑]

一阶逻辑的形式理论可分成几个部分:

  1. 语法英语Syntax (logic):决定哪些符号组合是合式公式。(直观上的"文法无误的叙述")
  2. 推理规则:由合式公式符号组合出新合式公式的规则(直观上的"推理")
  3. 公理:一套合式公式(直观上的基本假设)

基本符号[编辑]

一套理论能容许多少符号,取决于人类以物理定律的能塑造多少符号。但以目前无法确知宇宙是不是有限,或是是否可无限制分割。虽然所有的公理化集合论都以量词的形式隐晦的承认无穷的存在(如ZF集合论的无穷公理),甚至以这样自然数意义上的无穷为基础,去建构出不可数的实数。但将之对应到现实,还是会回到同样的物理问题。

谨慎起见,以下各种类的符号没有特别声明,数量将会是有限个。

逻辑符号[编辑]

词汇表中存在若干个逻辑符号,通常包括:

  1. 量化符号
    某些作者[3]会把符号定义为:
    如此只需要做为基础符号。
  2. 逻辑联结词:以下为可能的表示符号,而波兰表示法下的逻辑连接词请参见逻辑运算的波兰记法
    • 否定
    • 条件
    • ||
    • 双条件
    某些作者[4]会作如下的符号定义:
    如此一来只需要否定条件做为基础符号。
  3. 标点符号:括号、逗号及其他,依作者的喜好有所不同。
    为了更有效的将括号做配对,通常还会采用大括号{ }中括号[ ]
  4. 至多跟自然数一样多的变量,通常标记为英文字母末端的小写字母xyz、…,也常会使用下标(或上标、上下标兼有)来区别不同的变量:x0x1x2、…。(特别注意c有时候会被当成常数符号而引起混淆)
  5. 等式符号:
    有作者会因为语义上解释"相等"的不同,而将等式符号视为双元断言符号、甚至是某种合式公式的简写。
  6. 符号相等:
    为了将符号识别上为等同和等式符号做区隔,某些作者[5]会额外采用这个符号。

注意并非所有的符号都需要,比如说比较极端的理论,因谢费尔竖线(或异或)的布尔代数完备性使得所有不含量词的逻辑公理可以以谢费尔竖线表述,而大幅减少基础的逻辑联结词。

另外,一些作者并没有将语义学形式理论划分清楚,而会将真值常数纳入符号的一环;用T、Vpq来表示“真”,并用F、Opq来表示“假”。

断言符号[编辑]

“他们两人是夫妻”,代表一个关于两个"对象"的断言,而“他是人”、“三点共线”显示了断言是容许一个──甚至多个对象,所以对于自然数 约定:

为一阶逻辑的合法词汇,它在直观上表示一个有 个"对象"的断言,称它为 元断言符号。下标的自然数 只是拿来和其他同为 元的断言符号作区别。

实用上只要有申明,不至于和其他词汇引起混淆的话,可以用任意的形式简写一个断言符号,如公理化集合论里的 就是一个双元断言符号,也可以用 冗长地表达。

函数符号[编辑]

“物体的颜色”、“夫妻的长子”说明了一列对象所唯一对应的对象。但不同的夫妻有不同的长子;不同的物体有不同的颜色。据此,形式上对于自然数 约定:

为一阶逻辑的合法词汇,直观上表示 个"对象"所对应到的东西,称它为 元函数符号。但特别注意这种"唯一对应"的直观想法,必须配上关于"等式"的性质(详见下面等式定理),才能在形式理论中被实现。

就像断言符号,不引起混淆的话,可以用任何的形式简写函数符号,如公理化集合论里的 是依据并集公理而定义的新函数符号(请参见下面“函数符号与唯一性”的章节),也可以冗长的表记为

常数符号[编辑]

“刻度0”、“原点”、“苏格拉底”是直观上"唯一不变"的对象。据此,对自然数 约定

为一阶逻辑的合法词汇,直观上表示一个"唯一不变"的对象。称为常数符号,同样的"常数的不变"需配上"等式"的性质(详见下面等式定理)才能被实现。

为了不和变量的表记混淆,常数符号一样可以用任何的形式简写,如公理化集合论里的 是根据空集公理和“函数符号与唯一性”的章节,而定义的新常数符号。亦可冗长的表示为

语法[编辑]

和自然语言(如英语)不同,一阶逻辑的语言以明确的递归定义判断一个给定的词汇是否合法。大致上来说,一阶逻辑以“项”代表讨论的对象,而对“项”的断言组成了最基本的原子(合式)公式;而原子公式和逻辑符号组成了更复杂的合式公式(也就是"叙述")。

[编辑]

“那对夫妻的长子的职业”、“”、“”代表变量可以与函数符号组成"更一般的对象"。据此形式上,递归地规定一类合法词汇——为:

  1. 变量常数是项。
  2. 全都是项,那 也是项。
  3. 项只能透过以上两点,于有限步骤内置构出来。

习惯上以大写的西方字母(如英文字母、希伯来字母、希腊字母)代表项,如果变量不得不采用大写字母,而跟会项引起混淆的话,需额外规定分辨的办法。

原子公式[编辑]

为了比较简洁的规定什么是合式公式,先规定原子公式为:(若 是项)

这样的形式。

公式[编辑]

一阶逻辑的合式公式(简称公式或 )以下面的规则递归地定义:

  1. 原子公式为公式。(美观起见,在原子公式外面包一层括弧也是公式)
  2. 为公式,则 为公式。
  3. 为公式,则 为公式。
  4. 为公式, 为任意变量,则 为公式。 (美观起见 ,也就是里面的量词有无外包括弧都是公式)
  5. 合式公式只能透过以上四点,于有限步骤内置构出来。

另外成对的中括弧跟大括弧,符号识别上视为成对的小括弧,而草书的大写西方字母为公式的代号。

举例来说,

是公式而

则不是公式。

而接下来只要对任意公式 与变量 ,做以下符号定义

(同样美观起见

这样所有的逻辑连接词与量词就纳入了合式公式的规范。

施用[编辑]

所谓的施用/作用,是以下公式形式的口语说法:(其中 都是公式)

  • 称为 施用于 上。
  • 称为 施用于 上。
  • 称为 施用于 上。
  • 称为 施用于 上。
  • 称为 施用于 上。
  • 称为 施用于 上。
  • 称为 施用于 上。

就好似运算符作用在它们身上。

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

量词所施用的公式被称为量词的范围(scope)。同一个变量在公式一般来说不只出现一次,若变量 出现在 的范围内,称这样出现的 不自由/被约束的 (not free/bounded);反过来说,不出现在 的范围内的某个 被称为自由的

例如,对于公式:

就是量词 的范围;而 里的 就是不自由的;反之 里的 就是自由的。

于公式 完全自由,意为于 出现的 都是自由的;反之,说 于公式 完全不自由/完全被约束,意为 内根本没有 ,或是 内没有自由的 。若 内所有的变量都完全不自由, 特称为封闭公式/句子(closed formula/sentence)。

括弧的简写[编辑]

括弧是为了保证语义解释符合预期,但太多的括弧书写不易,为此规定以下的"重构法"(反过来就是"简写法"),从表面上不合法的一串符号找出作者原来想表达的公式:

  • 若整串符号的括弧不成对,直接视为无法重构
  • (左至右)的施用顺序重构括弧。
  • 相邻的逻辑连接词或量词无法决定施用顺序的话,以右边为先。
  • 重构施用的顺序,以被成对括弧包住的部分为优先施用,其次才是落单的断言符号。

举例来说

的重构过程如下

  1. (优先施用
  2. (施用
  3. (最后施用

可以被重构为公式的一串符号则宽松的认定为"合式公式"。(最明显的例子就是合式公式最外层的括弧可以"省略")

波兰表示法[编辑]

波兰表示法将逻辑连接词前置于被施用的公式而非传统的中间。如果沿用以上的"施用顺序",这个表示法允许舍弃所有括弧。如公式

转成波兰表示法的过程如下

(转成波兰表示法的顺序)
(逻辑链接词的符号变换)

推理规则[编辑]

MP律[编辑]

对于公式

组合出

直观意义非常明显,就是p=>qp可以推出q

公理[编辑]

逻辑公理[编辑]

如果都是公式则

  • (A1)
  • (A2)
  • (A3)

都是公理。

它们实际上是公理模式,代表着"跟自然数一样多"条的公理。

量词公理[编辑]

以下的 为任意变量, 为任意公式。

  • (A4) 是一个项, 中出现的任意变量;若 里,所有 的的范围里都没有自由的 (这个情况称为 里项 是自由的),则
为公理
其中 代表把 里自由的 都取代为 所得到的新公式。
  • (A5)如果 里完全被约束则
为公理
  • (A6) 为公理
  • (A7) 若 是公理, 是任意变量则
也是公理。

它们实际上是公理模式

等式和它的公理[编辑]

根据不同作者的看法,甚至是理论本身的需求,“等式”在形式理论里可能是断言符号或是一段公式(如a等于b可定义为对所有的xx属于a等价于x属于b)。而如何刻划直观上“等式的性质”,有一开始就将“等式的性质”视为公理(模式),但也有视为元定理的另一套处理方法,以下暂且以公理模式的方式处理。以元定理处理的方法会在等式定理详述。

是一段变量 完全自由,且型式完全被确定的公式 的简写要求:

  • (E1) 对任意变量 为公理。
  • (E2) 对于任意变量 ,若在公式 中自由的 都不在 的范围内。若以 代表 某些(而非全部)自由的 被取代成 而成的新公式,则
为公理。

事实上这两个公理模式也确保了函数符号"唯一对应"和常数符号的"唯一性",但证明这些性质需要一些元定理,简便起见合并于下面的等式定理一节讲述。

标准语义[编辑]

一阶逻辑的标准语义源于波兰逻辑学家Alfred Tarski所著《On the Concept of Truth in Formal Languages》。根据上面语法一节,公式是由原子公式递归地添加逻辑链接词而来的,而原子公式是由断言符号与项所构成的。所以要检验一条公式在特定的论域下正不正确,就要规定项的取值,然后检验这样的取值会不会落在断言符号所对应的关系里。由此延伸出所有公式的"真假值"。

也就是一套一阶逻辑的语义解释,要包含

  1. 变量取值的论域
  2. 如何解释函数符号(为论域中的某个函数)与常数符号(为论域中的某特定元素),以便从特定的变量取值得出项的取值。
  3. 如何将断言符号与论域里的某关系做对应。

通常一套解释方法(简称为解释)会以代号 表示。

项的取值[编辑]

量词的解释需要指明变量取值范围的论域——也就是一个集合 。而变量可能跟自然数一样多,换句话说,所有变量在论域 取的值可以依序以自然数标下标——也就是一个在 取值的数列。如果以 的代号(不一定是变量本身的表示符号)来枚举变量,那么从 的某套变量取值就以

或较直观的符号

来表示。

一套解释 会将 元函数符号 解释成某个 函数;而常数符号 解释成特定的 (亦称为 的取值为 ),这样就可以用上面语法一节定义项的方式,递归地规定项的取值

在解释 下的某套变量取值下,一列项 的取值分别为 ,则这套变量取值下,项 的取值规定为

真假的赋值[编辑]

直观上要解释关系最直接的方法,就是枚举所有符合关系的对象;例如如果想说明夫妻关系,可以枚举所有 (老公, 老婆) 的双元有序对,但并非所有的人类有序对都会在这个关系中。

以此为基础,若以 代表所有以 中的元素构成的 元有序对的集合(也就是 笛卡尔积) ,那一套解释 会将 元断言符号 解释为一个

有序对子集合。

这样就可以依据语法的递归定义,以下面的规则对每条公式赋予真值。(这种赋值方式称为T-模式,取名于逻辑学家Alfred Tarski

在一套解释 下:

  • 在一套特定的变量取值下,一列项 的取值为 ,那 为真定义为
反之
则定义为假。
  • 在一套特定的变量取值下,“ 为真” 等价于 “ 为假”。
  • 在一套特定的变量取值下, 为真,意为“ 为假或是 为真。” (p=>q为假只有p为真且q为假的状况)
  • 在变量取值 下, 为真,意为“对所有的 于变量取值 下为真”。(也就是把变量 的取值换为论域的任意元素仍然为真)

更进一步的来说

  1. 在一套解释 下,不管怎么样的变量取值,公式 都为真,则称为 为真,以符号 简记。若没有变量取值可以满足 ,则称 为假
  2. 若任意解释下公式 都为真,称 逻辑有效的(logically valid) (类似于命题逻辑恒真式
  3. 若一阶逻辑理论 的公理都于 为真,称解释 模型(model)

代数化语义[编辑]

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

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

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

空论域[编辑]

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

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

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

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

常用的推理性质[编辑]

定理与证明[编辑]

以下介绍一些基本用语和符号

在一阶逻辑理论 下, 代表有一列公式 满足:

  1. 符号识别上为
  2. 所有的 有下列两种可能情况
  • 的公理。
  • 存在 使得 (也就是由前面的公式以MP律组合出来)

口语上会称公式 (或 ) 为 下的定理(theorem)。而这列 会称为证明

例如定理 的证明:

(公理A2)
(公理A1)
(公理A1)
加上MP律)
加上MP律)

以上其实是蕴含了无限多定理的元定理的证明(因为没有给出合式公式的明确形式)。方便起见,这种元定理还是会称为定理并以同样的形式来表达。

直观上的证明,总是会有一些"前提假设",对此,若以 代表一列有限数目的公式,那

代表有一列公式 满足:

  1. 符号识别上为
  2. 所有的 有下列三种可能情况
  • 的公理。
  • 中的其中一条公式。
  • 存在 使得 (也就是由前面的公式以MP律组合出来)

这样称 为在前提 下, 证明;或是说 推论结果

若要特别凸显 里的一条"前提条件" 对"证明过程"的重要性,可以用 的符号去特别凸显。若 里的公式枚举出来有 ,那亦可表示为

证明过程没有被引用的公式尽可能不写出来。另一方面从以上对于证明定义可以发现,依怎样的顺序枚举前提条件,对于证明本身是不会有任何影响的。

本节所介绍的符号,在引用哪个理论很显然的情况下, 的下标 可以省略。

实际的证明常常会"引用"别的(元)定理,严格来说,就是照抄(元)定理的证明过程,然后作一些修改使符号一致。为了节省证明的篇幅,引用时只会单单列出配合引用(元)定理所得出的公式(形式),并在后面注明引用的(元)定理代号。

演绎元定理[编辑]

从公理(A1)和(A2)会得出不但直观且实用的演绎元定理

(D)Metatheorem of Deduction:

一阶逻辑理论 下,若有 ,则有

证明

(注意这是元逻辑英语Metalogic下的证明):

假设 为条件所说 的证明,如果 里的公式或 的公理,那根据(A1)

所以由MP律有

,那因为

所以有

至此的部分证明完毕。

接下来要用归纳法;假设对 都有 。 若 是公理、或从 来的、或是根本就是 ,仿造上面 的部分就有

剩下没考虑的状况是由MP律组合出 的状况,也就是有 使

由公理A2有

套用归纳法的假设,加上MP律,就会发现

如此可以一路归纳到 也就是 的情况,故元定理得证。

因为 代表的是有限条公式,所以透过演绎元定理可以将证明过程必要的前提条件递归地移到 后,直到不需要任何前提为止;然后由MP律可以知道,若有 ,则有 ,如此一来透过演绎元定理搬到推论结果的合式公式,也可以任意的搬回来。所以 等价于某定理 。因此也会将 称为一个定理

而从演绎元定理和MP律,会有以下直观且实用的元定理

(D1)

(D2)

以下如果需要将引用的定理以演绎元定理进行"搬移",会省略掉搬移的过程并在搬移后得到的结果后标注(D)。如果引用以上的(D1)和(D2)也会省略过程,单有结果和代号标注。

否定[编辑]

(DNe) Double negation, elimination

证明

(1) (A3)

(2) (I)

(3) (D2 with 1, 2)

(4) (A1)

(5) (D1 with 3, 4)

(DNi) Double negation, introduction

证明

(1) (A3)

(2) (MP with DNe, 1)

(3) (A1)

(4) (D1 with 2,3)

上面两定理表达了双否定推理上等价于于原公式,引用两者任一会都以(DN)简写。

(T1) Transposition-1

证明

(1) (A3)

(2) (Hyp)

(3) (MP with 1, 2)

(4) (A1)

(5) (D1 with 3, 4)

(T2) Transposition-2

证明

(1) (DN)

(2) (Hyp)

(3) (D with 1, 2)

(4) (DN)

(5) (D1 with 3,4)

(6) (T1, D)

(7) (MP with 5, 6)

以上二定理表说明 推理上等价于 ,引用这两个定理中任一都以(T)表示。

由(T)可以得到形式上类似于公理(A3)的定理

(A3')

证明

(1) (A3)

(2) (T, D)

(3) (Hyp)

(4) (MP with 2, 3)

(5) (MP with 1, 4)

(6) (T, D)

(7) (Hyp)

(8) (MP with 6, 7)

(9) (MP with 5, 8)

实质条件[编辑]

以下的定理重现了实质条件的直观理解。

(M0)material condition

(也就是

证明

(1) (Hyp)

(2) (Hyp)

(3) (A3)

(4) (A1)

(5) (MP with 4, 1)

(6) (A1)

(7) (MP with 6, 2)

(8) (MP with 3,5)

(9) (MP with 8,7)

(M1)material condition

证明

首先注意到 (MP)

(1) (0, D)

(2) (T)

(3) (Hyp)

(4) (MP with 1, 3)

(5) (MP with 2, 4)

(6) (Hyp)

(7) (MP 5, 6)

(M2)material condition

证明

(1) (A1)

(2) (T)

(3) (MP with 1, 2)

(4) (Hyp)

(5) (MP with 3, 4)

(M3)material condition

证明

(1) (M0, D)

(2) (T)

(3) (MP with 1, 2)

(4) (Hyp)

(5) (MP with 3,4)

(6) (MP with 5, DN)

反证法[编辑]

(C1)Proof by Contradiction

证明

(1) (T, D)

(2) (Hyp)

(3) (MP with 1, 2)

(4) (Hyp)

(5) (MP with DN, 4)

(6) (MP with 3, 5)

(C2)Proof by Contradiction

证明提示:仿(C1)。

逻辑与逻辑或[编辑]

交换性[编辑]

以下为"且"的交换性

证明

(1) (C1, D)

(2) (T, D)

(3) (MP with 1,2)

类似的,(C2)正是"或"的"可交换性":

(C2, D)

直观意义[编辑]

"且"的直观意义是实质条件元定理的直接结果

(AND)Intuitive meaning of And:

(M1)

(M3)

(M2)

从(AND)和 的符号定义可知, 的证明可以拆成两部分;习惯上会以“( ) ”标示 部分的证明,而“( ) ”标示 部分的证明。

类似的,"或"的直观意义是(M0)跟(D)的直截结果

(OR)Intuitive meaning of OR:

(M0, DN)

(A1, D)

(D)

(交换性, D)

以下的定理则是(A3')的直截结果

(DisJ)Disjunction:

证明

(1) (Hyp)

(2) (Hyp)

(3) (D1 with 1, 2)

(4) (Hyp)

(5) (A3' with 3, 4)

结合律[编辑]

对于"且",展开符号定义后,可以从直观意义轻松地得到

(ASO-AND)Associativity of AND:

证明提示: (AND)

"或"也有类似的性质

(ASO-OR)Associativity of OR

证明提示: (M1), (M2), (M3)

分配律[编辑]

"且"和"或"之间还有分配律

(DIS-1)Distribution:

证明

(1) (Hyp)

(2) (MP with 1, AND)

(3) (MP with 1, AND)

(4) (Hyp)

(5) (MP with 4, DN)

(6) (D1 with 3, 5)

(7) (MP with 2, 5)

(8) (MP twice with 2, 7, AND)

也就是

再套用(D)就会得到

(1) (Hyp)

(2) (D1 with 1, AND)

(3) (D1 with 1, AND)

(4) (MP with 2, C2)

(5) (MP with 3, C2)

(6) (D1 with 4, AND)

(7) (D1 with 4, AND)

(8) (A3' with 6, I)

(9) (MP twice with 7, 8, AND)

也就是

(DIS-2)Distribution:

证明

(1)(Hyp)

(2) (D1 with 1, AND)

(3) (D1 with 1, AND)

(4)(MP twice with 2, 3,AND)

也就是

(1) (Hyp)

(2) (MP with 1, AND)

(3) (MP with 1, AND)

(4) (Hyp)

(5) (MP with 2,4)

(6) (MP with 3,4)

(7) (MP twice with 5, 6, AND)

也就是

再使用一次推论元定理会得到

德摩根定理[编辑]

以下的元定理的名字来自于英国逻辑学家奥古斯塔斯·德摩根

De Morgan I

证明

(1) (Hyp)
(2) (MP with 1, DN)
(3) (DN)
(4) (D1 with 2, 3)

(1) (Hyp)
(2) (DN)
(3) (D1 with 1, 2)
(4) (MP with DN, 3)

De Morgan II

证明

证明

(1) (Hyp)
(2) (MP with M2, 1)
(3) (MP with M3, 1)
(4) (AND with 2, 3)

(1) (Hyp)
(2) (Hyp)
(3) (M1)

普遍化元定理[编辑]

公理模式(A7)可以稍加延伸成以下的元定理

元定理(定理的普遍化):

对任意变量 ,若 则有

证明

假设 就是 的证明,那 一定是公理,根据(A7)可以得到

若对 都有 ,如果 是公理的话显然

若有 使得

那根据归纳法的假设跟(A6)有

上式配上

就可以得到

以此归纳到 也就是 ,故本元定理得证。

更进一步,有以下元定里

元定理普遍化, GEN):

里变量 都完全被约束,若

则有

证明

以下对前提条件的数量 做归纳。

,根据前提有

以(D)将 往前搬,再套用定理的普遍化,会得到

再根据(A5)和MP律,就可以得到

也就是本元定理要求的结果。

现在假设 的情况下元定理会成立。元定理的前提条件根据(D)可以写为

则根据归纳法的假设

上式配上(A5),本元定理在 的情况就可以得到证明,故本元定理得证。

(GEN)可以稍加修饰,以套用在含有存在量词的公式上

元定理(GENe):

若变量 的公式和 里都完全被约束则

(1) 若

(2) 若

证明提示:对(GEN)使用(T)和(A5)

量词的可交换性[编辑]

由普遍化,很容易证明以下关于"交换性"的定理

(1)

(2)

(3)

注意最后(3)一般来说是不能反向的,只要想到"对每个 ,都有一个数(也就是 ),使 ",但是任取一个 的数 和任意的数 并不一定会为零。

量词的简写[编辑]

数学中常常有 "对所有 有...",或是 "存在 使的..."。而两句话比较清晰,接近一阶逻辑语言的说法是 "对所有 ,只要 则..." 与 "存在 且..."。“大于”直观上是一个二元关系,也就是说,在公理化集合论里对应于一条 ( 或 ) 在里面完全自由的合式公式。据此,可做以下的符号定义

如果变量 都于合式公式 里完全自由,那

但直观上也会说 "对所有 有...",这样连续,带有条件的全称量词也是有"交换性"的。 为了讨论这个问题,首先需要一些前置的定理

(abb)

证明

注意到
(AND)
(AND)
所以
再套上演绎元定理就可以得证。

注意到
(AND)
所以
再套上演绎元定理就可以得证。

这样就可以证明以下定理

如果变量 都于合式公式 里完全自由,若项 里没有

证明

(1) (Hyp)
(2) (MP with 1, A4)
(3) (D1 with 2, A4)
(4) (MP with abb, 3)
(5) (GEN with 4 twice)

(1) (Hyp)
(2) (MP with 2, A4 twice)
(3) (MP with abb, 2)
(4) (GEN with 3)
(5) (MP with A5, 4)
(6) (GEN with 5)

如果再加上 "项 里没有 " 那就是 "对所有 有...",也就是以上所讨论的情况了。以这个定理配上全称量词本身的交换性定理,那这句话就可以等价的说成 "对所有 则...",所以根据"且"的可交换性,可以进一步的说成 "对所有 有...",所以连续带有条件的全称量词是"可交换的"。也就是说

如果变量 都于合式公式 里完全自由,若项 里没有 ,且项 里没有

但对于存在量词,仿造上面的证明过程,只能得出以下非等价的定理。

这是因为一般来说, 不总是能推出 。所以带有条件的存在量词是没有交换性的。

等式定理[编辑]

一般来说,等式 会被视为某个合式公式 的简写。若使用元定理的形式刻划等式的性质,会作如下的定义

说一阶逻辑理论 相等符号 意为( 都是 的任意变量)

  • 除了变量 是完全自由外其他变量都完全被约束
  • (E1)
  • (E2') 不含函数符号与常数符号的原子公式 若以 表示 内某一个 被取代成 而成的新公式,则有
  • (E2") 若以 代表项 里的 被取代成 而成的新项,则有
  • (E3)

并在这种状况下,规定 的简写。

上面的定义符合函数符号直观上的"唯一对应"。为了证明常数符号的"唯一性",需要以下元定理

说一阶逻辑理论 带相等符号 ,等同于要求:

  • 除了变量 是完全自由外其他变量都完全被约束。
  • 符合(E1)。
  • (E2) 对于任意变量 ,若在公式 中自由的 都不在 的范围内。若以 代表 某些(而非全部)自由的 被取代成 而成的新公式,则
证明

从(E1)+(E2')+(E2")+(E3)推出(E2)的过程分成几个阶段推广(E2')

(1)含有常数符号的原子公式

为任意常数符号。目标是证明:对一段含常数符号 但不含任何函数符号的原子公式 ,若 里某一个 被取代为 的新公式,则
(a)
(a)证明过程如下:
取一个不曾在 出现的变量 。若以 表示 内的 被取代成 的新公式,将之带入 (E2')有
对上式,以变量 取(GEN)有
(b)
但从(A4)有
这样上式就可以与(b)式取MP,就会有(a)。

(2)含有任意项的原子公式

对一列项 ,若以 代表项 里的一个 被取代成 而成的新项,那这样可以用 代表 被取代成 所构成的新公式。那现在的目标是证明
(c)
但根据(A4)和(GEN),只需要证明
(c')
就足够了。更进一步的,由下面两定理可以推出(c')