Metatheorem

A metatheorem is a theorem about an object language. This is a very general statement, but metatheorem is a very general term. Many interesting metatheorems can be posed as ∀∃-statements, and these are the kind of metatheorems that can be verified in Twelf. Another kind of metatheorem is a totality assertion; these are more limited because any totality assertion can also be posed as a ∀∃-statement.

Twelf can prove ∀∃-metatheorems in one of two ways. The first method, the theorem prover, is incomplete and not currently recommended for use. It allows the user to directly specify a ∀∃-statement about LF terms, and then ask Twelf to verify that statement. The other method is to write out a proof of the ∀∃ statement in Twelf, and then use Twelf's ability to state and verify totality assertions to show that the proof is correct.

Object language

The object language is "the object of study": a logic, programming language, or other deductive system that the user wishes to reason about with Twelf. Simple examples of object languages are natural numbers and the simply-typed lambda calculus, more complex examples can be found in the case studies or research projects using Twelf. Object languages like the simply-typed lambda calculus and first-order logic demonstrate the power of Twelf's higher-order abstract syntax, but the example of natural numbers with addition is used here for its simplicity. The syntax and judgments over the natural numbers can be simply presented in Backus-Naur form:

We then declare to be a judgment that relates three natural numbers. We can define what kind of judgments we are allowed to relate by using inference rules:

         

Theorems

The usual interpretation of inference rules like the ones above is that we can consider some fact A to be true if we can create a complete derivation that has A a result. Truths that can be verified by writing a derivation are called theorems. If the object language is the natural numbers, then the following is a theorem theorem proving that 2 + 1 = 3.

Similarly, if the object language is the simply-typed lambda calculus, then a theorem might state that the expression steps to . This can be shown by using the rules step_app_beta and value_empty.

Totality assertions

The term "metatheorem," as previously stated, is a very general term. We first want to think about a specific kind of metatheorem, a totality assertion.

A totality assertion for the informal deductive system presented above might be that, for any two natural numbers and , there is a natural number for which is derivable. This means that the judgment forms a total relation, mapping any inputs in the first and second positions of the relation to some output in the third position. Note that the output need not be unique; the totality assertion holds even if there are many such numbers.

The totality assertions in Twelf establish a stronger property. The Twelf encoding of the judgment can be run as a logic program, and totality assertions that are verified by %total directives verify that, if an encoding is run as a higher-order logic program in Twelf, it will act as a function that, given appropriate inputs, will find an output in a finite amount of time. Twelf's totality analysis is incomplete in that some relations that are total cannot be verified by a %total declaration.

Twelf, when used in this way, can be thought of as a "theorem prover" in the limited sense that it proves that a relation is total by doing a program analysis that shows that, given appropriate inputs, it produces outputs when run as a logic program in Twelf. However, it is more common to describe Twelf as verifying the totality assertions, both because Twelf does not produce a proof witness and because the analysis is not as sophisticated as most theorem proving procedures. Usually, the relations about which programmers intend to prove totality assertions are specifically constructed to be analyzable by Twelf's %total directive. These relations often correspond closely to an informal proof by structural induction of the same fact, making Twelf's process of verifying totality similar to the human process of verifying that a proof is valid.

∀∃-statements

Totality assertions seem very limited in scope. We have merely shown that, given a judgment like , we can interpret as the judgment as a relation from some inputs to some outputs and prove that the relation, given inputs, have rules that will always allow us to find outputs. But we can't, for instance, write a totality assertion on that will allow us to prove that the relation is commutative or associative.

The theorem "addition is commutative" can be specified more precisely like this: for all natural numbers , , and derivation of the judgment , there exists a derivation of the judgment . The previous statement, at a high level, said "for all (some things) there exist (some other things." Statement with this forms are called ∀∃-statement.

The page about Twelf's theorem prover shows how the theorem prover could be used to state, and prove, this statement, but the currently recommended way of doing this is by using a totality assertion. The series of tutorials on proving metatheorems with Twelf explain in detail how to do this; the remainder of this article will only give a very general view based on the notes from Lecture 18 of Frank Pfenning's course on Logic Programming.

Simple types

First, think back at our presentation of the structure of natural numbers:

We will now think of this BNF grammar as defining the members of the type . In this view is an object of type , and is a constructor that, given an object of type , produces an object of type .

Proof terms

Now, look back at this derivation

and notice that applying the rule twice to the rule , as we do here, gives us a way to derive for any natural number N; in the example above, N happens to be .

Natural numbers are objects, and we can think of derivations as objects as well: we can represent this process of applying the rule twice to the rule using standard notation for application: . These objects are called generally called proof terms, and the type of a proof term is the judgment it can produce. This idea that judgments can be types is one of the important observations of the Curry-Howard isomorphism.

The proof term can be thought of as having the type , but it can also be thought of as having the type . Remembering our analysis above, we can see that the most general type we can give the proof object is .

Proving ∀∃-statements using totality assertions

Recall that when we first defined the judgment , we mentioned the type of objects that it related:

We will now write a judgment that, instead of relating objects with type , relates derivations of and . Call this derivation .

Describing the rules that define this judgment is beyond the scope of this article; see Frank Pfenning's notes notes for a continuation of this approach, or proving metatheorems with Twelf for a description that is closer to how Twelf is used in practice. However, without describing these rules, if they were written and written correctly, we could verify a totality assertion that stated that plus-comm is a total relation with derivations of as an input and derivations of as an output.

This means that, for any three natural numbers , , and , and any proof object with the type , there is a proof object with type . This is equivalent to the ∀∃-statement for the commutativity of addition that we started out with; the only difference is that we are now speaking in terms of proof objects and types instead of derivations and judgments.