## IsarMathLib 1.7.2

I have released a new version of IsarMathLib. It adds about 50 new lemmas, mostly in group theory and topology, leading to the following characterization of closure in topological groups:

$\overline{A} = \bigcap_{H\in \mathcal{N}_0} A+H$

Here, $\mathcal{N}_0$ is the collection of neighborhoods of zero (sets whose interior contains the neutral element of the group), and for two sets $A,B\subseteq G$ we define $A+B$ as $A+B=\{a+b | a\in A, b\in B\}$.

Also, I replaced jsMath with MathJax as the LaTeX rendering engine on the isarmathlib.org site. The results are very good, the math renders faster and it looks better. It forced me to do some Haskell programming again to modify the tool that parses Isar and generates HTML with LaTeX markup. I haven’t seen that code or programmed in Haskell for about two years, but with Leksah now in Ubuntu repositories it was rather easy: just modify the code in one place and keep fixing it until it builds. Once it built, it worked.

The tool will probably become obsolete after the next Isabelle release. There is a Google Summer of Code project that will allow generating nice HTML presentations of Isar theories from within Isabelle.

### 22 Responses to “IsarMathLib 1.7.2”

1. James Frank Says:

Thanks for library. I’m trying to figure out which road to travel, Isabelle or Coq; these two seem to be the most used and supported.

Not being an expert in logic, I’m trying to figure out which can be used to prove the most types of math theorems.

You’ve answered the question about Isabelle having the axiom of choice. You say that Coq doesn’t have the axiom of choice.

Now I’m trying to figure out if Isabelle has inaccessible cardinals. It’s not that I know I need them, but if Coq has them, then it makes me want Isabelle to have them.

It’s looking like Isabelle is the best choice.

Thanks again.

2. slawekk Says:

There are two somewhat independent choices to be made: one of the proof assistant and one of the foundation. Both Coq and Isabelle can support different logics. Higher Order Logic (HOL) is the best developed logic for Isabelle. If you have a computing science background and think about software verification you will like Isabelle/HOL. However, the standard foundation for modern mathematics is ZFC. Isabelle/ZF provides that choice, but this logic is much less developed than HOL. IsarMathLib is a library for Isabelle/ZF.

The AFP entry from your link is for Isabelle/HOL. Apparently, even though cardinals and ordinals are notions specific to set theory, one can consider something analogous in HOL as well.

As for inaccessible cardinals it is a feature of foundation, not of the proof assistant (or its logical framework). If you want them, you just add (declare) appriopriate axiom.

One can encode ZFC in COQ as well, but it doesn’t look such encoding is used much.

3. James Frank Says:

Thanks for the reply. I can program a little, and it was studying Haskell that led me proof assistants.

However, I’m mainly interested in applying theorem provers to math, though, unlike you, I don’t have a prejudice against programming style notation. One important factor is streamlined notation, like with Haskell. The fewer the delimiters and characters the better. So more efficient programming notation would be better than less efficient math notation.

Another big priority is development support, community support, and documentation. With Isabelle’s document generation and LaTeX support, that gives it a lot of appeal to me. Also, for math, it seems to have a more mathematical emphasis and style than Coq.

Having material to learn from is also important, so I’ll have to first focus on Isabelle/HOL rather than Isabelle/ZF. After doing that I’ll be able to figure out if ZF is where I need to go (if I decide that theorem provers will be fruitful timewise)

I’m always looking for opportunity in math, so getting on the IsarMathLib/ZF bandwagon may be the thing to do, but there’s no use talking about it right now.

I’m at the beginning graduate level, although right now I’m mainly working through some undergrad textbooks. My current idea is to get competent enough in Isabelle to be able to do the textbook proof exercises using Isabelle.

4. James Frank Says:

I might also develop a prejudice against programming notation. It’s just right now, I’m so happy with having discovered functional programming.

I was looking at Haskabelle, and dreaming about only having to operate in only one language, but after briefly looking at the Isabelle/HOL code it generates, and in spite of the little I know about it all, that the one programming language idea appears to be a loser idea.

5. James Frank Says:

For the 1.7.2 download, the version in the proof document says it’s 1.7.3.

Finally got Cygwin to work right, so I’m back in Windows land with jEdit and i3p.

6. slawekk Says:

Yes, I noticed that mistake after the release. The next version will be 1.7.4.
As for notation, I don’t admit having a prejudice against programming notation (vs mathematical notation). Syntax in programming languages is good for programming i.e. for writing programs. Math notation evolved as means of communication of ideas, with more emphasis on the reader side. I believe notation for formalized math should be similar to standard math to make it easier for readers, even though it may be more difficult for an author (writer) to input.

7. James Frank Says:

Trivial mistake, of course, but it shows I’m paying attention.

In researching the best route to take with theorem provers, I’ve come around to your view about the notation and foundational aspects. If I’m studying standard math, then the syntax and foundation of the theorem prover should model what I’m studying, as much as possible.

For others to be able to see that what I’m doing is math, I need to work with ZF rather than HOL.

But all the above thinking led me to Mizar, which I abandoned looking into several times because it wasn’t obvious there was any support and documentation. But there is.

I’m out to learn from people right now, and Mizar has the biggest library, it’s based on first-order logic, and it has the axiom of choice. Also, the syntax is reasonably readable in ASCII text.

As much as I like LaTeX, to be able to move faster, I’ve capitulated to just writing short math notes in ASCII text, like in the bookmarks tree of a PDF.

Anyway, I’ve discovered jEdit has enough plugins to tweek it to how I like to work, which living and dying by a tree view. With the outline plugin and sidekick plugin, jEdit will make a tree in any file based on the indentation.

For what I want to do right now, all I need to be given is an ordered field, or maybe even not even that much, since the exercise for me will be to take only the minimum axiom, theorems, and definitions that a textbook starts with.

Isabelle could give me that. The problem is that if I’m trying to implement a definition or theorem, and I can’t figure it out, I need to see how the masters did it, and Mizar seems to have the biggest library to learn from.

I’m still trying to figure out how to fit Isabelle in there. It took me a while, but I finally figured out how to build the heap for IsarMathLib. Your instructions are only good for building the documentation.

You might consider adding some instructions for building your library. I don’t know if you intend for people to build the heap, or if they’re simply supposed to import the IsarMathLib files.

Here’s my notes on how to build everything, based on using Cygwin, and a root folder of E:\E_main2\binp:

*******************************************
Build Instructions
*******************************************
Information on how to build files, on environment variables,
and on the setting file are in “system.pdf”:
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/

*******************************************
Isabelle Setting FILE
*******************************************
The setting file is E:\E_main2\binp\Isabelle2011\etc\settings.

*******************************************
Making HTML and Graph Docs
*******************************************
To have the build process automatically make html, graph, and pdf, add:
-i true -d pdf
to ISABELLE_USEDIR_OPTIONS in the file Isabelle2011\etc\settings.

*******************************************
Building the ZF or HOL Logic.
ZF doesn’t come built. Neither HOL or ZF
comes with the html, graph, and pdf documents.
*******************************************
1) Go to the Isabelle home folder, such as E:\E_main2\binp\Isabelle2011
2) Type ./build HOL or ./build ZF
3) This will create some binaries in the heaps folder:
E:\E_main2\binp\Isabelle2011\heaps\polyml-5.4.0_x86-cygwin
4) If the build says there’s nothing to do, you can delete the logics
in the heaps folder.

*******************************************
Building IsarMathLib heap, and HTML, session.graph,
and PDF documentation.
*******************************************
0) To build the documentation automatically,
change the settings files as shown above.
1) Unzip the file under Cygwin as follows:
tar xzf isarmathlib-1.7.2.tar.gz
2) Change to the sub-folder where the file “ROOT.ML” is:
isarmathlib-1.7.2\IsarMathLib
3) At the command line, type:
isabelle usedir -b ZF IsarMathLib
4) The documents will be put in a user folder like like:
E:\E_main2\binp\Cygwin\home\jv\.isabelle\Isabelle2011\browser_info\ZF\IsarMathLib
5) The heap will be put in a user folder like:
E:\E_main2\binp\Cygwin\home\jv\.isabelle\Isabelle2011\heaps\polyml-5.4.0_x86-cygwin

8. slawekk Says:

Thank you for this excellent writeup. I definitely need to update the INSTALL file in the IsarMathLib distribution.

It took me a while, but I finally figured out how to build the heap for IsarMathLib… I don’t know if you intend for people to build the heap, or if they’re simply supposed to import the IsarMathLib files

Building IsarMathLib heap is mentioned on the Isarmathlib-devel mailing list.
I usually import IsarMathLib files rather than building the heap.

I encourage you to ask when you run into problems, I will be happy to answer if I can.
IsarMathLib has a theory on ordered fields, I hope you have noticed that.

9. James Frank Says:

I’m happy to have someone to ask questions, but I also try not to wear out my welcome by asking questions, since answering questions takes time. Before I say more, I’ll ask several questions. You gotta get it while the gettin’s good.

(Q1) jEdit/Isabelle displays good math notation in the editor, but I haven’t found an easy way to do subscripts. For superscripts, I guess using the caret can be used, such as A^2.

But for subscript, all I’ve found is \, which is pretty obnoxious, plus neither jEdit or i3p do command completion for that command. The question: Is there an easy way to notate subscripts? I remember reading one of your posts where you were complaining about subscripts and superscripts.

(Q2) In thinking about exponents, I looked some for exponentiation being defined in ZF or in IsarMathLib. HOL has an exponentiation chapter, but I searched on “exponent” and I didn’t find anything in ZF or IsarMathLib. Is exponentiation defined in ZF or IsarMathLib?

(Q3) Do you have a preferred way for me to ask questions? Email can become a burden. What you need is a WordPress plugin to host some kind of question forum on this blog, but I’m sure WordPress doesn’t provide access to one. You could create a page or a post, and it could be used for running, misc., help-type questions not directly related to a post. If it got too long, you’d delete it or create another post. I have your blog comments feed in my RSS reader. The RSS reader won’t notify me of a new blog page (vs. post), but I don’t know if it’ll read a blog page comment.

(Remark 1) Yea, I saw that you have groups and fields. Like I’ve said, my main present goal is to take a textbook, figure out the minimum foundation the book is starting with, and as an exercise, implement the rest. For example, in analysis, you start with the definition of a field, so the foundation would be everything I would need to be able to define a field, which wouldn’t be a field. However, if I couldn’t figure out how to implement a field in Isabelle, I’d want to look at some library code which does implement a field. So that’s why I noticed you have fields and groups and functions and things.

(Q4) I’ve never figured out if the least upper bound property is something that has to be axiomized, or it’s somehting that can be proved. I can’t remember an analysis book introducing it as provable, but needing to take it as an axiom at that level. So, can the supremum property be proved, or does it have to be taken as an axiom?

(Remark 2) I’ve done a quick search on ZF and IsarMathLib for “supremum property” and “least upper bound property”, but I didn’t find anything. I found “supremum property” in HOL in RComplete.thy. This is an example where, in the future, the HOL code might give me some guidance on how to add the supremum property to an ordered field so I could have a complete ordered field.

(Remark Ending) In “Comparing mathematical provers” (http://www.cs.ru.nl/~freek/comparison/index.html 1st link), Freek Wiedijk talks about the Poincare principle, where trivial tasks shouldn’t have to be spelled out, and lists Mizar as having no automation. That’s sort of what I saw in looking around at Mizar code. Simple things had to be spelled out and labelled with the justification.

But I suppose Mizar has been very useful to those who’ve used it, and in the process of looking at it, I learned some important things about jEdit, and found some important jEdit plugins.

I’ve decided that I have to use HOL because the library is so big; it can teach me something. I could try and do everything twice, in HOL and in ZF, but that sounds impractical.

This all assumes I’ll decide there’ll be some return on investment for learning Isabelle. I’m all set up now with documentation and tools to try and figure that out.

• slawekk Says:

(Q2) What do you mean by exponentiation? If you mean taking a monoid element to some natural power, then it is easy to define in IsarMathLib (but is not yet) using the notions of Fold and ConstantFunction.
If you mean the function exp(x), then it is much more difficult. You need addition, multiplication and limits. So the natural setting would be a Hausdorff (topological) ring. You can try taking shortcuts to work in real numbers, but from my experience considering special cases does not save much work.

Q4. The least upper bound property is something you need to prove when you are constructing real numbers for example. Once you know an object with this property exists you can put this property as one of the assumptions in your context (locale in Isabelle) and prove different things that follow from that. IsarMathLib defines a property of an order relation to be complete in Order_ZF and uses this to define what does it mean that some quadruple of sets is a model of real numbers at the end of OrderedField_ZF.

10. James Frank Says:

Slawomir, I could ask my questions on http://math.stackexchange.com, and then send you an email notifying you, or you could have a blog post where I would post the link to the question. That would provide links about IsarMathLib for other people to click on here on your blog.

You could answer them, or not answer them if you didn’t have time. Asking math questions by text can take a lot of time too.

Trying to talk math by text is a hassle in general, and more so when you can’t edit your comments. Stackexchange is all set up for math talk. I don’t have an account there, but I could open one up.

You might consider putting the WordPress gadget in your sidebar that shows the 10 or 15 most recent comments.

The Isabelle command disappeared in my comment above, without the backslash, it’s {^sub}.

• slawekk Says:

Very good idea. I was thinking about isarmarthlib-devel mailing list, but StackExchange is much better. Which StackExchange site you think would be best? Search hits for “proof assistant” indicate cstheory or stackoverflow.
Mathoverflow gives some hits for “formalized mathematics” (it is not on the list of StackExhange sites).
We may get problems with moderators with questions very specific to Isabelle or IsarMathLib, but it’s worth to try.

11. James Frank Says:

I’m talking about simple exponents of elements for something like a field, so you answered the question about that. That’s the great thing about trying to mess around at actually implementing basic math ideas in code, it makes you have to get ideas much more clearer in your head.

As far as the least upper bound property, I’m just wanting to work with a field, rather than the real numbers, so I guess it’s just added as a definition.

These are simple questions, but simple things can kill you. It’s only today that I really started trying to learn programming in Isabelle. Up to now, I’ve just been trying to look into the future about which prover will work the best for me.

In the beginning, people like me need people like you to do simple things like provide an Isabelle definition called complete_ordered_field.

All my goals are math oriented, so I’d prefer http://math.stackexchange.com. Mathoverflow wouldn’t allow basic questions about Isabelle, but from what I’ve seen, math.stackexchange.com invites people to ask questions from simple to research level. Here’s what they say at http://math.stackexchange.com/faq :

What kind of questions can I ask here? Mathematics – Stack Exchange is for people studying mathematics at any level and professionals in related fields.

I don’t see how any question about Isabelle wouldn’t be math related. All I’m interested in is proving math or developing math algorithms.

What questions can I ask you? Questions only related to Isabelle/ZF or can I ask you anything about Isabelle? I’m sure I could always figure out a way to mention IsarMathLib in any question. How could it not be about math if I insert IsarMathLib in the question?

Personally, I don’t like mailing lists. I don’t like tons of mail coming in. I prefer blogs and public forums.

• slawekk Says:

As far as the least upper bound property, I’m just wanting to work with a field, rather than the real numbers, so I guess it’s just added as a definition.

This is a question of definition of course, but the way I see it when you add least upper bound property to definition of ordered field, you get real numbers.

12. James Says:

This is an example of why I think math.stackexchange.com would be the best place to be. Most people won’t know Isabelle, but if they do, they still have to have been thinking a whole lot about these kinds of math questions to discuss them.

I’m still weak in algebra, about isomorphisms, and stuff like that, but a complete ordered field would be more general than the real numbers, at least in some sense of the use of “general”.

Starting with a field is fairly simple. To define it you just need “binary operation” and “set”. You’d then add an order, and then the least upper bound property. Maybe you need a little more.

To get the real numbers requires a massive amount of work. I haven’t sorted it all out, but it used to nag at me that a book like Rudin would be proving things about fields, but use examples with Q and R when I had no idea why we could say that things like 1, 5, pi, 3/4, etc. were elements of a field.

To get the real numbers, you have to build them, show they’re a field, add an order and show the order works, and then the lub property. Then introduce a decimal representation to get your constants, and show that the decimal representation actually represents them. I still haven’t went through the exercise of doing all that, so I haven’t completely figured it out.

The reason I care is I want my code to reflect what it is I’m claiming, partly to be able to convince mathematicians who know nothing about Isabelle that my Isabelle proofs are applicable. Like you were saying, the language part of math is important.

There’s a difference between saying “let x be a real number”, and saying “let x be an element of F, a complete ordered field”. Maybe it’s just the emphasis. It emphasizes that I’m proving things about a complete ordered field, and that the proofs apply to any set I can show to be a complete ordered field.

Additionally, R is nothing less than a complete ordered field, but to prove that 1a=a, I’m only using the properties of a field. It’s easier to say “let x be in F” rather than say “let x be in R, but please notice that in the proof of 1a=a, that I’m not using the lub property or the order properties of R”.

Anyway, I’ll have questions in the future, but you may not hear from me much in the next 6 to 12 months, or maybe you will. I found a first-order logic and type theory tutorial which uses Isabelle:

I’ve been putting off first-order logic since that stuff keeps me from advancing, but it’s pretty applicable when having to try and understand Isabelle and how the underlying math is implemented.

• slawekk Says:

The process you describe as “massive amount of work” is constructing (an example of) real numbers i.e. proving that some specific set (with two operations and an order relation) is a complete ordered field. You can do many such constructions. You can construct a complete ordered field using Dedekind cuts (call it R1) and then construct another one using Cauchy sequences (or almost homomorphisms on integers like in IsarMathLib) and call it R2. Which one is the real numbers? It can’t be both since you can prove (in ZF) that R1 is not equal to R2.

13. James Says:

A short comment in case someone’s listening and having problems with jEdit starting the prover.

I have a hard time getting this message in the prover session window in jEdit:

Welcome to Isabelle/HOL (Isabelle2011: January 2011)

I’ll get a termination message instead much of the time. What works is this: I start i3p, start the prover in i3p, and leave the i3p window open. I then start jEdit, and the prover starts up in jEdit like it’s supposed to. That’s about the only way I can get the jEdit prover to start up on a particular XP machine.

14. James Frank Says:

So by telling me more, you’ve just added another weight to the heavy burden of “learning it all”. It’s not enough that I go through the exercise of building the reals using one of Cauchy sequences or Dedekind cuts. I have to do both. The burden gets heavy given that time is finite.

But I think you’ve supported my point for me wanting to use type complete_ordered_field, rather than type real, if I’m only wanting to prove theorems about complete ordered fields.

Being paranoid, I asked myself the question, “If my set is R, can I prove anything using R that doesn’t apply to a complete ordered field in general?”

With the two operations, I suppose no, since the field axioms completely describe their properties. With the order, I suppose no, since it’s a linear order, and the definition of linear order completely describes the properties of the order.

But there are special subsets of R, which are Q, Z, and the irrational numbers, which are not requirements of a general complete ordered field.

However, it’s basically as you said, when you add the supremum property, you get the real numbers, and as soon as most any analysis textbook gets to that point, it switches to an emphasis to real numbers. That indicates that their must not be very many useful complete ordered fields. I can’t remember having been given an example, other than the real numbers.

After after reading a few articles on the web, such as this,

intuitively, I’m guessing that even though the set of Cauchy reals doesn’t equal the set of Dedekind reals, the set of elements from each that are used in the binary operations are equal, so it’s a matter of definition of what set you want to call the real numbers. But that’s about all the time I have to think about it now.

Simplistic definitions add to the confusion of it all, such as this article, http://www.mathreference.com/top-ms,dcuts.html , saying the Dedekind and Cauchy definitions are equivalent.

Speaking of intuitiveness, or the lack thereof along with confusing the issue, at least for the novice, there’s the phrase “almost homomorphism” used with your construction in IsarMathLib, mentioned in wiki,

http://en.wikipedia.org/wiki/Construction_of_the_real_numbers#Construction_from_the_group_of_integers

and on the Isabelle site,

http://www.cl.cam.ac.uk/research/hvg/Isabelle/projects.html#FormalizedMathematics

I suppose you didn’t introduce the phrase, but to the novice, it gives the impression the job hasn’t been completely finished.

• slawekk Says:

It’s not enough that I go through the exercise of building the reals using one of Cauchy sequences or Dedekind cuts. I have to do both.

Actually I am saying the opposite. You need do a construction of one example of a complete ordered field using whatever method you like most and you are done, since all of them are isomorphic to each other. That means that although they are not equal in formal sense, they look the same in all their essential properties. That’s what is meant at the mathreference.com page you link to when they say that the “definitions” are equivalent (although they should say “constructions” rather than “definitions”).

The “almost homomorphisms” phrase means that the mappings (from integers to integers) considered in the construction are kind of like homomorphisms, but not quite. I took the phrase from one of the papers I was basing my formalization on.
The IsarMathLib’s real numbers (or complete ordered field) construction project is really finished since 2006, the Isabelle site is not up to date on that. The concluding theorem shows that certain quadruple of sets forms a model of real numbers which is defined in OrderedField_ZF as the same as a complete ordered field.

15. Sebastian Reichelt Says:

Hi! I follow this blog from time to time, and I would like to chime in on this interesting discussion from a different angle. Some of the issues discussed here are things most people seem to run into when they start thinking about foundations of mathematics, me included. One thing that helped me at that point was to take a more historical point of view.

In the 19th and early 20th century, math gradually became more rigorous. People have obviously been working with real numbers for a longer time, and their basic properties were really “intuitively obvious” until people started to actually name those properties. At some point someone (I don’t know who and when) noticed that you can prove all known theorems about real numbers from the axioms of a complete ordered field, and (this is important) the “intuitive” real numbers actually satisfy the axioms of a complete ordered field. (Note that the concept of a field is actually more modern, so this is not 100% accurate historically.) That’s why those axioms are a good starting point if you mainly want to work with real numbers (say, in a textbook), and you want to minimize the amount of things you take for granted. BTW, you can just take certain subsets of them and call them N, Z, and Q.

This amount of rigor was sufficient until a trend began to found all of mathematics in (informal!) set theory. At that point, it became advantageous to say: The real numbers are really nothing more than certain subsets of rational numbers (Dedekind cuts), or certain equivalence classes of Cauchy sequences. The point is that if you work with sets anyway, it is nicer if you get the other objects you want “for free.” That is, people were happy that they could now _prove_ all of the properties of real numbers (including the least upper bound property) from principles they considered more basic. That didn’t really change anything about the real numbers, though. In particular, whether there is a “correct” set of real numbers is an intricate, mostly philosophical question.

A bit later, set theory was made more explicit, and, even later, put into axiomatic terms. But it seems that all four of these foundational “steps” mostly just provided a justification for doing math exactly the way it had been done before, possibly a bit more carefully. So basically, every historical step just added another potential introductory chapter at the beginning of a textbook.

One source of conflict is that math education roughly follows historical progress in that rigor is introduced gradually, but proof assistants work the other way, as a proof assistant is itself a kind of foundational framework (sometimes a version of set theory, sometimes an even more basic “logical framework,” and sometimes an alternative to set theory). If you consider what I said above, it may not surprise you any more that each proof assistant (or associated library) treats such basic object as real numbers very differently. It all depends on what you consider your “foundation” to be.

Finally, I would like to invite you to take a look at my proof-assistant-in-progress HLM (http://hlm.sourceforge.net/). (Slawomir already mentioned it in some earlier post — thanks and sorry for hijacking this thread.) The reason I’m posting this is that the current library is in more or less exactly the state you desire: It contains a construction of the real numbers and not much more. Adding new definitions and theorems is actually very easy; someone just needs to do it. The downside is that the proof engine is still under-developed, so you can state theorems but not (yet) prove them. I don’t know exactly what you are trying to do, but you have been talking more about basics than about formal proofs, so… BTW, submissions are always welcome. 🙂

There hasn’t been much progress lately because I’m working on turning it into a more general-purpose math editing framework, but that’s a different story…

• James Frank Says:

I love the web; you find out about some of the things that people are doing all over the world.

Your interface looks nice. Fortunately, things have gotten developed with proof assistants to the point where there’s serious competition. As far as proof assistants, I’m primarily a user, and a big, existing library is important for me to have so I can learn what others have already done, but thanks for the link to your site.

16. James Frank Says:

Okay, isomorphism is creaping back into my mind. I could study it right now, but I have some Isabelle to learn. I guess I was on the right track, as far as the binary ops being what keeps everything equivalent. Isomorphism is defined in terms of the binary operations, phi(ab)=phi(a)phi(b), so it’ll preserve the operations, consequently the order (I guess).

The links hiding and expanding the proofs on isarmathlib.org are nice. When reading the PDF, I prefer for everything to be expanded, but on the web it’s nice to have the proof links hide or expand the proofs.

You bringing up that the Cauchy real numbers, R1, aren’t equal to the Dedekind real numbers, R2, thinking about that gave me hard proof of the value of the Axiom of Choice.

You didn’t say that your R1 and R2 are proved not equal with ZFC, but it gave me the idea of the usefulness of merely knowing that two sets aren’t equal. So if all we had is the Axiom of Choice to prove that two sets aren’t equal, then the Axiom of Choice is of value.

Recently, I’ve been entertaining the idea that the Axiom of Choice is nothing but a useless axiom to let people play logic games, not that I’m against playing mathematical logic games.

But back to Z, Q, and the irrationals being subsets of R, I suppose that for any two complete ordered fields, because they are isomorphic, they both have to contain Z, Q, and the irrationals, but now I’m back to trying to figure out why the order is preserved, but it’s all in a book somewhere, so it’s a waste for me to think much about it much now.

The one link referred to Pugh’s Real Mathematical Analysis. I’ll still need to look at both constructions to figure it out, so the burden is still there, since it’s not practical to do it timewise. It’s not obvious how two sets can have been built using the integers and end up at the same place, being bijective, but not be equal. There are simple examples of “smaller” sets being bijective to “larger” sets, but the complete ordered field part makes it more complex.

Anyway, I’m set up with more tools. I got sledgehammer set up, which will help me track down definitions and lemmas, and I learned just enough more about regular expressions to do some searches on the .thy files to look for definitions, lemmas, etc.

I’m using PowerGrep, and here’s the result of 6 or more hours work getting a regular expression to find words followed by “definition”, “lemma”, or “theorem”, and where there can be a change of case, such as completeField, or separation by underscores, such as complete_field:

(?x)
(definition|lemma|theorem)[\s]+.*
(
(?<![a-z])field(?![a-z])|
(?<![A-Z])Field(?![a-z])
)