Manfred Kerber
Fachbereich Informatik, Universitaet des Saarlandes
Im Stadtwald 15, D-66041 Saarbruecken, Germany
e-mail: kerber@cs.uni-sb.de
Tel.: (+49) 681-302-4628
This text is an excerpt made by the MU Editors. The whole paper, including logical formulas, is available in TeX (source file) form and PostScript form.
Sections: 1.Introduction. 2.Motivation. 3.Approach. 4.Example. 5.Conclusion. References.
1. Introduction
~~~~~~~~~~~
It has been one of the goals of the whole field of mechanized reasoning to
put into work Leibniz's old ideas of having a lingua characteristica, in
which each mathematical fact can be encoded, so that each dispute whether
a statement is true of not can be settled by simply calculating. This idea
has been a guideline for early reasoning systems like Automath or newer
ones like Nuprl, Getfol, Imps, Mizar, or our (Omega)MKRP. For different
reasons, however, unlike to computer algebra systems none of these systems
has gained a broader acceptance among mathematicians.
One of the most important problems with each of the above systems is the more or less fixed object logic, a user has to employ in order to encode and to prove theorems. In the following we propose a liberal approach to the question of this language. This approach is essentially based on the idea to stress a meta-system of reformulations between different object languages which allow each user to use his own object language, but nevertheless to be able to communicate the axioms, the definitions, the theorems, and the proofs. Thereby we propose an approach to QED {QED94} in which not just one further system in the list above is built but we concentrate on a very important point for the communication of proofs.
In such a liberal approach there are essentially two ways in order to guarantee correctness: either each proof must be reformulated into each other system, or there is a meta-proof that the proofs correspond to one another. In the following we propose a constructive meta-logic which satisfies both of these requirements: If you prove on a meta-level the correctness of the formal system one for the formal system two, then you can construct from each proof in system one a proof in system two.
2. Motivation
~~~~~~~~~~~
The objections of Gerard Huet against the feasibility of QED presented
in the QED discussion at CADE-94 should be taken very serious. His main
argument has been that there will be neither any consent on the logical
framework (type theory, set theory, constructive logic, classical logic,
generic logic, ...) nor on the implementation language. I think that this
is true, but in the same discussion Andrzej Trybulec has been right too,
when claiming that QED has already started in systems like Imps, Hol,
and Mizar.
As a matter of fact, mathematical foundation is opaque and there are different competing approaches, while the mathematical everyday language is quite standardized and foundational questions only play a minor role. The question which of these formalizations should be taken is not so easy to answer, since each of them has its own advantages and drawbacks. Even more severe for one single problem it might be that different formulations are appropriate, for instance, an explicit one in which a user can easily represent and recognize a theorem, and a more implicit one which is more suitable for a fully mechanical or a machine-supported proof (cp.Kerber92).
Let us shortly consider the advantages of different representations by means of sorts. In many situation a sorted formalization is more adequate for the formalization and the proof process (automatic as well as interactive) then an unsorted one. In some cases, however, it is not possible to use a (standard) sorted formalization, for instance, when you want to make a statement that a certain term has not a particular sort. The same situation holds for type theory compared to set theory. Certain statements cannot not be made in type theory, which are possible to make in set theory, nevertheless in most cases the types provide useful information which can be used during a proof search and they often allow a more compact representation and a shorter proof.
The main part of any formalization of QED has to rely on the basic language for formalizing mathematics and the notion of proof. If it should not be a mere description of static history, it has to take into account the ongoing development of the notion of a proof (compare for instance the graphically represented information in the Hyperproof system ({Barwise94}), as well as the ongoing development of the mathematical technical language. Furthermore it should not depend on the correctness or even adequacy of a single axiomatization, since mathematics went on in spite of disastrous setbacks (the discovery of the irrational numbers in the ancient world or of the Russell paradoxes in the beginning of our century). Since semantics is hard to fix, QED should start with a proof theory and let the semantics open.
The experience in our project (Omega)MKRP (Huang94) has been that a big deal of our efforts has been made in order to improve the mathematical input language (from unsorted first-order logic, sorted first-order logic, typed but unsorted higher-order logic to a sorted higher-order logic, currently we are trying to operationalize a higher-order logic with dependent types. Furthermore there has been some discussions how to represent partiality, e.g. by Kleene's strong three-valued logic). The technical language of mathematics has shown to be so rich that many concepts seem not to be adequately represented in one standard formalism (I don't speak of the expressivity in principle). A similar experience seems to have been made in the Mizar project: ``Freezing the changes in the input language and in the {\sf Mizar} processor has been a goal for quite a while, yet it seems to move away like the horizon when you try to approach it.'' (Rudnicki92, p.9).
3. Approach
~~~~~~~~~
As a consequence of the problems with one fixed language, QED should not
only support one single formal language, in which all statements have to
be made, but a (not too big) variety including the standard approaches
(like set theory or type theory). In order to be able to transfer proofs
from one format to another, it is necessary to have an exchange format for
different syntactic objects, namely terms, formulae, assertions (axioms,
definitions, theorems with their proof status), and proofs. This exchange
format should satisfy in particular the requirements that it is easy to
parse (prefix notation). Therefore it should be different from a
user-friendly high-level format that can easily be read by humans.
In order to avoid a variety of unrelated languages, they must have provable relationships. Ideally there is one constructive meta-logic, for instance, the Nuprl logic {Constable86}, in which the relationships between different formalizations can be formally proved. The main advantage of a constructive meta-logic consists in the possibility to extract from each meta-level proof an algorithm, which translates proof from one system to another.
In order to distinguish object level and meta-level, the notions of quoting and unquoting as well as the general definitions of {Genesereth87, ch.10} can be used, where primitive predicates like `Constant', `Variable' as well as functions like a function `subst' are defined.
Abstractly logical meta-level characterizations of all admitted logical systems are necessary. These characterization would make use of meta-formulae of a certain kind [ described in the full version. The rest of this Section, except for the last sentence, is omitted.] Then the interesting properties of reformulations like totality, soundness, and completeness are easy to define (for an example look at the end of the next section).
4. Example
~~~~~~~~
In a meta-logic like the one described in the last section, it is not too
hard to define for instance, the Natural Deduction (ND) calculus
(cp.{Gentzen 35ab}) for unsorted and sorted first-order logic.
Furthermore by proving on a constructive meta-level it is possible to show
that to each sorted proof there is an unsorted proof for the relativized
theorem.
[ The rest of this Section, except for the last sentence is omitted.]
technical reasons. Cp. the ftp version, as indicated above]
The proof [in question] can be given recursively by a case analysis on the
applied rules, its computational content constructs from each sorted proof
an unsorted one of the relativized theorem.
5. Conclusion
~~~~~~~~~~
The question of the concrete object language of QED is of course only one
among others, but nevertheless a very important one. Since a fixed
language seems to be too restrictive, we want to propose not to fix such a
language once and forever, but to take a liberal approach where different
languages can be linked together. For this purpose we propose a
constructive meta-language, in which the formal relationships between the
different languages used in QED can be stated and proved. By these
constructive proofs, idealist can directly employ the theorems of another
theory just by translating the theorem in his own language, while
nominalists translate the theorems and the proofs in their own formalism.
(For the notions of idealist and nominalist in the context of automated
theorem proving see Pelletier91.)
The proposed framework allows easily to integrate existing systems in the
QED system.
Another major point of discussion should be how data bases of mathematical facts can be built up. Axioms should clearly distinguished from definitions, since they can not be proved to consistent in general, whereas definitions should be restricted to conservative extensions. Nevertheless the addition of a definition has to be in accordance with its general use, therefor it is necessary to find some publically controlled manner of adding definitions. For theorems it is of course necessary to add them only as theorems, if the corresponding proofs can be delivered. Also here is not the problem that naming is accordance with general costums, they should be distinguished from only local lemmas, in order not to fill the data bases with unimportant information.
Much more fussy is problem of changing definitions or axioms: A trivial solution of this problem is to reprove all theorems in the data base, more sophisticated would be an approach, in which each theorem contains the information on which axioms, definitions and other theorems it depends. In this case only the concerned theorems have to be proved again.}
References
~~~~~~~~
{QED94}
Anonymous. The QED manifesto. In Alan Bundy, editor, "Proc. of the 12th
CADE", pp. 238--251, Nancy, France, 1994. Springer Verlag,
Berlin,Germany. LNAI 814.
{Barwise94} Jon Barwise and John Etchemendy. "Hyperproof". CSLI Lecture Notes. Chicago University Press, Chicago, USA, 1994.
{Constable86} R.L. Constable et al. "Implementing Mathematics with the Nuprl Proof Development System". Prentice Hall, Englewood Cliffs, New Jersey, USA, 1986.
{Genesereth87} Michael R. Genesereth and Nils J. Nilsson. "Logical Foundations of Artificial Intelligence". Morgan Kaufmann, San Mateo, California, USA, 1987.
{Gentzen35ab} Gerhard Gentzen. Untersuchungen ueber das logische {S}chlie{\ss}en {I} & {II}. "Mathematische Zeitschrift", 39: 176--210, 572--595, 1935.
{Huang94} Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Joern Richts, and Joerg Siekmann. {Omega}MKRP: A proof development environment. In Alan Bundy, editor, "Proc. of the 12th CADE", pages 788--792, Nancy, 1994. Springer Verlag, Berlin\Germany, LNAI 814.
{Kerber92} Manfred Kerber and Axel Praecklein. Tactics for the improvement of problem formulation in resolution-based theorem proving. SEKI Report SR-92-09, Fachbereich Informatik, Universitaet des Saarlandes, 1992.
{Pelletier91} Francis Jeffry Pelletier. The philosophy of automated theorem proving. In John Mylopoulos and Ray Reiter, editors, "Proc. of the 12th IJCAI", pages 538--543, Sydney, 1991. Morgan Kaufmann, San Mateo, California, USA.
{Rudnicki92} Piotr Rudnicki. An overview of the Mizar project. Bastaad, Sweden, 1992.