| name | example |
| version | 1.0 |
| description | A short phrase describing the contents of the package |
| author | The name and email address of the package maintainer |
| license | The package license |
| requires | A list of packages that collectively satisfy the assumptions of this package |
| show | A list of namespace abbreviations, to make the theorems below more readable |
A list of the package files. It's occasionally useful to browse the theory file to examine the theory package dependency graph, but the package tarball is best downloaded and installed using the opentheory tool.
The type operators that are defined by this theory package and which appear in the "Axioms" or "Theorems" sections below. Type operators that are defined and used in a proof but do not appear in the statement of an axiom or theorem are considered local and do not appear in this list.
As for the defined type operators above, but for constants.
A list of the assumptions that: (i) are required by the theory package; and (ii) contain a defined type operator or constant. Such an assumption can never be satisfied by interpreting the input type operators and constants of the theory package with definitions, and so will function as an axiom in any proof that this theory package contributes to.
It is standard practice in the higher order logic theorem proving community to avoid axioms, except for a small set that are used to set up the basic theories of higher order logic. The OpenTheory system uses the following three axioms:
AXIOM OF EXTENSIONALITY: ⊦ ∀t. (λx. t x) = t
AXIOM OF CHOICE: ⊦ ∀P x. P x ⇒ P ((select) P)
AXIOM OF INFINITY: ⊦ ∃f. injective f ∧ ¬surjective f
A list of the theorems proved and exported by the theory package. All type operators or constants that are present in a theorem statement must appear in either the list of defined type operators and constants (above) or the list of input type operators and constants (below).
A list of the type operators that are not defined by this theory package but which appear in the statement of an axiom, theorem or assumption. This will usually include the following three type operators that are used to set up the basic theories of higher order logic:
As for the input type operators above, but for constants. This will usually include the following two constants that are used to set up the basic theories of higher order logic:
A list of the assumptions that: (i) are required by the theory package; and (ii) contain only input type operators and constants. The idea is that the theory package can be interpreted by replacing the input type operators and constants with definitions such that all of the assumptions are satisfied. The resulting theory would then have no assumptions, and the interpreted theorems would be available for use.