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 .

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

Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)


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