Bachelor's Thesis: Studies in Higher-Order Equational Logic




Saarland University
Computer Science
Programming Systems



Thesis (PDF)
Thesis (PS)

Mark Kaminski, Betreuer: Gert Smolka


Motivation

Higher-order logic, also known as type theory, has been introduced in 1908 by Bertrand Russell [33] as a formal basis for mathematical reasoning, based on a functional view of logic originally developed by Gottlob Frege [13]. In its modern form, type theory is based on Alonzo Church’s simply typed lambda-calculus [8] and the formulations by Leon Henkin [22] and Peter Andrews [4]. Over the years type theory has become an integral part of every subject of study that is in some way concerned with the relationship between computation and logical reasoning. In computer science, higher-order logic has lots of applications, including proof assistant systems like e.g. Isabelle [28] or PVS [29].
Classical formulations of type theory employ rules of inference depending on some dedicated logical constants. Consider, for instance, the well-known rule "Modus ponens", commonly formulated as:
From A and A->B, infer B
The rule involves the constant -> and is therefore specific to logical systems where such a constant is built in.

Abstract

We show that higher-order logic (HOL) can be axiomatized in S, the simply typed lambda-calculus with equational deduction. Unlike traditional formulations of HOL, S does not rely on pre-defined semantics of logical constants.
First we show how deduction in traditional HOL can be simulated within S, thus proving S to be a general-purpose higher-order logical system. Afterwards we prove the completeness of S for first-order axioms.
An important task of the thesis is to investigate in how far the usual logical constants and semantic structures can be axiomatized within S. We start by considering Boolean algebras, i.e. systems generated by Boolean axioms and show how they can be axiomatically extended by quantification. We define the identity test and show some important properties of identity in S. We axiomatize in S the usual semantic structure of HOL, thus showing that the semantic expressiveness of S matches that of traditional higher-order formalisms. Finally we analyze the deductive power of S in more detail and obtain interesting incompleteness results for specific instances of the system.

Bibliography

  1. Akama, Y. On Mints' reduction for ccc-calculus. In Proceedings of the International Conference on Typed Lambda Calculi and Applications (TLCA '93) (1993), M. Bezem and J. Groote, Eds., vol. 664 of Lecture Notes in Computer Science, Springer-Verlag, pp. 1-12.
  2. Andrews, P. B. General models and extensionality. Journal of Symbolic Logic 37 (1972), 395-397.
  3. Andrews, P. B. General models, descriptions and choice in type theory. Journal of Symbolic Logic 37 (1972), 385-394.
  4. 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.
  5. Andrews, P. B., and Bishop, M. On sets, types, fixed points, and checkerboards. In Theorem Proving with Analytic Tableaux and Related Methods. 5th International Workshop. (TABLEAUX ’96) (May 1996), P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, Eds., vol. 1071 of Lecture Notes in Artificial Intelligence, Springer-Verlag, pp. 1-15.
  6. Baader, F., and Nipkow, T. Term Rewriting and All That. Cambridge University Press, 1998.
  7. Boolos, G. Logic, logic and logic. Harvard University Press, 1998.
  8. Church, A. A formulation of the simple theory of types. Journal of Symbolic Logic 5, 1 (1940), 56-68.
  9. Davey, B. A., and Priestley, H. A. Introduction to Lattices and Order, second ed. Cambridge University Press, 2002.
  10. de Vrijer, R. C. Exactly estimating functionals and strong normalization. Indagationes Mathematicae 49, 4 (1987), 479-493.
  11. di Cosmo, R., and Kesner, D. Simulating expansions without expansions. Mathematical Structures in Computer Science 4 (1994), 315-362.
  12. Dragalin, A. G. The computability of primitive recursion terms of finite type, and primitive recursive realization. Seminars in Mathematics (1968), 32-45. In Russian.
  13. Frege, G. Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle, 1879. Translated in [45], pp. 1-82.
  14. 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.
  15. Gandy, R. O. Proofs of strong normalization. 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. 457-477.
  16. 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 [45], pp. 596-616.
  17. Gödel, K. Über die Länge von Beweisen. Ergebnisse eines Mathematischen Kolloquiums 7 (1936), 23-24. Translated in [18], pp. 396-399.
  18. Gödel, K. Collected Works, Volume I. Oxford University Press, 1986.
  19. Hanatani, Y. Calculabilité des fonctionelles récursives primitives de type fini sur les nombres naturels. Annals of the Japan Association for Philosophy of Science 3 (1966), 19-30.
  20. Henkin, L. The completeness of formal systems. Thesis in candidacy for the degree of doctor of philosophy, Princeton University, 1947.
  21. Henkin, L. Completeness in the theory of types. Journal of Symbolic Logic 15, 2 (June 1950), 81-91.
  22. Henkin, L. A theory of propositional types. Fundamenta Mathematicae 52 (1963), 323-344.
  23. Henkin, L. Identity as a logical primitive. Philosophia 5 (1975), 31-45.
  24. Hinata, S. Calculability of primitive recursive functionals of finite type. Science Reports of the Tokyo Kyoiku Daigaku A 9 (1967), 218-235.
  25. Hindley, J. R. Basic Simple Type Theory, vol. 42 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1997.
  26. Kamareddine, F., Laan, T., and Nederpelt, R. A Modern Perspective on Type Theory. From its Origins until Today, vol. 29 of Applied Logic Series. Kluwer Academic Publishers, 2004.
  27. Meinke, K. Proof theory of higher-order equations: conservativity, normal forms and term rewriting. Journal of Computer and System Sciences 67 (2003), 127-173.
  28. Nipkow, T., Paulson, L. C., and Wenzel, M. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, vol. 2283 of Lecture Notes in Computer Science. Springer-Verlag, 2002.
  29. Owre, S., Rushby, J. M., and Shankar, N. PVS: A prototype verification system. In 11th International Conference on Automated Deduction (CADE) (Saratoga, NY, June 1992), D. Kapur, Ed., vol. 607 of Lecture Notes in Artificial Intelligence, Springer-Verlag, pp. 748-752.
  30. Pierce, B. C. Types and Programming Languages. The MIT Press, 2002.
  31. Plotkin, G. D. Lambda-definability and logical relations. Memorandum SAI-RM-4, University of Edinburgh, 1973.
  32. Plotkin, G. D. Lambda-definability in the full type theory. 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.
  33. Russell, B. Mathematical logic as based on the theory of types. American Journal of Mathematics 30 (1908), 222-262.
  34. Skolem, T. Begründung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbar Veränderlichen mit unendlichem Ausdehnungsbereich. Videnskapsselskapets skrifter, I. Matematisk-naturvidenskabelig klasse, 6 (1923), 1-38. Translated in [45], pp. 302-333.
  35. Skolem, T. Über die Unmöglichkeit einer vollständigen Charakterisierung der Zahlenreihe mittels eines endlichen Axiomensystems. Norskmatematisk forenings skrifter 2, 10 (1933), 73-82.
  36. 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.
  37. Smolka, G. Introduction to Computational Logic: Lecture Notes. Universität des Saarlandes, 2004. http://www.ps.uni-saarland.de/courses/cl-ss04/script/.
  38. Statman, R. Bounds for proof search and speed-up in the predicate calculus. Annals of Mathematical Logic 15 (1978), 225-287.
  39. Statman, R. Completeness, invariance and lambda-definability. Journal of Symbolic Logic 47, 1 (1982), 17-26.
  40. 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.
  41. Statman, R., and Dowek, G. On statman’s finite completeness theorem. Tech. Rep. CMU-CS-92-152, Carnegie Mellon University, 1992.
  42. Stone, M. H. The representation theorem for Boolean algebras. Transactions of the American Mathematical Society 40 (1936), 37-111.
  43. Tait, W. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic 32 (1967), 198-212.
  44. Terese. Term Rewriting Systems, vol. 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
  45. 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.
  46. van Oostrom, V. Confluence for Abstract and Higher-Order Rewriting. Dissertation, Vrije Universiteit, Amsterdam, 1994.


Legal notice, Privacy policy