Abstract
We introduce a type theory for infinitely branching trees, called the theory of free algebras. In this type theory we define an extensional equality based on decidable atomic formulas only. We show, that equality axioms, which add full extensionality to the theory, yield a conservative extension of the (intensional) type theory for formulas having types of level≤1. Types like nat → nat and well-founded trees with branching over the natural numbers (Kleene's O) have this property. We can therefore extract constructive proofs and programs from classical proofs of II 2-sentences with this restriction on the types.
Part of this research was supported by the EU-supported Twinning Project “Proofs and Computation”, Leeds-Munich-Oslo. The research was written up, while the author, at that time based in Munich, was visiting the universities of Stockholm and Uppsala. The author wants to thank P. Martin-Löf for inviting him and making this fruitful visit possible and the logic group in Uppsala for providing such a creative and thoughtful environment.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Berger, U.: Program extraction from normalization proofs. In: M. Bezem, J.F. Groote (Eds.): Typed Lambda Calculi and Applications. Springer Lecture Notes in Computer Science 664, 1993, pp. 91–106.
Berger, U.: A constructive interpretation of inductive definitions. Draft, Dept. of Mathematics, University of Munich, 1994.
Berger, U.: Programs from classical proofs. In: Behara, M., Fritsch, R., Lintz, R. G. (Eds.): Symposia Gaussiana. Proceedings of the 2nd Gauss Symposium. Conference A: Mathematics and Theoretical Physics, Walter de Gruyter, Berlin, 1995, pp. 187–200.
Berger, U., Schwichtenberg, H.: Program extraction from classical proofs. In: Leivant, D. (Ed.): Logic and Computational Complexity, Springer Lecture Notes in Computer Science 960, 1995, pp. 77–97.
Berger, U., Schwichtenberg, H.: Program development by proof transformation, In: Schwichtenberg, H. (Ed.): Proof and Computation. NATO Advanced Study Institute, International Summer School held in Marktoberdorf, Germany, July 20–August 1, 1993. Springer, Heidelberg, 1995, pp. 1–45.
Berger, U., Schwichtenberg, H.: The greatest common divisor: a case study for program extraction from classical proofs. To appear in: Proceedings of Proofs and Types, Turin 1995, 1996.
Gandy, R.: On the axiom of extensionality — part I, Journal of Symbolic Logic, 21, 1956, pp. 36–48.
Gandy, R.: On the axiom of extensionality — part II, Journal of Symbolic Logic, 24, 1959, pp. 287–300.
Luckhardt, H.: Extensional Gödel Functional Interpretation. A Consistency Proof of Classical Analysis. Springer Lecture Notes in Mathematics 306, 1973.
Martin-Löf, P.: Intuitionistic type theory, Bibliopolis, Naples, 1984.
Murthy, C.: Extracting constructive content from classical proofs. PhD thesis. Technical Report 90-1151, Dept. of Computer Science, Cornell University, Ithaca, New York, 1990.
Nordström, B., Petersson, K., Smith, J.: Programming in Martin-Löf's type theory. An Introduction, Oxford University Press, Oxford, 1990.
Paulin-Mohring, C: Inductive definitions in the system Coq. Rules and Properties. In: Bezem, M., Groote, J.F. (Eds.): Typed lambda calculi and applications, Springer Lecture Notes in Computer Science 664, 1993, pp. 328–345.
Schwichtenberg, H.: Normalization. In: Bauer, F. L. (Ed.): Logic, Algebra and Computation. Springer, Heidelberg, 1991, pp. 201–237.
Schwichtenberg, H.: Minimal from classical proofs. In: Börger, E., Jäger, G., Kleine-Büning, H., Richter, M. M.: Computer Science Logic, Springer Lecture Notes in Computer Science 626, 1992, pp. 326–328.
Schwichtenberg, H.: Minimal Logic for computable functions. In: Bauer, F. L., Brauer, W., Schwichtenberg, H.: Logic and Algebra of Specification, NATO Advanced Study Institute, International Summer School held in Marktoberdorf, Germany, July 23–August 4, 1991, Springer, Heidelberg, 1993, pp. 289–320.
Schwichtenberg, H.: Proofs as Programs. In: Aczel, P., Simmons, H., Wainer, S. S.: Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990. Cambridge University Press, 1993, pp. 81–113.
Schwichtenberg, H.: Proof Theory. Manuskript, Dept. of Mathematics, University of Munich, 1994. Available via http://www.mathematik.uni-muenchen.de/~schwicht/lectures/proofth/ss94/pt.dvi.Z.
Schwichtenberg, H.: Computational Content of Proofs. To appear in Proceedings of the Summerschool in Marktoberdorf, 1995.
Setzer, A.: Proof Theoretical Strength of Martin-Löf Type Theory with W-Type and One Universe, PhD thesis, University of Munich, Dep. of Mathematics, 1993.
Setzer, A.: A type theory for iterated inductive definitions, Draft, Munich, 1994. Available via http://www.mathematik.uni-muenchen.de/~setzer/articles.
Setzer, A.: Well-ordering proofs for Martin-Löf Type Theory with W-type and one universe. Submitted. A preliminary version is available via http://www.mathematik.uni-muenchen.de/~setzer/articles.
Troelstra, A. S., Dalen, D. v.: Constructivism in Mathematics. An introduction, volume 121, 123 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1988
Troelstra, A. S. (Ed.): Metamathernatical Investigation of Intuitionistic Arithmetic and Analysis. Springer Lecture Notes in Mathematics 344, 1973.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Setzer, A. (1997). Inductive definitions with decidable atomic formulas. In: van Dalen, D., Bezem, M. (eds) Computer Science Logic. CSL 1996. Lecture Notes in Computer Science, vol 1258. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63172-0_53
Download citation
DOI: https://doi.org/10.1007/3-540-63172-0_53
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63172-9
Online ISBN: 978-3-540-69201-0
eBook Packages: Springer Book Archive