%\documentclass[11pt]{article}
%\usepackage{a4}\oddsidemargin 6pt\textwidth 431pt
\documentstyle[11pt]{article}
\pagestyle{plain}\def\mizar{{\sf Mizar}}\def\nuprl{{\sf Nuprl}}\def\qed{{\sf
 QED}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%
\title{                          Possible Use of Already Formalized Mathematical
 Knowledge\\[1ex]
\large                           \qed\ Workshop II, Warsaw, July 20--22, 1995}

\author{                         Manfred Kerber\thanks
{                                Fachbereich Informatik, Universit\"at des
 Saarlandes,
                                 Im Stadtwald 15, D-66041 Saarbr\"ucken,
 Germany,
                                 e-mail: {\tt kerber@cs.uni-sb.de}, Tel.:
 (+49)681-302-4628.
                                 An extended version of this abstract can be
 found in URL: {\tt 
http://js-sfbsun.cs.uni-sb.de/pub/papers/abstracts.html\#Kerber95-QED}}}
\date{
        }
\begin{document}\maketitle
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%
\section{                           Motivation
               }

In this sessions the problems with a fixed representation language for \qed\
have been discussed. In particular the objections of G\'erard Huet against the
feasibility of \qed\ presented in the \qed\ discussion at CADE-12 (1994) were taken as
starting point. Huet said that there will be never any consent on the logical
framework (type theory, set theory, constructive logic, classical logic, generic
logic, ...).  If this is true, \qed\ must provide different formal systems for
the representation of mathematical knowledge.

It seems to be quite obvious that different formalizations have their own
advantages and drawbacks. Even 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.  The advantages of
different representations can easily be seen by means of sorts. In many
situations a sorted formulation is more adequate for the formalization and the
proof process (automatic as well as interactive) than 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 {\em not\/}
a particular sort. The same situation holds for type theory compared to set
theory.

Another important aspect concerns the reuse of big amounts of mathematical
knowledge that has been accumulated in systems like \mizar\ or \nuprl\ and
should be reusable in \qed.

\section{                                     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 of languages 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 {\em constructive meta-logic\/}, for
instance, the \nuprl-logic\footnote{see: Robert~L.\ Constable~et~al., {\em
    Implementing Mathematics with the Nuprl Proof Development System}. Prentice
  Hall, 1986.}, 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.

\begin{center}\def\fb#1{\framebox(104,40){#1}}\setlength{\unitlength}{0.15mm}
\begin{picture}(510,211)(101,540)\thicklines
\put(296,701){\fb{MLogic}}\put(510,547){\fb{OLogic$_n$}}
\put(103,549){\fb{OLogic$_1$}}\put(287,549){\fb{OLogic$_2$}}
\put(335,693){\vector(-2,-3){ 80.154}}\put(335,693){\vector( 3,-4){ 91.200}}
\put(217,564){\vector(-1, 0){  0}}\put(217,564){\vector( 1, 0){ 63}}
\put(399,564){\vector(-1, 0){  0}}\put(399,564){\vector( 1, 0){ 63}}
\put(472,554){\makebox(0,0)[lb]{...}}\put(158,631){\makebox(0,0)[lb]{formalizes}
 }
\end{picture}\end{center}

While a classical meta-language can be used for the purpose of stating the
relationship between different object logics as well, we propose to use a {\em
  constructive\/} meta-language. This has the advantage that by the constructive
meta-proofs idealists can directly employ the theorems of another theory just by
translating the theorem in their own language (and thereby avoiding the
reconstruction of possibly lengthy proofs), while nominalists\footnote{For the
  notions idealist and nominalist in the context of automated theorem proving
  see: Francis~Jeffry Pelletier. The philosophy of automated theorem proving. In
  John Mylopoulos and Ray Reiter, editors, {\em Proceedings of the 12th IJCAI},
  pages 538--543, Sydney, 1991. Morgan Kaufmann.} can translate the theorems
{\em and\/} the proofs in their own formalism. The proposed framework allows
easily to integrate existing systems in the \qed\ system.

\section{Discussion}
In the discussion the following points were made:
\begin{itemize}
\item There should be one common meta-logic only. Is PRA the best choice for a
  meta-logic?
\item After the discussion of the proposal that there should be only one single
  object logic, the idea arose that there could be a tower of object languages
  such that each can be encoded in a lower level one, with some set theory as
  the least level one.
\item In oder to restrict the number of object logics to a small number certain
  types of languages have to be offered like set theory and type theory.
\item The meta-logic should include a theory of definitions and expansion of
  definitions.
\item An alternative to a meta-logic would be the approach of having a
  collection of (program-level) translations between different formalizations
  and proof checking on this level.
\item As the last point the question was discussed on which level proofs should
  be communicated. The general opinion was that as much information as possible
  should be contained in the proofs.
\end{itemize}

\end{document}