杜国平

(中国社会科学院 哲学研究所， 北京 100732)

本文拟基于括号表示法[1-4]以二元联结词“合舍”作为唯一初始联结词，建立一个命题逻辑自然推演系统；严格给出关涉定理证明的“化归”定义，进而探讨定理机械证明的能行性步骤。

一、形式语言

定义1 形式语言LDP包括如下两类符号：

(1)命题符号：p1，p2，…，pn，pn+1，…；

(2)联结词符号：「，」。

形式语言LDP中初始联结词只有一对左右括号“「」”。

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

(1)单独的一个命题符号是公式；

(2)若符号串F、G是公式，则「FG」是公式。

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

联结词「FG」的语义可用真值表直观表示如下(表1)：

表1 联结词「FG」语义真值表

由此可见，「FG」就是F、G的合舍[5]。为了表达方便，定义引入如下一些缩写符号：

定义3

(A)=def「AA」

[AB]=def「「AA」「BB」」

=def「「AB」「AB」」

『AB』=def(「(A)B)」)=def「「「AA」B」「「AA」B」」

命题1 联结词“「」”对于二值真值函数其表达能力是足够的。

二、公理系统

以合舍作为初始联结词的命题逻辑自然推演系统NPD1包括如下5条推理规则：

规则D1D├D。简记为Ref。

规则D2 如果Σ├D，那么Σ,Σ′├D。简记为+。

规则D3 如果∑，A├B，且Σ├「BB」，那么Σ├「AB」。简记为「」+。

规则D4 如果Σ，「CC」├「AB」，并且Σ，「CC」├A，那么Σ├C。简记为「」l-。

规则D5 如果Σ，C├「AB」，并且Σ，C├B，那么Σ├「CC」。简记为「」r-。

规则D1、规则D2是通常的命题逻辑自然推理规则。规则D3、规则D4和规则D5这3条规则是关于唯一联结词括号“「」”的特征推理规则，其中规则D3是括号“「」”的引入规则，规则D4、规则D5是括号“「」”的消去规则，规则D4是括号左消去规则，规则D5是括号右消去规则。

三、只含初始联结词“「」”定理的推演

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