三、自然演算系统

自然演算系统和公理系统不同。在公理系统中，只能从几个给定的公理出发，运用系统中的推理规则进行推演。

在自然演算系统中，不存在公理，可以从任意给定的前提出发，运用系统中的推理规则进行推演。

自然演算系统有不同的种类。不同的自然演算系统，给出的具体推理规则往往是不同的。现在介绍其中一个，称之为NP₁系统。

（一）初始符号

1.p，q，r，s，P₁，q₁，F₁，…

2.┓，V，Λ，→，↔

3.(,)

上述符号中，1类符号表示命题变项。2类符号表示命题联结词，其中，┓表示否定，V表示析取，Λ表示合取，→表示蕴涵，↔表示等值。括号是用来区别公式的结构关系的。

（二）形成规则

1.任何一个命题变项都是合式公式。

2.如果A是合式公式，则┓A是合式公式。

3.如果A和B是合式公式，则AVB，AΛB，A→B和A↔B都是合式公式。

4.只有符合以上三条规则的符号序列才是合式公式。

合式公式以下简称公式。

（三）推理规则

1.假设引入规则：在证明的任何步骤上，可以根据需要随时引入一个假设。

2.结论引入规则：在证明的任何步骤上，可以根据需要随时引入已证公式。

3.重复规则：在一个假设下出现的公式(包括假设），既可在该假设下重复出现，又可在随后的假设下重复出现。

4.蕴涵引入规则，简记为→₊：如果在前提公式的集合基础上，再加上一个假设A，进而可以推出B，那么，从这个前提公式的集合可以推出A→B。

5.蕴涵消除规则，简记为→_：从A→B和A，可以推出B。

6.合取引入规则，简记为Λ₊：从A和B，可以推出AΛB。

7.合取消除规则，简记为Λ_：从AΛB，可以推出A；从AΛB，可以推出B。

8.析取引入规则，简记为V₊：从A，可以推出AVB；从B，可以推出AVB。

9.析取消除规则，简记为V_：从AVB和┓A，可以推出B；从AVB和┓B可以推出A。

10.等值引入规则，简记为↔₊：从A→B和B→A，可以推出A↔B。

11.等值消除规则，简记为→_：从A↔B，可以推出A→B；从A↔B，可以推出B→A。

12.否定引入规则，简记为┓₊：在给定前提下，如果引入假设A，由此推出B和┓B，那么，由原来的前提可以推出┓A。

13.否定消除规则，简记为┓_：在给定前提下，如果引入假设┓A，由此推出B和┓B，那么，由原来的前提可以推出A。

（四）定理

以下列举一些定理及有关证明。

定理1：A→A

证明：

1 A 假设引入规则

2 A 重复规则

3 A→A 1，2，→₊

定理2：AΛB→A

证明：

1 AΛB 假设引入规则

2 A 1，Λ_

3 AΛB→A 1，2，→₊

定理3：AΛB→B

定理4：A→AVB

证明：

1 A 假设引入规则

2 AVB 1，V₊

3 A→AVB 1，2，→₊

定理5：B→AVB

定理6:(AVB)Λ┓A→B

证明：

1 (AVB)Λ┓A 假设引入规则

2 AVB 1，Λ_

3 ┓A 1，Λ_

4 B 2，3，V_

5 (AVB)Λ┓A→B 1，4，→₊

定理7：(AVB)Λ┓B→A

定理8：(A→B)ΛA→B

定理9：(A→B)Λ(B→A)→(A↔B）

证明：

1 (A→B)Λ(B→A) 假设引入规则

2 A→B 1，Λ_

3 B→A 1，Λ_

4 A↔B 2，3，↔₊

5 (A→B)Λ(B→A)→(A↔B) 1，4，→₊

定理10：(A↔B)→(A→B)

定理11：(A↔B)→(B→A)

定理12:（B→C)Λ(A→B)→(A→C)

证明：

1 (B→C)Λ(A→B) 假设引入规则

2 A 假设引入规则

3 A→B 1，Λ_

4 B→C 1，Λ_

5 B 3，2，→_

6 C 4，5，→_

7 A→C 2，6，→₊

8 (B→C)Λ(A→B)→(A→C) 1，7，→₊

定理13：┓┓A→A

证明：

1 ┓┓A 假设引入规则

2 ┓A 假设引入规则

3 ㄱㄱA 1，重复规则

4 ┓A 2，重复规则

5 A 2，3，4，┓_

6 ㄱㄱA→A 1，5，→₊

定理14：A→┓┓A

证明：

1 A 假设引入规则

2 ㄱㄱㄱA 假设引入规则

3 ㄱㄱA 假设引人规则

4 ㄱㄱㄱA 2，重复规则

5 ㄱㄱA 3，重复规则

6 ┓A 3，4，5，┓_

7 A 1，重复规则

8 ㄱㄱA 2，6，7，┓_

9 A→┓┓A 1，8，→₊

定理15：(A→B)Λ(A→┓B)→┓A

证明：

1 (A→B)Λ(A→┓B) 假设引入规则

2 A→B 1，Λ_

3 A→┓B 1，Λ_

4 A 假设引入规则

5 A→B 2，重复规则

6 A→┓B 3，重复规则

7 B 5，4，→_

8 ┓B 6，4，→_

9 ㄱA 4，7，8，┓₊

10 (A→B)Λ(A→┓B)→┓A 1，9，→₊

定理16：(A→B)→(┓B→┓A）

证明：

1 A→B 假设引入规则

2 ┓B 假设引入规则

3 A 假设引入规则

4 A→B 1，重复规则

5 B 4，3，→_

6 ┓B 2，重复规则

7 ㄱA 3，5，6，┓₊

8 ┓B→┓A 2，7，→₊

9 (A→B)→(┓B→┓ A) 1，8，→₊

定理17:(┓B→┓A)→(A→B)

定理18:(A→┓B)↔(B→┓A)

定理19：(┓A→B)↔(┓B→A)

定理20:(A→B)Λ┓B→┓A

定理21：((AVB)Λ(A→C)Λ(B→C))→C

证明：

1 (AVB)Λ(A→C)Λ(B→C) 假设引人规则

2 AVB 1，Λ_

3 A→C 1，Λ_

4 B→C 1，Λ_

5 ㄱ C 假设引入规则

6 A→C 3，重复规则

7 (A→C)Λ┓C→┓A 定理20，结论引入规则

8 (A→C)Λ┓C 6，5，Λ₊

9 ┓A 7，8，→_

10 AVB 2，重复规则

11 B 10，9，V_

12 B→C 4，重复规则

13 C 12，11，→_

14 ┓C 5，重复规则

15 C 5，13，14，ㄱ_

16 ((AVB)Λ(A→C)Λ(B→C))→C 1，15，→₊

定理22：AΛB↔BΛA

定理23:AVB↔BVA

证明：

先证AVB→BVA

1 AVB 假设引入规则

2 A→BVA 定理5

3 B→BVA 定理4

4 (A→BVA)Λ(B→BVA) 2，3，Λ₊

5 ((AVB)Λ(A→BVA)Λ(B→BVA))→BVA 定理21

6 (AVB)Λ(A→BVA)Λ(B→BVA) 1，4，A₊

7 BVA 5，6，→_

8 AVB→BVA 1，7，→₊

再证BVA→AVB,具体方法同上。

根据AVB→BVA和BVA→AVB以及↔₊，可以推出AVB↔BVA。

需要指出，在NP1系统的推导过程中，除了运用前面提出的推理规则，还可以引入“导出规则”。

导出规则的提出，是基于系统中的已证定理或形成规则。这些规则的运用，将会使有些推导过程明显简化。

在NP₁系统中，可以提出以下导出规则：

1.假言三段论规则：从B→C和A→B，可以推出A→C。

2.双重否定消除规则，简记为┓┓_：从┓┓A，可以推出A。

3.双重否定引入规则，简记为┓┓₊：从A，可以推出┓┓A。

4.否定后件规则：从A→B和┓B,可以推出┓A。

5.等值置换规则：如果A，B等值，那么，从Φ(A)可以推出Φ(A/B)；从Φ(B)可以推出Φ(B/A)。

其中，Φ表示任一合式公式，Φ(A)表示包含A的某一合式公式，Φ(B)表示包含B的某一合式公式，Φ(A/B)表示在(A)中用B替换A后得到的合式公式，Φ(B/A)表示在Φ(B)中用A替换B后得到的合式公式。

当然，随着已证定理的增多，还可以概括出其他一些导出规则，以供后面的证明使用。

下面以定理21为例，说明导出规则的引入可以使NP1系统的部分定理证明过程简化。

定理21：((AVB)Λ(A→C)Λ(B→C))→C

1 (AVB)Λ(A→C)Λ(B→C) 假设引入规则

2 AVB 1，Λ_

3 B→C 1，Λ_

4 A→C 1，Λ_

5 ┓C 假设引入规则

6 ┓A 4，5，否定后件规则

7 B 2，6，V_

8 C 3，7，→_

9 ㄱC 5，重复规则

10 C 5，8，9，ㄱ_

11 ((AVB)Λ(A→C)Λ(B→C))→C 1，10，→₊

四、命题演算系统的性质

构造形式系统的目的，在于用一种严密的方法来研究逻辑。所以，形式系统本身是否严密也就成为人们关注的问题。

有关逻辑系统本身的研究，称为元逻辑研究。就命题演算系统而言，此类研究涉及独立性、一致性、完全性等问题。

(一）独立性

一个命题演算系统具有独立性，当且仅当，该形式系统的公理之间彼此独立，即任何一个公理相对于系统中给定的推理规则，都不可能从其他公理推出。

针对一个具体的形式系统，独立性要求可以放宽。有的系统为了推演方便，所选取的公理往往会比较多，不管它们彼此是否独立，这种情况是允许的。

对自然演算系统而言，由于没有公理，所以也就不存在独立性问题。公理化命题演算系统P具有独立性。

（二）一致性

命题演算系统的一致性，可以有三种不同的定义：语义定义、语法定义和古典定义。

一个命题演算系统具有语义一致性，当且仅当，该系统的定理都是重言式。语义一致性也称可靠性。

一个命题演算系统具有语法一致性，当且仅当，并非任一合式公式都在该系统中可以证明。

一个命题演算系统具有古典意义下的一致性，当且仅当，不存在任何合式公式A，A和┓A都在该系统中可以证明。古典意义下的一致性，又称无矛盾性。

公理化命题演算系统P和自然演算系统NP1，具有以上三种定义下的一致性。同时，具有一致性也是逻辑学对任何一个形式系统提出的起码要求。

（三）完全性

命题演算系统的完全性，可以有不同的定义：语义定义、语法定义和古典定义。

一个命题演算系统具有语义完全性，当且仅当，一切重言式都在该系统中可以证明。

一个命题演算系统具有语法完全性，当且仅当，如果把一个该系统的不可证公式当作公理，那么，该系统就将是不一致的。

一个命题演算系统具有古典意义下的完全性，当且仅当，对于任一合式公式A而言，或者A可证，或者┓A可证。

公理化命题演算系统P和自然演算系统NP1具有语义完全性和语法完全性，但不具有古典意义下的完全性。