Negri, Sara A sequent calculus for constructive ordered fields. (English) Zbl 1010.03050 Schuster, Peter (ed.) et al., Reuniting the antipodes–constructive and nonstandard views of the continuum. Symposium proceedings, San Servolo, Venice, Italy, May 16-22, 1999. Dordrecht: Kluwer Academic Publishers. Synth. Libr. 306, 143-155 (2001). Summary: 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 fields, starting from a quantifier-free axiomatization.For the entire collection see [Zbl 0982.00037]. MSC: 03F65 Other constructive mathematics 12J15 Ordered fields 03F05 Cut-elimination and normal-form theorems Keywords:constructive axiomatizations; cut-elimination; constructive ordered fields; sequent calculus; real closed fields Software:Pesca PDFBibTeX XMLCite \textit{S. Negri}, Synth. Libr. 306, 143--155 (2001; Zbl 1010.03050)