Lattice-valued representation of the cut-elimination theorem
Lattice-valued representation of the cut-elimination theorem
复制标题
割消去定理的格值表示
DOI：
10.21099/tkbjm/1496161672
复制
发表时间：
1991
影响因子：
0.7
通讯作者：
S. Maehara
中科院分区：
文献类型：
--
作者：
S. Maehara
1934年G. Gentzen [1] 提出了第一阶经典直觉谓词演算$LK$ 和$LJ$，并表达并证明了它们的Hauptsatz 或割消去定理。 1953 年，G. Takeuti [11] 宣布他的基本猜想或 $GLC$ 的割消定理意味着有限性分析的一致性，其中 $GLC$ 是一个类似于 $LK$ 的简单类型理论。从那时起，他连续但建设性地证明了基本猜想对于 $GLC$ 的许多子系统都是正确的。 1967年，M. Takahashi[9]通过非构造性方法对Takeuti的基本猜想给出了一般肯定解（另见[10]）。 Takahashi 的证明基于 K. Sch\"utte [7] 和之前的 W. Tait [8] 的结果，证明了二阶谓词逻辑的割消除定理。 1971 年，G. Y. Girard [2] 对于直觉主义的 $GLC$ 给出了一个句法割消除过程，并通过使用非构造性论证而不是使用法则来证明了该过程的有限性。 排除中间。 Gentzen [1] 说他的 Hauptsatz 最初是为自然直觉微积分 $NJ$ 而发现的，这是 [1] 中给出的自然演绎的一阶直觉系统，但他没有详细论述。 1965 年，D. Prawitz [5] 为 $NJ^{2)}$ 制定了 Hauptsatz 或他的范式定理（对于经典的自然演绎系统，承认 没有析取，也没有存在量化）。对于高阶自然演绎系统的范式定理有一些研究：Prawitz [6]、P. Martin-Lof [3]、[4] 等。在本文中，作为我们的主定理，我们将给出割消去定理的半代数表示。无具体切割消除程序
In 1934 G. Gentzen [1] presented the first order classical and intuitionistic predicate calculi $LK$ and $LJ$, and expressed and proved his Hauptsatz or the cut-elimination theorem for them. In 1953 G. Takeuti [11] announced the fact that his fundamental conjecture or the cut-elimination theorem for his $GLC$ implies finitistically the consistency of analysis, where $GLC$ is a simple type theory formulated analogously to $LK$ From that time on he has proved successively but constructively that the fundamental conjecture is true for many subsystems of $GLC$ . In 1967 M. Takahashi [9] gave a general affirmative solution to Takeuti’s fundamental conjecture by means of non-constructive methods (see also [10]). Takahashi’s proof based on a result of K. Sch\"utte [7] and previously W. Tait [8] had proved the cut-elimination theorem for second order predicate logic. In 1971 G. Y. Girard [2], for the intuitionistic $GLC$ , gave a syntactical cutelimination procedure and proved the finiteness of the procedure by use of nonconstructive arguments but by no use of the law of excluded middle. Gentzen [1] says his Hauptsatz had been found originally for the natural intuitionistic calculus $NJ$, that is a first order intuitionistic system of natural deductins given in [1], but he did not discourse in detail. In 1965 D. Prawitz [5] formulated the Hauptsatz or his normal form theorem for $NJ^{2)}$ (and for a classical natural deduction system admitting no disjunctions nor existential quantifications). There are several studies of the normal form theorem for higher order natural deduction systems: Prawitz [6], P. Martin-Lof [3], [4], and so on. In this paper, as our Main Theorem, we shall give a semi-algebraic representation of the cut-elimination theorem. No concrete cut-elimination procedure