《离散数学》的学习已经过去蛮久了，突然发现还有一些简单概念又变得模糊起来。这里区分小记Mark一下。

数理逻辑，是用数学方法研究逻辑或形式逻辑的学科，属形式逻辑形式上符号化、数学化的逻辑，本质上仍属于知性逻辑的范畴。 数理逻辑又称符号逻辑、理论逻辑。它既是数学的一个分支，也是逻辑学的一个分支。其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。数理逻辑是基础数学的一个不可缺少的组成部分。虽然名称中有逻辑两字，但并不属于单纯逻辑学范畴。

广义上，数理逻辑包括集合论、模型论、证明论、递归论。这里我们先介绍它的两个最基本的也是最重要的组成部分，就是“命题演算”和“谓词演算”。

命题演算是研究关于命题如何通过一些逻辑连接词构成更复杂的命题以及逻辑推理的方法。 命题是指具有具体意义的又能判断它是真还是假的句子。

谓词演算也叫做命题涵项演算。 在谓词演算里，把命题的内部结构分析成具有主词和谓词的逻辑形式，由命题涵项、逻辑连接词和量词构成命题，然后研究这样的命题之间的逻辑推理关系。

数理逻辑和计算机科学有许多重合之处，两者都属于模拟人类认知机理的科学。许多计算机科学的先驱者既是数学家、又是逻辑学家，如阿兰·图灵、邱奇等。

程序语言学、语义学的研究从模型论衍生而来，而程序验证则从模型论的模型检测衍生而来。

柯里——霍华德同构给出了“证明”和“程序”的等价性，这一结果与证明论有关，直觉逻辑和线性逻辑在此起了很大作用。λ演算和组合子逻辑这样的演算现在属于理想程序语言。

计算机科学在自动验证和自动寻找证明等技巧方面的成果对逻辑研究做出了贡献，比如说自动定理证明和逻辑编程。

命题逻辑是指以逻辑运算符结合原子命题来构成代表“命题”的公式，以及允许某些公式建构成“定理”的一套形式“证明规则”。相对于谓词逻辑，它是量化的并且它的原子公式是谓词函数；和模态逻辑，它可以是非真值泛函的。

在命题演算中语言由命题变量（或者叫占位符（placeholder））和句子/判决算子（或者叫连结词）。wff 是任何原子公式或在句子操作符之上建造的公式。

很多不同的公式系统存在，它们都或多或少等价但在下列方面不同： ⑴它们的语言（就是说哪些操作符和变量是语言的一部分）； ⑵ 它们有哪些（如果有的话）公理； ⑶采用了哪些推理规则。

在谓词逻辑中，原子命题分解成个体词和谓词。

个体词是可以独立存在的事或物，包括现实物、精神物和精神事三种。 谓词则是用来刻划个体词的性质的词，即刻画事和物之间的某种关系表现的词。

命题逻辑： 大致理解成 fact representation ： A事实，B事实，A可以推出B或C等。

谓语逻辑： 增加了function操作，函数操作，function（A）可以推出B， C可以推出function（B）等。

命题逻辑是一种比较简单，泛泛的逻辑。

比如令命题A表示“小明喜欢数学” 而谓词逻辑，是将命题逻辑表达不出来的逻辑继续细化。 比如A（x,y）表示x喜欢y，则“小明喜欢数学”可以表示为A（小明，数学）。

将命题细分得到谓词逻辑命题。

Ending！ 更多课程知识学习记录随后再来吧！

注： 1、人生在勤，不索何获。 2、命题逻辑和谓词逻辑之间有什么关系参见知乎：https://www.zhihu.com/question/47703279 3、数理逻辑、命题逻辑、谓词逻辑之概念参见百度百科。