“不可得兼”型命题逻辑自然推演系统

杜国平

作为文化传承载体的自然语言——汉语有着丰富的逻辑联结词，其中表达“两者不可并立”关系的二元联结词就有“若A，则非B”“并非A且B”“AB 两者不可得兼”等[1]。如《孟子·告子上》：“鱼，我所欲也，熊掌，亦我所欲也，二者不可得兼，舍鱼而取熊掌者也。生，亦我所欲也，义，亦我所欲也，二者不可得兼，舍生而取义者也。”

本文拟基于括号表示法[2-5]，以二元联结词“不可得兼”作为唯一初始联结词，建立一个命题逻辑自然推演系统，并分析、探讨其与常用命题逻辑系统之间的关系。

一、形式语言

定义1.01 形式语言£DP包括如下两类符号：

（1）命题符号：p1，p2，…，pn，pn+1，…；

（2）联结词符号：（，）。

其中初始联结词只有一对左右圆括号“（）”。

定义1.02 形式语言£DP中的公式当且仅当有限次使用如下规则而得：

（1）单独的一个命题符号是公式；

（2）若符号串D、E 是公式，则（DE）是公式。

通常以大写字母A、B、C等表示任意的公式。£DP中所有公式的集合记为Form（£DP）。

“不可得兼”型联结词（AB）的语义可用真值表直观表示如下：

命题1.01 联结词（AB）对于二值真值函数其表达能力是完备的。

证明：

基始。对于任一一元二值真值函数，存在如下4 种可能：

不难验证：

Å1[A]=（（AA）A）

Å2[A]=（（AA）（AA））

Å3[A]=（AA）

Å4[A]=（（（AA）A）（（AA）A））①等式左边的方括号为通常的括号用法，等式右两边的圆括号为初始二元真值联结词。

归纳步骤。假设对于任一n 元真值函数均可由初始联结词“不可得兼”定义，则对于任一n+1元二值真值函数H[p1，p2，…，pn，pn+1]，有：

H[p1，p2，…，pn，pn+1]=（（pn+1H[p1，p2，…，pn，1]）（（pn+1pn+1）H[p1，p2，…，pn，0]））

不难验证：

若pn+1=1，则上式

若pn+1=0，则上式

不论在哪种情况下，均有左边=右边。

因此，定理得证。

由此可见，在表达能力上，括号“（AB）”与舍弗函数之一的析舍“A|B”[6]以及二元联结词“”等价，从真值表也可以看出这一点。但是，括号“（AB）”不再像析舍及二元联结词那样对于复杂的公式需要外加另外的符号如括号等来标志结合的先后顺序和层次等，其辖域是非常清楚的，因此比舍弗函数及联结词集{￢，∨}等表达更加简练。

二、自然推理规则

基于形式语言£DP的一个“不可得兼”型命题逻辑自然推演系统NP1包括如下5 条推理规则：

规则SR1 A ├A。简记为Ref。

规则SR2 如果Σ├A，那么Σ，Σ′├A。简记为+。

规则SR3 如果Σ，A，B ├C，且Σ，A，B ├（CC），那么Σ ├（AB）。简记为（）+。

规则SR4 如果Σ ├（（AA）B），并且Σ ├B，那么Σ ├A 。简记为（）r–。

规则SR5 如果Σ ├（AB），并且Σ ├A，那么那那么Σ ├（BB）。简记为（）l-。

规则SR1、规则SR2 是通常的命题逻辑自然推理规则。规则SR3、规则SR4 和规则SR5 这3条规则是关于唯一联结词括号“（）”的特征推理规则，其中规则SR3 是括号引入规则，规则SR4、规则SR5 是括号消去规则，规则SR4 是括号右消去规则，规则SR5 是括号左消去规则。

规则SR3 的直观意思是，若由前提 A、B 推出矛盾，则 A、B 不可得兼；规则SR4 的直观意思是，若B 与A 的否定不可得兼（即有B 则 A），且B 成立，则A 亦成立；规则SR5 的直观意思是，若A 与B 不可得兼，且A 成立，则B 不成立。

三、定理的推演

定义3.01 公式A 在系统NP1中由公式集Σ形式可推演，记为Σ├A，当且仅当Σ├A 能由有限次使用规则SR1-规则SR5 而生成。

引理3.01 若 A ∈Σ，则Σ├A。

该引理简记为∈。

引理3.02 若Σ├Σ′，且Σ′├C，则Σ├C。

（一）关于“否定”联结词

定理3.11 B├（（BB）（BB））。

证明：

这是双否引入律。

定理3.12

（1）Σ├（（BB）B）

（2）Σ├（B（BB））

证明：

（1）

（2）类似可证。

这是排中律。

定理3.13 若Σ，（BB）├C，且Σ，（BB）├（CC），则Σ├B。

证明：

这是反证律。

定理3.14 若Σ├（（BB）（BB）），则Σ├B。证明：

这是双否消去律。

定理3.15 若Σ，B├C，且Σ，B├（CC），则Σ├（BB）。

证明：

这是归谬律。

定理3.16 若Σ├B，且Σ├（BB），则Σ├C。

这是司各脱法则。

（二）关于“蕴涵”联结词

定理3.21 若Σ，A├B，则Σ├（A（BB））

证明：

这是演绎定理。

定理3.22 若Σ├（A（BB）），且Σ├A，则Σ├B。

证明：

这是与规则SR5 相应的另一种形式的左消去规则。

定理3.23 若Σ├（A（BB）），且Σ├（B（CC）），则Σ├（A（CC））。

证明：

这是蕴涵的传递律。

定理3.24 Σ├（A（（B（AA））（B（AA））））。

证明：

定理3.25 若Σ├（A（（B（CC））（B（CC）））），且Σ├（A（BB）），则Σ├（A（CC））。

证明：

定理3.26 Σ├（（A（（B（CC））（B（CC））））（（（A（BB））（（A（CC））（A（CC））））（（（A（BB））（（A（CC））（A（CC））））））

证明：

定理3.27 若Σ├（AB），并且Σ├B，那么Σ├（AA）。

证明：

这是与规则SR4 相应的另一种形式的右消去规则。

定理3.28

（1）若Σ，（AA）├B，则Σ，（BB）├A；

（2）若Σ，A├（BB），则Σ，B├（AA）；

（3）若Σ，（AA）├（BB），则Σ，B├A；

（4）若Σ，A├B，则Σ，（BB）├（AA）。

证明：

（1）

（2）（3）（4）类似可证。

这是假言易位律。

定理3.29 Σ├（（（AA）（BB））（（（（AA）B）（AA））（（（AA）B）（AA））））。

证明：

（三）关于“析取”联结词

定理3.31 若Σ├（AB），且Σ├（A（BB）），则Σ├（AA）。

证明：

定理3.32 若Σ├（AB），且Σ├（（AA）B），则Σ├（BB）。

证明：

定理3.33

（1）若Σ├（AA），则Σ├（AB）；

（2）若Σ├（BB），则Σ├（AB）。

证明：

（2）类似可证。

定理3.34 若Σ├（AB），则Σ├（BA）。

证明：

定理3.35 若Σ，（AA）├C，且Σ，（BB）├C，则Σ，（AB）├C。

证明：

（四）关于“合取”联结词

定理3.41

（1）若Σ├（（AB）（AB）），则Σ├A；

（2）若Σ├（（AB）（AB）），则Σ├B。

证明：

（1）

（2）类似可证。

定理3.42 若Σ├A，且Σ├B，则Σ├（（AB）（AB））。

证明：

（五）关于“等值”联结词

定理3.51

（1）Σ，A，（（AB）（（AA）（BB）））├B；

（2）Σ，B，（（AB）（（AA）（BB）））├A。

证明：

（1）

（2）类似可证。

定理3.52

（1）Σ，A，B├（（AB）（（AA）（BB）））；

（2）Σ，（AA），（BB）├（（AB）（（AA）（BB）））。

证明：

（1）

（2）类似可证。

四、系统NP1 和常见系统之间的关系

为了使表达更加简洁，下面引入若干定义符号。

定义4.11

根据上述定义，前述相关定理可简记为（相应的定理使用原序号加“′”表示）：

定理3.11′ B├<>。

定理3.12′

定理3.13′ 若Σ，├C，且Σ，├，则Σ├B。

定理3.14′ 若Σ├<>，则Σ├B。

若把看作B 的否定，则定理3.11′—定理3.14′分别清晰地表述了双否引入律、排中律、反证律和双否消去律。

特别地，有：

定理3.24′ Σ├「A 「B「A」」」。

定理3.26′ Σ├「「A 「BC」」「「AB」「AC」」」

定理3.29′ Σ├「「B」「「」A」」。

定理3.22′ 若Σ├「AB」，且Σ├A，则Σ├B。

如所知，下列公理和推理规则构成了一个常见的只含联结词否定和蕴涵的命题逻辑公理系统：

公理1：A →（B →A）

公理2：（A →（B →C）→（（A →B）→（A →C））

公理3：（￢A →B）→（（￢A →￢B）→A）

推理规则：若A →B，且A，则B。

将定理3.24′、定理3.26′、定理3.29′和定理3.22′与上述公理及推理规则相比，不难发现其中除了联结词的符号差异之外，两者在推理功能方面并无二致。

如所知，下列推理规则构成了一个常见的只含联结词否定和蕴涵的命题自然推理系统：

规则1 A├A。

规则2 若Σ├A，则Σ，Σ′├A。

规则3 若Σ，A├B，则Σ├A→B。

规则4 若Σ├A→B，且Σ├A，则Σ├B。

规则5 若Σ，￢A├B，且Σ，￢A├￢B，则Σ├A。

将规则SR1、规则SR2、定理3.21、定理3.22和定理3.13 与上述推理规则相比，不难发现其中除了联结词的符号差异之外，两者在推理功能方面并无差别。

由此可知，系统NP1和常见的命题逻辑推理系统是等价的。因此，系统NP1相对于经典的二值语义具有可靠性和完全性。

由此可见，仅仅使用一对括号就可以建立基于“不可得兼”型联结词的逻辑推理系统，括号表示法极大地简化了构建逻辑系统所需的初始联结词，括号表示法也可以比较直观地、有效率地（不需要使用其他辅助的句法符号）表达各种逻辑推理规律。