<div dir="ltr">Hi Rob,<div><br></div><div>I think you have worked out your problem, but I wanted to explain the origin of the monster assumption you found in the natural theory package.<br><div><br></div><div>There are 3 axioms used to set up the standard theory library (extensionality, choice and infinity), and two primitive constants (= and select). A problem I found is that the usual presentation of the basic axioms refers to other constants, for example extensionality contains a universal quantifier. If you were to assert an axiom in terms of a non-primitive constant you run the risk of a theory package defining the non-primitive constant in an unexpected way, and then the axiom might make the system inconsistent.</div>
<div><br></div><div>My resolution is to expand the standard axioms using the definition of the constants, and have little theory packages that prove the usual presentation of the axiom in terms of the expanded axiom and the definition of the non-primitive constants that it refers to. For example, here is the axiom-extensionality package:<br>
<div><br></div><div><div>$ opentheory info --summary --show-assumptions axiom-extensionality</div><div>2 external type operators: -> bool</div><div>3 external constants: = ! T</div><div>3 assumptions:</div><div> |- T <=> (\p. p) = \p. p</div>
<div> |- (!) = \p. p = \x. T</div><div> |- let a d <- (\e. d e) = d in a = \b. (\c. c) = \c. c</div><div>1 theorem:</div><div> |- !t. (\x. t x) = t</div></div><div><br></div></div></div><div>The "real" extensionality axiom is the third assumption, and the usual presentation is proved as a theorem in terms of the real axiom and the standard definition of logical quantifiers. So if you were to define the universal quantifier in a different way, it wouldn't match the assumptions of this package and so you wouldn't get access to the axiom of extensionality.</div>
<div><br></div><div>The monster assumption you found in the natural theory package is the expanded version of the axiom of the infinity, which refers to injectivity and surjectivity, the definition of which refer to other constants which must be recursively expanded. The resulting "real" axiom of infinity is indeed a real monster.</div>
<div><br></div><div>Cheers,</div><div><br></div><div>Joe</div><div><br></div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sat, Nov 23, 2013 at 3:53 PM, Rob Arthan <span dir="ltr"><<a href="mailto:rda@lemma-one.com" target="_blank">rda@lemma-one.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">Joe,<div><br><div><div class="im"><div>On 22 Nov 2013, at 18:58, Joe Leslie-Hurd wrote:</div>
<br><blockquote type="cite"><div dir="ltr">Hi Rob,<div><br></div><div>The derived syntax in OpenTheory is rather ad-hoc: I just hard-coded some common mathematical syntax such as numerals, pairs and sets which is triggered by specific names in the OpenTheory namespace.</div>
<div><br></div><div>When exporting HOL Light theories to the OpenTheory library, one of the more involved things I had to do is remove as many HOL Light-specific tags as possible. So for example, the NUMERAL tag is easily removed, and OpenTheory numerals are instead recognized by sequences of bit0 and bit1 functions terminated by natural number zero.</div>
<div><br></div><div>The OpenTheory version of GSPEC is called fromPredicate, and you can see the standard library renamings in the OpenTheory fork of HOL Light in the file</div><div><br></div><div>opentheory/stdlib/<a href="http://stdlib.int/" target="_blank">stdlib.int</a></div>
<div><br></div><div>This is how sets are recognized for printing purposes (assuming that the term argument to fromPredicate has the right shape).</div><div><br></div><div>Finally, I'm rather pleased by my scheme for recognizing let expressions, although it sounds like it might be causing you problems displaying your theory.</div>
</div></blockquote><div><br></div></div>I haven't got that far yet. I have just been looking at the article files and HTML pages in the repo.</div><div><div class="im"><br><blockquote type="cite"><div dir="ltr"><div> Lets are simply terms that can be beta-reduced, so</div>
<div><br></div><div>(\v. t[v]) x</div><div><br></div><div>is printed as</div><div><br></div><div>let v = x in t[v]</div><div><br></div><div>No need for any special term tags, and in all the theories I have so far encountered there are no subterms in theorems that can be beta-reduced (and thus accidentally print as let).</div>
</div></blockquote><div><br></div></div><div>Nice idea. I don't think you would want that feature while doing interactive theorem-proving, but it makes sense in your context. I have just had a go with the ProofPower theorem finder and it supports your approach: there are no theorems saved in the ProofPower-HOL theory hierarchy containing beta-redexes.</div>
</div><div><br></div><div>However, some packages contain assumptions that do contain beta-redexes and hence have been printed out as let-expressions in the HTML. See:</div><div><br></div><div><a href="http://opentheory.gilith.com/opentheory/packages/axiom-choice-1.7/axiom-choice-1.7.html" target="_blank">http://opentheory.gilith.com/opentheory/packages/axiom-choice-1.7/axiom-choice-1.7.html</a></div>
<div><a href="http://opentheory.gilith.com/opentheory/packages/axiom-extensionality-1.8/axiom-extensionality-1.8.html" target="_blank">http://opentheory.gilith.com/opentheory/packages/axiom-extensionality-1.8/axiom-extensionality-1.8.html</a></div>
<div><a href="http://opentheory.gilith.com/opentheory/packages/natural-1.81/natural-1.81.html" target="_blank">http://opentheory.gilith.com/opentheory/packages/natural-1.81/natural-1.81.html</a></div><div><br></div><div>The assumption in the last one of these is a real monster. They all look like intermediate lemmas generated by some proof procedure whose proofs have somehow gone missing.</div>
<div><br></div><div><blockquote type="cite"><div dir="ltr">
<div><br></div><div>Hope that helps,</div></div></blockquote><div><br></div>It does indeed. I have some other questions about using the article files in the repo, but I think I will start a separate thread for that.</div>
<div><br></div><div>Regards,</div><div><br></div><div>Rob.</div><div class="im"><div><br><blockquote type="cite"><div dir="ltr"><div><br></div><div>Joe</div><div><br></div><div><br></div></div><div class="gmail_extra"><br>
<br><div class="gmail_quote">On Fri, Nov 22, 2013 at 8:08 AM, Rob Arthan <span dir="ltr"><<a href="mailto:rda@lemma-one.com" target="_blank">rda@lemma-one.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">What is the status of things like let-terms and set comprehensions in the Gilith Open Theory Repo. I can't see the definitions of the magic constants that are used to represent these things (LET and GSPEC in HOL Light and HOL4)? A peculiar sequence of complicated assumptions involving let builds up in the HTML listings.<div>
<br></div><div>Regards,</div><div><br></div><div>Rob.</div></div><br>_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div>
_______________________________________________<br>opentheory-users mailing list<br><a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br><a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</blockquote></div><br></div></div></div><br>_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div>