Package example: A short phrase describing the theory
Information
| name | example |
| version | 1.0 |
| description | A short phrase describing the theory |
| author | The name and email address of the package maintainer |
| license | The package license |
| checksum | The package checksum |
| 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 |
Files
A list of the package files. It's occasionally useful to browse the theory source file to examine the theory package dependency graph, but the package tarball is best downloaded and installed using the opentheory tool.
Defined Type Operators
The type operators defined in 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 to the theory and do not appear in this list.
Defined Constants
As for the defined type operators above, but for constants.
Axioms
A list of the theory assumptions that refer to one of the defined type operators or constants above. Such assumptions must remain unsatisfied in any context in which the theory is interpreted, and thus act as axioms of the theory.
Note: It is standard practice in the higher order logic theorem proving community to avoid asserting axioms, but rather to explicitly construct mathematical objects by making definitions and proving that they satisfy the desired properties. The method of definitional construction has the advantage that the resulting theories are conservative extensions, guaranteed to preserve soundness. "The method of 'postulating' what we want has many advantages; they are the same as the advantages of theft over honest toil" – Bertrand Russell.
Theorems
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 external type operators and constants (below).
External Type Operators
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. The external type operators may include the following three primitive type operators that are used to set up the basic theories of higher order logic:
- →
- bool
- ind
External Constants
As for the external type operators above, but for constants. The external constants may include the following two primitive constants that are used to set up the basic theories of higher order logic:
- =
- select
Assumptions
A list of the theory assumptions that refer only to the external type operators and constants above. The idea is that the theory package can be imported into a context by interpreting the external type operators and constants in such a way that all of the assumptions are satisfied. The resulting theory would then have no assumptions, and the interpreted theorems would be available in the context. The theory assumptions may include the following three standard axioms that are used to set up the basic theories of higher order logic:
⊦ AXIOM OF EXTENSIONALITY
⊦ AXIOM OF CHOICE
⊦ AXIOM OF INFINITY