Hostname: page-component-848d4c4894-wzw2p Total loading time: 0 Render date: 2024-05-04T16:23:34.102Z Has data issue: false hasContentIssue false
  • English
  • Français

Hauptsatz for higher order logic

Published online by Cambridge University Press:  12 March 2014

Dag Prawitz
Dag Prawitz*
Affiliation:
University of Lund
Get access Rights & Permissions [Opens in a new window]

Extract

I shall prove in this paper that Gentzen's Hauptsatz is extendible to simple type theory, i.e., to the predicate logic obtained by admitting quantification over predicates of arbitrary finite type and generalizing the second order quantification rules to cover quantifiers of other types. (That Gentzen's Hauptsatz is extendible to this logic has been known as Takeuti's conjecture; see [4].) Gentzen's Hauptsatz has been extended to second order logic in a recent paper by Tait [3]. However, as remarked by Tait, his proof seems not to be extendible to higher orders. The present proof is rather an extension of a different proof of the Hauptsatz for second order logic that I have presented in [1].

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 33 , Issue 3 , 10 October 1968 , pp. 452 - 457
Copyright
Copyright © Association for Symbolic Logic 1968

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

[1]Prawitz, Dag, Completeness and Hauptsatz for second order logic, Theoria, vol. 33 (1967), pp. 246–258.CrossRefGoogle Scholar
[2]Schütte, Kurt, Syntactical and semantical properties of simple type-theory, this Journal, vol. 25 (1960), pp. 305–326.Google Scholar
[3]Tait, William, A nonconstructive proof of Gentzen's Hauptsatz for second order predicate logic, Bulletin of the American Mathematical Society, vol. 72 (1966). pp. 980–983.CrossRefGoogle Scholar
[4]Takeuti, Gaisi, On a generalized logical calculus, Japanese journal of mathematics, vol. 23 (1953), pp. 39–96. (Errata, ibid., vol. 24 (1954), pp. 149–156.)CrossRefGoogle Scholar
[5]Takahashi, Moto-o, A proof of cut-elimination theorem in simple type-theory, Journal of the mathematical society of Japan, vol. 19, no. 4 (1967), pp. 399–410.Google Scholar