Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Defining Real numbers axiomatically

view this post on Zulip Email Gateway (Aug 18 2022 at 13:19):

From: Jyothis V <jyothisv@gmail.com>
Hi,
Can somebody tell me if there is a way to define the real number type
axiomatically in Isabelle, preferably using IFOL or FOL? I guess what I
basically what I need is a way to define a partial function so that I can
define the properties of say addition without actually implementing
addition.

Thanking in advance,
Sincerely,

Jyothis V,
IIT Kharagpur,
India

view this post on Zulip Email Gateway (Aug 18 2022 at 13:19):

From: Slawomir Kolodynski <skokodyn@yahoo.com>
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)

Last updated: May 03 2024 at 08:18 UTC