Abstract
We present an illative system \(\ensuremath{{\cal I}}_s\) of classical higher-order logic with subtyping and basic inductive types. The system \(\ensuremath{{\cal I}}_s\) allows for direct definitions of partial and general recursive functions, and provides means for handling functions whose termination has not been proven. We give examples of how properties of some recursive functions may be established in our system. In a technical appendix to the paper we prove consistency of \(\ensuremath{{\cal I}}_s\). The proof is by model construction. We then use this construction to show conservativity of \(\ensuremath{{\cal I}}_s\) over classical first-order logic. Conservativity over higher-order logic is conjectured, but not proven.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Barendregt, H., Bunder, M.W., Dekkers, W.: Systems of illative combinatory logic complete for first-order propositional and predicate calculus. Journal of Symbolic Logic 58(3), 769–788 (1993)
Seldin, J.P.: The logic of Church and Curry. In: Gabbay, D.M., Woods, J. (eds.) Logic from Russell to Church. Handbook of the History of Logic, vol. 5, pp. 819–873. North-Holland (2009)
Czajka, Ł.: Higher-order illative combinatory logic. Journal of Symbolic Logic (2013), http://arxiv.org/abs/1202.3672 (accepted)
Dekkers, W., Bunder, M.W., Barendregt, H.: Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic. Journal of Symbolic Logic 63(3), 869–890 (1998)
Czajka, Ł.: Partiality and recursion in higher-order logic. Technical report, University of Warsaw (2013), http://arxiv.org/abs/1210.2039
Sørensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard isomorphism. Studies in Logic and the Foundations of Mathematics, vol. 149. Elsevier, Amsterdam (2006)
Barendregt, H.P.: The lambda calculus: Its syntax and semantics. Revised edn. North Holland (1984)
Blanqui, F., Jouannaud, J., Okada, M.: Inductive-data-type systems. Theoretical Computer Science 272(1), 41–68 (2002)
Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering 24(9) (1998)
Bove, A., Krauss, A., Sozeau, M.: Partiality and recursion in interactive theorem provers: An overview. Mathematical Structures in Computer Science (2012) (to appear)
Bunder, M.W.: Predicate calculus of arbitrarily high finite order. Archive for Mathematical Logic 23(1), 1–10 (1983)
Feferman, S.: Definedness. Erkenntnis 43, 295–320 (1995)
Beeson, M.J.: Proving programs and programming proofs. In: Marcus, R.B., Dorn, G., Weingartner, P. (eds.) Logic, Methodology and Philosophy of Science VII, pp. 51–82. North-Holland (1986)
Farmer, W.M., Guttman, J.D., Thayer, F.J.: IMPS: An interactive mathematical proof system. Journal of Automated Reasoning 11(2), 213–248 (1993)
Farmer, W.M.: A partial functions version of Church’s simple theory of types. Journal of Symbolic Logic 55(3), 1269–1291 (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Czajka, Ł. (2013). Partiality and Recursion in Higher-Order Logic. In: Pfenning, F. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2013. Lecture Notes in Computer Science, vol 7794. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37075-5_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-37075-5_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37074-8
Online ISBN: 978-3-642-37075-5
eBook Packages: Computer ScienceComputer Science (R0)