A proof of the cut-elimination theorem in simple type theory
Satoko Titani · Journal of Symbolic Logic · 1973
In [4], I introduced a quasi-Boolean algebra, and showed that in a formal system of simple type theory, from which the cut rule is omitted, wffs form a quasi-Boolean algebra, and that the cut-elimination theorem can be formulated in algebraic language. In this paper we use the result of [4] to prove the cut-elimination theorem in simple type theory. The theorem was proved by M. Takahashi [2] in 1967 by using the concept of Schütte's semivaluation. We use maximal ideals of a quasi-Boolean algebra instead of semivaluations. The logical system we are concerned with is a modification of Schütte's formal system of simple type theory in [1] into Gentzen style. Inductive definition of types. 0 and 1 are types. If τ1, …, τn are types, then (τ1, …, τn) is a type. Basic symbols. a1τ, a2τ, … for free variables of type τ. x1τ, x2τ, … for bound variables of type τ. An arbitrary number of constants of certain types. An arbitrary number of function symbols with certain argument places.