Abstract
Baaz and Fermueller gave in 2003 an original characterization of constructive existence in classical logic [2]. In this note, we give a simple proof of this result based on cut-elimination in sequent calculus. The interest of this proof besides its simplicity is that it allows in particular to generalize the result to other logics enjoying cut-elimination. We also briefly discuss the significance of the characterization itself.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baaz, M.: Note on a translation to characterize constructivity. Proceedings of the Steklov Institute of Mathematics 242, 125,129 (2003)
Baaz, M., Fermueller, C.: A translation characterizing the constructive content of classical theories. In: Vardi, M.Y., Voronkov, A. (eds.) LPAR 2003. LNCS (LNAI), vol. 2850, pp. 107–121. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Parigot, M. (2006). On Constructive Existence. In: Filliâtre, JC., Paulin-Mohring, C., Werner, B. (eds) Types for Proofs and Programs. TYPES 2004. Lecture Notes in Computer Science, vol 3839. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11617990_17
Download citation
DOI: https://doi.org/10.1007/11617990_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31428-8
Online ISBN: 978-3-540-31429-5
eBook Packages: Computer ScienceComputer Science (R0)