Knowledge 2
一、写在前面
我们上一篇写了命题逻辑，和命题逻辑中语义逻辑推理entailment部分内容，我们知道学习一个逻辑，包含两个部分，一个是语义推理，另一个就是形式推演deduction
二、形式推演deduction
我们在讲形式推演的时候，我们就不要去想这些符号的语义是什么？它就是一种形式上的推演。
形式推演规则很多，我们重点讲一套系统，这一套系统一共有11条规则。之后我们讲另外一套系统，另外一套只有1条规则。
这两套系统我们都可以证明他的完备性和可靠性。一套复杂的，一套简单的，复杂的我们不再证明完备性和可靠性。简单的我们会证明的。
备注：
1.∑ 指代我们之前 的 KB 知识库
2.A 另外一个合法的sen集合 指代之前的a，b
3.∑ |-A 表示推出，形式上推演
三、第一个形式推演系统（11条规则）
四、什么叫形式推演（形式可推演性）
当且仅当 能由有限次使用命题逻辑推演规则生成。同时最后一项是我们的想要证明的答案，序列中每一项都可以由规则中11条得到。
形式推演的例子：
逻辑推导（语义蕴含）VS 形式推演
五、哥德尔不完全定理
怎么说是一个好的logic ，我们说它即是sound正确，又是complete完备的，那么是一个好的logic。
在一个非常大的范围内，不存在这样的系统的，就是说我们没法构建一个数学大厦，自动推演其他的定理性质，这就是伟大的哥德尔不完备定理。