Master's Thesis: Completeness Results for Higher-Order Equational Logic




Saarland University
Computer Science
Programming Systems



Thesis (PDF)
Thesis (PS)

Mark Kaminski, Advisor: Gert Smolka


Higher-Order Equational Logic

The simply typed lambda-calculus, introduced by Church [13], is nowadays considered one of the most important formal frameworks in mathematical logic and computer science, both in its own right and as a basis for more expressive calculi. Fundamental properties of the pure simply typed lambda-calculus, the simplest version of the calculus without constants or axioms, include decidability of deductive equality, essentially proven by Turing [17], and deductive completeness with respect to general and standard set-theoretic semantics, first shown by Friedman [16].

The equational proof system of the simply typed lambda-calculus with constants can be used to investigate the logical consequences of arbitrary sets of equational axioms in the same way as first-order equational reasoning is used to study algebraic theories (see [33]). Therefore, in the same sense as first-order equational reasoning from algebraic axioms is called first-order equational logic, equational reasoning in the simply typed lambda-calculus from higher-order axioms may be called higher-order equational logic.

The theory of beta-eta-conversion in the pure simply typed lambda-calculus, i.e. the set of all constant-free equations derivable by a finite number of beta-eta-conversion steps, can then be seen as a particular theory of higher-order equational logic, namely the one generated by the empty set of axioms. Of course, higher-order equational logic allows us to specify many more interesting theories, like equational formulations of Church's higher-order logic [13] or fragments thereof, Gödel's T [21] or Scott's PCF [41] (see also [40,38,42,30,45]).

Abstract

We present several results concerning deductive completeness of the simply typed lambda-calculus with constants and equational axioms.

First, we prove deductive completeness of the calculus with respect to standard semantics for axioms containing neither free nor bound occurrences of higher-order variables. Using this result, we analyze some fundamental deductive and semantic properties of axiomatic systems without higher-order variables and compare them to those of established logical frameworks like first-order logic and Church's higher-order logic.

Second, we present a finite higher-order equational formulation of Henkin's Propositional Type Theory (PTT) [25] and prove its deductive completeness. We introduce a simple criterion which allows to reduce deductive completeness of systems with axiomatically defined constants to completeness of simpler axiomatic systems, and present an application of this criterion to our formulation of PTT.

Third, we prove the simply typed lambda-calculus both with and without eta-conversion complete with respect to general semantics. The result holds for systems with arbitrary axioms and constants.

Bibliography

  1. Andrews, P. B. A reduction of the axioms for the theory of propositional types. Fundamenta Mathematicae 52 (1963), 345-350.
  2. Andrews, P. B. A transfinite type theory with type variables. Journal of Symbolic Logic 33, 1 (March 1965), 112-113.
  3. Andrews, P. B. General models and extensionality. Journal of Symbolic Logic 37 (1972), 395-397.
  4. Andrews, P. B. General models, descriptions and choice in type theory. Journal of Symbolic Logic 37 (1972), 385-394.
  5. Andrews, P. B. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, second ed., vol. 27 of Applied Logic Series. Kluwer Academic Publishers, 2002.
  6. Baader, F., and Nipkow, T. Term Rewriting and All That. Cambridge University Press, 1998.
  7. Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics, 2nd ed., vol. 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1984.
  8. Barendregt, H. P. Lambda calculi with types. In Handbook of Logic in Computer Science, S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, Eds., vol. 2. Oxford University Press, 1992.
  9. Benzmüller, C., Brown, C. E., and Kohlhase, M. Higher-order semantics and extensionality. Journal of Symbolic Logic 69, 4 (December 2004), 1027-1088.
  10. Birkhoff, G. On the structure of abstract algebras. Proceedings of the Cambridge Philosophical Society 31 (1935), 433-454.
  11. Brown, C. E. Set Comprehension in Church's Type Theory. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University, 2004.
  12. Burris, S., and Sankappanavar, H. P. A Course in Universal Algebra. Graduate Texts in Mathematics. Springer-Verlag, 1981.
  13. Church, A. A formulation of the simple theory of types. Journal of Symbolic Logic 5, 1 (1940), 56-68.
  14. Davey, B. A., and Priestley, H. A. Introduction to Lattices and Order, second ed. Cambridge University Press, 2002.
  15. Fitting, M. First-Order Logic and Automated Theorem Proving, second ed. Graduate Texts in Computer Science. Springer-Verlag, 1996.
  16. Friedman, H. Equality between functionals. In Proceedings of the Logic Colloquium 72-73 (1975), R. Parikh, Ed., vol. 453 of Lecture Notes in Mathematics, Springer-Verlag, pp. 22-37.
  17. Gandy, R. O. An early proof of normalization by A. M. Turing. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. R. Hindley and J. P. Seldin, Eds. Academic Press, 1980, pp. 453-455.
  18. Girard, J.-Y. Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur. Thèse de doctorat d'état, Université de Paris VII, 1972.
  19. Gödel, K. Die Vollständigkeit der Axiome des logischen Funktionenkalküls. Monatshefte für Mathematik und Physik 37 (1930), 349-360. Translated in [49], pp. 582-591.
  20. Gödel, K. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik 38 (1931), 173-198. Translated in [49], pp. 596-616.
  21. Gödel, K. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica 12 (1958), pp. 280-287. Translated in [22], pp. 240-252.
  22. Gödel, K. Collected Works, Volume II, Publications 1938-1974. Oxford University Press, 1990.
  23. Henkin, L. The completeness of formal systems. Thesis in candidacy for the degree of doctor of philosophy, Princeton University, 1947.
  24. Henkin, L. Completeness in the theory of types. Journal of Symbolic Logic 15, 2 (June 1950), 81-91.
  25. Henkin, L. A theory of propositional types. Fundamenta Mathematicae 52 (1963), 323-344.
  26. Henkin, L. Identity as a logical primitive. Philosophia 5 (1975), 31-45.
  27. Hindley, J. R. Basic Simple Type Theory, vol. 42 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1997.
  28. Hindley, J. R., and Seldin, J. P. Introduction to Combinators and Lambda-calculus. Cambridge University Press, 1986.
  29. Hrbacek, K., and Jech, T. Introduction to Set Theory, third ed. Pure and Applied Mathematics. Marcel Dekker, 1999.
  30. Kaminski, M. Studies in Higher-Order Equational Logic. Bachelor's thesis, Saarland University, 2005.
  31. Manca, V., and Salibra, A. First-order theories as many-sorted algebras. Notre Dame Journal of Formal Logic 25, 1 (1984), 86-94.
  32. Meyer, A. R. The inherent computational complexity of theories of ordered sets. In Proceedings of the International Congress of Mathematicians (Vancouver, August 1974), pp. 477-482.
  33. Mitchell, J. C. Foundations for Programming Languages. Foundations of Computing. The MIT Press, 1996.
  34. Mycielski, J. Equational treatment of first-order logic. Algebra Universalis 33, 1 (1995), 26-39.
  35. Peano, G. Arithmetices principia, nova methodo exposita. Turin, 1889. Translated in [49], pp. 83-97.
  36. Pierce, B. C. Types and Programming Languages. The MIT Press, 2002.
  37. Plotkin, G. D. Lambda-definability and logical relations. Memorandum SAI-RM-4, University of Edinburgh, 1973.
  38. Plotkin, G. D. LCF considered as a programming language. Theoretical Computer Science 5, 3 (1977), 223-255.
  39. Plotkin, G. D. Lambda-definability in the full type hierarchy. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. R. Hindley and J. P. Seldin, Eds. Academic Press, 1980, pp. 365-373.
  40. Sazonov, V. Expressibility of functions in D. Scott's LCF. Algebra and Logic 15, 3 (1976), 192-206.
  41. Scott, D. S. A type-theoretical alternative to ISWIM, CUCH, OWHY. Unpublished manuscript, 1969.
  42. Scott, D. S. A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science 121, 1-2 (1993), 411-440.
  43. Skolem, T. Über die Unmöglichkeit einer vollständigen Charakterisierung der Zahlenreihe mittels eines endlichen Axiomensystems. Norskmatematisk forenings skrifter 2, 10 (1933), 73-82.
  44. Skolem, T. Über die Nicht-charakterisierbarkeit der Zahlenreihe mittels endlich oder abzählbar unendlich vieler Aussagen mit ausschließlich Zahlenvariablen. Fundamenta mathematicae 23 (1934), 150-161.
  45. Smolka, G. Introduction to Computational Logic: Lecture Notes. Universität des Saarlandes, 2006. http://www.ps.uni-saarland.de/courses/cl-ss06/script/.
  46. Statman, R. Equality between functionals revisited. In Harvey Friedman's Research on the Foundations of Mathematics, L. A. Harrington et al., Eds. North-Holland, 1985, pp. 331-338.
  47. Tait, W. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic 32 (1967), 198-212.
  48. Terese. Term Rewriting Systems, vol. 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
  49. van Heijenoort, J., Ed. From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931. Source Books in the History of the Sciences. Harvard University Press, 2002.
  50. Vorobyov, S. The most nonelementary theory. Information and Computation 190, 2 (May 2004), 196-219.


Legal notice, Privacy policy