Abstract
The theory of constructive ordered fields, based on a relation of strict linear order, is formalized as a proof-theoretical system, a sequent calculus extended with nonlogical rules. It is proved that structural rules, the rules of cut and contraction in particular, can be eliminated from derivations. The method of extension by nonlogical rules is applied also to the theory of real closed fileds, starting from a quantifier-free axiomatization.
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
Bridges, D.S. (1999) Constructive mathematics: a foundation for computable analysis, Theoretical Computer Science, vol. 219, pp. 95–109.
Delzell, C. N. (1996) Kreisel’s unwinding of Artin’s proof, in P. Odifreddi (ed.), Kreiseliana: about and around Georg Kreisel. Wellesley, A.K.Peters, pp. 113–246.
Dragalin, A. (1988) Mathematical Intuitionism: Introduction to Proof Theory, American Mathematical Society, Providence, Rhode Island.
Negri, S. (1999) Sequent calculus proof theory of intuitionistic apartness and order relations, Archive for Mathematical Logic, vol. 38, pp. 521–547.
Negri, S. and J. von Plato (1998) Cut elimination in the presence of axioms, The Bulletin of Symbolic Logic, vol. 4, pp. 418–435.
Negri, S. and J. von Plato (2001) Structural Proof Theory,Cambridge University Press.
Negri, S. and D. Soravia (1999) The continuum as a formal space, Archive for Mathematical Logic, vol. 38, pp. 423–447.
Palmgren, E. (1998) A note on constructive real closed fields, 3 pages.Available at http://www.math.uu.se/ palmgren/publicat.html.
von Plato, J. (1998) A structural proof theory of geometry, manuscript.
von Plato, J. (1998a) Proof theory of full classical propositional logic,manuscript.
Troelstra, A. and H. Schwichtenberg (1996) Basic Proof Theory,Cambridge University Press.
Truss, J. (1997) Foundations of Mathematical Analysis,Oxford University Press.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Negri, S. (2001). A Sequent Calculus for Constructive Ordered Fields. In: Schuster, P., Berger, U., Osswald, H. (eds) Reuniting the Antipodes — Constructive and Nonstandard Views of the Continuum. Synthese Library, vol 306. Springer, Dordrecht. https://doi.org/10.1007/978-94-015-9757-9_13
Download citation
DOI: https://doi.org/10.1007/978-94-015-9757-9_13
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5885-0
Online ISBN: 978-94-015-9757-9
eBook Packages: Springer Book Archive