Abstract
The λII-calculus, a theory of first-order dependent function types in Curry-Howard-de Bruijn correspondence with a fragment of minimal first-order logic, is defined as a system of (linearized) natural deduction. In this paper, we present a Gentzen-style sequent calculus for the λII-calculus and prove the cut-elimination theorem.
The cut-elimination result builds upon the existence of normal forms for the natural deduction system and can be considered to be analogous to a proof provided by Prawitz for first-order logic. The type-theoretic setting considered here elegantly illustrates the distinction between the processes of normalization in a natural deduction system and cut-elimination in a Gentzen-style sequent calculus.
We consider an application of the cut-free calculus, via the subformula property, to proof-search in the λII-calculus. For this application, the normalization result for the natural deduction calculus alone is inadequate, a (cut-free) calculus with the subformula property being required.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Avron, A., 1990, ‘Gentzenizing Schroeder-Heister's Natural Extension of Natural Deduction’,Notre Dame J. of Formal Logic 31, 127–135.
Avron, A., F. Honsell, I.A. Mason and R. Pollack, 1992, ‘Using Typed Lambda Calculus to Implement Formal Systems on a Machine’,J. Automated Reasoning 9, 309–354.
Barendregt, H., 1991, ‘Introduction to generalized type systems’,J. Func. Prog. 1(2), 125–154.
Cartmell, J., 1986, ‘Generalized Algebraic Theories and Contextual Categories’,Annals of Pure and Applied Logic 32, 209–243.
Clocksin, W. F., C.S. Mellish, 1984,Programming in Prolog, Springer-Verlag.
Coquand, Th., 1991, ‘An Algorithm for testing conversion in type theory’, in: G. Huet and G. Plotkin (editors),Logical Frameworks. Cambridge University Press, 255–279.
Daalen, D. T. van, 1980,The Language Theory of AUTOMATH. Ph.D. thesis, Technical University of Eindhoven.
Dowek, G., 1991,Démonstration Automatique dans le Calcul des Constructions. Thèse de Doctorat, Université de Paris 7.
Elliott, C. M., 1990,Extensions and Applications of Higher-order Unification. Ph.D. thesis, School of Computer Science, Carnegie Mellon University. Available as Technical Report CMU-CS-90-134.
Felty, A., 1987, ‘Implementing Theorem Provers in Logic Programming’, University of Pennsylvania report MS-CIS-87-109.
Gentzen, G., 1934, ‘Untersuchungen über das logische Schliessen’,Mathematische Zeitschrift 39, 176–210, 405–431.
Harper, R. 1988, ‘An Equational Formulation oflf’, LFCS, report ECS-LFCS-88-67, University of Edinburgh.
Harper, R., F. Honsell, G. Plotkin 1987, ‘A Framework for Defining Logics’,Proc. Second Annual Symposium on Logic in Computer Science, 194–204. IEEE.
Harper, R., F. Honsell, G. Plotkin, 1993, ‘A Framework for Defining Logics’,J. ACM Vol. 40, No. 1, January, 143–184.
Hindley, J. R. and J. P. Seldin, 1986,Introduction to Combinators and λ-Calculus. Cambridge University Press.
Howard, W. A., 1980, ‘The formulae-as-types notion of construction’, in:To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (editors J.P. Seldin & J.R. Hindley), Academic Press.
Kleene, S. C., 1968,Mathematical Logic. Wiley and Sons.
Martin-Löf, P., 1985, ‘On the meanings of the logical constants and the justifications of the logical laws’, Technical Report 2, Scuola di Specializziazione in Logica Matematica, Dipartimento di Matematica, Università di Siena.
Meyer, A., 1982, ‘What is a Model of the Lambda Calculus?Information and Control 52, 87–122.
Miller, D., G. Nadathur, A. Ščedrov and F. Pfenning, 1991, ‘Uniform Proofs as a Foundation for Logic Programming’,Ann. Pure and Appl. Logic 51, 125–157.
Pfenning, F., 1991, ‘Logic programming in the LF logical framework’, in: G. Huet and G. Plotkin (editors),Logical Frameworks, Cambridge University Press, 149–181.
Prawitz, D. 1965,Natural deduction: a proof-theoretical study. Almqvist & Wiksell.
Pym, D. J., 1990,Proofs, Search and Computation in General Logic. Ph.D. thesis, University of Edinburgh, 1990. Available as report CST-69-90, Department of Computer Science, University of Edinburgh. (Also published as LFCS report ECS-LFCS-90-125.)
Pym, D. J., 1992, ‘A Unification Algorithm for the λII-calculus’,Int. J. of Foundations of Computer Science, Vol. 3, No. 3, 333–378.
Pym, D. J. and L. A. Wallen, 1990, ‘Investigations into Proof-search in a system of first-order dependent function types’,Proc. 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 1990, M. Stickel (editor), Lecture Notes in Artificial Intelligence449, 236–250, Springer-Verlag.
Pym, D. J. and L. A. Wallen, 1991, ‘Proof-search in the λII-calculus’, in: G. Huet and G. Plotkin (editors),Logical Frameworks, Cambridge University Press, 309–340.
Pym, D. J. and L. A. Wallen, 1992, ‘Logic Programming via Proof-valued Computations’, in:ALPUK92, Proc. of the 4th U.K. Conference on Logic Programming, K. Broda (editor), 253–262. Springer-Verlag.
Pym, D. J., 1993, ‘Errata and Remarks’, LFCS Report ECS-LFCS-93-265. University of Edinburgh.
Robinson, J., 1965, ‘A machine-oriented logic based on the resolution principle’,J. Assoc. Comp. Mach. 12, 23–41.
Salvesen, A., 1989, Manuscript, University of Edinburgh.
Schroeder-Heister, P., 1984, ‘A Natural Extension of Natural Deduction’,J. Symb. Log. 49, 1284–1299.
Sieg, W., 1991, ‘Herbrand analyses’,Arch. Math. Logic 30, 409–441.
Smullyan, R. M., 1968, ‘First-order logic’,Ergebnisse der Mathematik 43, Springer-Verlag.
Zucker, J., 1974, ‘The correspondence between cut-elimination and normalisation’,Ann. Math. Logic 7 1–112.
Author information
Authors and Affiliations
Additional information
This paper was written whilst the author was affiliated to the University of Edinburgh, Scotland, U.K. and revised for publication whilst he was affiliated to the University of Birmingham, England, U.K.
Rights and permissions
About this article
Cite this article
Pym, D.J. A note on the proof theory the λII-calculus. Stud Logica 54, 199–230 (1995). https://doi.org/10.1007/BF01063152
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/BF01063152