\documentstyle[12pt]{article}
\scrollmode
% DINA4-Format
\oddsidemargin 6pt\evensidemargin 6pt\marginparwidth 48pt\marginparsep 10pt
\topmargin -18pt\headheight 12pt\headsep 25pt\footheight 12pt\footskip 30pt
\textheight 625pt\textwidth 431pt\columnsep 10pt\columnseprule 0pt
\title{An Approach of Formalizing Mathematics\\ by Reformulations\\
\Large -- A Proposal for \qed\ --}

\author{\sl Manfred Kerber\\
\sl Fachbereich Informatik, Universit\"at des Saarlandes\\
\sl Im Stadtwald 15, D-66041 Saarbr\"ucken, Germany\\
\sl e-mail: {\tt kerber@cs.uni-sb.de}\quad
\sl Tel.: (+49) 681-302-4628
}

\pagestyle{plain}
%\input{macros.tex}
\newcounter{theo}%[chapter]
%\input{generalmacros.tex}
%Exchange of greek symbols
%\phi<->varphi
\let\phivar\phi
\let\phi\varphi
\let\varphi\phivar
%\theta<->vartheta
\let\thetavar\theta
\let\theta\vartheta
\let\vartheta\thetavar
%\rho<->varrho
\let\rhovar\rho
\let\rho\varrho
\let\varrho\rhovar

%General Macros
\newcommand{\comment}[1]{}
\newcommand{\zzabstand}{\; \;}

%Logical Macros
%Connectives
\newcommand{\eqv}{\leftrightarrow}
\newcommand{\defeqv}{\stackrel{\rm def}{\eqv}}
\newcommand{\impl}{\rightarrow}
\newcommand{\implies}{\impl}
\newcommand{\implby}{\leftarrow}
\newcommand{\nicht}{\neg}
\newcommand{\non}{\neg}
\newcommand{\und}{\wedge}
\newcommand{\oder}{\vee}
%Quantifier
\newcommand{\sdot}{\rule{2pt}{2pt}}
\newcommand{\all}[1]{\forall {#1} \sdot\,}
\newcommand{\allin}[2]{\forall {#1}\in #2\sdot\,}
\newcommand{\alltype}[2]{\forall {#1} \! : \! #2\sdot\,}
\newcommand{\allsort}[3]{\forall {#1}_{#2}^{#3}\sdot\,}
\newcommand{\ex}[1]{\exists {#1}\sdot\,}
\newcommand{\exin}[2]{\exists {#1}\in {#2}\sdot\,}
\newcommand{\extype}[2]{\exists {#1} \! : \! {#2}\sdot\,}
\newcommand{\exsort}[3]{\exists {#1}_{#2}^{#3}\sdot\,}
%Sets
\newcommand{\set}[1]{\{ #1 \} }
\newcommand{\setdevider}{\mbox{\,$|$\,}}
%Misc
\newcommand{\strongmodels}{\mbox{$|\hskip-0.47em\equiv$}}
\newcommand{\quo}[1]{\mbox{``}#1\mbox{''}}
\newcommand{\unquo}[1]{\langle #1\rangle}
\newcommand{\omicron}{o}
\newcommand{\pair}[1]{\langle #1\rangle}
\newcommand{\subst}[3]{#1[#2/#3]}

%Environments
\makeatletter
\newcommand{\bi}{\begin{itemize}}
\newcommand{\ei}{\end{itemize}}
\newcommand{\bd}{\begin{description}}
\newcommand{\ed}{\end{description}}
\def\bt{\@ifnextchar[{\@btzwei}{\@bteins}}
\def\@btzwei[#1]#2{\begin{tabular}[#1]{#2}}
\def\@bteins#1{\begin{tabular}{#1}}
\newcommand{\et}{\end{tabular}}
\newcommand{\be}{\begin{enumerate}}
\newcommand{\ee}{\end{enumerate}}
\def\ba{\@ifnextchar[{\@bazwei}{\@baeins}}
\def\@bazwei[#1]#2{\begin{array}[#1]{#2}}
\def\@baeins#1{\begin{array}{#1}}
\newcommand{\ea}{\end{array}}
\makeatother

%Theorems, definitions, etc.
\newenvironment{aux}[1]{
\vspace{1.5ex}\partopsep0.0ex\topsep0.2ex\itemsep0.2ex\parindent0.0ex
\par\refstepcounter{theo}
{\renewcommand{\baselinestretch}{1}\small\normalsize {\definitionfont\thetheo\
#1:}}
\renewcommand{\baselinestretch}{1}\small\normalsize}%
{\nopagebreak\vspace{1.5ex}\par}

\makeatletter
\def\definition{\@ifnextchar[{\@definitionzwei}{\@definitioneins}}
\def\@definitionzwei[#1]{\begin{aux}{Definition (#1)}}
\def\@definitioneins{\begin{aux}{Definition}}
\def\enddefinition{\end{aux}}

\def\assumption{\@ifnextchar[{\@assumptionzwei}{\@assumptioneins}}
\def\@assumptionzwei[#1]{\begin{aux}{\ifgerman{Annahme}\else{Assumption}\fi
(#1)}}
\def\@assumptioneins{\begin{aux}{\ifgerman{Annahme}\else{Assumption}\fi}}
\def\endassumption{\end{aux}}

\def\notation{\@ifnextchar[{\@notationzwei}{\@notationeins}}
\def\@notationzwei[#1]{\begin{aux}{Notation (#1)}}
\def\@notationeins{\begin{aux}{Notation}}
\def\endnotation{\end{aux}}

\def\example{\@ifnextchar[{\@examplezwei}{\@exampleeins}}
\def\@examplezwei[#1]{\begin{aux}{\ifgerman{Beispiel}\else{Example}\fi (#1)}}
\def\@exampleeins{\begin{aux}{\ifgerman{Beispiel}\else{Example}\fi}}
\def\endexample{\end{aux}}

\def\theorem{\@ifnextchar[{\@theoremzwei}{\@theoremeins}}
\def\@theoremzwei[#1]{\begin{aux}{Theorem (#1)}\it}
\def\@theoremeins{\begin{aux}{Theorem}\it}
\def\endtheorem{\end{aux}}

\def\lemma{\@ifnextchar[{\@lemmazwei}{\@lemmaeins}}
\def\@lemmazwei[#1]{\begin{aux}{Lemma (#1)}\it}
\def\@lemmaeins{\begin{aux}{Lemma}\it}
\def\endlemma{\end{aux}}

\def\remark{\@ifnextchar[{\@remarkzwei}{\@remarkeins}}
\def\@remarkzwei[#1]{\begin{aux}{\ifgerman{Bemerkung}\else{Remark}\fi (#1)}}
\def\@remarkeins{\begin{aux}{\ifgerman{Bemerkung}\else{Remark}\fi}}
\def\endremark{\end{aux}}

\newenvironment{proof}{\par{\bf Proof:}}{\hspace*{\fill} \rule{2mm}{2mm}}
\makeatother

%Fonts
\def\cA{{\cal A}} \def\cB{{\cal B}} \def\cC{{\cal C}} \def\cD{{\cal D}}
\def\cE{{\cal E}} \def\cF{{\cal F}} \def\cG{{\cal G}} \def\cH{{\cal H}}
\def\cI{{\cal I}} \def\cJ{{\cal J}} \def\cK{{\cal K}} \def\cL{{\cal L}}
\def\cM{{\cal M}} \def\cN{{\cal N}} \def\cO{{\cal O}} \def\cP{{\cal P}}
\def\cQ{{\cal Q}} \def\cR{{\cal R}} \def\cS{{\cal S}} \def\cT{{\cal T}}
\def\cU{{\cal U}} \def\cV{{\cal V}} \def\cW{{\cal W}} \def\cX{{\cal X}}
\def\cY{{\cal Y}} \def\cZ{{\cal Z}}

\def\bfA{{\bf A}} \def\bfB{{\bf B}} \def\bfC{{\bf C}} \def\bfD{{\bf D}}
\def\bfE{{\bf E}} \def\bfF{{\bf F}} \def\bfG{{\bf G}} \def\bfH{{\bf H}}
\def\bfI{{\bf I}} \def\bfJ{{\bf J}} \def\bfK{{\bf K}} \def\bfL{{\bf L}}
\def\bfM{{\bf M}} \def\bfN{{\bf N}} \def\bfO{{\bf O}} \def\bfP{{\bf P}}
\def\bfQ{{\bf Q}} \def\bfR{{\bf R}} \def\bfS{{\bf S}} \def\bfT{{\bf T}}
\def\bfU{{\bf U}} \def\bfV{{\bf V}} \def\bfW{{\bf W}} \def\bfX{{\bf X}}
\def\bfY{{\bf Y}} \def\bfZ{{\bf Z}}
\def\bfa{{\bf a}} \def\bfb{{\bf b}} \def\bfc{{\bf c}} \def\bfd{{\bf d}}
\def\bfe{{\bf e}} \def\bff{{\bf f}} \def\bfg{{\bf g}} \def\bfh{{\bf h}}
\def\bfi{{\bf i}} \def\bfj{{\bf j}} \def\bfk{{\bf k}} \def\bfl{{\bf l}}
\def\bfm{{\bf m}} \def\bfn{{\bf n}} \def\bfo{{\bf o}} \def\bfp{{\bf p}}
\def\bfq{{\bf q}} \def\bfr{{\bf r}} \def\bfs{{\bf s}} \def\bft{{\bf t}}
\def\bfu{{\bf u}} \def\bfv{{\bf v}} \def\bfw{{\bf w}} \def\bfx{{\bf x}}
\def\bfy{{\bf y}} \def\bfz{{\bf z}}

\def\sfA{{\sf A}} \def\sfB{{\sf B}} \def\sfC{{\sf C}} \def\sfD{{\sf D}}
\def\sfE{{\sf E}} \def\sfF{{\sf F}} \def\sfG{{\sf G}} \def\sfH{{\sf H}}
\def\sfI{{\sf I}} \def\sfJ{{\sf J}} \def\sfK{{\sf K}} \def\sfL{{\sf L}}
\def\sfM{{\sf M}} \def\sfN{{\sf N}} \def\sfO{{\sf O}} \def\sfP{{\sf P}}
\def\sfQ{{\sf Q}} \def\sfR{{\sf R}} \def\sfS{{\sf S}} \def\sfT{{\sf T}}
\def\sfU{{\sf U}} \def\sfV{{\sf V}} \def\sfW{{\sf W}} \def\sfX{{\sf X}}
\def\sfY{{\sf Y}} \def\sfZ{{\sf Z}}
\def\sfa{{\sf a}} \def\sfb{{\sf b}} \def\sfc{{\sf c}} \def\sfd{{\sf d}}
\def\sfe{{\sf e}} \def\sff{{\sf f}} \def\sfg{{\sf g}} \def\sfh{{\sf h}}
\def\sfi{{\sf i}} \def\sfj{{\sf j}} \def\sfk{{\sf k}} \def\sfl{{\sf l}}
\def\sfm{{\sf m}} \def\sfn{{\sf n}} \def\sfo{{\sf o}} \def\sfp{{\sf p}}
\def\sfq{{\sf q}} \def\sfr{{\sf r}} \def\sfs{{\sf s}} \def\sft{{\sf t}}
\def\sfu{{\sf u}} \def\sfv{{\sf v}} \def\sfw{{\sf w}} \def\sfx{{\sf x}}
\def\sfy{{\sf y}} \def\sfz{{\sf z}}

\def\frakA{\mbox{\frak A}} \def\frakB{\mbox{\frak B}} \def\frakC{\mbox{\frak C}}
\def\frakD{\mbox{\frak D}}
\def\frakE{\mbox{\frak E}} \def\frakF{\mbox{\frak F}} \def\frakG{\mbox{\frak G}}
\def\frakH{\mbox{\frak H}}
\def\frakI{\mbox{\frak I}} \def\frakJ{\mbox{\frak J}} \def\frakK{\mbox{\frak K}}
\def\frakL{\mbox{\frak L}}
\def\frakM{\mbox{\frak M}} \def\frakN{\mbox{\frak N}} \def\frakO{\mbox{\frak O}}
\def\frakP{\mbox{\frak P}}
\def\frakQ{\mbox{\frak Q}} \def\frakR{\mbox{\frak R}} \def\frakS{\mbox{\frak S}}
\def\frakT{\mbox{\frak T}}
\def\frakU{\mbox{\frak U}} \def\frakV{\mbox{\frak V}} \def\frakW{\mbox{\frak W}}
\def\frakX{\mbox{\frak X}}
\def\frakY{\mbox{\frak Y}} \def\frakZ{\mbox{\frak Z}}
\def\fraka{\mbox{\frak a}} \def\frakb{\mbox{\frak b}} \def\frakc{\mbox{\frak c}}
\def\frakd{\mbox{\frak d}}
\def\frake{\mbox{\frak e}} \def\frakf{\mbox{\frak f}} \def\frakg{\mbox{\frak g}}
\def\frakh{\mbox{\frak h}}
\def\fraki{\mbox{\frak i}} \def\frakj{\mbox{\frak j}} \def\frakk{\mbox{\frak k}}
\def\frakl{\mbox{\frak l}}
\def\frakm{\mbox{\frak m}} \def\frakn{\mbox{\frak n}} \def\frako{\mbox{\frak o}}
\def\frakp{\mbox{\frak p}}
\def\frakq{\mbox{\frak q}} \def\frakr{\mbox{\frak r}} \def\fraks{\mbox{\frak s}}
\def\frakt{\mbox{\frak t}}
\def\fraku{\mbox{\frak u}} \def\frakv{\mbox{\frak v}} \def\frakw{\mbox{\frak w}}
\def\frakx{\mbox{\frak x}}
\def\fraky{\mbox{\frak y}} \def\frakz{\mbox{\frak z}}

%Special sets N,Z,Q,R,N_0

\newcommand{\Nat}{{\mathchoice{\displaystyle\sf I\hskip-0.14em N}
{\textstyle\sf I\hskip-0.14em N}
{\scriptstyle\sf I\hskip-0.09em N}
{\scriptscriptstyle\sf I\hskip-0.09em N}}}
\newcommand{\Int}{{\mathchoice{\displaystyle\sf Z\hskip-0.42em Z}
{\textstyle\sf Z\hskip-0.42em Z}
{\scriptstyle\sf Z\hskip-0.35em Z}
{\scriptscriptstyle\sf Z\hskip-0.35em Z}}}
\newcommand{\Rat}{{\mathchoice{\displaystyle\sf I\hskip-0.42em Q}
{\textstyle\sf I\hskip-0.42em Q}
{\scriptstyle\sf I\hskip-0.35em Q}
{\scriptscriptstyle\sf I\hskip-0.35em Q}}}
\newcommand{\Real}{{\mathchoice{\displaystyle\sf I\hskip-0.14em R}
{\textstyle\sf I\hskip-0.14em R}
{\scriptstyle\sf I\hskip-0.09em R}
{\scriptscriptstyle\sf I\hskip-0.09em R}}}
\newcommand{\Nnull}{\Nat_{0}}

%Diagrammpfeile
\def\mapright#1{\smash{\mathop{\hbox to 23 pt%
{\rightarrowfill}} \limits^{#1}}}
\def\mapleft#1{\smash{\mathop{\hbox to 23pt%
{\leftarrowfill}}\limits^{#1}}}
\def\mapdown#1{\Big\downarrow\rlap{$\vcenter{\hbox%
{$\scriptstyle #1$}}$}}
\def\mapup#1{\Big\uparrow\rlap{$\vcenter{\hbox%
{$\scriptstyle #1$}}$}}

%Variables
\newif\ifgerman\germanfalse
\newcommand{\eispace}{\vspace*{-5ex}}
\newcommand{\definitionfont}{\bf}

\newcommand{\Rel}{\Re}
\newcommand{\sigax}{{\bf AX}}
\newcommand{\subsorteq}{\sqsubseteq}
%\newcommand{\strich}{\mbox{-}}
%\newcommand{\vek}[1]{\overline{#1}}
\newcommand{\Termset}{\mbox{\boldmath$T$}}
\newcommand{\Varset}{\mbox{\boldmath$V$}}
\newcommand{\equal}{\equiv}

%Listen
\newcommand{\bl}[1]{\begin{list}{#1}%
{\labelwidth12.0ex\leftmargin16.0ex\labelsep3.0ex}}
\newcommand{\el}{\end{list}}
\let\llabelenumi\labelenumi
\newcommand{\llabel}[1]{\renewcommand\labelenumi{#1\arabic{enumi}}}
\newcommand{\llabelreset}{\let\labelenumi\llabelenumi}
\newcommand{\myfill}{\hspace*{\fill}}

%Outfit
%Listengestaltung
\renewcommand{\labelitemi}{--}
\renewcommand{\labelitemii}{$\ast$}
\renewcommand{\labelitemiii}{$\cdot$}
\itemsep-0.5ex
%\topsep0.0ex
\arraycolsep0.0ex

%Fussnoten

%Header und Footer
\def\addvspacetableofcontents{1pt}%{1.0em plus 1pt}
%\renewcommand{\footnoterule}{\rule{0cm}{0cm} \vspace{0cm}}

%Absaetze
\parskip0.5ex plus 0.15ex minus 0.25ex
\newcommand{\zeilenabstand}{1.0em plus 0.3em minus 0.5em}
\newcommand{\halbzeilenabstand}{0.5em plus 0.15em minus 0.25em}


\def\hat{\widehat}

\newenvironment{remarks}[1]{\begin{aux}{#1}{Remarks}}{\end{aux}}

%myhyphen.tex
\hyphenation{Mo-nats-hef-te rep-re-sen-ta-tion Ma-the-ma-tik
mathe-mat-ics meta-mathe-mat-ics e-quiv-a-lence con-struct con-structed
Sprin-ger Kai-sers-lau-tern Be-griffs-schrift Ver-lag in-tui-tio-ni-sti-schen
Sy-ste-me Fach-be-reich}


%---------------------------------- Systems
\newcommand{\automath}{{\sf Automath}}
\newcommand{\clam}{\mbox{\rm CL\kern-.36em\raise.39ex\hbox{\sc a}\kern-.15emM}}
\newcommand{\cyc}{{\sf CYC}}
\newcommand{\fol}{{\sf FOL}}
\newcommand{\getfol}{{\sf Getfol}}
\newcommand{\hol}{{\sf HOL}}
\newcommand{\imps}{{\sf IMPS}}
\newcommand{\isabelle}{{\sf Isabelle}}
\newcommand{\klone}{{\sc Kl-one}}
\newcommand{\lcf}{{\sf LCF}}
\newcommand{\mizar}{{\sf Mizar}}
\newcommand{\mkrp}{{\sf MKRP}}
\newcommand{\ontic}{{\sf Ontic}}
\newcommand{\oyster}{\mbox{\rm O\kern-.12em\raise.39ex\hbox{\sc y}\kern-.07emS
\kern-.39em\raise.39ex\hbox{\sc t}\kern-.15em\hbox{\sc e}R}}
\newcommand{\nqthm}{{\sf NQTHM}}
\newcommand{\nuprl}{{\sf Nuprl}}
\newcommand{\omegamkrp}{\mbox{$\Omega$-{\sf MKRP}}}
\newcommand{\otter}{{\sf Otter}}
\newcommand{\qed}{{\sf QED}}
\newcommand{\tps}{{\sf TPS}}


\newcommand{\tuple}[1]{\left\langle #1 \right\rangle}
\newcommand{\syntax}{{\rm syntax}}
\newcommand{\semantics}{{\rm semantics}}
\newcommand{\calculus}{{\rm calculus}}
\def\bac#1#2{$\begin{array}{c}#2\end{array}$\quad #1}
\def\bacthree#1#2{$\begin{array}{ccc}#2\end{array}$\quad #1}
\begin{document}
\maketitle

\section{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 \omegamkrp. 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 {\em 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\ \cite{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 {\em 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.

\section{Motivation}

The objections of G\'erard 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.~\cite{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 {\em 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 {\sf Hyperproof} system \cite{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 \omegamkrp\ \cite{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 {\sf 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.'' \cite[p.9]{Rudnicki92}.

\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 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 \cite{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
$\quo{.}$ and unquoting $\unquo{.}$ as well as the general definitions of
\cite[Chapter10]{Genesereth87} can be used, where primitive predicates like {\sf
  Constant}, {\sf Variable} as well as functions like a function {\sf subst} are
defined.

Abstractly logical meta-level characterizations of all admitted logical systems
are necessary. These characterization would make use of
meta-formulae of the kind ${\sf formula}^j(\quo{\phi^j})$  which stands for the
fact that $\phi^j$ is a formula in the formal system $S^j$.
Correspondingly predicates
$\Pi^j(\quo{\Delta\vdash^j\Gamma},\pi^j)$, standing for $\pi^j$ is a proof
for $\Delta\vdash^j\Gamma$ in the formal system $S^j$, can be employed.  Of
course, the
meta-language has to be rich enough that the notions of formula and proof can be
defined in it. For instance, if we have some derivability relations like\\[1ex]
\myfill    $\begin{array}{c} \Delta_1\vdash^j
           \Gamma_1;\ldots;\Delta_n\vdash^j\Gamma_n \\\hline
           \Delta\vdash^j\Gamma\end{array}$ ${\sf RULE}_k^j$ \myfill and\myfill
          $\begin{array}{c} \emptyset\\\hline
           \Delta\vdash^j\Gamma\end{array}$ ${\sf AXIOM}_k^j$\myfill\\[1ex]
we have the following formulae in the meta-language in order to
axiomatize the notion of proof
$$\ba{ll}
\Pi^j(\quo{\unquo{\Delta_1}\vdash^j\unquo{\Gamma_1}},\pi_1)\und\ldots\und
\Pi^j(\quo{\unquo{\Delta_n}\vdash^j\unquo{\Gamma_n}},\pi_n)\implies\\
\phantom{\Pi^j(\quo{\unquo{\Delta_1}\vdash^j\unquo{\Gamma_1}},\pi_1)\und}
\Pi^j(\quo{\unquo{\Delta}\vdash^j\unquo{\Gamma}},{\sf
RULE}_k^j(\pi_1,\ldots,\pi_n))\\[1ex]
\Pi^j(\quo{\unquo{\Delta}\vdash^j\unquo{\Gamma}},{\sf AXIOM}_k^j)
\ea$$
where all variables $\Delta_j$, $\Gamma_j$, and $\pi_j$ are implicitly
universally quantified.\vspace{1ex}

Let $\cS^1$ and $\cS^2$ be two formal systems. A reformulation $\Theta$ is a
partial mapping between $\cS^1$ and $\cS^2$, that is, a functor which maps
formula sets to formula sets and proofs to proofs, with elements $\sfU_f$ for an
undefined formula and $\sfU_\pi$ for an undefined proof, such that for all
formula sets $\Gamma$ of $\cS^1$, $\Theta(\Gamma)$ is either $\sfU_f^2$ or a
formula set of $\cS^2$.  Analogously for all proofs $\pi$ in $\cS^1$,
$\Theta(\pi)$ is equal to $\sfU_\pi^2$ or a proof in $\cS^2$. Furthermore we
assume $\Theta(\sfU_f^1)=\sfU_f^2$ and $\Theta(\sfU_\pi^1)=\sfU_\pi^2$. We need
the elements \sfU\ since certain expressions in one formal system may have no
correspondence in another one.

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).


\section{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.~\cite{Gentzen35ab}) 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.

In an ND calculus for sorted as for unsorted first-order logic you
have the axioms (with $j\in\set{s,u}$, $s$ standing for ``sorted'' and
$u$ standing for ``unsorted''):\\[1ex]
\myfill $\phi\vdash^j \phi$ (Assumption)\myfill and \myfill
$\vdash^j \phi\vee\neg\phi$ (Tertium non datur)\myfill\\[1ex]
For each connective and quantifier, there are introduction and
elimination rules. For the connectives they are the same, e.g.\\[1ex]
\begin{tabular}{p{0.47\textwidth}@{\qquad}p{0.4\textwidth}}
\bac{$\impl$E}{\Gamma\vdash^j \phi\qquad \Gamma\vdash^j \phi\impl\psi\\\hline
\Gamma\vdash^j \psi}&
\bac{$\wedge$I}{\Gamma\vdash^j \phi\qquad \Gamma\vdash^j \psi\\\hline
\Gamma\vdash^j \phi\wedge\psi}
\end{tabular}\par\vspace{1ex}

\noindent For the quantifiers the rules differ. For instance, in the sorted case
we
have:\\[1ex]
\begin{tabular}{p{0.47\textwidth}@{\qquad}p{0.44\textwidth}}
\bac{$\forall$I}{\Gamma\vdash^s\subst{\phi}{x}{a}\\\hline
                 \Gamma\vdash^s\allin{x}{S} \phi}
  {\renewcommand{\baselinestretch}{0}\footnotesize
  \begin{minipage}{0.24\textwidth}{
  \footnotesize with eigenvariable condition and $a$ has sort $S$}
  \end{minipage}} &

\bac{$\forall$E\ }{\Gamma\vdash^s\allin{x}{S} \phi\\\hline
                 \Gamma\vdash^s\subst{\phi}{x}{t}}%
 {\renewcommand{\baselinestretch}{0}\footnotesize
 \begin{minipage}{0.2\textwidth}{if sort of $t$ compatible to sort of $x$}
 \end{minipage}}
\end{tabular}\par\vspace{1ex}

\noindent The corresponding unsorted rules are:\\[1ex]
\begin{tabular}{p{0.47\textwidth}@{\qquad}p{0.41\textwidth}}
\bac{$\forall$I}{\Gamma\vdash^u\subst{\phi}{x}{a}\\\hline
                 \Gamma\vdash^u\all{x} \phi}
 {\renewcommand{\baselinestretch}{0}\footnotesize
 \begin{minipage}{0.24\textwidth}{\footnotesize with eigenvariable condition}
 \end{minipage}}&

\bac{$\forall$E}{\Gamma\vdash^u\all{x} \phi\\\hline
                 \Gamma\vdash^u\subst{\phi}{x}{t}}
\end{tabular}\par\vspace{1ex}

\noindent These rules can be expressed in the constructive meta-logic. In the
following, we employ a sorted first-order variant of constructive logic, where
each term has two sorts, one for indexing the formal system $\cS^j$ the term
belongs to (here again $j=s,u$ for sorted or unsorted) and one for abbreviating
unary meta-predicates like variable, term, or formula.  For instance the sorted
version of the $\forall$E rule becomes:
$$\ba[t]{ll}\allsort{\Gamma}{\sf formula\_set}{s}&\allsort{x}{\sf
variable}{s}\allsort{S}{\sf sort}{s}\allsort{\phi}{\sf
formula}{s}\allsort{t}{\sf
term}{s}\allsort{\pi}{\sf proof}{s}\\
&\Pi^s(\quo{\unquo{\Gamma}\vdash^s\allin{\unquo{x}}{\unquo{S}}\unquo{\phi}},\pi)
\und
{\sf sort\_compatible}(x,t)\impl\\ &\Pi^s(\quo{\unquo{\Gamma}\vdash^s\unquo{{\sf
subst}(\phi,x,t)}},\mbox{$\forall$E}(t)\circ\pi)\ea$$
In the unsorted case we have:
$$\ba[t]{l}
\allsort{\Gamma}{\sf
formula\_set}{u}\allsort{x}{\sf variable}{u}\allsort{\phi}{\sf
formula}{u}\allsort{t}{\sf term}{u}\allsort{\pi}{\sf proof}{u}\\
\phantom{\Gamma_{\sf
formula}}\Pi^u(\quo{\unquo{\Gamma}\vdash^u\all{\unquo{x}}\unquo{\phi}},\pi)\impl
\Pi^u(\quo{\unquo{\Gamma}\vdash^u\unquo{{\sf
subst}(\phi,x,t)}},\mbox{$\forall$E}(t)\circ\pi)\ea$$
In order to prove the sort theorem, we have to show
$$\ba[t]{l}\allsort{\phi}{\sf formula}{s}\allsort{\pi}{\sf proof}{s} \Pi^s
(\quo{\emptyset\vdash^s\unquo{\phi}},\pi)\implies \exsort{\mu}{\sf proof}{u}
\Pi^u(\quo{\emptyset\vdash^u\unquo{\Rel(\phi)}},\mu)\ea.$$ This proof 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.


\section{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\footnote{For the notions idealist and nominalist in
  the context of automated theorem proving see \cite{Pelletier91}.} translate
the theorems {\em and\/} the proofs in their own formalism. The proposed
framework allows easily to integrate existing systems in the \qed\ system.

\comment{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.}

%\input{bib.macros}
%\bibliography{bib}
%\bibliographystyle{plain}
\newcommand{\newblock}{}
\newcommand{\AI}{Artificial Intelligence}
\newcommand{\CADE}{{CADE}}
\newcommand{\GWAI}{{GWAI}}
\newcommand{\ECAI}{{ECAI}}
\newcommand{\IJCAI}{{IJCAI}}
\newcommand{\KI}{{KI}}
\newcommand{\LPAR}{{LPAR}}
\newcommand{\JACM}{Journal of the ACM}
\newcommand{\JAR}{Journal of Automated Reasoning}
\newcommand{\JLC}{Journal of Logic and Computation}
\newcommand{\JSC}{Journal of Symbolic Computation}
\newcommand{\JSL}{Journal of Symbolic Logic}
\newcommand{\LNAI}{LNAI}
\newcommand{\LNCS}{LNCS}
\newcommand{\MATHANN}{Ma\-the\-ma\-ti\-sche An\-na\-len}
\newcommand{\MI}{Machine Intelligence}
\newcommand{\SR}{{SEKI R}eport}
\newcommand{\SWP}{{SEKI W}orking {P}aper}

\newcommand{\PROC}{{Proceedings}}
\newcommand{\fc}{\ifgerman{im Druck}\else{forthcoming}\fi}
\newcommand{\VerlagNH}{{North-Holland Publishing Company}}
\newcommand{\VerlagReidel}{D.~Reidel Publishing Company}
\def\clam{{\rm CL\kern-.36em\raise.39ex\hbox{\sc a}\kern-.15emM}}
\def\oyster{{\rm O\kern-.12em\raise.39ex\hbox{\sc y}\kern-.07emS
\kern-.39em\raise.39ex\hbox{\sc t}\kern-.15em\hbox{\sc e}R}}
\def\qed{{\sf QED}}

\def\UdS{Universit\"at des Saarlandes}
\def\AddressUdS{Im Stadtwald, Saarbr\"ucken\Germany}
\def\SRI{SRI International}
\def\IRST{IRST (Istituto per la Ricerca Scientifica e Tecnologica)}

\def\mkrp{{\sc mkrp}}
\def\keim{{KEIM}}
\def\post{\mbox{$\cal POST$}}
\def\omegamkrp{\mbox{$\Omega$-\mkrp}}
\def\nUMBER{\ifgerman{Nummer}\else{number}\fi}
\def\NUMBER{\ifgerman{Nummer}\else{Number}\fi}
\def\EDITION{\ifgerman{Auflage}\else{edition}\fi}
\def\EDITOR{\ifgerman{Hrsg.}\else{ed.}\fi}
\def\EDITORS{\ifgerman{Hrsg.}\else{eds.}\fi}
\def\CHAPTER{\ifgerman{Kapitel\ }\else{chapter\ }\fi}
\def\TECHNICALREPORT{\ifgerman{Technischer Bericht}\else{technical report}\fi}
\def\technicalreport{\ifgerman{Technischer Bericht}\else{technical report}\fi}
\def\VOLUME{\ifgerman{Band\ }\else{Volume\ }\fi}
\def\PAGE{\ifgerman{Seite\ }\else{page\ }\fi}
\def\PAGES{\ifgerman{Seiten\ }\else{pages\ }\fi}
\def\AND{\ifgerman{und\ }\else{and\ }\fi}
\def\PHD{\ifgerman{Dissertation}\else{PhD thesis}\fi}
\def\KOMMAAND{\ifgerman{ }\else{,\ }\fi}
\def\EDITOR{\ifgerman{Herausgeber}\else{editor}\fi}
\def\EDITORS{\ifgerman{Herausgeber}\else{editors}\fi}
\def\vOLUME{\ifgerman{Band}\else{volume}\fi}
\def\VOLUME{\ifgerman{Band}\else{Volume}\fi}
\def\OF{\ifgerman{in}\else{of}\fi}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Laender %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\GERMANY}{\ifgerman{}\else{, Germany}\fi}
\newcommand{\Germany}{\GERMANY}
\def\CALIFORNIA{\ifgerman{Kalifornien}\else{California}\fi}
\def\FRANCE{\ifgerman{Frankreich}\else{France}\fi}
\def\ITALY{\ifgerman{Italien}\else{Italy}\fi}
\def\NETHERLANDS{\ifgerman{Niederlande}\else{The Netherlands}\fi}
\def\NEUSEELAND{\ifgerman{Neuseeland}\else{New Zealand}\fi}
\def\RUSSIA{\ifgerman{Ru{\ss}land}\else{Russia}\fi}
\def\SCHWEIZ{\ifgerman{Schweiz}\else{Switzerland}\fi}
\def\SWEDEN{\ifgerman{Schweden}\else{Sweden}\fi}
\def\UK{\ifgerman{Gro{\ss}britannien}\else{United Kingdom}\fi}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Monate  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\JANUARY{\ifgerman{Januar}\else{January}\fi\ }
\def\FEBRUARY{\ifgerman{Februar}\else{February}\fi\ }
\def\MARCH{\ifgerman{M\"arz}\else{March}\fi\ }
\def\APRIL{April}
\def\MAY{\ifgerman{Mai}\else{May}\fi\ }
\def\JUNE{\ifgerman{Juni}\else{June}\fi\ }
\def\JULY{\ifgerman{Juli}\else{July}\fi\ }
\def\AUGUST{August}
\def\SEPTEMBER{September}
\def\OCTOBER{\ifgerman{Oktober}\else{October}\fi\ }
\def\NOVEMBER{November}
\def\DECEMBER{\ifgerman{Dezember}\else{December}\fi\ }
\def\TOGETHER{\ifgerman{zusammen mit}\else{together with}\fi\ }
\begin{thebibliography}{1}

\bibitem{QED94}
Anonymous.
\newblock The \qed\ manifesto.
\newblock In Alan Bundy, editor, {\em \PROC\ of the 12th \CADE}, pages
  238--251, Nancy, \FRANCE, 1994. Springer Verlag, Berlin\Germany.
\newblock \LNAI\ 814.

\bibitem{Barwise94}
Jon Barwise and John Etchemendy.
\newblock {\em Hyperproof}.
\newblock {\sc csli} Lecture Notes. Chicago University Press, Chicago, USA,
  1994.

\bibitem{Constable86}
R.L. Constable~et al.
\newblock {\em Implementing Mathematics with the Nuprl Proof Development
  System}.
\newblock Prentice Hall, Englewood Cliffs, New Jersey, USA, 1986.

\bibitem{Genesereth87}
Michael~R.\ Genesereth and Nils~J.\ Nilsson.
\newblock {\em Logical Foundations of Artificial Intelligence}.
\newblock Morgan Kaufmann, San Mateo, \CALIFORNIA, USA, 1987.

\bibitem{Gentzen35ab}
Gerhard Gentzen.
\newblock Untersuchungen {\"u}ber das logische {S}chlie{\ss}en {I} \& {II}.
\newblock {\em Mathematische Zeit\-schrift}, {\bf 39}:176--210, 572--595, 1935.

\bibitem{Huang94}
Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith,
  J{\"o}rn Richts, and J{\"o}rg Siekmann.
\newblock \omegamkrp: A proof development environment.
\newblock In Alan Bundy, editor, {\em \PROC\ of the 12th \CADE}, pages
  788--792, Nancy, 1994. Springer Verlag, Berlin\Germany.
\newblock \LNAI\ 814.

\bibitem{Kerber92}
Manfred Kerber and Axel Pr{\"a}cklein.
\newblock Tactics for the improvement of problem formulation in
  resolution-based theorem proving.
\newblock \SR\ SR-92-09, Fachbereich Informatik, \UdS, \AddressUdS, 1992.

\bibitem{Pelletier91}
Francis~Jeffry Pelletier.
\newblock The philosophy of automated theorem proving.
\newblock In John Mylopoulos and Ray Reiter, editors, {\em \PROC\ of the 12th
  \IJCAI}, pages 538--543, Sydney, 1991. Morgan Kaufmann, San Mateo,
  \CALIFORNIA, USA.

\bibitem{Rudnicki92}
Piotr Rudnicki.
\newblock An overview of the {M}izar project.
\newblock Bastaad, \SWEDEN, 1992.

\end{thebibliography}

\end{document}

