(PROVE-LEMMA COMMUTATIVITY-OF-TIMES (REWRITE) (EQUAL (TIMES X Y) (TIMES Y X)))
Give the conjecture the name *1.
We will appeal to induction. Two inductions are suggested by terms in
the conjecture, both of which are flawed. We limit our consideration to the
two suggested by the largest number of nonprimitive recursive functions in the
conjecture. Since both of these are equally likely, we will choose
arbitrarily. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP X) (p X Y))
(IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y))
(p X Y))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT X) decreases according to the well-founded relation
LESSP in each induction step of the scheme. The above induction scheme
produces the following two new conjectures:
Case 2. (IMPLIES (ZEROP X)
(EQUAL (TIMES X Y) (TIMES Y X))).
This simplifies, applying TIMES-ZERO and TIMES-NON-NUMBERP, and opening up
the functions ZEROP, EQUAL, and TIMES, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP X))
(EQUAL (TIMES (SUB1 X) Y)
(TIMES Y (SUB1 X))))
(EQUAL (TIMES X Y) (TIMES Y X))),
which simplifies, unfolding the functions ZEROP and TIMES, to:
(IMPLIES (AND (NOT (EQUAL X 0))
(NUMBERP X)
(EQUAL (TIMES (SUB1 X) Y)
(TIMES Y (SUB1 X))))
(EQUAL (PLUS Y (TIMES Y (SUB1 X)))
(TIMES Y X))).
Appealing to the lemma SUB1-ELIM, we now replace X by (ADD1 Z) to eliminate
(SUB1 X). We employ the type restriction lemma noted when SUB1 was
introduced to constrain the new variable. We must thus prove:
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL (ADD1 Z) 0))
(EQUAL (TIMES Z Y) (TIMES Y Z)))
(EQUAL (PLUS Y (TIMES Y Z))
(TIMES Y (ADD1 Z)))).
However this further simplifies, applying the lemma TIMES-ADD1, to:
T.
That finishes the proof of *1. Q.E.D.
[1] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
Just an aside, but I was under the impression that Set Theory (these days) is regarded as not-necessarily-all-that-well-founded or, perhaps, not ideal for "foundations"? Is that hopelessly misguided?
If it isn't already apparent, I'm pretty much a noob in formal verification, but I've read enough to hopefully have a very shallow understanding...?!?
EDIT: I just thought I'd add what "makes math beautiful" for me: The mere difficulty of defining equality of 'things' and deciding what it should mean.
I believe what you have in mind regarding set theory as "not ideal for 'foundations'" (why is the word foundations in quote, btw?) is that there is a recent push to reexamine the prospects more intensional foundations based on type theory. The most promising and currently fashionable version of this push is Homotopy Type Theory (HoTT), which has been given press and prestige from the IAS at Princeton and interest from Fields Medalist Vladimir Vovodsky (sp?). There are plausible reasons given, though often polemical, for preferring some sort of type theoretical or category theoretical foundations over set theoretical ones. Perhaps most importantly, for readers of HN, the comparatively easy formalization into computer-checkable proof and computer-assisted proof (look up, for instance, Coq).
That said, there is a long way to go before HoTT (or something like it) displaces traditional foundations and set theory. For one thing, there is no obvious axiomatization or way to confirm that HoTT is a suitable foundation for extant non-foundational mathematics. For one thing, standard type theory (MLTT) plus Vovodsky's univalence axiom is proof-theoretically equivalent to a subsystem of analysis. I would guess that, for instance, you can't prove that all Borel sets are measurable using MLTT plus univalence (but this is totally speculative and I would appreciate being corrected).
Last -- I suspect the only mathematicians who find set theory proofs beautiful are set theorists. Most other mathematicians don't really give af about set theory.
I've seen HoTT seem receiving quite a bit of attention, but after reading a few papers and texts it seems that it's just out of reach without additional introductory material. I got about 50% though TAPL, if that's any indication of (my lack of) sophistication in type theory. I really should pick that up...
Any recommendations for introductory texts?
As a practical matter, what do the mathematicians who don't give AF about set theory (as you say) do? Just assume other axioms that "do enough" adn then go from there?
You could check out Lambek and Scott (1970s), which is excellent. Also Girard (citation for this one was in TAPL). I also think Martin Lof himself is pretty good for the feel of things, but he has always seemed kind of cryptic and mystical to me. There are also some good videos on YouTube that Steve Awodey (CMU) recorded for more intro/motivation. I'd also add Vovodsky's three Bernays lectures on YouTube for the general idea of using typed lambda calculus vs set theory as foundations.
Sociologically, my impression is that most mathematicians trust that the usual axioms of set theory are consistent and safely ignore them. So, yes -- they choose axioms in their own field that are known to be derivable in set theory. Even in intro Analysis textbooks, where the role of set theoretic axioms themselves can be pretty easily extracted from the construction of the reals, I don't think you'd see set theoretic axioms explicitly appealed to (might be wrong about this). In constructive mathematics, it ends up mattering where Choice is used I guess. And it matters how these uses can be "constructivized." But constructive analysis is primarily motivated by foundational considerations. So it is not really an example of ordinary mathematics. Some axioms, like Regularity, are almost never even implicitly used outside of set theory itself except in very specific cases.
Most every case where there is a question of whether a given bit of mathematics is derivable from the usual axioms of set theory arise only within set theory itself (CH, measurability of projective sets of reals, etc), and so such questions are easy to ignore for the vast majority of mathematicians. They simply don't care that much about logic and set theory aside from "just working" under the hood, as it were.
If one is a mathematician, I think it's entirely reasonable to just "trust" your basic axioms of your "sub-field", but OTOH I can really understand the worry that the rug is going to get pulled out from under you... which is a pretty remote worry given the complexity of math nowadays.
Anyway, thank you for taking the time for that response.
∀ f, x = y ⇒ f(x) = f(y)
In Boyer-Moore theory, there's no "hiding", in the sense of an object with private members. One could define a "weak equality" for sets which were lists of values, true if the same values were in both lists. Weak equality would not require that the lists have the same order. But you couldn't hide the representation. Functions could peek into the list representation, and the property above would not hold. So "weak equality" would not be very useful in proofs.
I once proposed a sort of "object oriented" extension to Boyer-Moore theory. The idea is that you create something like a set represented by lists, prove some theorems about such objects, and then "hide" the private functions that can look into the interior of the representation. Then you can define a weak equality function p. If you can prove ∀ f, p(x,y) ⇒ f(x) = f(y) for every non-hidden function, you have proven that p(x,y) ⇒ x = y. Then, p can be treated as equality. Proving this requires proving it for every function already defined. Any newly defined functions are composed from existing functions, so the equality still holds. There's trouble with newly defined types, though, because they come with some built-in functions such as the type predicate.
If you pursue this, you probably get to some theory of types, but I didn't want to go there, so I gave this up.
My impression was that even that might be a bit contentious[1]. Well, maybe not contentious, but maybe... disputable? It also requires a theory of functions, or at least a syntax to derivation rules.
That was just to be absurdly nitpicky, I think I understand what you're saying here, and it's much appreciated.
[1] https://pdfs.semanticscholar.org/806a/92153c4b8d344edec45eec...
So I set this up in Boyer-Moore notation.
But Boyer-Moore theory is constructive; everything must have a definition that can be evaluated as a function. So I had to define arrays and the "selecta" and "storea" functions so that this would work. I could do this by defining an array as a list of (subscript, value) tuples. This is simply a structure definition for a list. An array-shell has an array-elt-value, an array-elt-subscript, and array-prev, which is the rest of the elements. "array-shell" is the constructor, "empty-array" is essentially "nil" for this type, and "array-recognizer" is a predicate which is true for objects of type array-shell.For array equality to work, the list of tuples had to be ordered by subscript, so that two arrays with the same values would always have the same representation. So selecta and storea are complicated. selecta is a recursive lookup in a list:
Store into array is ugly, because it's an update of an ordered list. This recursive function is complicated enough that it needs a lemma to help with proof of termination. This says that the array-prev list component of a is always shorter than a. The Boyer-Moore prover must prove termination for all defined functions, which it does by examining any recursive call and proving that there is a measure defined on the arguments which is a smaller nonnegative integer. For the easy cases, the prover can do this automatically, but sometimes you have to define a lemma to help it. The lemma, of course, also has to be proved.So, given all that, the Boyer-Moore theorem prover could be turned loose to grind out proofs of the rules for arrays. It took about 45 minutes of grinding in 1982 on a 1 MIPS VAX 11/780. You can rerun it now. Here's the prover, which requires clisp.[1]. Here's the entire set of definitions and theorems we used for program verification.[2]. Read the instructions at [1], and get the system up to where it's done "boot-strap". Then load the file at [2]. Long, detailed, human-readable explanations of the proof steps are displayed. The entire proof run for all those basic theorems takes about a second, and that's probably mostly scrolling.
So, having rigorously proved the "axioms" for arrays from first principles, I submitted a paper to JACM. The reviewer comments I got back were mainly about the uglyness of the approach. All that case analysis! One comment was that the reviewer was upset about having a proof that ugly at the foundations of computer science. The paper was rejected.
The reason it's ugly is that it doesn't get to use set theory. Informally, a set is a collection whose order does not matter. "Order does not matter" is not a meaningful concept in strict Boyer-Moore theory. If order matters, there are many cases to prove, stemming from all those IF statements in the definitions.
A generation later, fewer mathematicians would be bothered by this form of "uglyness". But back then, machine proofs were so rare that this was considered awful. Also, now that computers can do this in a second, complaining that it's too complicated seems whiny.
[1] https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...