The MetaPRL *meta*-logic defines a higher order logic
of *Horn* formulas. The logic includes a *term* language,
described in the page on MetaPRL terms,
and a meta-logic defined with a meta-implication over second-order
term patterns. Each inference rule in a theory defines
a set of valid inferences in the logic. At the moment, inferences
are non-recursive: they have the syntax:

inference::=term | term-->inference

A *theory* is defined by stating its inference
rules. Some times we call an inference rule that is just a single
term an *axiom* (axioms don't use the meta-implication). The theories are modular:
each module defines a theory that contains the rules defined in
the module, and in all ancestor modules. The module system is
discussed in the module system page.

A module interface declares the *signature* of a theory;
it includes declarations for each of the *public*
inference rules. Rules are not required to be listed in an
interface, but for clarity, many of the theories in MetaPRL,
including `Itt_theory`, include the inference rule declarations
in their signatures.

Inference rules are declared with the `rule`
form. The general syntax is the following:

rulename[params] :inference

The *params* are extra parameters that are passed to the
inference rule, including *context* addresses, *term*
arguments, and *new variable* names. The `Itt_struct`
module contains a basic rule:

rulehypothesis 'H 'J 'x :sequent['ext] { 'H; x: 'A; 'J['x] >- 'A }

The *name* of the rule is `hypothesis`. The parameters
include two context identifiers `'H` and `'J`, and
a variable identifier `'x`. The inference of this rule
defines a set of *sequents*, containing a number of hypotheses
defined by the context `'H`, a single hypothesis `x`
of type `'A`, additional hypotheses defined by the context
`'J['x]`, where the variable `x` may occur free,
and a single conclusion `'A`. The sequent also contains
an extra parameter `'ext` that defines the *computational
status* in the `Itt_theory`.
The parameter is the term `squash` if the sequent has no
computational value, and it is a variable otherwise (in this case
the variable `'ext`).

The `hypothesis` rule defines a set of valid inferences
defined by the terms that is matches. Put another way, the inference
states that all *substitution instances* are valid formulas,
where the contexts `'H` and `'J['x]` are replaced
by lists of hypotheses, the variable `'A` is replaced by
a term, the variable `'x` is replaced by another variable
and the variable `'ext` is replaced by arbitrary term.
For instance, the following formulas are valid in the `Itt_struct`
module:

sequent['ext] { i: int; z: false >- false }sequent[squash] { z: 1; y: 'z + 1 >- 1 }

The second example is strange because `1` is not a type.
However, the semantics of sequents in the `Itt_theory` theory
validates the truth of the expression. A hypothesis `(x:'A)`
in the `Itt` theory implies two assumptions: that `'A`
is a type, and that `'A` is true. If `'A` is not
a type, the assumption is false, so the sequent is trivially true.

Inference rules are also defined using the `rule` directive.
An inference is a *conditional* rule; it states assumptions
that must be proved in order for the conclusion to hold. Most introduction
and elimination rules have this form. For example, in the `Itt_logic`
module, the introduction rule for logical conjunction is stated
as follows:

ruleand_intro 'H : sequent ['ext] { 'H >- 'a1 } --> sequent ['ext] { 'H >- 'a2 } --> sequent ['ext] { 'H >- "and"{'a1; 'a2} }

The `'H` is the context identifier used to instantiate
the hypotheses, and the `'a1` and `'a2` terms are
the subterms of the conjunction. The rule states that in order
to prove the conjunction `'a1 & 'a2` in any context
`'H`, it is sufficient to prove `'a1` and `'a2`
in the same context.

The `metaprl/doc/private/sequents.tex` file gives the formal definition of
the complete rule syntax.

Inference rules are implemented two ways: they can
be derived from previous rules and they can be declared as *primitive*
axioms of a theory. The difference between these two forms is in
the way the system does logical accounting.

A primitive inference is "justified" by giving a
relation on *proofs* with the `prim` form, which has
the following syntax:

primname[params] :binference=term

A *binference* is like an inference, but it contains bindings
for the proofs. The bindings are bound in the *term* part
of the `prim` form, which provides the final proof term.
In constructive theories, the "proof" is usually the proof
*extract:* a term that defines the computational content
of the proof. For example, the following definition gives an implementation
of the `and_intro` rule declared above:

primand_intro 'H :('t1 : sequent ['ext] { 'H >- 'a1 }) -->('t2 : sequent ['ext] { 'H >- 'a2 }) -->sequent ['ext] { 'H >- "and"{'a1; 'a2} } =pair{'t1; 't2}

The `pair` term is the proof term of the proof: if `'t1`
is a proof of `'a1`, and `'t2` is a proof of `'a2`,
then `pair{'t1; 't2}` is a proof of `'a1 & 'a2`.
The proof term is especially useful in constructive theories; in
classical theories the proof term may just be a *canonical*
proof term, indicating the truth of the proof statement without
any computational value.

The system automatically constructs proof terms for complete
proofs, using the constructions provided by the `prim`
form in the theory. Inferences can also be *derived* from
previous rules in a theory. Derived rules are declared with the
following form:

interactivename: [params] :inference

The interactive form has exactly the same form as an `rule`,
and it introduces a proof obligation. The proof is constructed
with the proof editor.

When an `rule` is declared, the system creates a *tactic*
that can be used to apply the rule. Tactics are the general reasoning
mechanism used for interactive proving. Tactics are ML programs,
and they can be combined with the *tacticals* in the system description to provide
automated proving.

Each inference rule declaration also provides a tactic
declaration. The exact form of the tactic depends on the types
of its parameters. A *context* parameter requires an `address`
argument, a *variable* parameter requires a string, and a
*term* argument requires a `term`. For instance, the
ML definitions provided by the rules above are the following:

valhypothesis : address -> address -> string -> tacticvaland_intro : address -> tactic

For more informations about MetaPRL tactics refer to