可靠性

可靠性
术语名称	可靠性
英语名称	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] ，即其为普遍有效公式。

性质

一个推理系统满足可靠性，要求全体真理为重言式且全体句法规则保存重言性。

证明论
研究动机与结果	Gödel 完备性定理、 Hilbert 纲领、 Gödel 不完备定理
结构化证明	推理系统 形式化公理系统 （形式化、公理化）	Hilbert 风格/公理系统（在无前提的定理间推理）： Hilbert 表示
		Gentzen 风格-自然演绎系统（在有前提、有假设的结论间推理）： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎
		Gentzen 风格-相继式演算（在描述可演绎关系的元定理间推理）： Gentzen 式相继式演算
	证明、演绎	演绎、可演绎、证明、可证明
	命题、定理	命题、元命题、公理/公理模式、定理、元定理
	推理规则性质描述	保存真实性、保存重言性
	推理系统性质描述	可靠性、完备性/完全性、一致性、独立性
	重要元定理	演绎定理、切消定理（切割消除定理）
		（某种推理系统的）可靠性定理、完备性定理
序数分析	证明论序数
构造性证明 程序化证明	Curry–Howard 对应
	证明复杂度理论	证明复杂度