|
1 History
First there was Frege [Frege1879] which was sort of higher-order, but Russell showed Frege's system was inconsistent using Russell's paradox. Russell created (ramified) type theory to avoid Russell's paradox [Russell08]. Russell did not use λ-calculus to formulate type theory. Often λ-calculus is not used in formulations of higher-order logic. Church [Church40] introduced the form of higher-order logic as a theory in the simply typed λ-calculus (sometimes called “simple type theory”).
2 Cut-Elimination
Schütte [Schutte60] gives a nice early discussion of issues regarding type theory, but with a “relational formulation” (not using λ-calculus). At this point cut-elimination was still an open problem. Cut-elimination was proven by Prawitz [Prawitz68] and Takahashi [Takahashi67] independently – though both without λ-calculus. Important: Andrews modified the technique to show cut-elimination for a nonextensional form of type theory with λ-calculus in [Andrews71]. Prawitz used the term “possible values“ in association with the technique for showing cut-elimintation. Andrews proved cut-elimination has a relationship to consistency of analysis [Andrews74a]. Due to this result combined with Godel's second incompleteness theorem, no proof of cut-elimination for higher-order logic can be formalized in higher-order logic (with infinity) – unless higher-order logic with infinity is inconsistent.
3 Semantics
Henkin gave a definition of a model for Church's type theory in [Henkin50] and proved completeness. Andrews later showed Henkin's original definition of model was incorrect (a form of extensionality failed for Leibniz equality) – see [Andrews72b]. Andrews added the condition that Henkin models should include an interpretation for equality (and called these “general models”). See also [Andrews72a] for more about semantics. The semantics with (and without) different forms of extensionality are discussed in [BBK04]. Brown's thesis [Brown2004a] discusses many semantic issues in a more general framework than Church's type theory (in which logical constants may or may not be present).
4 Simply Typed λ-calculus
Note that this is not higher-order logic. This is about simply typed lambda calculus. Church's type theory is a theory in the simply typed lambda calculus.
Hindley's book [Hindley97] gives a nice introduction. Huet's unification is vital [Huet75] for automated reasoning in systems which use simply typed λ-calculus.
5 Overviews
See [Leivant94] (without λ-calculus) and [Andrews00c] (with λ-calculus) for nice discussions.
Bibliography
[Andrews71] Peter B. Andrews.
Resolution in type theory. Journal of Symbolic Logic,
36:414–432, 1971.
[Andrews72b] Peter B. Andrews.
General models and extensionality. Journal of Symbolic
Logic, 37:395–397, 1972.
[Andrews72a] Peter B. Andrews.
General models, descriptions, and choice in type theory.
Journal of Symbolic Logic, 37:385–394, 1972.
[Andrews74a] Peter B. Andrews.
Resolution and the consistency of analysis. Notre Dame Journal
of Formal Logic, 15(1):73–84, 1974.
[Andrews00c] Peter B. Andrews.
Classical type theory. In Alan Robinson and Andrei Voronkov,
editors, Handbook of Automated Reasoning, volume 2, chapter
15, pages 965–1007. Elsevier Science, 2001.
[BBK04] Christoph Benzmüller,
Chad Brown, and Michael Kohlhase. Higher-order semantics and
extensionality. Journal of Symbolic Logic,
69(4):1027–1088, 2004.
[Brown2004a] Chad E. Brown. Set
Comprehension in Church's Type Theory. PhD thesis, Department
of Mathematical Sciences, Carnegie Mellon University, 2004.
[Church40] Alonzo Church. A
formulation of the simple theory of types. Journal of Symbolic
Logic, 5:56–68, 1940.
[Frege1879] Gottlob Frege.
Begriffsschrift, eine der arithmetischen nachgebildete
Formelsprache des reinen Denkens. Halle, 1879. Translated in
[Heijenoort67].
[Henkin50] Leon Henkin. Completeness
in the theory of types. Journal of Symbolic Logic,
15:81–91, 1950.
[Hindley97] J. Roger Hindley.
Basic Simple Type Theory. Cambridge University Press, 1997.
[Huet75] Gérard P. Huet. A
unification algorithm for typed λ-calculus. Theoretical
Computer Science, 1:27–57, 1975.
[Leivant94] Daniel Leivant. Higher
order logic. In Dov M. Gabbay, C.J. Hogger, and J.A. Robinson,
editors, Handbook of Logic in Artificial Intelligence and Logic
Programming, volume 2, pages 229–321. Oxford University
Press, 1994.
[Prawitz68] Dag Prawitz. Hauptsatz
for higher order logic. Journal of Symbolic Logic,
33:452–457, 1968.
[Russell08] Bertrand Russell.
Mathematical logic as based on the theory of types. American
Journal of Mathematics, 30:222–262, 1908. Reprinted in
[Heijenoort67], pp. 150–182.
[Schutte60] K. Schütte.
Syntactical and semantical properties of simple type theory.
Journal of Symbolic Logic, 25(4):305–326, 1960.
[Takahashi67] Moto-o Takahashi. A
proof of cut-elimination theorem in simple type theory. Journal
of the Mathematical Society of Japan, 19:399–410, 1967.
[Heijenoort67] Jean van Heijenoort.
From Frege to Gödel. A Source Book in Mathematical Logic
1879–1931. Harvard University Press, Cambridge,
Massachusetts, 1967.