可靠性：修订间差异

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

可靠性
术语名称	可靠性
英语名称	soundness

可靠性(soundness)指一个形式化公理系统中，能从一个前提演绎出的结论都是前提所逻辑蕴涵（若为命题逻辑，则为重言蕴涵）的。也就是说，这个推理系统在推理上是安全的、保守的，凡是能推导出的，都是成立的。其中任意可以从语法上推演的东西在语义上都一定在语义上也有后承关系，不会因为只看语法而从一个语义上正确的公式推理出语义上荒谬的公式。

定义

对公理系统 [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 式相继式演算
证明、演绎	演绎、可演绎、证明、可证明
命题、定理	公理/公理模式、定理、元定理、变形规则
推理规则性质	保存真实性、保存重言性
公理系统性质	可靠性、完备性/完全性、一致性、独立性

@@ 第11行： / 第11行： @@
 }}
 '''可靠性'''('''soundness''')指一个[[形式化公理系统（逻辑）|形式化公理系统]]中，能从一个前提[[演绎]]出的结论都是前提所[[逻辑蕴涵]]（若为命题逻辑，则为[[重言蕴涵]]）的。
-也就是说，这个推理系统中任意可以从语法上推演的东西在语义上都一定在语义上也有后承关系，不会因为只看语法不看语义而从一个语义上正确的公式推理出语义上错误的公式。
+也就是说，这个推理系统在推理上是安全的、保守的，凡是能推导出的，都是成立的。其中任意可以从语法上推演的东西在语义上都一定在语义上也有后承关系，不会因为只看语法而从一个语义上正确的公式推理出语义上荒谬的公式。
 == 定义 ==
@@ 第17行： / 第17行： @@
 对公理系统 <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> ，即其为[[普遍有效公式]]。
-注：也可以表述为全体句法规则[[保存重言性]]。
+== 性质 ==
+一个推理系统满足可靠性，要求全体真理为[[重言式]]且全体句法规则[[保存重言性]]。
 {{证明论}}