# 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