A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic
W. W. Tait · Bulletin of the American Mathematical Society · 1966
Takeuti [3] showed that the consistency of analysis (i.e. second order number theory) is finitistically implied by the Hauptsatz for second order logic » i.e. by the proposition that every theorem of this system is derivable without cut. 1 We will prove that, conversely, the Hauptsatz for this system follows from a certain generalization of the consistency of analysis; namely from: I. Every countable set of relations among natural numbers is included in an o)-model. An co-model is a collection of relations among natural numbers which is closed under the second order comprehension axiom. Henkin [l] has shown that a second order formula is derivable with the cut rule if and only if it is valid in all (countable) co-models. When the given set of relations consists only of the successor relation, I asserts the consistency of analysis. The formalism for second order predicate logic which we will use is obtained from the system of predicate logic of finite order given in Schutte [2] by dropping all expressions and bound variables of types other than 0 (individuals), 1 (propositions) and (0, 0, • • • , 0) (relations among individuals). Thus, expressions of type 0 are built up from constants and free variables of type 0 using function constants. The expressions of type (0, • • • , 0) are constants, free variables and expressions Xx? • • • x£4(x?, • • • , x£), where A (a°u • • • , a£) is a wff (expression of type 1). The logical symbols other than X are —*, v and V. The notation and terminology of [2] will be assumed. In particular, the notions of strict derivation and partial valuation will be the same as in [2], except that they refer to the second order logic and not the full system of [2], and that we require of a partial valuation that whenever Vx T A(x T) is true (t), then so is A{a T) for some free 1 Actually, Takeuti asserts this result, not for second order logic, but for G