序列微积分

在数理逻辑中，序列微积分是一种形式逻辑论证的风格，其中证明的每一行都是一个条件同义词（格哈德·根岑 (GerhardGentzen)称之为序列），而不是一个无条件同义词。

每一个条件同义词都是根据推理的规则和程序从形式论证中的其他条件同义词推断出来的，与大卫-希尔伯特早期的形式逻辑风格相比，它更接近于数学家使用的自然演绎风格，在这种风格中，每一行都是无条件的同义词。

更微妙的区别可能存在；例如，命题可能隐含地依赖于非逻辑公理。在这种情况下，序列标志着一阶语言中的条件定理，而不是条件同义词。

序列微积分是现存的几种用于表达逐行逻辑论证的证明微积分风格之一。

希尔伯特风格，每一行都是一个无条件的同义词（或定理）。

根岑(Gentzen)风格，每一行都是有条件的同义词（或定理），左边有零个或多个条件。

自然演绎，每条（条件）线的右边正好有一个断言的命题。

序列微积分，每个（条件）行的右边都有零个或更多的断言命题。

换句话说，自然演绎和序列微积分系统是特殊的不同类型的根岑(Gentzen)式系统。希尔伯特式系统通常有非常少的推理规则，更多地依赖于公理集。根岑(Gentzen)式系统通常只有很少的公理（如果有的话），更多地依赖于规则集。与希尔伯特式系统相比，根岑式系统具有明显的实践和理论优势。

例如，自然演绎和序列微积分系统都有利于消除和引入普遍的和存在的量词，这样就可以根据更简单的命题微积分规则来处理未量化的逻辑表达。

在一个典型的论证中，量词被消除了，然后命题微积分被应用于未量化的表达式（通常包含自由变量），然后量词被重新引入。这与数学家在实践中进行数学证明的方式非常相似。

使用这种方法，谓词微积分的证明通常更容易发现，而且通常更短。自然演绎系统更适合于实际的定理证明。序列微积分系统更适合于理论分析。

在证明理论和数理逻辑中，序列微积分是共享某种推理风格和某些形式属性的形式系统家族。第 一个序列计算系统，LK和LJ，由格哈德·根岑 (GerhardGentzen) 在1934/1935年推出，作为研究一阶逻辑自然演绎的工具（分别为经典和直觉版本）。

根岑(Gentzen)所谓的关于LK和LJ的主要定理（基本定理）是切割消除定理，这一结果具有深远的元理论后果，包括一致性。几年后，根岑(Gentzen)进一步证明了这一技术的威力和灵活性，他应用割除论证给出了皮亚诺 (Peano) 算术一致性的（无限）证明，对哥德尔的不完备性定理做出了令人惊讶的回应。

自这项早期工作以来，顺序计算（也称为Gentzen系统）以及与之相关的一般概念已被广泛应用于证明理论、数理逻辑和自动演绎等领域。

对不同风格的演绎系统进行分类的一种方法是看系统中的判断形式，即哪些事情可以作为（子）证明的结论出现。

最简单的判断形式被用于希尔伯特式演绎系统，其中判断的形式为是一阶逻辑（或演绎系统适用的任何逻辑，如命题微积分、高阶逻辑或模态逻辑）的任何公式。定理是那些在有效证明中作为结论判断出现的公式。

希尔伯特式的系统不需要区分公式和判断；我们在这里做这样的区分只是为了与后面的案例进行比较。为希尔伯特式系统的简单语法所付出的代价是，完整的形式证明往往会变得非常长。

在这样的系统中，关于证明的具体论证几乎总是诉诸于演绎定理。这导致了将演绎定理作为形式规则纳入系统的想法，这发生在自然演绎中。