跳转到内容

一阶逻辑

本页使用了标题或全文手工转换
维基百科,自由的百科全书

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

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

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

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

简介

[编辑]

基本符号

[编辑]

命题逻辑顾名思义,会将“苏格拉底是哲学家”、“帕雷托是哲学家”之类直观上有真有假的叙述简记为 (也就是有真有假的命题),然后讨论 (非p)、(若p则q)、(p且q)与(p或q)之间的推理关系。

但一阶逻辑尝试从一些比较基础的词汇去建构“句子”,比如说,可用符号 代表 “ x 是哲学家”,也就是赋予断言符号语义的解释。这个解释默认一个“所有人类的群体”(也就是下面标准语义一节会说到的论域),并将变量 对应为自群体中取出来的某人。

以此类推,断言符号可以包含一个以上的变量。例如:可以将 解释为“ x 与 y 是夫妻”。

一阶逻辑类似于命题逻辑,可以将断言符号与 (非)、(则)、(且)和 (或)组成更复杂的叙述,例如:把断言符号 解释成“ 是学者”,那“若 x 为哲学家,则 x 为学者”可表示为:

但相较之下,一阶逻辑又加入了描述“所有”与“存在”的量词,比如说“对所有 x ,若 x 为哲学家,则 x 为学者”可记为:

也就是自左方开始阅读,将 解释成“对所有 x 有…”。 这个符号被称为全称量词

而对于“有 x 是哲学家”这一叙述,一阶逻辑则引入另一种量词:

也就是自左方开始阅读,将 解释成“存在 使…”。 这个符号被称为存在量词

顺带一提“并非所有 x 不是哲学家”等价于“有 x 是哲学家”;且“不存在 x 不是学者”也等价于“所有的 x 是学者”。所以可以用“否定”和“全称量词”来组合出“存在量词”。换句话说,可作以下的符号定义( 代表一段“叙述”):

相等

[编辑]

一阶逻辑也考虑到“相等”这个概念在叙述中的重要性,例如想表达“若所有是哲学家,那的长子也会是哲学家”,可先把 解释为 “ x 的长子”,那么这段叙述可记为:

换句话说, 被解释成“与 有特定且唯一对应关系”的某对象(被称为函数符号)。换句话话说,只要“就是”,那“的长子也会是的长子”。换句话说:

这些性质被一阶逻辑视为“理所当然”。

类似地,叙述中也有一些“不变的实体”,如苏格拉底,表示这些“实体”的符号被称为常数符号。例如将 解释为苏格拉底,那“苏格拉底为哲学家”就可以写成:

所谓的“不变”隐含的代表:

“苏格拉底就是苏格拉底”
“对所有x,对所有y,如果x就是苏格拉底,且y就是苏格拉底,那x就是y”

换句话说

这两个性质也被一阶逻辑视为“理所当然”。

形式理论

[编辑]

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

  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

在只以谢费尔竖线”为基础逻辑连接词的公理系统里,MP律会被改写成

修改的MP律 — 对于公式 组合出

公理

[编辑]

逻辑公理

[编辑]

公理 — 如果都是公式,则:

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

都是公理。

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

在有(A1)与(A2)的前提下,(A3)等价于以下的公理模式:(证明请参见下面否定一节。)

(T1) — 

另外,在只以谢费尔竖线”为基础逻辑连接词的公理系统里,上面三条公理模式等价于下面这条公理模式[3]

公理 — 如果 都是公式,则:

都是公理。

量词公理

[编辑]

公理 —  为任意变量, 为任意公式,则

  • (A4) 是一个项, 中出现的任意变量;若 里,自由的 都不在 的范围里(这样取代成 时才不会被 约束),则
为公理
其中 代表把 里自由的 都替换成 所得到的新公式。
  • (A5)如果 里完全被约束,则
为公理
  • (A6) 为公理
  • (A7) 若 是公理, 是任意变量,则
也是公理。

它们实际上也是公理模式

等式和它的公理

[编辑]

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

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

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

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

标准语义

[编辑]

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

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

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

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

项的取值

[编辑]

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

或较直观的符号

来表示。

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

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

真假的赋值

[编辑]

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

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

有序对子集合。

这样就可以依据语法的递归定义,以下面的规则对每条公式赋予真值。(这种赋值方式称为T-模式,取名于逻辑学家阿尔弗雷德·塔斯基)

元定义 — 在一套解释 下:

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

更进一步的来说

元定义 — #在一套解释 下,不管怎么样的变量取值,公式 都为真,则称为 为真,以符号 简记。若没有变量取值可以满足 ,则称 为假

  1. 若任意解释下公式 都为真,称 逻辑有效的(logically valid) (类似于命题逻辑恒真式
  2. 若一阶逻辑理论 的公理都于 为真,称解释 模型(model)

代数化语义

[编辑]

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

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

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

空论域

[编辑]

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

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

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

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

常用的推理性质

[编辑]

定理与证明

[编辑]

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

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

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

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

例如定理 的证明:

证明 — 

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

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

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

元定义 —  代表有一列公式 满足:

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

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

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

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

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

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

演绎元定理

[编辑]

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

元定理 — 
一阶逻辑理论 下,若有 ,则有

证明

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

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

所以由MP律有

,那因为

所以有

至此的部分证明完毕。

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

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

由公理A2有

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

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

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

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

元定理 — 
(D1)

(D2)

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

否定

[编辑]

以下的证明会分成使用(A3)的部分跟将公理(A3)取代为(T1)的部分,用以证明两者的等价性。

(DNe) Double negation, elimination — 

证明(使用A3)

(1) (A3)

(2) (I)

(3) (D2 with 1, 2)

(4) (A1)

(5) (D1 with 3, 4)

证明(使用T1)

(1) (A1)

(2) (Hyp)

(3) (MP with 2, 1)

(4) (MP with 3, T1)

(5) (MP with 4, T1)

(6) (MP with 2, 5)

(DNi) Double negation, introduction — 

证明(使用A3)

(1) (A3)

(2) (MP with DNe, 1)

(3) (A1)

(4) (D1 with 2,3)

证明(使用T1)

(1) (DNe)

(2) (MP with 1, T1)

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

(T1) Transposition-1 — 

证明(使用A3)

(1) (A3)

(2) (Hyp)

(3) (MP with 1, 2)

(4) (A1)

(5) (D1 with 3, 4)

(T2) Transposition-2 — 

证明(使用T1)

(1) (DN)

(2) (Hyp)

(3) (D with 1, 2)

(4) (DN)

(5) (D1 with 3,4)

(6) (T1, D)

(7) (MP with 5, 6)

注意到(T2)的证明引用了(T1)+(DN),但之前已经证明了(A1)+(A2)+(A3)可以推出(T1);还有(A1)+(A2)+(T1)也可以推出(DN),所以注明使用(T1)即可。

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

至此,已经可以证明(A1)+(A2)+(T1)可以推出(A3):

(T1)可推出(A3)的证明

MP律显然有

(1) (对上面的定理使用两次演绎元定理)

(2)(D1 with 1, T2)

(3)(MP with A2, 2)

(4)(MP with I, 3)

(5)(MP with T1, 4)

(6)(Hyp)

(7)(Hyp)

(8)(MP with T2, 7)

(9)(D1 with 6, 8)

(10)(D1 with DN, 9)

(11)(MP with 5, 10)

所以综合以上所述,在有(A1)+(A2)的前提下,公理(T1)等价于公理(A3)。

由(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 — 

逻辑与和逻辑或

[编辑]
且与或的交换性
[编辑]

以下为逻辑与的交换性

元定理 — 

证明

(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 — 

"或"也有类似的性质

(ASO-OR)Associativity of OR — 

且与或的分配律
[编辑]

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

(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) 若

等价代换

[编辑]

以下的定理,说明两条“等价”的公式可以互相代换

(Equv)Equivalence of WF — 
代表一群公式,若公式 满足:

则对变量 和任意公式

  1. 变量 完全被约束 ,则
证明
以下的证明都会用到这三条公式:

(a) (from

(b) (MP with AND, a)

(c) (MP with AND, a)

1.

(1) (MP with T, b)

(2) (MP with T, c)

(3) AND with 3, 5)

2.

()

(1) (Hyp)

(2) D1 with 1, b)

()

(1) (Hyp)

(2) D1 with 1, c)

3.

()

(1) (Hyp)

(2) (MP with T, 1)

(3) (MP with T, c)

(4) D1 with 2, 3)

(5) (MP with T, 4)

()

(1) (Hyp)

(2) (MP with T, 1)

(3) (MP with T, b)

(4) D1 with 2, 3)

(5) (MP with T, 4)

4.

()

(1)GEN with , a)

(2)(MP with A6 , 1)

()

(1)GEN with , c)

(2)(MP with A6 , 1)

这些定理通常是混合使用,以达到“等价代换”的结果,例如,考虑到“逻辑与”是以下的符号定义:

那如果假设 ,就有: