回顾
上文我们介绍了一阶逻辑的语义模型，它包括结构和赋值两个部分，
其中，结构给出了常元符号、函数符号以及谓词符号在论域中的解释，
而赋值给出了变元符号在论域中的解释。
我们通过这种方式，建立了形式符号和论域中数学对象之间的关联，
本文将继续研究符号和其语义之间的关系。
1. 语义方面（模型）
1.1 公式的可满足性
我们知道在公理化系统中，逻辑公式可以用来表示推导规则的前提和结论，
它在给定模型中的语义是一个真假值。
这是合情合理的。
因为推导本来就应该是从真命题推导出另一个真命题的过程。
由于模型是可以人为选择的，所以，给定一个逻辑公式，
其语义的真假性，有可能会受到所选模型的影响。
如果存在模型，使得成立，
我们就称公式关于模型是可满足的，
记为。
此外，如果有公式集，
其中的每一个公式关于模型都是可满足的，
我们就称，公式集关于模型是可满足的，
记为。
1.2 重言式
如果公式，对于任意模型都是可满足的，
即，对任意结构和赋值，都成立，
我们就称是永真公式，也称为重言式，记为。
重言式，是与模型无关的公式，
它们在任何模型下都为真。
例：，都是重言式。
1.3 逻辑推理
有了可满足性，我们就可以进行逻辑推理了。
设为公式，为公式集，为任意结构，为任意赋值，并且，
如果成立，就有成立，
我们就称，是公式集的逻辑结论或语义结论，
记为，也称结论有效。
因此，表示了一种语义关系，
它指出，对任意和任意，如果为真，那么也为真。
2. 语法方面（符号）
2.1 序贯
在《你好，类型》系列文章中，
我们介绍过序贯的概念。
我们知道，在公理系统中，序贯可以用来表示前提和结论之间的符号联系。
序贯，表示从公式集出发，根据推导规则，
可以证明出中至少有一条公式成立。
习惯上，序贯成立，也称可证。
值得注意的是，序贯谈论的都是语法层面（符号层面）上的，
和这些符号的所选择的具体语义无关。
2.2 协调性（一致性）
设为公式集，
如果不存在一个公式使得序贯与均可证，
我们就称，公式集是协调的，也称一致的。
设是一阶语言的公式集，该集合可以是有限集或可数集，
如果协调，则称是一阶语言的形式理论。
3. 语法（符号）和语义（模型）
3.1 可靠性和完全性
把公理系统的语法和语义联合起来，
我们还可以定义出以下这些系统性质。
如果序贯可证，那么成立，就说系统是可靠的。
如果成立，那么可证，就说系统是完全的。
3.2 不完全性与协调性不可证
是不是任意一个公理系统都是可靠且完全的呢？
可惜并不是如此。
哥德尔在1931年给出了两个定理，终结了人们的幻想，
分别称为哥德尔不完全性定理，和哥德尔协调性定理。他指出，
不完全性
如果是一个有穷，并包含初等算术的形式理论，
那么是一个不完全的形式理论。
协调性
如果形式理论包含初等算术，
那么的协调性不能在中被证明。
所以，在软件开发过程中，检查一个软件系统是否符合设计要求，所使用的方法就是对它进行测试，在这个软件系统之外进行证明。
总结
文本介绍语法（符号证明）和语义（模型）之间的关系，
让我们认识到了形式化方法的局限性。
一个足够有用的系统，总会出现不可证的事实，
并且，在该系统内部，我们甚至都无法证明它是否含有矛盾。