Skip to main content
SpringerLink
Log in

Translating set theoretical proofs into type theoretical programs

  • Contributed Papers
  • Conference paper
  • First Online:
Computational Logic and Proof Theory (KGC 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1289))

Included in the following conference series:

  • 237 Accesses

Abstract

We show how to translate proofs of II 02 -sentences in the fragment of set theory KPI +U , which is an extension of Kripke-Platek set theory, into proofs of Martin-Löf's Type Theory using a cut elimination argument. This procedure is effective. The method used is an implementation of techniques from traditional proof theoretic analysis in type theory. It follows that KPI +U and ML1 W show the same II 02 -sentences and have therefore the same programs. As a side result we get that II 02 -sentences provable in intensional and extensional version of ML1W are the same, solving partly a problem posed by M. Hofmann.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barwise, J.: Admissible Sets and Structures. An Approach to Definability Theory, Springer, 1975.

    Google Scholar 

  2. Beeson, M.: Foundations of Constructive Mathematics Springer, Berlin, 1985

    Google Scholar 

  3. Berger, U. and Schwichtenberg, H.: Program Extraction from Classical Proofs. In: D. Leivant (Ed.): Logic and Computational Complexity, LCC '94, Indianapolis, October 1994, Springer Lecture Notes in Computer Science 960, pp. 77–97.

    Google Scholar 

  4. Buchholz, W.: Notation systems for infinitary derivations. Arch. Math. Logic (1991) 30:277–296.

    Google Scholar 

  5. Buchholz, W.: A simplified version of local predicativity. In: Aczel, P. et al. (Eds.): Proof Theory. Cambridge University Press, Cambridge, 1992, pp. 115–147.

    Google Scholar 

  6. Jäger, G.: Theories for Admissible Sets: A Unifying Approach to Proof Theory. Bibliopolis, Naples, 1986.

    Google Scholar 

  7. Schwichtenberg, H.: Proofs as programs. In:Aczel, P. et al. (Eds.): Proof Theory. Cambridge University Press, Cambridge, 1992, pp. 81–113.

    Google Scholar 

  8. Setzer, A.: Proof theoretical strength of Martin-Löf Type Theory with W-type and one universe. PhD-thesis, Munich, 1993.

    Google Scholar 

  9. Setzer, A.: Extending Martin-Löf Type Theory by one Mahlo-Universe. Submitted.

    Google Scholar 

  10. Setzer, A.: Well-ordering proofs for Martin-Löf Type Theory with W-type and one universe. Submitted.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics, Uppsala University, P.O. Box 480, S-751 06, Uppsala, Sweden

    Anton Setzer

Authors
  1. Anton Setzer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Georg Gottlob Alexander Leitsch Daniele Mundici

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Setzer, A. (1997). Translating set theoretical proofs into type theoretical programs. In: Gottlob, G., Leitsch, A., Mundici, D. (eds) Computational Logic and Proof Theory. KGC 1997. Lecture Notes in Computer Science, vol 1289. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63385-5_50

Download citation

  • DOI: https://doi.org/10.1007/3-540-63385-5_50

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63385-3

  • Online ISBN: 978-3-540-69806-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation