独立性

独立性
术语名称	独立性
英语名称	independency

独立性(independency)在证明论中有两种含义。 其一可指一个形式化公理系统中，给定公式及其否定在这个公理和推演规则下均是不可证明的。 其二可指一个形式化公理系统中的公理之间，每个公理及其否定在其他公理和推演规则下均是不可证明的。

定义

对给定公理系统，包括公理及推演规则，若对公式 [math]\displaystyle{ \phi }[/math] ，不存在一条从 [math]\displaystyle{ \Gamma }[/math] 到 [math]\displaystyle{ \phi }[/math] 的演绎路径，则称 [math]\displaystyle{ \phi }[/math] 相对于这一公理系统内的公理及推演规则独立于 [math]\displaystyle{ \Gamma }[/math]；若 [math]\displaystyle{ \Gamma }[/math] 为空，则称 [math]\displaystyle{ \phi }[/math] 相对于这一公理系统内的推演规则独立于这一公理系统内的公理，或独立于这一公理系统。

对给定公理系统，若其中任意公理 [math]\displaystyle{ \phi }[/math] 独立于由这一公理系统中其他公理与相同的推演规则组成的新的公理系统，则称公理 [math]\displaystyle{ \phi }[/math] 独立于这一公理系统中的其他公理。

对给定公理系统，若系统中的公理都各自独立于各自的其他公理，则称公理系统的公理都是独立的。

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