[音乐] 嗨，你好，欢迎回来。
我们接着呢介绍这个形式系统。
那么我们说，这个重言式呢反应了人类逻辑思维的一些基本的规律。
比如说，像排中律，它就是任意的 公式A∨¬A，它是跟 t 是逻辑等价的。
那就说明排中律是一个永恒的真理。
那么，比如说，矛盾律 A∧¬A是跟
f 就跟force是逻辑等价，这就说明了 自相矛盾，这是不符合逻辑的。
还有呢像假言推理，这样的一个 逻辑蕴含式，它是说A∧（A→B）
如果这两个都同时成立的话，那么就必然会有B成立。
这个也是我们进行推理的一个过程。
还有呢，像归谬。
归谬呢，是说（A→B）同时呢如果B不成立的话， 那么，A就肯定不成立。
那么这一个呢，也是我们作为反证法的一种 推理的一种方式。
还有呢，穷举推理， 这个是说呢，（A∨B）也就是说A B，A或B成立。
然后呢，如果有（A→C）又有（B→C）的话，那么 C一定会成立，这是用穷举法来进行推理。
那么，我们在前面
用了真值计算以及代入原理、 替换原理进行这个逻辑推演的时候，
我们就发现了，实际上只用这样的工具，它是难以反应我们 人类的这个思维推理的一个过程的。
我们需要做把这个推理过程进行严格化的话，进行严密化的话，
就必须要建立严密的一个符号推理体系，这也就是前面我们说
需要像做计算一样，数学计算一样，进行推理。
那我们来看看这个形式系统。
那么形式系统呢，它总的来说是一个符号的体系，所以呢它会分成三个部分。
那么在形式系统当中的这个概念，它首先呢，它会用一些符号来表示上。
那么推理的过程，也就是符号变换的一个过程。
那么第二个部分，就是它会把一些若干最基本的一些符号，
也就是一些最基本的重言式作为基础，把这些重言式就称之为公理，就是 不证自明，就称之为公理。
然后呢在系统里面， 这个符号变换，如何变换呢？那么它也是有一些依据的。
那么这个依据就是有若干条规则， 这些规则呢，它要确保由重言式
还能够导出重言式，也就是说，能够从真理走向真理。
那么把这些规则称之为形式系统当中的推理规则。
那么，公理和推理规则 两个一起，那么它能够确保这个形式系统里面
由正确的前提总是能够得到正确的推理的结果。
这个一点非常重要。
那么在形式系统当中的这个推理过程， 我们就把它归成两个概念，一个是证明，一个是演绎。
首先我们来看证明，那么证明在形式系统里头，它是一个公式的一个序列。
公式序列A1，A2 一直到Am，这是包含了m公式的一个公式序列。
那么我们把这个公式呢，公式序列称之为最后一个公式，就是Am的一个证明。
那么它就必须要满足这样的一些条件，在序列当中的每一个公式Ai，
每一个公式，它呢，要么自身就是一个公理，
那么它就是正确的，要么呢，它是由排在它前面的，你看， j1 到
jk 是小样，也就是排在它前面的若干个公式用推理规则来推出来的。
那么如果这样的一个公式序列存在，也就是说这样的证明存在的话，
那么我们就把最后这样的一个，最后的公式Am
就称之为系统的定理，同时呢记作为推出Am。
那么当然，这个推出Am当中可以写上这个形式系统的名称。
或者呢你可以省略了它，可以简记为推出Am。
这样说明Am是一个定理，那接下来我们来看演绎。
我们知道这个演绎的推理过程呢，它是有一些假设条件或者说叫作前提条件，
所以我们把这些前提条件呢，把它归在一起， 成为一个公式集合，所以呢，我们设Γ是一个公式集合，
那么同样呢，它推理过程也是一个公式序列，也是A1，A2一直到Am。
那么把这个序列称之为最后这个公式Am Am以Γ为前提的演绎，那么，
这个序列呢，当中的每一个公式也需要满足一些条件。
第一条件就是，要么这个Ai这个公式呢，
它是Γ中的公式，也就说它本身就是我们假设的前提条件。
要么呢，它是永真的公理。
要么呢，它是由排在它前面的一些公式， 由推理规则来推得的。
我们看到的这个呢，就跟前面的证明其实挺相似的，它除了
还差这么一个Γ这个前提之外，其实其它的基本上大体是一样的。
那么如果有这样的公式序列，也就说有这样的演绎存在的时候，那么我们
把最后这个公式Am就称之为Γ的演绎结果，我们记作Γ推出Am。
当然可以写上形式系统的名称，也可以把它省略掉。
那么我们就会把这个Γ以及Γ的每一个成员都称之为
Am的前提，也就是Am成立的一个前提条件。
那么我们刚才也说了，
那么对比证明和演绎这两个定义，我们很容易得到结论，
也就说，证明实际上是演绎在Γ等于空集的时候，也就是说在没有任何前提条件就可以推出A- m的时候，
这么一个特例。
陈斌副教授
