[音乐] 嗨，欢迎回来。
现在呢我们来看看ND当中的定理的证明。
我们先给出ND当中的定理，证明和演绎的这个定义。
那么在ND当中，我们称A是γ的演绎结果。
也就是说γ能够在ND当中导出A，或者说简记成 γ就导出A。
那么如果是这样子的话， 存在这么一个序列。
这些序列呢，它的每一项 都是象γ导出A，γ导出A这样的一个形式，就是
导出的左边是一系列的公式集合，然后右边呢是一个公式，这样的一个。
那么有 γ1，A1，γ2，A2，一直到γn，An，那么最后呢这个
γn呢是等于γ，然后An呢是应该等于A的。
存在这样的一个序列，而且呢这个序列当中的任何一个成分，
γi导出Ai，这样的形式呢，它需要具有这三个特点。
第一呢，或者它本身就是公理，那我们知道这个 ND当中只有一条公理，就是γ加上A能够导出A，这么一个公理。
然后或者呢，第二就是或者呢是这个γi，Ai是 放在它前面的某一个成分给它抄下来。
给它抄下来，就是或者是γj导出Aj，而j呢是小于i的， 它可以复制过来。
第三个呢，或者就是说 在这个i之前的，j1，j2一直到jk，
这个若干个成分使用这个推理规则导出来， 导出这个γi，然后推出Ai，这样的一个形式。
那么当然这个推理规则呢，就是我们前面所说的这个18条推理规则之一， 然后能够导出来它。
那么这样呢，我们就可以 把A称之为γ的一个演绎结果，就是γ能够导出A。
当然如果说有γ导出A，而且呢γ是一个空集，所以就是它没有任何的公式的话，
那么就把这个A呢就称之为ND当中的一个定理，A是ND的定理。
好，我们下面来看看，用ND证明一个定理的一个典型的过程。
我们证明一个定理，A∨上非A。
这是这个排中律，显然它是一个真理了对吧？
但是呢在ND当中需要证明，我们来证明一下看看。
第一，我们引入一个公理，就是A能导出A，这当然是一个公理。
因为公理的形式就是γ加上A能够导出A，我们只要把那个γ 呢变成一个空集，那么就有A导出A，这它确实是一个公理。
那第二呢，是一个∨引入的规则。
那么这样有右边有A，那我可以A∨上一个非A， 这也是没问题的。
就是从第1，公理 再加上∨的引入规则，我们得到了2。
然后第3呢，我们再抄一条公理，就是非A导出非A。
然后第4呢，再根据公理第3这个公理， 再用一次这个∨的引入，
那当然∨引入呢，就是非A再∨上一个A，那当然就是A∨非A这样的形式。
然后我们观察这个2和4这两条， 他们的右边都是一样的，但是左边呢是一个是A，一个是非A。
那这样呢最终我们就可以引用，对2和4引用一个假设消除规则。
那么这样呢，A和非A这些都可以去掉，那么最终呢我们就得到了
A∨上非A它是一个定理。
对吧，这就完成了这个整个定理的这个证明。
接下来我们证明另外一个定理。
就是任意x，然后A(x)蕴涵B(x)，再蕴涵着 任意x，任意xA(x)然后蕴涵着任意xB(x)。
这个实际上是FC当中的一个公理，是好像记得应该是A5吧。
这么一个公理。
但是公理呢，是FC当中的公理是需要在 ND当中再重现来证明一下，他并不是ND当中的公理，对吧？
好，我们来看看这个证明的过程。
首先呢，我们写下一个公理。
我们γ呢就设作是左边这两个公式，
那么左边这两个公式呢，搬出其中的一个，任意xA(x)把他搬到右边。
那么这当然是一个公理，对吧？ND当中的公理。
然后第2呢，我们用全称消除规则，把这个x呢换成t，这也是没问题的。
第3条也是一个公理。
那只不过是我们把第1个公式放到了右边。
这是一个公理。
第4条呢，是 也是同样的这个全称消除，我们把这个
第3条里边右边的这个x都换成t，都换成t，所以呢它会有导出，
A(t)蕴涵B(t)，这样。
所以接下来一条是 用第2条和第4条，你看我们有第2条，有第4条。
那么就可以用上 这个蕴含消除规则，那么直接就得到B(t)，直接得到B(t)。
然后呢接下来呢，我们又再紧接着引用 这个第5条，再加上一个全称的引入规则，
然后把B(t)呢变成任意xB(x)， 这是全称引入。
最后呢，我们用这个 蕴涵的引入，实际上就是把左边
γ当中的一个公式，任意xA(x)挪到右边，
然后呢再把左边呢再挪到右边，还是一个蕴涵引入规则。
那么最终呢，我们就得到了我们所要证明的这个定理。
当然ND呢也有一些重要的性质， 它跟这个FC和PC都类似。
那么实际上呢，FC或者说PC当中的这些公理和定理，
它实际上都是ND当中的定理，那么都可以象前面那个
A5的证明一样都可以得到，在ND当中得到证明。
当然ND呢，跟FC、 PC也是一样的，它也同样
是具有合理、 一致和完备性。
陈斌副教授
