Hostname: page-component-7c8c6479df-94d59 Total loading time: 0 Render date: 2024-03-27T16:48:19.325Z Has data issue: false hasContentIssue false

Types in Logic and Mathematics Before 1940

Published online by Cambridge University Press:  15 January 2014

Fairouz Kamareddine
Affiliation:
Computing and Electrical Engineering, Heriot-Watt University, Riccarton, Edinburgh EH14 4AS, ScotlandE-mail: fairouz@cee.hw.ac.uk
Twan Laan
Affiliation:
Weerdstede 45, 3431 LS Nieuwegein, The NetherlandsE-mail: twan.laan@wxs.nl
Rob Nederpelt
Affiliation:
Mathematics and Computing Science, Eindhoven University of Technology, P.O. BOX 513, 5600 MB Eindhoven, The NetherlandsE-mail: r.p.nederpelt@tue.nl

Abstract

In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([71], 1910–1912) and Church's simply typed λ-calculus of 1940. We first argue that the concept of types has always been present in mathematics, though nobody was incorporating them explicitly as such, before the end of the 19th century. Then we proceed by describing how the logical paradoxes entered the formal systems of Frege, Cantor and Peano concentrating on Frege's Grundgesetze der Arithmetik for which Russell applied his famous paradox and this led him to introduce the first theory of types, the Ramified Type Theory (RTT). We present RTT formally using the modern notation for type theory and we discuss how Ramsey, Hilbert and Ackermann removed the orders from RTT leading to the simple theory of types STT. We present STT and Church's own simply typed λ-calculus (λ→C) and we finish by comparing RTT, STT and λ→C.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 2002

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

REFERENCES

[1] Abramsky, S., Gabbay, Dov M., and Maibaum, T. S. E. (editors), Handbook of logic in computer science, Volume 2: Background: Computational structures, Oxford University Press, 1992.Google Scholar
[2] Bar-Hillel, Y., Fraenkel, A., and Levy, A., Foundations of set theory, North-Holland, 1973.Google Scholar
[3] Barendregt, H. P., Lambda calculi with types, in [1], pp. 117309, Oxford University Press, 1992.Google Scholar
[4] Barendregt, H. P., The lambda calculus: its syntax and semantics, revised ed., Studies in Logic and the Foundations of Mathematics, vol. 103, North-Holland, Amsterdam, 1984.Google Scholar
[5] Benacerraf, P. and Putnam, H. (editors), Philosophy of mathematics, second ed., Cambridge University Press, 1983.Google Scholar
[6] Beth, E. W., The foundations of mathematics, Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1959.Google Scholar
[7] Boolos, G., The iterative conception of set, Philosophy, vol. LXVIII (1971), pp. 215231.Google Scholar
[8] Burali-Forti, C., Una questione sui numeri transfiniti, Rendiconti del Circolo Matematico di Palermo, vol. 11 (1897), pp. 154164, English translation in [68], pp. 104–112.CrossRefGoogle Scholar
[9] Cantor, G., Beiträge zur Begründung der transfiniten Mengenlehre (Erster Artikel), Mathematische Annalen, vol. 46 (1895), pp. 481512.Google Scholar
[10] Cantor, G., Beiträge zur Begründung der transfiniten Mengenlehre (Zweiter Artikel), Mathematische Annalen, vol. 49 (1897), pp. 207246.Google Scholar
[11] Cauchy, A.-L., Cours d'Analyse de l'Ecole Royale Polytechnique, Debure, Paris, 1821, also as Œuvres Complètes (2), vol. III, Gauthier-Villars, Paris, 1897.Google Scholar
[12] Church, A., A set of postulates for the foundation of logic (1), Annals of Mathematics, vol. 33 (1932), pp. 346366.CrossRefGoogle Scholar
[13] Church, A., A set of postulates for the foundation of logic (2), Annals of Mathematics, vol. 34 (1933), pp. 839864.Google Scholar
[14] Church, A., A formulation of the simple theory of types, The Journal of Symbolic Logic, vol. 5 (1940), pp. 5668.CrossRefGoogle Scholar
[15] Church, A., Comparison of Russell's resolution of the semantic antinomies with that of Tarski, The Journal of Symbolic Logic, vol. 41 (1976), pp. 747760.Google Scholar
[16] Cocchiarella, N. B., Frege's double correlation thesis and Quine's set theories NF and ML, Philosophical Logic, vol. 13 (1984).Google Scholar
[17] Cocchiarella, N. B., Philosophical perspectives on formal theories of predication, Handbook of Philosophical Logic, vol. 4 (1986).Google Scholar
[18] Curry, H. B., Functionality in combinatory logic, Proceedings of the National Academy of Science of the USA, vol. 20 (1934), pp. 584590.Google Scholar
[19] Curry, H. B., Foundations of mathematical logic, McGraw-Hill Series in Higher Mathematics, McGraw-Hill Book Company, Inc., 1963.Google Scholar
[20] Curry, H. B. and Feys, R., Combinatory logic I, Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1958.Google Scholar
[21] Dedekind, R., Stetigkeit und irrationale Zahlen, Vieweg & Sohn, Braunschweig, 1872.Google Scholar
[22] Euclid, , The Elements, 325 B.C., English translation in [36].Google Scholar
[23] Feferman, S., Towards useful type-free theories I, Symbolic Logic, vol. 49 (1984), pp. 75111.CrossRefGoogle Scholar
[24] Frege, G., Letter to Russell, English translation in [68], pp. 127128, 1902.Google Scholar
[25] Frege, G., Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, Nebert, Halle, 1879, also in [68], pp. 182.Google Scholar
[26] Frege, G., Grundlagen der Arithmetik, eine logisch-mathematische Untersuchung über den Begriff der Zahl, Breslau, 1884.Google Scholar
[27] Frege, G., Funktion und Begriff, Vortrag gehalten in der Sitzung vom 9. Januar der Jenaischen Gesellschaft für Medicin und Naturwissenschaft, Hermann Pohle, Jena, 1891, English translation in [50], pp. 137156.Google Scholar
[28] Frege, G., Grundgesetze der Arithmetik, begriffsschriftlich abgeleitet, vol. I, Pohle, Jena, 1892, reprinted 1962 (Olms, Hildesheim).Google Scholar
[29] Frege, G., Über Sinn und Bedeutung, Zeitschrift für Philosophie und philosophische Kritikf (new series), vol. 100 (1892), pp. 2550, English translation in [50], pp. 157177.Google Scholar
[30] Frege, G., Ueber die Begriffschrift des Herrn Peano und meine eigene, Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig, Mathematisch-physikalische Klasse 48, 1896, English translation in [50], pp. 234–248, pp. 361378.Google Scholar
[31] Frege, G., Grundgesetze der Arithmetik, begriffsschriftlich abgeleitet, vol. II, Pohle, Jena, 1903, reprinted 1962 (Olms, Hildesheim).Google Scholar
[32] Gerhardt, C. I. (editor), Die Philosophischen Schriften von Gottfried Wilhelm Leibniz, Berlin, 1890.Google Scholar
[33] Gödel, K., Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, Monatshefte für Mathematik und Physik, vol. 38 (1931), pp. 173198, in German; English translation in [68], pp. 592–618.Google Scholar
[34] Gödel, K., Russell's mathematical logic, The philosophy of Bertrand Russell (Schlipp, P. A., editor), Northwestern University, Evanston & Chicago, 1944, also in [5], pp. 447469.Google Scholar
[35] Grattan-Guinness, I., The search for mathematical roots, 1870–1930, Princeton University Press, 2001.Google Scholar
[36] Heath, T. L., The thirteen books of Euclid's Elements, Dover Publications, Inc., New York, 1956.Google Scholar
[37] Hilbert, D. and Ackermann, W., Grundzüge der Theoretischen Logik, first ed., Die Grundlehren der Mathematischen Wissenschaften in Einzeldarstellungen, Band XXVII, Springer-Verlag, Berlin, 1928.Google Scholar
[38] Holmes, R., Systems of combinatory logic related to predicative and “mildly impredicative” fragments of quine's “new foundations”, Annals of Pure and Applied Logic, vol. 59 (1993), pp. 4553.CrossRefGoogle Scholar
[39] Holmes, R., Subsystems of Quine's “New Foundations” with predicativity restrictions, Notre Dame Journal of Formal Logic, vol. 40 (1999), no. 2, pp. 183196.Google Scholar
[40] Jackson, P. B., Enhancing the nuprl proof development system and applying it to computational abstract algebra, Ph.D. thesis , Cornell University, Ithaca, New York, 1995.Google Scholar
[41] Jensen, R. B., On the consistency of a slight modification of Quine's NF, Synthese, vol. 19 (1969), pp. 250263.Google Scholar
[42] Kamareddine, F. and Laan, T., A reflection on Russell's ramified types and Kripke's hierarchy of truths, Journal of the Interest Group in Pure and Applied Logic, vol. 4 (1996), no. 2, pp. 195213.Google Scholar
[43] Kamareddine, F. and Laan, T., A correspondence between Martin-Löf type theory the ramified theory of types and pure type systems, Logic, Language and Information, vol. 10 (2001), no. 3, pp. 375402.Google Scholar
[44] Kneebone, G. T., Mathematical logic and the foundations of mathematics, D. Van Nostrand Comp., London, New York, Toronto, 1963.Google Scholar
[45] Kripke, S., Outline of a theory of truth, Journal of Philosophy, vol. 72 (1975), pp. 690716.Google Scholar
[46] Laan, T., A formalization of the Ramified Type Theory, Technical Report 94-33, TUE Computing Science Reports, Eindhoven University of Technology, 1994.Google Scholar
[47] Laan, T., The evolution of type theory in logic and mathematics, Ph.D. thesis , Eindhoven University of Technology, 1997.Google Scholar
[48] Laan, T. and Nederpelt, R. P., A modern elaboration of the Ramified Theory of Types, Studia Logica, vol. 57 (1996), no. 2/3, pp. 243278.Google Scholar
[49] Landini, G., Russell's hidden substitutional theory, Oxford University Press, 1998.
[50] McGuinness, B. (editor), Gottlob Frege: Collected papers on mathematics, logic, and philosophy, Basil Blackwell, Oxford, 1984.Google Scholar
[51] Peano, G., Arithmetices principia, nova methodo exposita, Bocca, Turin, 1889, English translation in [68], pp. 8397.Google Scholar
[52] Peano, G., Formulaire de Mathématique, Bocca, Turin, 18941908, 5 successive versions; the final edition issued as Formulario Mathematico.Google Scholar
[53] Peremans, W., Ups and downs of type theory, Technical Report 94-14, TUE Computing Science Notes, Eindhoven University of Technology, 1994.Google Scholar
[54] Poincaré, H., Du rôle de l'intuition et de la logique en mathematiques, C. R. du Ilme Cong. Intern. des Math., Paris 1900, (1902), pp. 200202.Google Scholar
[55] Quine, W. Van Orman, New foundations for mathematical logic, American Mathematical Monthly, vol. 44 (1937), pp. 7080, also in [57], pp. 80–101.Google Scholar
[56] Quine, W. Van Orman, Mathematical logic, Norton, New York, 1940, revised edition Harvard University Press, Cambridge, 1951.Google Scholar
[57] Quine, W. Van Orman, From a logical point of view: 9 logico-philosophical essays, second ed., Harvard University Press, Cambridge, Massachusetts, 1961.Google Scholar
[58] Quine, W. Van Orman, Set theory and its logic, Harvard University Press, Cambridge, Massachusetts, 1963.Google Scholar
[59] Ramsey, F. P., The foundations of mathematics, Proceedings of the London Mathematical Society (second series), vol. 25 (1926), pp. 338384.Google Scholar
[60] Rosser, J. B., Highlights of the history of the lambda-calculus, Annals of the History of Computing, vol. 6 (1984), no. 4, pp. 337349.Google Scholar
[61] Russell, B., Letter to Frege, English translation in [68], pp. 124125, 1902.Google Scholar
[62] Russell, B., The principles of mathematics, Allen & Unwin, London, 1903.Google Scholar
[63] Russell, B., Mathematical logic as based on the theory of types, American Journal of Mathematics, vol. 30 (1908), pp. 222262, also in [68], pp. 150–182.Google Scholar
[64] Schönfinkel, M., Über die Bausteine der mathematischen Logik, Mathematische Annalen, vol. 92 (1924), pp. 305316, also in [68], pp. 355–366.Google Scholar
[65] Schütte, K., Beweistheorie, Die Grundlehren der Mathematischen Wissenschaften in Einzeldarstellungen, Band 103, Springer-Verlag, Berlin, 1960.Google Scholar
[66] Seldin, J. P., Personal communication, 1996.Google Scholar
[67] Specker, E. P., The axiom of choice in Quine's New Foundations for mathematical logic, Proceedings of the National Academy of Sciences of the USA, vol. 39 (1953), pp. 972975.Google Scholar
[68] van Heijenoort, J. (editor), From Frege to Godel: A source book in mathematical logic, 1879–1931, Harvard University Press, Cambridge, Massachusetts, 1967.Google Scholar
[69] van Roou, A. C. M., Analyse voor Beginners, Epsilon Uitgaven, Utrecht, 1986.Google Scholar
[70] Weyl, H., Das Kontinuum, Veit, Leipzig, 1918, in German; also in: Das Kontinuum und andere Monographien , Chelsea Pub. Comp., New York, 1960.Google Scholar
[71] Whitehead, A. N. and Russell, B., Principia Mathematica, vol. I, II, III, Cambridge University Press, 1910, 1912, 19131, 1925, 1925, 19272, all references are to the first volume unless otherwise stated.Google Scholar
[72] Wilder, R. L., The foundations of mathematics, second ed., Robert E. Krieger Publishing Company, Inc., New York, 1965.Google Scholar
[73] Zermelo, E., Untersuchungen über die Grundlagen der Mengenlehre, Mathematische Annalen, vol. 65 (1908), pp. 261281.Google Scholar