[opentheory-users] article reader for HOL4

[Joe Hurd]

Hi Ramana,

> I'd love to see how you envision the purpose of opentheory and
> articles and how they would interact with various proof assistants, if
> you've written that down anywhere I might not have seen yet. I know
> there are those two papers on your website.

I recently wrote a paper on the OpenTheory standard library that
contains some details on this:

http://www.gilith.com/research/papers/stdlib.pdf

Any comments would be gratefully received.

> Suppose you're reading an article without any clashing definitions,
> i.e. any constant the article wants to define is not already defined
> in the reader's world.
> The axioms of the article will be about those undefined constants.
> When the reader comes to process the axiom command, it needs to
> provide a theorem.
> How is the reader supposed to have a theorem about a constant it
> hasn't yet defined?

I think there are a couple of important points here:

1. OpenTheory axioms are theory assumptions that mention type
operators or constants defined in the theory. Assumptions that only
mention undefined type operators and constants are not called axioms
(even though the same "axiom" command is used to generate them), and
the client theorem prover must provide theorems for these.

2. The whole of higher order logic as implemented in HOL theorem
provers only depends on the 3 axioms listed in base-1.0, and each
theorem prover already has local versions of these. Everything else is
constructed definitionally, so the situation of needing additional
axioms should never occur, which is why I initially said that axioms
can be safely ignored.

Does that make sense now?

Cheers,

Joe