完备性（逻辑）：修订间差异

2026年1月25日 (日) 13:17的最新版本

完备性
术语名称	完备性
英语名称	completeness
别名	完全性

完备性(completeness)指一个公理系统中，一个前提所逻辑蕴含（若为命题逻辑，则为重言蕴含）的结论都是能从前提演绎出的。也就是说，这个推理系统在推理上是充分的、强大的，凡是成立的，都是能推导出的。其中任意在语义上有后承关系东西在语义上都一定也可以从语法上推演，不会有任何语义上正确的公式无法通过这个推理系统推理出。

定义

对公理系统 [math]\displaystyle{ \mathbf{H} }[/math] 中，给定其中任意前提 [math]\displaystyle{ \Gamma }[/math] 和结论 [math]\displaystyle{ \phi }[/math] ，若 [math]\displaystyle{ \Gamma \vDash \phi }[/math] ，则 [math]\displaystyle{ \Gamma \vdash \phi }[/math] 。特别地，对 [math]\displaystyle{ \vDash\phi }[/math] 的情况有 [math]\displaystyle{ \vdash\phi }[/math] ，即普遍有效公式一定是可证明的。

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

@@ 第1行： / 第1行： @@
-[[分类:证明论]]
+[[分类:证明论]]{{DEFAULTSORT:wan2bei4xing4}}
+{{#seo:
+|keywords=推理规则, 完备性, 完全性
+|description=证明论中，描述形式化公理系统的性质时，如果一个公式所逻辑蕴涵的新公式都在其中能推理出，则称其具有完备性。本文介绍了完备性的定义和性质。
+|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
+|published_time=2023-08-06
+}}
 {{InfoBox
-|name=完全性
+|name=完备性
 |eng_name=completeness
+|aliases=完全性
 }}
-'''完全性'''('''completeness''')指一个[[形式化公理系统（逻辑）|公理系统]]中，一个前提所[[逻辑蕴含]]（对命题逻辑，为[[重言蕴含]]）的命题都是能从前提[[演绎]]出的。
+'''完备性'''('''completeness''')指一个[[形式化公理系统（逻辑）|公理系统]]中，一个前提所[[逻辑蕴含]]（若为命题逻辑，则为[[重言蕴含]]）的结论都是能从前提[[演绎]]出的。
-也就是说，这个系统中不会有语义上可推出的东西是无法语法上推演的。
+也就是说，这个推理系统在推理上是充分的、强大的，凡是成立的，都是能推导出的。其中任意在语义上有后承关系东西在语义上都一定也可以从语法上推演，不会有任何语义上正确的公式无法通过这个推理系统推理出。
 == 定义 ==
-公理系统 <math>\mathbf{H}</math> 中，对任意前提 <math>\Gamma</math> 和结论 <math>\phi</math> ，若 <math>\Gamma \vDash \phi</math> ，则 <math>\Gamma \vdash \phi</math> 。
+对公理系统 <math>\mathbf{H}</math> 中，给定其中任意前提 <math>\Gamma</math> 和结论 <math>\phi</math> ，若 <math>\Gamma \vDash \phi</math> ，则 <math>\Gamma \vdash \phi</math> 。特别地，对 <math>\vDash\phi</math> 的情况有 <math>\vdash\phi</math> ，即[[普遍有效公式]]一定是[[可证明]]的。
 {{证明论}}