小时候，我就对侦探非常着迷，
买了很多介绍破案的漫画书，故事书，小说。
什么《大宇神秘惊奇系列》啊，
《名侦探柯南》啊，
《福尔摩斯探案全集》啊，等等。
可是，对于什么是推理，
以及怎样进行推理，
并没有清晰系统的认识。
学生时代，从平面几何开始，
我们就知道了证明题。
经过一步一步的推导，
最后证明结论成立。
可是，对于什么是证明，
并没有人能说出精确的定义。
这一切，难道真是只是个谜吗？
是人类的未知领域吗？
其实不然。
逻辑学就是研究推理和证明的学科，
研究思维的形式，规律和方法。
其中，数理逻辑是逻辑学与数学的交叉学科，
用数学的方法研究逻辑，
我想，答案应该在这里吧。
大局观
数理逻辑虽然博大精深，
但是研究方法却非常简洁优美。
给定一套逻辑系统，
分别从两个侧面来描述这个系统的性质。
语法层面，语义层面。
语法，指的是构成这个逻辑系统的符号规则，
由公理和定理的推导规则组成，
让我们可以从一串合法的符号得到另一串合法符号，
称之为形式证明。
语义，指的是用什么样的数学对象可以解释这些符号，
由论域和解释函数组成，我们得到的是一些代数结构，
而且，从已知符号串的语义性质得到了其他符号串的性质，
称之为逻辑推理。
学校中的数理逻辑教科书，介绍了命题演算和一阶谓词演算这两个典型的逻辑系统。
它们各自的语义解释，恰好描述了日常生活中推理问题。
总之，数理逻辑，用一套符号，对生活中常见的逻辑问题，进行了数学建模，
研究它，希望得到与证明和推理相关的更多性质和结论。
形式证明
为了说明问题，而又不引入过多的逻辑学概念，
我们从命题逻辑开始。
命题逻辑的形式化演算系统大体上可分为两种类型，
一是希尔伯特式的公理化演算系统，
二是甘岑(Gentzen)式的自然推理系统。
这两个系统各有所长，
前者更能体现公理化的思想，但其推理过程比较繁琐，
后者形式推理比较自然，但是规则较多。
下面只说命题演算的自然推理系统。
语法：
（1）可数个命题符号：
（2）5个联接词符号：
（3）2个辅助符号：
公式：（BNF）
推导规则：
（1）包含律：
（2）消去律：
（3）消去律：
（4）引入律：
（5）消去律：
（6）引入律：
（7）消去律：
（8）引入律：
（9）消去律：，
（10）引入律：
例子：
使用这些推理规则，我们就可以从一些合法的符号串，
推导出另一些合法的符号串了。
（1）：包含律
（2）：包含律
（3）：消去律，式（1），式（2）
（4）：包含律
（5）：消去律，式（3），式（4）
（6）：引入律，式（5）
有了这些以后，我们就可以定义什么是一个证明了。
证明序列：
若有限序列，满足，
（1）为有限公式集
（2）为公式
（3）每个都是它之前若干个应用某条推导规则得到的
则称这个有限序列为的一个（形式）证明序列。
此时，也称可由（形式）证明，
记为，其中表示自然推理系统。
逻辑推理
上文提到的是命题演算的自然推理系统，
这是一个形式系统，我们介绍了它的语法和推导规则，
根据这些推导规则，可以从一些合法的符号串推导出另一些，
在这个基础上，我们定义了什么叫做（形式）证明。
如何解释这些符号呢？
它们有什么含义呢？
我们给每一个合法的公式指定一个逻辑命题，作为这个公式的解释。
为每一个联接词符号指定一个真值函数，作为这个联接词符号的解释。
命题：
命题是可以判断真假值的句子。
真值函数：
上的元函数，
称为一个元真值函数。
我们将每个联接词与一个真值函数一一对应起来，
那么，复合命题的真假值就可以通过子命题的真假值计算出来了。
指派：
设为一个命题，中出现的所有命题变元构成了一个序列，
对该序列指定的任一真假值序列称为关于的一个指派，
其中。
真值表：
命题在所有可能的指派下，所取值列成的表，称为真值表。
永真式：
如果命题关于其中出现命题变元的所有指派均为真，则称该命题是一个永真式。
有了这些以后，我们就可以定义推理了。
设都是命题，
称推理『推出』是有效的，
如果对中出现的命题变元的任一指派，
若都为真，则也为真，
记为
否则，称推理『推出』是无效的。
例子：
证明与推理之间的关系
命题演算的自然推理系统，有很多性质，其中，
可靠性
完备性
它们表明，如果一个公式可以被证明，那么它所对应命题的推理就是有效的，
如果某些命题的推理是有效的，那么它就可以被证明。
然而，形式化系统这种研究方法，并不是完美无缺的。
哥德尔不完全性定理
如果是一个有穷并包含初等算术的形式理论，那么是一个不完全的形式理论。
哥德尔协调性定理
如果形式理论包含初等算术，那么的协调性不能在中被证明。
结语
证明和推理也是可以研究的，
并且，一直以来都是人们的感兴趣的研究对象。
逻辑学对自动定理证明，程序设计语言中的类型系统，
协议验证，软硬件的安全等领域，
有很重要的理论价值。
以命题逻辑和一阶谓词逻辑为基础，
人们构造出了各式各样种类繁多的逻辑系统，
包括模态逻辑，直觉主义逻辑，时序逻辑，动态逻辑，
多值逻辑，模糊逻辑，非单调逻辑，λ演算，组合逻辑等等。
现代逻辑学已经应用到了越来越多的学科之中。