数理逻辑

大一学离散数学时，zyj讲逻辑讲得又臭又长。 于是开始自学一部分，找了一本《面向计算机科学的数理逻辑》。 里面的内容由于我不是数学专业，不知道如何评价，但就是以CS的学生来说，它确实讲清楚了形式逻辑的由来和区别，这一点倒是很关键。

以下就说明一下这本书带给我的，对逻辑的感性的认识。

当前提的”真”蕴涵逻辑的真时，称其具有可推导性。 即”前提$\rightarrow$结论”的推理是正确的。 这就是演绎推理，研究可推导性关系。 可推导性追求的是逻辑形式(语法)，而非其实质内容(语义)。

当我们通过实质的内容，也就是真值表来分析命题间的可推导性关系时，也许我们能够通过形式化的推导来讨论命题间的可推导性关系。

这就将启发式地证明变成一个形式化规则的应用（有限次的生成）。这就是形式推演。但是这种推演必须要证明是可靠的。

• $\Sigma \vdash A \Longrightarrow \Sigma \vDash A$

也就是说，形式化的规则无法超出非形式的内容，形式化证明可靠。

• $\Sigma \vDash A \Longrightarrow \Sigma \vdash A$

即形式化的规则能够完备地反映非形式的证明。即完备。

抽象的转换需要可靠和完备的保证。