The MetaPRL meta-logic defines a higher order logic of Horn formulas. The logic includes a term language, defined in the page on MetaPRL terms, and a meta-logic defined with a meta-implication over second-order term patterns. Each axiom and inference rule in a logic 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 logic is defined by stating its axioms and inference rules. An axiom is an inference rule that is just a single term (axioms don't use the meta-implication). The logics are modular: each module defines a logic 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 logic; it includes declarations for each of the public axioms and inference rules. Rules are not required to be listed in an interface, but for clarity, many of the logics in MetaPRL, including Itt_logic, include the inference rule declarations in their signatures.
Axioms and inference rules are declared with the axiom form. The general syntax is the following:
axiom name [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 axiom:
axiom hypothesis 'H 'J 'x :
sequent ['ext] { 'H; x: 'A; 'J['x] >- 'A }
The name of the axiom is hypothesis. The parameters include two context identifiers 'H and 'J, and a variable identifier 'x. The inference of this axiom defines a set of sequents, contaning 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 axiom has no computational value, and it is a variable otherwise (in this case the variable 'ext).
The hypothesis axiom 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, and the variable 'x is replaced by another variable. 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_logic theory validates the truth of the expression. A hypothesis (x:'A) in the Itt logic 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 axiom directive. An inference is a conditional axiom; it states assumptions that must be proved in order for the axiom 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:
axiom and_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.
Axioms and inference rules are implemented two ways: they can be derived from previous rules, are they can be as primitive axioms of a logic. 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:
prim name [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 logics, 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:
prim and_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 logics; in classical logics 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 logic. Inferences can also be derived from previous rules in a logic. Derived rules are delcared with the following form:
interactive name : [params] : inference
The interactive form has exactly the same form as an axiom, and it introduces a proof obligation. The proof is constructed with the proof editor.
When an axiom 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 axiom and 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:
val hypothesis : address -> address -> string -> tactic val and_intro : address -> tactic