应用这些变形于第三个例子的表达式ＣｐＣＮｑＣＮＣｑｐｒ与ＣｑＣＮＣｑｐｒ我们得到：（α）ＣｐＣＮｑＣＮＣｑｐｒ～ＣｐＣＮＣｑｐＣＮｑｒ由Ⅵ；ＣｐＣＮＣｑｐＣＮｑｒ～ＣＮＣｑｐＣｐＣＮｑｒ由Ⅴ；ＣＮＣｑｐＣｐＣＮｑｒ～ＣｑｐＣＮｐＣｐＣＮｑｒ由Ⅲ；ＣｑｐＣＮｐＣｑＣＮｑｒ～ＣＮｑＣＮｐＣｐＣＮｑｒ，ＣｐＣＮｐＣｐＣＮｑｒ由Ⅳ。
（β）ＣｑＣＮＣｑｐｒ～ＣＮＣｑｐＣｑｒ由Ⅴ；ＣＮＣｑｐＣｑｒ～ＣｑｐＣＮｐＣｑｒ由Ⅲ；ＣｑｐＣＮｐＣｑｒ～ＣＮｑＣＮｐＣｑｒ，ＣｐＣＮｐＣｑｒ由Ⅳ。
这样ＣＣｐｑＣｑｐｐ化归为四个初等表达式：ＣＮｑＣＮｐＣｐＣCＮｑｒ，ＣｐＣＮｐＣｐＣＮｑｒ，ＣＮｑＣＮｐＣｑｒ与ＣｐＣＮｐＣｑｒ。
变形Ⅶ用于复杂前件出现在第四个位置或者更远的地方的所有那些情况。
这个变形允许我们减少前件的数目；事实上，ＮＣｐＮｑ与Ｋｐｑ的意思是一样的，并且Ｓ１２与Ｓ１３相应地都是输入定律与输出定律的另外的形式。
现在ＣＮＣαＮβγ，像ＣＫαβγ一样，只有一个前件，而其等值的表达式ＣαＣβγ有两个前件。
所以，如果一个复杂的表达式出现于第四个位置，如δ在ＣαＣβＣγＣδ∈中那样，我们相继应用Ⅶ和Ⅵ能够把它移至
-- 175
３２。化归为初等表达式A ３６１
第三个位置：
ＣαＣβＣγＣδ∈～ＣＮＣαＮＣγＣδ∈由Ⅶ；
ＣＮＣαＮβＣγＣδ∈～ＣＮＣαＮβＣδＣγ∈由Ⅵ。
从这个最后的表达式，我们由Ⅶ的逆向的应用（ｔｈｅ
ＣｏｎCｖｅｒｓｅ
ａｐｌｉｃａｔｉｏｎ）得到公式：
ＣＮＣαＮβＣδＣγ∈～ＣαＣβＣδＣγ∈由Ⅶ。
现在用Ⅵ和Ⅴ就易于将δ带到第一个位置：ＣαＣβＣδＣγ∈～ＣαＣδＣβＣγ∈由Ⅵ，ＣαＣβＣδＣγ∈～ＣαＣδＣβＣγ∈由Ⅴ。
重复地在两个方向应用变形Ⅶ我们能够把任何前件从第ｎ个位置移到第一个位置，如果它是复杂的，就用Ⅱ、Ⅲ与Ⅳ使之变形为一个简单表达式。
定理（ＴＢ）
的证明就这样完成了。
现在容易表明这个定理推出对于演绎理论Ｃ—Ｎ系统的判定的证明。
如果一个给定的表达式α已经被化归为若干初等表达式，而所有这些初等表达式都是真的，亦即，如果在它们的诸前件中有两个Ｐ与Ｎｐ型的表达式，那么α就是一个断定命题并必须加以断定。
另一方面，如果α已经化归成的初等表达式中，至少有一个表达式在其中没有两个前件是Ｐ与Ｎｐ型的，那么α必须被排斥。
在第一种情况下，我们能用断定命题Ｓ１—Ｓ１３来证明。
在第二种情况下，我们能够反驳它，除了用上面的断定命题外，还得加上两条新的：Ｓ１４。
ＣｐＣｐｑＳ１５。
ＮＣｐ，以及排斥的公理：
-- 176
４６１第五章 判定问题
PＳ１６。
Ｐ。
用两个例子来把这一点说清楚。
第一个例子：断定命题ＣｐＣｐｑｑ的证明。
这个断定命题必须首先化归为初等表达式。
这是由以下的分析（Ｌ）作出的：
ＣｐＣｐｑ～ＣＮＣｐＣｐｑｒ由Ⅰ；
ＣＮＣｐＣｐｑｒ～ＣｐＣＮＣｐｑｒ由Ⅲ；
ＣｐＣＮＣｐｑｒ～ＣＮＣｐｑＣｐｒ由Ⅴ；
ＣＮＣｐｑＣｐｒ～ＣｐｑＣＮｑＣｐｒ由Ⅲ；
ＣｐｑＣＮｑＣｐｒ～ＣＮｐＣＮｑＣｐｒ，ＣｑＣＮｑＣｐｒ由Ⅳ。
ＣｐＣｐｑｑ化归成的初等表达式是ＣＮｐＣＮｑＣｐｒ与ＣｑＣＮCｑＣｐｒ。
像所有曾应用过变形Ⅰ的表达式一样，这两个都有一个不在前件中出现的变项作为最后一个词项。
这样的表达式只有在它们有两个前件是Ｐ与Ｎｐ型的条件下，才能是真的，并且这类的任何表达式都能用变形Ⅴ，Ⅵ与Ⅶ化归为Ｓ１的一个代入式，一个断定命题的证明总必须由此开始。
这里就是所需要的推演：
Ｓ１。
ｑＣＮｑｒ×（１）
]（１）ＣｐＣＮｐＣＮｑｒ
Ｓ１０。
ｑＮｐ，ｒＣＮｑｒ×Ｃ（１）—（２）
]（２）ＣＮｐＣｐＣＮｑｒ
Ｓ１。
ｐＮｐ，ｑｐ，ｒＮｑ，ｓｒ×Ｃ（２）—（３）
]（３）ＣＮｐＣＮｑＣｐｒ
Ｓ１。
ｐｑ，ｑＣｐｒ×（４）
]（４）ＣｑＣＮｑＣｐｒ。
-- 177
３２。化归为初等表达式A ５６１
在（３）和（４）之中已得到了与我们的分析（Ｌ）之末达到的相同的初等表达式，现在我们用这些相继的变形所依靠的那些断定命题从它们进到其左方的等值式，这样，一步一步地，借助于Ｓ９，Ｓ６，Ｓ１０与Ｓ２，我们得到我们原来的断定命题：
Ｓ９。
ｒＣＮｑＣｐｒ×Ｃ（３）—Ｃ（４）—（５）
]（５）ＣＣｐｑＣＮｑＣｐｒ
Ｓ６。
ｐＣｐｑ，ｒＣｐｒ×Ｃ（５）—（６）
]（６）ＣＮＣｐｑＣｐｒ
Ｓ１０。
ｐＮＣｐｑ，ｑｐ×Ｃ（６）—（７）
]（７）ＣｐＣＮＣｐｑｒ
Ｓ６。
ｑＣＣｐｑ×Ｃ（７）—（８）
]（８）ＣＮＣｐＣｐｑｒ（８）
ｒＣｐＣｐｑ×（９）
]（９）ＣＮＣｐＣｐｑＣｐＣｐｑ
Ｓ２。
ｐＣｐＣｐｑ×Ｃ（９）—（１０）
]（１０）ＣｐＣｐｑ。
凭借这种方式，我们能够证明任何我们想要证明的断定命题。
第二个例子：表达式ＣＣＮｐｑｑ的反驳。
我们首先在以下分析的基础上把这个表达式化归为初等表达式：ＣＮｐｑ～ＣＮＣＮｐｑｒ由Ⅰ；ＣＮＣＮｐｑｒ～ＣＮｐｑＣＮｑｒ由Ⅲ；ＣＮｐｑＣＮｑｒ～ＣＮｐＣＮｑｒ，ＣｑＣＮｑｒ由Ⅳ；ＣＮｐＣＮｑｒ～ＣｐＣＮｑｒ由Ⅱ。
-- 178
６１第五章 判定问题
表达式ＣＣＮｐｑｑ就这样化归为两个初等表达式，ＣｑＣＮｑｒ与ＣｐＣＮｑｒ，其中第一个是一个断定命题，但第二个不是真的，因为它没有两个ｐ与Ｎｐ型的前件。
所以，导致这个不真的后果的表达式ＣＣＮｐｑｑ必须加以排斥。
我们根据给定的变形相继地应用断定命题Ｓ１，Ｓ５，Ｓ７与Ｓ３来从头开始这一反驳：
Ｓ１。
ｐＣＣＮｐｑ，ｑｒ×（１）
] ]（１）ＣＣＮｐｑＣＮＣＮｐｑｒ
Ｓ５。
ｐＣＮｐｑ×（１２）
]（１２）ＣＣＮＣＮｐｑｒＣＮｐｑＣＮｑｒ
Ｓ７。
ｐＮｐ，ｒＣＮｑｒ×（１３）
]（１３）ＣＣＮｐｑＣＮｑｒＣＮｐＣＮｑｒ
Ｓ３。
ｑＣＮｑｒ×（１４）
]（１４）ＣＣＮｐＣＮｑｒＣｐＣＮｑｒ。
现在我们必须反驳表达式ＣｐＣＮｑｒ；为此目的我们需要新的断定命题Ｓ１４与Ｓ１５以及排斥的公理。
Ｓ１４。
ｐＮＮＣｐ，ｑｐ×ＣＳ１５—（１５）
] ]（１５）ＣＣＮＣｐ（１５）×Ｃ（１６）—Ｓ１６c（P１６）ＣＮＣｐ
Ｓ１４。
ｐＣｐＣＮｐｑ，ｑＣＮＣｐ×ＣＳ１—（１７）
]（１７）ＣＣｐＣＮｐｑＣＮＣｐＣＮＣｐ（１７）×Ｃ（P１８）—（P１６）
（P１８）ＣＣｐＣＮｐｑＣＮＣｐ（P１８）×（P１９）ｐＣｐＣＮｐｑ，ｑＮＣｐ，ｒｐ]（P１９）ＣｐＣＮｑｒ
-- 179
３２。