×

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

Software:

Pesca
PDFBibTeX XMLCite