[opentheory-users] Status of derived syntax

[Joe Leslie-Hurd]

Hi Rob,

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.

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.

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:

$ opentheory info --summary --show-assumptions axiom-extensionality
2 external type operators: -> bool
3 external constants: = ! T
3 assumptions:
  |- T <=> (\p. p) = \p. p
  |- (!) = \p. p = \x. T
  |- let a d <- (\e. d e) = d in a = \b. (\c. c) = \c. c
1 theorem:
  |- !t. (\x. t x) = t

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.

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.

Cheers,

Joe




On Sat, Nov 23, 2013 at 3:53 PM, Rob Arthan <rda at lemma-one.com> wrote:

> Joe,
>
> On 22 Nov 2013, at 18:58, Joe Leslie-Hurd wrote:
>
> Hi Rob,
>
> 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.
>
> 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.
>
> 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
>
> opentheory/stdlib/stdlib.int
>
> This is how sets are recognized for printing purposes (assuming that the
> term argument to fromPredicate has the right shape).
>
> 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.
>
>
> I haven't got that far yet. I have just been looking at the article files
> and HTML pages in the repo.
>
> Lets are simply terms that can be beta-reduced, so
>
> (\v. t[v]) x
>
> is printed as
>
> let v = x in t[v]
>
> 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).
>
>
> 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.
>
> However, some packages contain assumptions that do contain beta-redexes
> and hence have been printed out as let-expressions in the HTML. See:
>
>
> http://opentheory.gilith.com/opentheory/packages/axiom-choice-1.7/axiom-choice-1.7.html
>
> http://opentheory.gilith.com/opentheory/packages/axiom-extensionality-1.8/axiom-extensionality-1.8.html
>
> http://opentheory.gilith.com/opentheory/packages/natural-1.81/natural-1.81.html
>
> 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.
>
>
> Hope that helps,
>
>
> 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.
>
> Regards,
>
> Rob.
>
>
> Joe
>
>
>
>
> On Fri, Nov 22, 2013 at 8:08 AM, Rob Arthan <rda at lemma-one.com> wrote:
>
>> 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.
>>
>> Regards,
>>
>> Rob.
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131125/50596ef2/attachment-0001.html>