一致性：修订间差异

2026年1月26日 (一) 06:16的最新版本

一致性
术语名称	一致性
英语名称	consistency

一致的
术语名称	一致的
英语名称	consistent

一致性(consistency)在证明论中有两种含义。其一可指一个形式化公理系统中，不会同时证明出一对互为否定的定理。其二可指形式化公理系统中给定多个前提不会同时演绎出一对互为否定的结论。

通常的可演绎关系都会满足爆炸原理成立，如果一个推理系统不一致，可以推导出一对矛盾，则可以证明出任何公式，失去使用这一系统推理的意义。因此也可以表述为：公理系统是一致的，当且仅当其所有定理的集合不是所有公式的集合。

定义

对给定形式化公理系统 [math]\displaystyle{ \mathbf{H} }[/math] ，若不存在公式 [math]\displaystyle{ \phi }[/math] 使得 [math]\displaystyle{ \vdash \phi }[/math] 且 [math]\displaystyle{ \vdash \lnot \phi }[/math] ，称公理系统 [math]\displaystyle{ \mathbf{H} }[/math] 是一致的(consistent)。否则称公理系统 [math]\displaystyle{ \mathbf{H} }[/math] 是不一致的(inconsistent)。

对给定形式化公理系统 [math]\displaystyle{ \mathbf{H} }[/math] 及公式集 [math]\displaystyle{ \Gamma }[/math] ，若不存在公式 [math]\displaystyle{ \phi }[/math] 使得 [math]\displaystyle{ \Gamma \vdash \phi }[/math] 且 [math]\displaystyle{ \Gamma \vdash \lnot \phi }[/math] ，称公式集 [math]\displaystyle{ \Gamma }[/math] 在公理系统 [math]\displaystyle{ \mathbf{H} }[/math] 中是一致的(consistent)。否则称公式集 [math]\displaystyle{ \Gamma }[/math] 在公理系统 [math]\displaystyle{ \mathbf{H} }[/math] 中是不一致的(inconsistent)。

性质

对形式化公理系统中的一个公式集：

若公式集是一致的，则其演绎结论的集合也是一致的。
若公式集是可满足的，则公式集一定是一致的。
公式集 [math]\displaystyle{ \Gamma }[/math] 是不一致的，当且仅当，对所有公式 [math]\displaystyle{ \phi }[/math] 有 [math]\displaystyle{ \Gamma\vdash\phi }[/math] 。
对公式集 [math]\displaystyle{ \Gamma }[/math] 和公式 [math]\displaystyle{ \phi }[/math] ， [math]\displaystyle{ \Gamma\vdash\phi }[/math] 当且仅当 [math]\displaystyle{ \Gamma\cup\{\lnot\phi\} }[/math] 不一致。
对非空公式集 [math]\displaystyle{ \Gamma }[/math] ， [math]\displaystyle{ \Gamma }[/math] 是不一致的，当且仅当，对任意公式 [math]\displaystyle{ \phi }[/math] 有 [math]\displaystyle{ \Gamma\setminus\{\phi\}\vdash \lnot\phi }[/math] 。
对公式集 [math]\displaystyle{ \Gamma }[/math] 和公式 [math]\displaystyle{ \phi }[/math] ，若 [math]\displaystyle{ \Gamma }[/math] 是一致的，则 [math]\displaystyle{ \Gamma\cup\{\phi\} }[/math] 和 [math]\displaystyle{ \Gamma\cup\{\lnot\phi\} }[/math] 中有一个是一致的，一个是不一致的。

对形式化公理系统的一致性也有类似以上的性质。

证明论
形式化公理系统（形式化、公理化）
推理系统	Hilbert 风格/公理系统：Hilbert 表示
	Gentzen 风格-自然演绎系统： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎
	Gentzen 风格-相继式演算： Gentzen 式相继式演算
证明、演绎	演绎、可演绎、证明、可证明
命题、定理	公理/公理模式、定理、元定理、变形规则
推理规则性质	保存真实性、保存重言性
公理系统性质	可靠性、完备性/完全性、一致性、独立性

@@ 第1行： / 第1行： @@
-[[分类:证明论]]
+[[分类:证明论]]{{DEFAULTSORT:yi2zhi4xing4}}
+{{#seo:
+|keywords=推理规则, 一致性
+|description=证明论中，描述形式化公理系统的性质时，如果能证明出一对矛盾则称其不一致，相反称其具有一致性。本文介绍了一致性的定义和性质。
+|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
+|published_time=2023-08-06
+}}
 {{InfoBox
 |name=一致性
@@ 第8行： / 第14行： @@
 |eng_name=consistent
 }}
-'''一致性'''('''consistency''')指一个[[形式化公理系统（逻辑）|形式化公理系统]]中，不会同时[[证明]]出一对互为否定的[[定理]]。
+'''一致性'''('''consistency''')在证明论中有两种含义。
-也指一个形式化公理系统中的多个前提不会同时[[演绎]]出一对互为否定的结论。
+其一可指一个[[形式化公理系统（逻辑）|形式化公理系统]]中，不会同时[[证明]]出一对互为否定的[[定理]]。
+其二可指形式化公理系统中给定多个前提不会同时[[演绎]]出一对互为否定的结论。
-通常的可演绎关系都会满足[[爆炸原理]]成立，如果一个推理系统不一致则可以证明出任何公式，失去使用这一系统推理的意义。因此也可以表述为：公理系统是一致的，当且仅当其所有定理的集合不是所有公式的集合。
+通常的可演绎关系都会满足[[爆炸原理]]成立，如果一个推理系统不一致，可以推导出一对矛盾，则可以证明出任何公式，失去使用这一系统推理的意义。因此也可以表述为：公理系统是一致的，当且仅当其所有定理的集合不是所有公式的集合。
 == 定义 ==
-在给定[[形式化公理系统（逻辑）|公理系统]]中，若不存在公式 <math>\phi</math> 使得 <math>\vdash \phi</math> 且 <math>\vdash \lnot \phi</math> ，称公理系统是'''一致的'''('''consistent''')。否则称公理系统是'''不一致的'''('''inconsistent''')。
+对给定形式化公理系统 <math>\mathbf{H}</math> ，若不存在公式 <math>\phi</math> 使得 <math>\vdash \phi</math> 且 <math>\vdash \lnot \phi</math> ，称公理系统 <math>\mathbf{H}</math> 是'''一致的'''('''consistent''')。否则称公理系统 <math>\mathbf{H}</math> 是'''不一致的'''('''inconsistent''')。
-在给定[[形式化公理系统（逻辑）|公理系统]]中，对公式集 <math>\Gamma</math> ，若不存在公式 <math>\phi</math> 使得 <math>\Gamma \vdash \phi</math> 且 <math>\Gamma \vdash \lnot \phi</math> ，称公式集 <math>\Gamma</math> 是'''一致的'''('''consistent''')。否则称公式集是'''不一致的'''('''inconsistent''')。
+对给定形式化公理系统 <math>\mathbf{H}</math> 及公式集 <math>\Gamma</math> ，若不存在公式 <math>\phi</math> 使得 <math>\Gamma \vdash \phi</math> 且 <math>\Gamma \vdash \lnot \phi</math> ，称公式集 <math>\Gamma</math> 在公理系统 <math>\mathbf{H}</math> 中是'''一致的'''('''consistent''')。否则称公式集 <math>\Gamma</math> 在公理系统 <math>\mathbf{H}</math> 中是'''不一致的'''('''inconsistent''')。
 == 性质 ==
+对形式化公理系统中的一个公式集：
 * 若公式集是一致的，则其演绎结论的集合也是一致的。
 * 若公式集是可满足的，则公式集一定是一致的。
-* 公式集 <math>\Gamma</math> 是不一致的，当且仅当，对所有公式 <math>\phi</math> 有 <math>\Gamma\vdash\phi</math>
+* 公式集 <math>\Gamma</math> 是不一致的，当且仅当，对所有公式 <math>\phi</math> 有 <math>\Gamma\vdash\phi</math> 。
 * 对公式集 <math>\Gamma</math> 和 公式 <math>\phi</math> ， <math>\Gamma\vdash\phi</math> 当且仅当 <math>\Gamma\cup\{\lnot\phi\}</math> 不一致。
-* 对非空公式集 <math>\Gamma</math> ， <math>\Gamma</math> 是不一致的，当且仅当，对所有公式 <math>\phi</math> 有 <math>\Gamma\setminus\{\phi\}\vdash \lnot\phi</math>
+* 对非空公式集 <math>\Gamma</math> ， <math>\Gamma</math> 是不一致的，当且仅当，对任意公式 <math>\phi</math> 有 <math>\Gamma\setminus\{\phi\}\vdash \lnot\phi</math> 。
-* 对公式集 <math>\Gamma</math> 和 公式 <math>\phi</math> ，若 <math>\Gamma</math> 本身是一致的，则 <math>\Gamma\cup\{\phi\}</math> 和 <math>\Gamma\cup\{\lnot\phi\}</math> 一个一致一个不一致。
+* 对公式集 <math>\Gamma</math> 和 公式 <math>\phi</math> ，若 <math>\Gamma</math> 是一致的，则 <math>\Gamma\cup\{\phi\}</math> 和 <math>\Gamma\cup\{\lnot\phi\}</math> 中有一个是一致的，一个是不一致的。
+对形式化公理系统的一致性也有类似以上的性质。
 {{证明论}}