<div dir="ltr">Hello Ramana!<div><br></div><div>Yes, in fact I modified the existing two files, setSpecScript.sml and setModelScript.sml, to produce the versions I put in the "flame" subdirectory. But actually, they could go right in place, as drop-in replacements, for the original two.</div><div><br></div><div>I didn't do that because I didn't want to disturb any other files that could have perhaps depended on the original versions. I try very hard to not make trouble for other people. So I put these out publicly, hoping that we could vet them safely, and as a community come to an agreement whether or not we would like to see this extended version as the main version.</div><div><br></div><div>The two files should be backwards compatible in most things, simply extended. For example, in setModelScript.sml there is a model presented that satisfies most of the axioms except for the Axiom of Infinity. This proof has been extended to now include the Axiom of Regularity and the Axiom of Replacement, and to show they are satisfied by the model as well.</div><div><br></div><div>The major difference in the new version would be the use of the inductive definition for the Axiom of Infinity instead of the prior version that was based on the notion of infinity defined in standard HOL. But I suspect that there may not be much in the rest of cakeml that depends meaningfully on the Axiom of Infinity. Even if there is, setSpecScript.sml does prove a theorem that the new axiom implies the prior version, so it shouldn't be hard to patch broken proofs.</div><div><br></div><div>Someone should try an experiment of substituting the new versions in place and trying to rebuild, just to see what breaks. But I was holding off on this until people had some time to take a look at the formalization, and make their own judgements and talk about what they prefer. The axioms of set theory are not large, but they are very consequential, so it is important to get them right.</div><div><br></div><div>So far, you and Konrad are the only ones who have responded. I'd love to hear more people's opinions, especially Michael's and Rob Arthan's.</div><div><br></div><div>Cheers,</div><div>Peter</div><div class="gmail_extra"><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Jul 8, 2016 at 7:22 PM, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div><div><div><div>Hi Peter,<br><br></div>This indeed looks very nice.<br><br></div>One suggestion I would make: would it be possible to extend the existing theory, rather than making an extended copy?<br></div>It seems to me that your additional definitions and proofs could go into the existing setSpecScript.sml without any problem.<br></div>The only place of conflict is where you want to define is_set_theory with the additional axioms. Perhaps you could simply define a new constant is_full_set_theory or similar for that purpose?<br><br></div>I am hoping to avoid diverging forks in the future, in case we make any updates to setSpecScript.sml (unlikely, but there may be a few little cleanups).<br><br></div>Cheers,<br></div>Ramana<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 30 June 2016 at 12:48, Konrad Slind <span dir="ltr"><<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Looks nice! Note that Michael has done an extensive development of the ordinals in<div><br></div><div> <holdir>/examples/set-theory/hol_sets</div><div><br></div><div>and transfinite induction is in there somewhere.</div><div><br></div><div>Konrad.</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div>On Wed, Jun 29, 2016 at 5:09 PM, Peter Vincent Homeier <span dir="ltr"><<a href="mailto:palantir@trustworthytools.com" target="_blank">palantir@trustworthytools.com</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div><div dir="ltr">I've just made my first contribution to CakeML. This consists of two files within the subdirectory "flame/set-theory", which are modified versions of the corresponding files under "candle/set-theory".<div><br></div><div>My primary reference for this work was "Set Theory, The Third Millennium Edition" by Thomas Jech, Springer, 2006.<br><div><br></div><div>These files extend the existing specification of set theory to full ZFC. This includes two axioms that were previously omitted, the Axiom of Regularity and the Axiom Schema of Replacement:</div><div><div><br></div><div><font face="monospace, monospace">val regular_def = Define`</font></div><div><font face="monospace, monospace"> regular ^mem ⇔ ∀x. (∃y. mem y x) ⇒ ∃y. mem y x ∧ ∀z. ~(mem z x ∧ mem z y)`</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">val is_functional_def = Define`</font></div><div><font face="monospace, monospace"> is_functional (R:'a -> 'b -> bool) ⇔ ∀x y z. R x y ∧ R x z ⇒ y = z`</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">val replacement_def = Define`</font></div><div><font face="monospace, monospace"> replacement ^mem ⇔</font></div><div><font face="monospace, monospace"> ∀R. is_functional R ⇒</font></div><div><font face="monospace, monospace"> ∀d. ∃r. ∀y. mem y r ⇔ ∃x. mem x d ∧ R x y`</font></div></div><div><br></div><div><div><div><font face="monospace, monospace">val is_set_theory_def = Define`</font></div><div><font face="monospace, monospace"> is_set_theory ^mem ⇔</font></div><div><font face="monospace, monospace"> extensional mem ∧</font></div><div><font face="monospace, monospace"> (∃sub. is_separation mem sub) ∧</font></div><div><font face="monospace, monospace"> (∃power. is_power mem power) ∧</font></div><div><font face="monospace, monospace"> (∃union. is_union mem union) ∧</font></div><div><font face="monospace, monospace"> (∃upair. is_upair mem upair) ∧</font></div><div><font face="monospace, monospace"> regular mem ∧</font></div><div><font face="monospace, monospace"> replacement mem`</font></div></div></div><div><font face="monospace, monospace"><br></font></div><div>In addition, I have modified the Axiom of Infinity,</div><div><br></div><div><div><font face="monospace, monospace">val is_infinite_def = Define`</font></div><div><font face="monospace, monospace"> is_infinite ^mem s = INFINITE {a | a <: s}`</font></div><div><br></div><div><div>not really deleting it, but replacing it by the inductive property, taken from page 12 of "Set Theory, The Third Millennium Edition" by Thomas Jech, Springer, 2006, using the successor operator as defined (Definition 1.20) on page 19 of "Introduction to Set Theory" by J. Donald Monk, McGraw Hill, 1969.</div></div><div><div><br></div><div><font face="monospace, monospace">val suc_def = Define`</font></div><div><font face="monospace, monospace"> suc ^mem x = x ∪ Unit x`</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">val _ = Parse.overload_on("Suc",``suc ^mem``)</font></div></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">val is_inductive_def = Define`</font></div><div><font face="monospace, monospace"> is_inductive ^mem s ⇔</font></div><div><font face="monospace, monospace"> ∅ <: s ∧ ∀x. x <: s ⇒ Suc x <: s`</font></div></div><div><div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">val is_model_def = Define`</font></div><div><font face="monospace, monospace"> is_model ^s ⇔</font></div><div><font face="monospace, monospace"> is_set_theory mem ∧</font></div><div><font face="monospace, monospace"> is_inductive mem indset ∧</font></div><div><font face="monospace, monospace"> is_choice mem ch`</font></div></div></div><div><br></div><div>There is included a proof that the inductive axiom implies the prior infinity axiom; this proof depends on the Axiom of Regularity.</div><div><br></div><div><div><font face="monospace, monospace"> inductive_set_infinite</font></div><div><font face="monospace, monospace"> |- is_set_theory mem ∧ is_inductive mem indset ⇒</font></div><div><font face="monospace, monospace"> is_infinite mem indset</font></div></div><div><br></div><div>I also added several new set theory constants, such as binary intersection, inverse of a function, image of a function on a set, dependent function space, and dependent product space. The last three required the Axiom Schema of Replacement to define.</div><div><br></div><div>I am hoping to stimulate some discussion and debate. It is necessary to extend the existing partial specification of set theory to support the construction of the set-theory model of HOL-Omega. Besides that, there will probably be other uses for ZFC set theory, and I felt we needed a more complete axiomatic basis.</div><div><br></div><div>The next steps would presumably be the definition of the ordinals, with transfinite induction, and the cardinals.</div><div><br></div><div>Enjoy, and please let me know what you think.</div><div><br></div><div>Peter</div><div><div data-smartmail="gmail_signature"><div dir="ltr"><div><br></div><div><br></div>"In Your majesty ride prosperously <br>because of truth, humility, and righteousness;<br>and Your right hand shall teach You awesome things." (Psalm 45:4)</div></div>
</div></div></div>
<br></div></div>_______________________________________________<br>
Users mailing list<br>
<a href="mailto:Users@cakeml.org" target="_blank">Users@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/listinfo/users</a><br>
<br></blockquote></div><br></div>
<br>_______________________________________________<br>
Users mailing list<br>
<a href="mailto:Users@cakeml.org" target="_blank">Users@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/listinfo/users</a><br>
<br></blockquote></div><br></div>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div> </div><div><br></div>"In Your majesty ride prosperously <br>because of truth, humility, and righteousness;<br>and Your right hand shall teach You awesome things." (Psalm 45:4)</div></div>
</div></div>