Hostname: page-component-586b7cd67f-rcrh6 Total loading time: 0 Render date: 2024-11-22T05:35:02.407Z Has data issue: false hasContentIssue false
  • English
  • Français

POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE

Published online by Cambridge University Press:  26 April 2018

PAOLO PISTONE
PAOLO PISTONE*
Affiliation:
DIPARTIMENTO DI MATEMATICA E FISICA UNIVERSITÀ ROMA TRE L.GO S. LEONARDO MURIALDO 1 00146 ROME, ITALYE-mail:[email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

The investigations on higher-order type theories and on the related notion of parametric polymorphism constitute the technical counterpart of the old foundational problem of the circularity (or impredicativity) of second and higher-order logic. However, the epistemological significance of such investigations has not received much attention in the contemporary foundational debate.

We discuss Girard’s normalization proof for second order type theory or System F and compare it with two faulty consistency arguments: the one given by Frege for the logical system of the Grundgesetze (shown inconsistent by Russell’s paradox) and the one given by Martin-Löf for the intuitionistic type theory with a type of all types (shown inconsistent by Girard’s paradox).

The comparison suggests that the question of the circularity of second order logic cannot be reduced to Russell’s and Poincaré’s 1906 “vicious circle” diagnosis. Rather, it reveals a bunch of mathematical and logical ideas hidden behind the hazardous idea of impredicative quantification, constituting a vast (and largely unexplored) domain for foundational research.

Keywords

03A0503F0303F05second order logicimpredicativityintuitionistic type theorynormalization proofs
Type
Articles
Information
Bulletin of Symbolic Logic , Volume 24 , Issue 1 , March 2018 , pp. 1 - 52
Copyright
Copyright © The Association for Symbolic Logic 2018 

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

Asperti, A. and Longo, G., Categories, Types and Structures: An Introduction to Category Theory for the Working Computer Scientist, The M.I.T. Press, Cambridge, MA, 1991.Google Scholar
Bainbridge, E. S., Freyd, P. J., Scedrov, A., and Scott, P. J., Functorial polymorphism. Theoretical Computer Science, vol. 70 (1990), pp. 35–64.Google Scholar
Carnap, R., The logicist foundations of mathematics (1931), Philosophy of Matemathics: Selected Readings (Benacerraf, P. and Putnam, H., editors), Cambridge University Press, Cambridge, 1983, pp. 41–52.Google Scholar
Church, A., A formulation of the simple theory of types. The Journal of Symbolic Logic, vol. 5 (1940), no. 2, pp. 56–68.CrossRefGoogle Scholar
Coquand, T., An analysis of Girard’s paradox, First IEEE Symposium on Logic in Computer Science, Boston, IEEE Computer Society Press, Washington, DC, 1986, pp. 227–236.Google Scholar
Coquand, T., Gunter, C., and Winskel, G., Domain theoretic models of polymorphism. Information and Computation, vol. 81 (1989), no. 2, pp. 123–167.Google Scholar
Curry, H. B. and Feys, R., Combinatory Logic, vol. I, North-Holland, Amsterdam, 1958.Google Scholar
De Bruijn, N. G., The mathematical language AUTOMATH, its usage and some of its extensions, Symposium on Automatic Demonstration (Versailles 1968) (Laudet, M., Lacombe, D., and Schuetzenberger, M., editors), Lecture Notes in Mathematics, vol. 125, Springer-Verlag, Berlin, 1970, pp. 29–61.CrossRefGoogle Scholar
Dosen, K., Cut Elimination in Categories, Kluwer, Dordrecht, 1999.Google Scholar
Dummett, M., Frege: Philosophy of Mathematics, Duckworth, Cambridge, MA, 1991.Google Scholar
Dummett, M., The Logical Basis of Metaphysics, Duckworth, London, 1991.Google Scholar
Dummett, M., The vicious circle principle, Cambridge and Vienna: Frank P. Ramsey and the Vienna Circle (Galavotti, M. C., editor), Vienna Circle Institute Yearbook, vol. 12, Springer, Dordrecht, 2006, pp. 29–33.Google Scholar
Frege, G., The Basic Laws of Arithmetic (1893), trans. Furth, M., University of California, Berkeley, 1967.Google Scholar
Gallier, J., On Girard’s “Candidats de Réductibilité”, Logic and Computer Science (Odifreddi, P., editor), Academic Press, London, 1990, pp. 123–203.Google Scholar
Gentzen, G., Investigations into logical deduction (1934). American Philosophical Quarterly, vol. 1(1964), no. 4, pp. 288–306.Google Scholar
Girard, J.-Y., Interprétation fonctionnelle et élimination des coupures de l’arithmetique d’ordre supérieur, Ph.D. thesis, Université Paris VII, 1972.Google Scholar
Girard, J.-Y., The system F of variable types, fifteen years later. Theoretical Computer Science, vol. 45 (1986), no. 2, pp. 159–192.Google Scholar
Girard, J.-Y., Proof Theory and Logical Complexity, vol. 1, Studies in Proof Theory, Elsevier Science, Napoli, 1990.Google Scholar
Girard, J.-Y., Light linear logic. Information and Computation, vol. 143 (1998), pp. 175–204.Google Scholar
Girard, J.-Y., Lafont, Y., and Taylor, P., Proofs and Types, Cambridge Tracts in Theoretical Computer Science, vol. 7, Cambridge University Press, New York, 1989.Google Scholar
Girard, J.-Y., Scedrov, A., and Scott, P. J., Normal forms and cut-free proofs as natural transformations, Logic from Computer Science (Moschovakis, Y., editor), Mathematical Sciences Research Institute Publications, vol. 21, Springer-Verlag, New York, 1992, pp. 217–241.Google Scholar
Gödel, K., Russell’s mathematical logic, The Philosophy of Bertrand Russell (Schilpp, P. A., editor), Northwestern University, Evanston, IL, 1944, pp. 123–153.Google Scholar
Goldfarb, W. D., Jacques Herbrand, Logical Writings, Harvard University Press, Cambridge, MA, 1987.Google Scholar
Harper, R. and Mitchell, J. C., Parametricity and variants of Girard’s J operator. Information Processing Letters, vol. 70 (1999), no. 1, pp. 1–5.Google Scholar
Heck, R. G., Grundgesetze der Arithmetik I §§29–32 29–32. Notre Dame Journal of Formal Logic, vol. 38 (1998), pp. 437–474.Google Scholar
Hermida, C., Reddy, U. S., and Robinson, E. P., Logical relations and parametricity. A Reynolds programme for category theory and programming languages. Electronic Notes in Theoretical Computer Science, vol. 303 (2014), pp. 149–180.Google Scholar
Howard, W. A., The formula-as-types notion of construction (1969), To H.B. Curry. Essays on Combinatory Logic, Lambda Calculus and Formalism (Seldin, J. P. and Hindley, J. R., editors), Academic Press, New York, 1980.Google Scholar
Hurkens, A. J. C., A simplification of Girard’s paradox, Second International Conference on Typed Lambda Calculi and Applications (Dezani-Ciancaglini, M. and Plotkin, G., editors), Springer-Verlag, Berlin, Heidelberg, New York, 1995, pp. 266–278.Google Scholar
Kamareddine, F., Laan, T., and Nederpelt, R., A Modern Perspective on Type Theory, from its Origins until Today, Kluwer Academics, Dordrecht, 2004.Google Scholar
Krivine, J.-L., Realizability in classical logic, Interactive Models of Computation and Program Behaviour. Panoramas et synthèses, vol. 27, Société Mathématique de France, Paris, 2009, pp. 187–229.Google Scholar
Lambek, J. and Scott, P. J., Introduction to Higher Order Categorical Logic, Cambridge University Press, Melbourne, 1986.Google Scholar
Longo, G. and Fruchart, T., Carnap’s remarks on impredicative definitions and the genericity theorem, Logic and Foundations of Mathematics (Cantini, A., Casari, E., and Minari, P., editors), Synthese Library (Studies in Epistemology, Logic, Methodology, and Philosophy of Science), vol. 280, Springer, Dordrecht, 1999, pp. 41–55.Google Scholar
Longo, G., Milsted, K., and Soloviev, S., The genericity theorem and the notion of parametricity in the polymorphic λ-calculus. Theoretical Computer Science, vol. 121 (1993), pp. 323–349.Google Scholar
Martin-Löf, P., A theory of types, unpublished manuscript, 1970.Google Scholar
Parigot, M., Classical proofs as programs, Kurt Gödel Colloquium (Gottlob, G., Leitsch, A., and Mundici, D., editors), Lecture Notes in Computer Science, vol. 713, Springer-Verlag, Berlin, Heidelberg, New York, 1993, pp. 263–276.Google Scholar
Poincaré, H., Les mathématiques et la logique. Revue de Métaphysique et de Morale, vol. 14 (1906), no. 3, pp. 294–317.Google Scholar
Prawitz, D., Hauptsatz for higher order logic. The Journal of Symbolic Logic, vol. 33 (1968), no. 3, pp. 452–457.CrossRefGoogle Scholar
Prawitz, D., Ideas and results in proof theory, Proceedings of the 2nd Scandinavian Logic Symposium (Oslo) (Fenstad, J. E., editor), Studies in Logic and Foundations of Mathematics, vol. 63, North-Holland, Amsterdam, 1971, pp. 235–307.Google Scholar
Reynolds, J. C., Towards a theory of type structure, Programming Symposium (Robinet, B., editor), Lecture Notes in Computer Science, vol. 19, Springer-Verlag, Berlin, Heidelberg, New York, 1974, pp. 408–423.CrossRefGoogle Scholar
Reynolds, J. C., Types, abstraction and parametric polymorphism, Information Processing ’83 (Mason, R. E. A., editor), North-Holland, Amsterdam, 1983, pp. 513–523.Google Scholar
Russell, B., On some difficulties in the theory of transfinite numbers and order types. Proceedings of the London Mathematical Society, vol. 4 (1906), pp. 29–53.Google Scholar
Russell, B., Mathematical logic as based on the theory of types. Americal Journal of Mathematics, vol. 30 (1908), no. 3, pp. 222–262.Google Scholar
Russell, B., The Principles of Mathematics, second ed. [first published 1903], W.W. Norton & Company, New York, 1938.Google Scholar
Russell, B. and Whitehead, A. N., Principia Mathematica, Cambridge University Press, London, 1910.Google Scholar
Strachey, C., Fundamental concepts in programming languages. Higher Order and Symbolic Computation, vol. 13 (1967), pp. 11–49.Google Scholar
Sundholm, G., Intuitionism and logical tolerance, Alfred Tarski and the Vienna Circle (Wolenski, J. and Köhler, E., editors), Vienna Circle Institute Yearbook, vol. 6, Springer, Dordrecht, 1999, pp. 135–148.Google Scholar
Tait, W. W., Intensional interpretation of functionals of finite type I. The Journal of Symbolic Logic, vol. 32 (1967), no. 2, pp. 198–212.Google Scholar
Tait, W. W., A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic. The Journal of Symbolic Logic, vol. 33 (1968), no. 2, pp. 289–290.Google Scholar
Takahashi, M., A proof of the cut-elimination theorem in simple type-theory. Journal of the Mathematical Society of Japan, vol. 19 (1967), no. 4, pp. 399–410.Google Scholar
Tranchini, L., Pistone, P., and Petrolo, M., The naturality of natural deduction. Studia Logica (2017), online first, https://doi.org/10.1007/s11225-017-9772-6.Google Scholar