根岑系统

一种谓词逻辑的形式系统，由G．根岑在20世纪30年代建立，根岑系统分为自然推演系统(仿效通常数学推理形式因而特别适于记录它们)和矢列(Sequenz)演算(着重于分析给定的公式的可能的证明，得到证明的范式以及它们在证明论中的应用)。有时也不作这种区分。下面介绍一个矢列型的根岑系统G1。G1系统相当于根岑原来的LK，由S．C．克利尼给出。G1的原始符号包括联结词、∧、∨、，量词符号和。元语言符号→(读作“推出”)，它的性质和其它系统中的符号“┝”的性质相似。G1的推演规则不是施行于希尔伯特型系统的公式，而是由系统的公式依照新形成规则所组成的新客体，叫做矢列。一矢列是指如下形式的表达式：A，…，A→B，…，B，这里m，n≥0，A，…，A，B，…，B为公式，在箭头左边的部分叫做它的前件，箭头右边的部分叫做它的后件。

形式系统G1的公理和推演规则。

约定条件：A、B、C、D为公式：Γ，Δ，，A为0个或多个公式的有穷序列；x为一变元；A(x)为一公式；t为一项，对A(x)中的x是自由的；b是一变元，对A(x)中的x是自由的并且不自由出现于A(x)中。

在各个推演规则中，在横线上的矢列叫做该规则的前提，在横线下的矢列叫做该规则的结论。

G1的直觉主义系统与经典系统之间的差异在于有两个规则受到了直觉主义的限制。

公理模式

C→C。

命题演算中的逻辑推演规则：

引入　　　　于后件

对直觉主系统Δ须为空。

谓词演算中补充的逻辑推演规则。

引入　　　　于后件

变元b不得自由出现于结论中。

结构的推演规则。

　　　　　　于后件

对直觉主义系统Δ须空。

　　于前件

　　于前件

变元b不得自由出现于结论中；

　　于前件

设S是一矢列，用“┝S”表示矢列S是在G1中可证的。系统G1与希尔伯特型谓词演算系统是等价的，即对于任何公式E，在G1中有┝→E当且仅当在希尔伯特型系统中有┝E。

关于系统G1，有一条切割消除定理(cut elimination theorem)，也称为根岑“主(Hauptsatz)定理”或范式定理：给出一个在G1中的某矢列的证明，该矢列中没有变元是既自由出现的又约束出现的，那末对该矢列必可找出另外一个G1中的证明，其中不用到切割规则。这个证明是纯洁变元的证明，在它里面所使用的逻辑规则是原先证明中使用过的。

根岑“主定理”的意义和重要性在于不用切割的证明具有子公式性质：G1的任何不用切割的证明，在它的任何矢列中所出现的公式都是出现于尾矢列的某个公式的子公式；G1的一个证明，如果不用切割，不用规则或规则，则在其中任何矢列的前件(后件)中所出现的每个公式都是出现于尾矢列的前件(后件)中的某个公式的子公式。由此可以得一个关于命题演算的判定方法，它与真值表方法不同，可以同样地适用于经典系统和直觉主义系统。“主定理”的另一项重要应用是用于数学理论的协调性证明。用根岑的系统作的数论系统的协调性证明，比用其它方法作的证明容易。