协调性

又称无矛盾性(或一致性、相容性)，是形式系统(公理系统、理论)的一个重要性质。一个形式系统S是协调的，如果不是每一公式都是在S中可证的。在相反的情况下，一个系统就称为是矛盾的或不协调的。对于其语言中含有否定号的系统，协调性又可以定义为：一个形式系统S是协调的，如果不存在一个公式A，使得A和A都是在S中可证的。对于在语言中含有符号的系统，上述两个定义是等价的。

设Φ是某个形式系统的公式集，Φ是协调的，如果不存在该系统的一个公式A，使得Φ┝A 并且Φ┝A。否则称Φ是不协调的。

上面所说的协调性定义是语法的。对协调性也可以作语义的定义：一个形式系统S是协调的，如果S的所有可证公式(定理)都是真的。(对纯逻辑系统来说，凡是可证公式都是常真的。)一个公式集Φ是协调的，如果有一模型使得Φ中的公式都真，即Φ。

对于建立在一阶逻辑框架上的任何形式系统，由哥德尔完全性定理，都有：

一形式系统S是协调的，当且仅当，S是有模型的。

因此，证明一形式系统的协调性的一种方法，是给它找出或建立一个模型。证明协调性的另一种方法是D．希尔伯特提出的希尔伯特计划：关于某个形式系统的无矛盾性的断言被看作是关于该系统的可能的证明的一个命题。以任意的数学证明为研究对象的理论称为证明论或元数学。

协调性是一切形式系统都要求满足的一种性质。逻辑系统的协调性更是首先要关注的问题。