逻辑学真是博大精深，
first-order logic，propositional logic，predicate logic，
mathematical logic，second-order Logic，intuitionistic logic，
modal logic，free logic，plural logic...
所涉及的内容也很广，
set theory，proof theory，model theory，recursion theory，
theory of computation，computability and decidability...
学习它，对数学，计算机科学或其他学科都有指导意义。
例如，哥德尔协调性定理指出了公理化方法的局限性，
它告诉我们，在理论上就不能通过逻辑推理解决所有的问题，
必要时，要通过构造模型来进行检验。
对软件进行测试，就是这样的一个例子。
例如，类型系统，相当于加在程序语言语法层面上的(谓词)逻辑，
类型系统的可靠性保证了语法正确的程序，
语义上也是满足规范的。
这样的例子还有很多，
实际工作中，只有见多识广，站在更高的角度，
才能做到庖丁解牛，游刃有余。
到此，我们还是从一阶谓词逻辑开始，慢慢打好基础吧。
以下摘自《数理逻辑》——李未
一阶语言的定义
每个一阶语言的字符集由两类符号集合组成。
一类称为逻辑符号集合，另一类称为非逻辑符号集合。
逻辑符号集合包括：
：变元符号集合，
：逻辑连接词符号集合，
：量词符号集合，
：等词符号集合，
：括号集合，
非逻辑符号集合包括：
：常元符号集合，
：函数符号集合，
：谓词符号集合，
例子：初等算术语言
初等算术语言是一个一阶语言，
它的常元符号集为，
函数符号集为，
谓词符号集合为。
项
一阶语言中的项被下述三个规则归纳的定义：
：每一个常元是一个项
：每一个变元是一个项
：如果是项，而f是一个n元函数符号，那么，是一个项
此定义也可以表述成下述形式：
例子：的项
逻辑公式
语言中的逻辑公式，简称公式，用大写字母表示，并用下述五条规则归纳的定义：
：如果和为项，那么是公式
：如果为项，而是一个n元谓词，那么是公式
：如果是公式，则是公式
：若是公式，则都是公式
：若是公式并且是一个变元，那么和也是公式，称为约束变元
上述结构归纳定义的Backus范式为：
例子：的公式
的结构
一阶语言的结构是一个偶对，记为，其中，
（1）是一个非空集合，称为论域
（2）是从到的映射，称为解释，记为，它满足下面三个条件
对中的每一个常元符号，是中的元素
对中的每一个n元函数符号，是上的n元函数
对中的每一个n元谓词符号，是上的一个n元关系
例子：的结构
的常元符号为，
函数符号有，
谓词符号只有一个，它是。
我们定义偶对，其中论域为自然数系。
令为上的加1函数，即，
代表上的加法和乘法，
为上的小于关系。
我们定义解释映射如下：
解释映射将常元符号解释为自然数，
将一元函数符号解释为自然数集合上的加1运算，
将二元函数符号和分别解释为自然数集合上的加法和乘法，
将二元谓词符号解释为自然数集合上的小于关系，
而是初等算术语言的一个结构。
赋值
赋值是一个定义域为变元集合，值域为的一个映射，记为。
赋值把中的每一个变元，赋以论域中的一个元素，
记为。
模型
给定一阶语言，以及它的结构和赋值，
偶对称为的一个模型。
项的语义
给定一阶语言，结构和赋值。
在模型下，项的语义是中的一个元素，它用表示，并被归纳的定义：
（1），为变元符号
（2），为常元符号
（3）
例子：项的语义
逻辑连接词符号的语义
为了避免逻辑连接词符号的多义性，我们把每一个逻辑连接词符号的语义都定义为一个真值函数，
此函数的定义域是一个真值集合或两个真值集合的笛卡尔积，而函数值是一个真假值。
对于一阶语言而言，逻辑连接词符号的真值函数为，
其自变量是，只能取和，
而函数值由下述真值表定义：
二元函数分别为逻辑连接词符号的真值函数。
公式的语义
设和分别为一阶语言的结构和赋值，而为的公式。
公式在模型下的语义是一个真假值，用表示，被归纳的定义如下：
（1）
（2）
（3）
（4）
（5）
（6）
（7）
（8）
（9）
可满足性
给定一阶语言和它的公式以及公式集合。
如果存在模型，使得成立，
那么称公式关于模型是可满足的，
简称可满足，也称为模型满足，记为。
如果是一个语句，那么记为，记为
如果中的每一个公式关于模型都是可满足的，即，
对于任意成立，
那么称为公式集合关于模型可满足，
简称公式集合可满足，
也称模型满足公式集合，或是的模型，记为。
如果是由语句组成的集合，那么记为。
永真性
称公式是永真的或有效的，如果对的任意模型均可满足，
即，对任意结构和赋值，成立，记为。
称公式集合是永真的或有效的，如果中的每一个公式都是永真的，记为
永真公式，也称为重言式，是与模型无关的公式，它们在任何模型下都为真。
例子：重言式
逻辑结论
设为公式，为公式集合，如果为任意结构，为任意赋值，并且，
如果成立，则有成立，
那么称是的逻辑结论或语义结论，记为，也称有效。
注：符号可以出现在4种不同类型的语义关系式中，它们是，
在每种语义关系式中的含义不同，
区别这些关系式的简单办法是，
当和同时出现时，表示此式仅对给定的和成立，
当不出现时，表示此式对任意成立，
当及均不出现时，表示此式对任意和任意成立。
也是一个语义关系式，它表示对任意和任意，
如果为真，那么也为真。
序贯
设为公式的有穷集合，称为序贯。
称为序贯的前提，称为序贯的结论。
公理
设为有穷公式集合，为公式，
则序贯称为公理。
注：公理序贯之所以成立，是因为证明结论中至少有一个公式包含在公理序贯的前提之中。
G推理系统
（1）规则
（2）规则
（3）规则
（4）规则
（5）规则
（6）规则
可靠性，紧致性，协调性，完全性
可靠性
如果序贯可证，那么成立。
紧致性
如果是一个公式集合，是一个公式，并且序贯可证，
那么必然存在有穷公式集合，使得并且可证。
协调性
设为公式集合，如果不存在一个公式使得序贯与均可证，
那么称是协调的。
完全性
令为一个公式集合，为一个公式，
如果成立，那么可证。
定理：令为一个公式集合，为一个公式，
（1）有效，当且仅当
（2）可满足，当且仅当协调
形式理论
设是一阶语言的有穷或可数无穷的语句集合，
如果协调，则称是一阶语言的形式理论，简称形式理论。
而称中的语句为的公理。
如果是一个形式理论，
那么称语句集合，是的语句，并且可证，
为的理论闭包。
如果，那么，是的语句，并且可证，
是由全体重言式组成的集合。
如果是的模型，并且，那么称是的模型。
关于模型的形式理论
如果是一阶语言的模型，那么称语句集合，
是的语句，并且
为关于模型的形式理论。
形式理论的完全性
称形式理论是完全的，如果对任意语句，
及中必有一个可证。
函数的可表示性
设是上的元函数，
如果存在公式，使得对任意自然数，
如果，那么可证
如果，那么可证
在这种情况下，称函数在中可表示，
并称公式是函数在中的表示。
定理：如果是上的元可计算函数，
那么函数在中可表示。
关系的可表示性
设是上的元关系，
如果存在公式，使得对任意自然数，有
如果，那么可证
如果，那么可证
在这种情况下，称关系在中可表示，
并称公式在中表示关系。
定理：如果是上的元可判定关系，
那么在中可表示。
哥德尔定理
哥德尔不完全性定理
如果是一个有穷并包含初等算术的形式理论，
那么是一个不完全的形式理论。
哥德尔协调性定理
如果形式理论包含初等算术，
那么的协调性不能在中被证明。
结语
以上，只是对谓词逻辑中用到的部分公式，进行了整理，
对建立用证明论和模型论的观点来理解公理系统，是很有帮助的。
然而，从更高的角度来看，有些观点很有可能就是错误的，
因此，此篇只是一个开始，督促我朝着更广阔的方向努力学习。
参考