Metamathematical Extensibility in Type Theory
by Todd B. Knoblock
Cornell University Ph.D. Thesis
An automated theorem prover is said to be metamathematically extensible if a metalanguage can be employed by the user to soundly extend the reasoning capabilities of the system. In this thesis, we present a framework for metamathematical extensibility for a system based upon a type-theoretic logic, the Nuprl system. Using this framework, the user can construct programs called proof tactics that may be used to provide new reasoning capabilities for the logic. These proof tactics can encode reasoning methods assimple asd a derived rule of inference or as ambitious as a theorem prover.The design of the framework ensures that all proof tactics are correct.
A formal metalanguage called Metaprl is defined that represents the proof theory of Nuprl in a natural and computationally-oriented fashion. The logic of Metaprl is an extension of the constructive type theory of Nuprl. Type theories like Nuprl and Metaprl are distinguished by the uniform treatment of computations (programs) and logical propositions and by rich languages for expressing computations. In Metaprl, formal specifications for tactics may be written and formally correct tactics extracted from the proofs of the specification.Three classes of tactics are defined: complete tactics, partial tactics, and search tactics. Complete tactics are analogous to derived axioms for the Nuprl logic. Partial tactics are analogous to derived rules of inference. Search tactics are analogous to the procedural tactics of LCF and the current Nuprl system. Examples from each class of tactics are presented.There are a number of advantages to using a formal logic as a metalanguage for metamathematical extensibility. System-implemented reflection principles guarantee that the framework is a conservative extension of Nuprl. The expressiveness of the Metaprl logic allows the validity of tactics to be ensured. Often it is not even necessary to execute tactics since they have been proved correct and all that is required is that a proof exists; the exact form for the proof is not needed. This can result in substantial computational savings. Finally, the construction of a metalanguage for metamathematical extensibility for Nuprl is generalized to a hierarchy of metalanguages, each logic providing for metamathematical extensibility of the preceeding logic.
bibTex ref: Knob87