Re: [isabelle] Defining Real numbers axiomatically



> tell me if there is a way to define the
> real number type
> axiomatically in Isabelle, preferably using IFOL or FOL?

In Isabelle/ZF you can do it as in IsarMathLib's OrderedField_ZF theory,
see section "Definition of real numbers" at the end of 

http://isarmathlib.org/OrderedField_ZF.html .

It is not a type then of course but a quadruple of sets.

Slawekk 


http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)




      





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.