\documentclass[runningheads]{llncs}
\usepackage[all]{xypic}
\usepackage{latexsym,amssymb}
\raggedbottom
\def\Z{{\mathbb Z}}
\def\toolong{$\hspace{-3.2cm}$}
\begin{document}
\title{Formal proof sketches}
\author{Freek Wiedijk}
\institute{University of Nijmegen}
\maketitle
\begin{abstract}
We define the notion of {\em formal proof sketch\/}
for the mathematical language Mizar.
We show by examples that formal proof sketches are very close
to informal mathematical proofs.
We discuss some ways in which formal proof sketches might be used
to improve mathematical proof assistants.
\end{abstract}
\section{Introduction}
\subsection{Problem}
Large mathematical formalizations are often difficult to understand.
They generally consist of several files, each containing a
long series of definitions and lemmas, with for each lemma a proof which
is a maze of steps.
As such, they are like large computer programs, which consist
of several files, each containing a long series of declarations
and functions,
with for each function an implementation
which is a maze of statements.
However the analogy is not perfect.
It is much easier to follow the steps through the
implementation of a program
than to follow the steps through the formalization of a theorem.
There are two levels on which it is difficult to understand
a large mathematical formalization.
It is difficult to understand the overall
structure of the formalization, i.e., to know what are the
important definitions and lemmas and in which files to find them.
And it is difficult to find one's way through the formal proof of
a lemma, i.e., to understand what the structure of that proof is.
In this note we address this second difficulty.
Something that makes a formalization easier to understand,
does not necessarily make it easier to create.
The approach presented in this note makes it easier to read
a mathematical formalization, but it will not make it easier to
write one.
This means that the representation of proofs that this note
proposes are {\em not\/} meant to be a `better way' for writing a formal proof.
A representation that can be checked by machine is much
more involved than the representation that we study here,
and it will be as difficult to write as ever.
In other words, our work is on right hand side of the
following diagram:\vspace{-6pt}
$$
\xymatrix@C=4em{
\ar@(dr,l)[rrd]|-{\txt{\em formalizing\/}} && && \\
&& *++[F]\txt{formalization}\ar@(r,dl)[rru]|-{\txt{\em presenting\/}} &&
}
\medskip
$$
and it is not especially relevant for the left hand side.
Here are some of the main ways to present
a formalization in such a way
that it becomes easier to understand for a human:
\begin{itemize}
\item {\em Removing the proofs.}
For instance in the Coq system one can generate a so-called
`\verb|.g|' file, which is just the Coq input script with the proofs removed.
Likewise, in the Mizar system one generates so-called `abstracts',
again just the formalizations with all proofs removed.
\item {\em Rendering the formulas with mathematical symbols.}
For instance in the prover interface Proof General one
can use the X-Symbols feature of emacs, showing mathematical symbols
instead of ASCII strings.
In a similar approach, the Theorema system uses the Mathematica front-end to
present its formulas in mathematical style.
Some systems (like Agda and NuPRL) even have a full-fledged structure
editor that displays mathematical formulas in a structural way.
\item {\em Generating natural language text from the formalization.}
\item {\em Merging natural language text with the formalization in the
spirit of `literate programming'.}
\end{itemize}
Generally the problem with a formal proof is that it is
big (because the steps are small), and that one looses grip on the whole
because of this.
The last two approaches in this list tend to make a formalization even bigger.
In contrast with this we believe that to make a formalization accessible, one
has to make it smaller.
Many people think that in order to make a formalization easier to
understand, one has to transform it.
However this means that one creates distance between the formalization
and its presentation.
This can be a problem if we
add a third arrow to the diagram:\vspace{-6pt}
$$
\xymatrix@C=4em{
\ar@(dr,l)[rrd]|-{\txt{\em formalizing\/}} && && \\
&& *++[F]\txt{formalization}\ar@{-}@(r,r)[d]\ar@(r,dl)[rru]|-{\txt{\em presenting\/}} && \\
&& *\txt{\em editing\/}\ar@(l,l)[u] &&
}
\smallskip
$$
To be able to successfully edit a formalization, one has to
look at the presentation
(in order to be able to understand it),
but one also has to work in the underlying formalization itself
(because that is where things really happen).
If those two versions of the proof
differ too much, then the presentation does not help.
In that case, for a user who just understands the presentation,
the formalization
will be a static thing (because it cannot easily be modified)
instead of a `living proof'.
Therefore, we claim that the presentation should be as close to the
original formalization as possible.
In this paper we are looking for a presentation of a formalization
which is:
\begin{itemize}
\item {\em Shorter than the full formalization}, in the sense that
the most trivial details of the proof are not shown.
\item {\em Close to the full formalization}, in the sense that it is
easy to go back and forth between the two and to find matching locations in
both versions.
\end{itemize}
\subsection{Approach}
We introduce the notion of {\em formal proof sketch}.
A formal proof sketch is a notion related to the
mathematical language Mizar \cite{muz:93,wie:99:1}.
A formal proof sketch is a completely correct Mizar text, apart from
errors \verb|*4| and \verb|*1|.
These errors say that reasoning steps are not justified.
(Therefore, in a formal proof sketch
one can leave out all labels and justifications to make it more readable.)
A formal proof sketch falls between a formalization with
full proofs and an abstract with all proofs removed.
In a formal proof sketch some of the steps, as well as
the connections between the steps, have been removed.
A formal proof sketch is called {\em correct}, if one can add labels,
justifications and steps to it, in such a way that one gets a correct
Mizar formalization.
We call such a formalization the {\em completion\/} of the sketch.
Being correct is a semi-decidable notion.
If a sketch is correct one can show so by exhibiting a completion,
but if it is not, there is no guaranteed way to find out.
The observation of this note is that, given an informal natural language proof,
it is possible to write a correct formal proof sketch which is
linguistically very close to it.
In this note we will show two examples of this,
one in Section~\ref{sketch}, and one in Section~\ref{geomath}.
The process of formalizing an informal proof, and then presenting it through
a formal proof sketch, is
represented in the following diagram:
$$
\xymatrix{
*+\txt{informal statement\strut\\of theorem}\ar[d] &&& *+\txt{formal\\`abstract'}\\
*+[F]\txt{informal\\English proof}\ar[r]\ar@{.>}@/_1pc/[rrd]|-{\txt{\em formalizing\/}} &
*+[F--]\txt{formal\\proof sketch}\ar[rd]\ar@{--}[rr] &&
*+[F--]\txt{formal\\proof sketch}\ar[u]\\
&& *+[F]\txt{full\\formalization}\ar@/_1pc/[ru]!D|(.72){\txt{\em presenting\/}} &
}
\medskip
$$
For our first example the informal English proof and the formal proof sketch
are in Section~\ref{sketch}, while the full formalization is in
Section~\ref{full}.
For our second example, all three representations are next to each
other in Section~\ref{geomath}.
When completing a formal proof sketch into a full formalization,
sometimes one modifies the structure of the proof a bit.
This makes the formal proof sketch change too: hence the two
boxes for the formal proof sketch in the diagram.
We show an example of such a change in Section~\ref{geomath}.
\subsection{Related Work}
Rob Nederpelt
has a language called {\em weak type theory\/} or WTT \cite{ned:01},
that is meant to formalize mathematics in a way that is closer to natural
language than currently is the case in formal systems.
It is basically a formalization language like the others, but
without any proofs.
We are not convinced that having a separate language for this purpose
is desirable or even necessary.
To us Mizar abstracts (which also are formalizations without
proofs) are at least as readable as Nederpelt's WTT formalizations.
Paul Jackson told us that in the NuPRL community it is customary
to present proofs by showing the statements from the goals interleaved
with the tactics from the proof script.
To improve the presentation one then `groups' the tactics and gets
a much shorter presentation.
This is very similar to what we describe in this note.
The main difference is that in the case of NuPRL it is not
easy to write the proof sketch {\em before\/} working out the
full formalization.
In the case of Mizar it is.
Another difference is that in the case of Mizar the result is
much closer to that informal English version of the proof than
in NuPRL.
\subsection{Contribution}
Our contribution is twofold:
\begin{itemize}
\item We note that it is possible to get very close to informal
mathematical English using Mizar syntax, as long as one does not
mind omitting justifications for the steps.
\item We note that one can give a formal definition of a notion called
{\em formal proof sketch\/} for this.
(Note that in this note we do not give this formal definition,
but it does exist.)
\end{itemize}
\subsection{Outline}
The plan of the paper:
in Section~\ref{sketch} we present
an informal English proof with its formal proof sketch approximation.
In Section~\ref{typography} we discuss how the typographical differences
obfuscate
the similarity of those two versions of the proof.
In Section~\ref{full} we give the full Mizar formalization of the proof.
In Section~\ref{meson} and Section~\ref{algebra} we study
whether we can make the full formalization be closer to the
formal proof sketch by using a complete first order prover
(instead of the restricted inference engine of Mizar)
and by using computer algebra.
In Sections~\ref{dual} and \ref{folding} we
look at possibilities of using formal proof sketches
in the interface of a proof assistant.
Finally, in Section~\ref{geomath} we present a second example
of a formal proof sketch.
\section{A formal proof sketch}\label{sketch}
In Hardy and Wright's {\em An Introduction to the Theory of Numbers\/}
\cite{har:wri:60},
the irrationality of $\sqrt{2}$ is proved on pp.~39--40 in the following
way:
\begin{quote}
{\sc Theorem 43 (Pythagoras' theorem).} {\em $\sqrt{2}$ is irrational.}
\medskip
The traditional proof ascribed to Pythagoras runs
as follows. If $\sqrt{2}$ is rational, then the equation
$$a^2 = 2b^2 \eqno{(4.3.1)}$$
is soluble in integers $a$, $b$ with $(a,b) = 1$. Hence $a^2$ is even, and there%-
fore $a$ is even. If $a = 2c$, then $4c^2 = 2b^2$, $2c^2 = b^2$, and $b$ is also even,
contrary to the hypothesis that $(a,b) = 1$.
$\hfill\Box$
\end{quote}
If one writes this text in Mizar syntax, it turns out to be almost identical:
\begin{center}
\begin{tabular}{ll}
\verb|theorem Th43: sqrt 2 is irrational| & \\
\verb|proof| & \\
\verb| assume sqrt 2 is rational;| & \\
\verb| consider a,b such that| & \\
\verb|4_3_1: a^2 = 2*b^2 and| & \\
\verb| a,b are_relative_prime;| & \rlap{\quad$\mathord{\leftarrow}1$} \\
\verb| a^2 is even;| & \rlap{\quad$\mathord{\leftarrow}2$} \\
\verb| a is even;| & \rlap{\quad$\mathord{\leftarrow}3$} \\
\verb| consider c such that a = 2*c;| & \rlap{\quad$\mathord{\leftarrow}4$} \\
\verb| 4*c^2 = 2*b^2;| & \rlap{\quad$\mathord{\leftarrow}5$} \\
\verb| 2*c^2 = b^2;| & \rlap{\quad$\mathord{\leftarrow}6$} \\
\verb| b is even;| & \rlap{\quad$\mathord{\leftarrow}7$} \\
\verb| thus contradiction;| & \rlap{\quad$\mathord{\leftarrow}8$} \\
\verb|end;|
\end{tabular}
\end{center}
With an appropriate \verb|environ| header, this is correct
Mizar, except for eight `reasoning errors', as indicated by the numbered
arrows.
We call such a Mizar text that only has reasoning errors a
formal proof sketch.
\section{Comparing typography}\label{typography}
The informal proof and the corresponding formal proof sketch are more similar
than might seem at a first glance,
because one of them is printed as natural
language in a text font, while the
other is printed with one step per line in a typewriter font.
To stress the similarity of the texts, here they are next to each other:
\begin{center}
\begin{tabular}{rcl}
{\sc Theorem 43\rlap{.}} & $\quad$ & {\verb|theorem Th43:|} \\
{\em $\sqrt{2}$ is irrational\rlap{.}} && {\verb| sqrt 2 is irrational|} \\
&& {\verb|proof|} \\
If $\sqrt{2}$ is rational\rlap{,} && {\verb| assume sqrt 2 is rational;|} \\
then the equation && {\verb| consider a,b such that|} \\
{(4.3.1)}\quad $a^2 = 2b^2$\quad is soluble in && {\verb|4_3_1: a^2 = 2*b^2 and|} \\
integers $a$, $b$ with $(a,b) = 1$\rlap{.} && {\verb|A1: a,b are_relative_prime;|} \\
Hence $a^2$ is even\rlap{,} && {\verb| a^2 is even;|} \\
and therefore $a$ is even\rlap{.} && {\verb| a is even;|} \\
If $a = 2c$\rlap{,} && {\verb| consider c such that a = 2*c;|} \\
then $4c^2 = 2b^2$\rlap{,} && {\verb| 4*c^2 = 2*b^2;|} \\
$2c^2 = b^2$\rlap{,} && {\verb| 2*c^2 = b^2;|} \\
and $b$ is also even\rlap{,} && {\verb| b is even;|} \\
contrary to the hypothesis && {\verb| thus contradiction|} \\
that $(a,b) = 1$\rlap{.} && {\verb| by A1;|} \\
$\Box\!$ && {\verb|end;|}
\end{tabular}
\end{center}
On the left there is the Hardy \& Wright original, on the
right is the formal proof sketch translation.
%
We also can write the `Mizar' of the formal proof sketch in `natural
language typography' like this:
\begin{quote}
{\sc Theorem}\enskip {\em $\sqrt 2$ is irrational.}
\medskip
{\sc Proof}\enskip
Assume
$\sqrt 2$ is rational.
Then consider $a,b$ such that
$$a^2 = 2 b^2$$ and
$a,b$ are relative prime.
$a^2$ is even.
Then $a$ is even.
Then consider $c$ such that
$a = 2 c$.
$4 c^2 = 2 b^2$.
Then $2 c^2 = b^2$.
Then $b$ is even.
Hence contradiction.
$\hfill\Box$
\end{quote}
This text exactly follows the Mizar syntax.
The only changes are that the formulas have been written
with symbols and that the capitalization and punctuation has
been modified slightly.
\section{The full proof}\label{full}
If we `fill out' the formal proof sketch from Section~\ref{sketch}
to a full Mizar article, we get:
\begin{quote}
\underbar{\tt{theorem Th43: sqrt 2 is irrational}} \\
\underbar{\tt{proof}} \\
\verb| |\underbar{\tt{assume sqrt 2 is rational;}} \\
\verb| then |\underbar{\tt{consider a,b such that}} \\
\verb|B1: b <> 0 and| \\
\verb|B2: sqrt 2 = a/b and| \\
\verb|A1: |\underbar{\tt{a,b are\_relative\_prime}}\verb| by Def1|\underbar{\tt{;}} \\
\verb|B3: b^2 <> 0 by B1,SQUARE_1:73;| \\
\verb| 2 = (a/b)^2 by B2,SQUARE_1:def 4| \\
\verb| .= a^2/b^2 by SQUARE_1:69;| \\
\verb| then| \\
\underbar{\tt{4\_3\_1: a\^{}2 = 2*b\^{}2}}\verb| by B3,REAL_1:43|\underbar{\tt{;}} \\
\verb| a^2 is even by 4_3_1,ABIAN:def 1;| \\
\verb| then| \\
\verb|A2: |\underbar{\tt{a is even}}\verb| by PYTHTRIP:2|\underbar{\tt{;}} \\
\verb| then |\underbar{\tt{consider c such that}} \\
\verb|A3: |\underbar{\tt{a = 2*c}}\verb| by ABIAN:def 1|\underbar{\tt{;}} \\
\verb|B4: |\underbar{\tt{4*c\^{}2 =}}\verb| (2*2)*c^2| \\
\verb| .= 2^2*c^2 by SQUARE_1:def 3| \\
\verb| .= |\underbar{\tt{2*b\^{}2}}\verb| by A3,4_3_1,SQUARE_1:68|\underbar{\tt{;}} \\
\verb| 2*(2*c^2) = (2*2)*c^2 by AXIOMS:16| \\
\verb| .= 2*b^2 by B4;| \\
\verb| then |\underbar{\tt{2*c\^{}2 = b\^{}2}}\verb| by REAL_1:9|\underbar{\tt{;}} \\
\verb| then b^2 is even by ABIAN:def 1;| \\
\verb| then |\underbar{\tt{b is even}}\verb| by PYTHTRIP:2|\underbar{\tt{;}} \\
\verb| then 2 divides a & 2 divides b by A2,Def2;| \\
\verb| then| \\
\verb|B5: 2 divides a gcd b by INT_2:33;| \\
\verb| a gcd b = 1 by A1,INT_2:def 4;| \\
\verb| |\underbar{\tt{hence contradiction}}\verb| by B5,INT_2:17|\underbar{\tt{;}} \\
\underbar{\tt{end;}}
\end{quote}
In this, the formal proof sketch parts have been underlined.
This proof needs two `lemmas' (in the form of redefinitions)
that are not present in the Mizar library:
\begin{quote}
\begin{verbatim}
redefine attr x is rational means
:Def1: ex a,b st b <> 0 & x = a/b & a,b are_relative_prime;
\end{verbatim}
\end{quote}
and:
\begin{quote}
\begin{verbatim}
redefine attr a is even means
:Def2: 2 divides a;
\end{verbatim}
\end{quote}
\section{Bigger steps from a stronger first order prover}\label{meson}
One can show the relation between the full proof and the formal proof
sketch by studying relations between graphs.
We draw graphs in which the steps of a proof are represented by the
vertices, and
where justifications are represented by the edges.
The graph that we give here is not the graph of the
example (that one would be too big), but a simplified version of the upper
part of it.
The graph on the left corresponds to the full article.
The steps that are in the formal proof sketch as well,
have been put in boxes.
The graph on the right corresponds to the formal proof sketch.
The graph in the middle is an intermediate version: here the appropriate
connections have been left in.
These justifications are too `big' for Mizar to be verified.
If Mizar inferences would be allowed to be arbitrarily difficult
first order inferences, the article corresponding to this graph
would be correct Mizar.
$$
\xymatrix@=1.5em{
& *+[F]{a}\ar[d] & & &&
{a}\ar[d] & & &&
{a} & \\
& *+[F]{b}\ar[dl]\ar[d]\ar[dr] & & &&
{b}\ar@/_1pc/[ddd]\ar[dr] & & &&
{b} & \\
{c}\ar[d] & {d}\ar[d] & *+[F]{e}\ar[dl]\ar[ddd] &&
& & {e}\ar[ddl]\ar@/^1pc/[dddd] & &&
& {e} \\
{f}\ar[dr] & {g}\ar[d] & & &&
& & &&
& \\
& *+[F]{h}\ar[d] & & &&
{h}\ar[ddr] & & &&
{h} & \\
& {i}\ar[dr] & {j}\ar[d] & &&
& & &&
& \\
& & *+[F]{k} & &&
& {k} & &&
& {k}
}
$$
The Mizar text for the example that corresponds to the middle
graph is:
\begin{center}
\begin{tabular}{ll}
\verb|theorem Th43: sqrt 2 is irrational| & \\
\verb|proof| & \\
\verb| assume sqrt 2 is rational;| & \\
\verb| then consider a,b such that| & \\
\verb|4_3_1: a^2 = 2*b^2 and| & \\
\verb|A1: a,b are_relative_prime by Def1,SQUARE_1:73,| & \\
\verb| SQUARE_1:def 4,SQUARE_1:69,REAL_1:43;| & \rlap{\quad$\mathord{\leftarrow}1$} \\
\verb| a^2 is even by 4_3_1,ABIAN:def 1;| & \rlap{\quad$\mathord{\leftarrow}2$} \\
\verb| then| & \\
\verb|A2: a is even by PYTHTRIP:2;| & \rlap{\quad$\mathord{\leftarrow}3$} \\
\verb| then consider c such that| & \\
\verb|A3: a = 2*c by ABIAN:def 1;| & \rlap{\quad$\mathord{\leftarrow}4$} \\
\verb| 4*c^2 = 2*b^2 by A3,4_3_1,SQUARE_1:def 3,SQUARE_1:68;| & \rlap{\quad$\mathord{\leftarrow}5$} \\
\verb| then 2*c^2 = b^2 by AXIOMS:16,REAL_1:9;| & \rlap{\quad$\mathord{\leftarrow}6$} \\
\verb| then b is even by ABIAN:def 1,PYTHTRIP:2;| & \rlap{\quad$\mathord{\leftarrow}7$} \\
\verb| hence contradiction by A1,A2,ABIAN:def 1,INT_1:def 9,| & \\
\verb| INT_2:33,INT_2:def 4,INT_2:17;| & \rlap{\quad$\mathord{\leftarrow}8$} \\
\verb|end;|
\end{tabular}
\end{center}
The lists of references to theorems in the justifications
get quite long,
because the justifications of several steps have been `put together'.
In practice determining those lists is as much work as doing the
intermediate steps one-selves.
Therefore no-one would write a proof like this, even if Mizar could justify
arbitrarily big first order steps.
Still it is interesting to see how well a full first order prover can
do on these steps.
The HOL Light system by John Harrison \cite{har:00} implements a
full first order prover called \verb|MESON_TAC|.
We gave the first order problems corresponding to the eight inference
steps to this prover.
The steps in TPTP format were provided
to us by Josef Urban.
The result of this test was:
\begin{center}
\begin{tabular}{rcccrr}
&& $\quad\mbox{\em Mizar\/}\quad$ & {\em Meson\/} && \\
$\qquad 1\mathord{\rightarrow}$ && $-$ & $-$ && \\
$2\mathord{\rightarrow}$ && $+$ & $+$ & 61 & $\quad$1.49$\,${\em s} \\
$3\mathord{\rightarrow}$ && $+$ & $+$ & 20 & 0.14$\,${\em s} \\
$4\mathord{\rightarrow}$ && $+$ & $+$ & 142 & 1.02$\,${\em s}\\
$5\mathord{\rightarrow}$ && $-$ & $-$ && \\
$6\mathord{\rightarrow}$ && $-$ & $-$ && \\
$7\mathord{\rightarrow}$ && $-$ & $+$ & $\quad$18839 & 4.71$\,${\em s} \\
$8\mathord{\rightarrow}$ && $-$ & $-$ &&
\end{tabular}
\end{center}
The last two columns are number of inferences for the step
and the time it took to find those inferences.
For the steps for which HOL Light could not find a justification,
we let \verb|MESON_TAC| run for at least an hour on a 1$\,$GHz machine,
and we let it try at least ten million inferences.
Surprisingly, although the first order prover in HOL Light can {\em in theory\/}
do arbitrarily complicated first order problems, {\em in practice\/}
it does about as well as Mizar.
\section{Bigger steps from computer algebra}\label{algebra}
Most of the eight `problems' from the previous section do not
involve logical quantifiers, but are basically algebraic in character:
\begin{center}
\begin{tabular}{rrcl}
\llap{1$\rightarrow$\qquad}& $\displaystyle b\ne 0 \;\land\; \sqrt{2} = {a\over b}$ & $\;\vdash\;$ & $a^2 = 2 b^2$\\
\noalign{\smallskip}
\llap{2$\rightarrow$\qquad}& $b\in\Z \;\land\; a^2 = 2 b^2$ & $\;\vdash\;$ & $2\,|\,a^2$\\
\noalign{\smallskip}
\llap{3$\rightarrow$\qquad}& $a\in\Z \;\land\; 2\,|\,a^2$ & $\;\vdash\;$ & $2\,|\,a$\\
\noalign{\bigskip}
\llap{5$\rightarrow$\qquad}& $a^2 = 2 b^2 \;\land\; a = 2c$ & $\;\vdash\;$ & $4 c^2 = 2 b^2$\\
\noalign{\smallskip}
\llap{6$\rightarrow$\qquad}& $4 c^2 = 2 b^2$ & $\;\vdash\;$ & $2 c^2 = b^2$\\
\noalign{\smallskip}
\llap{7$\rightarrow$\qquad}& $b\in\Z \;\land\; c\in\Z \;\land\; 2 c^2 = b^2$ & $\;\vdash\;$ & $2\,|\,b$\\
\noalign{\smallskip}
\llap{8$\rightarrow$\qquad}& $(a,b) = 1 \;\land\; 2\,|\,a \;\land\; 2\,|\,b$ & $\;\vdash\;$ & $\bot$
\end{tabular}
\end{center}
The omitted fourth step (and the omitted part of the first step)
involves an existential quantifier.
It is not practical to use a first order reasoning tool to find
the steps to get from
$a^2 = 2b^2$
and
$a = 2c$
to
$4 c^2 = 2 b^2$.
This is a problem to be solved algorithmically, and not by searching.
To be able to be allowed steps like this in a formalization,
one would like to have
an algebraic decision procedure that knows about the notions in these
inferences.
If one had such a decision procedure,
one would be able to get closer to the formal
proof sketch.
\section{Hyperlinks between formal proof sketch and full formalization}\label{dual}
We will now turn to the question of how to integrate formal
proof sketches into an interface to make a formalization more accessible.
The simplest is to put two windows next to each other
in the interface:
one with the full formalization and one with the formal proof sketch.
In such an interface it would be nice if those two windows were `synchronized'
in such a way that when scrolling one, the corresponding
part of the other always appear next to it.
Alternatively one could have `hyperlinks' between the two representations
to easily go from a position in the one to the corresponding position in the
other.
In such an interface the underlined parts of the proof from
Section~\ref{full} would
be links to the corresponding place in the abstract.
One would like to have a tool to {\em extract\/} a formal proof sketch
from a Mizar formalization.
For that one would like to have some syntax in the Mizar language
to `mark' the steps that
should appear in the formal proof sketch.
Such a tool has to be a bit subtle, because it should also extract all
constructions like `\verb|let|', `\verb|consider|' and `\verb|set|'
which introduce variables that are used in the extracted
steps in the formal proof sketch.
\section{Folding in the interface}\label{folding}
Alternatively one could have only one window, with a `folding interface'.
On request of the user some parts of the full formalization might
be `hidden', to make the text look more like the formal proof sketch,
and therefore easier to understand.
The naive way to do this, is to complete the formal proof sketch
with {\em subproofs\/} and then hide the subproofs on request.
That way the proof will look like:
%\def\foldedproof#1{$\spadesuit_{#1}$}
\def\foldedproof#1{$\,\ldots\,$}
\begin{quote}
\verb|theorem Th43:|\\
\verb| sqrt 2 is irrational|\\
\verb|proof|\\
\verb| assume|\\
\verb|C1: sqrt 2 is rational;|\\
\verb| |\foldedproof{1}\verb|; then consider a,b such that|\\
\verb|4_3_1: a^2 = 2*b^2 and|\\
\verb|A1: a,b are_relative_prime;|\\
\verb| a^2 is even by 4_3_1,ABIAN:def 1;|\\
\verb| then|\\
\verb|A2: a is even by PYTHTRIP:2;|\\
\verb| then consider c such that|\\
\verb|A3: a = 2*c by ABIAN:def 1;|\\
\verb|B4: 4*c^2 = 2*b^2 |\foldedproof{2}\verb|;|\\
\verb|C3: 2*c^2 = b^2 |\foldedproof{3}\verb|;|\\
\verb|C4: b is even |\foldedproof{4}\verb|;|\\
\verb| thus contradiction |\foldedproof{5}\verb|;|\\
\verb|end;|
\end{quote}
Here the ellipsis symbols `$\ldots$' represent hidden subproofs
of on average six lines each.
The disadvantage of this approach is that
the full formalization will not be `ordinary' Mizar.
In a normal Mizar article subproofs occur much less often
than here.
A more natural way for Mizar to fold parts of a proof is to fold away steps.
That way one gets:
%\def\foldedline#1{$\clubsuit_{#1}$}
\def\foldedline#1{$\,\ldots\,$}
\begin{quote}
\verb|theorem Th43: sqrt 2 is irrational| \\
\verb|proof| \\
\verb| assume sqrt 2 is rational;| \\
\verb| then consider a,b such that| \\
\verb| |\foldedline{1}\verb| and |\foldedline{2}\verb| and| \\
\verb|A1: a,b are_relative_prime by Def1;| \\
\verb| |\foldedline{3}\verb|; |\foldedline{4}\verb| |\foldedline{5}\verb|; then| \\
\verb|4_3_1: a^2 = 2*b^2 by B3,REAL_1:43;| \\
\verb| a^2 is even by 4_3_1,ABIAN:def 1;| \\
\verb| then| \\
\verb|A2: a is even by PYTHTRIP:2;| \\
\verb| then consider c such that| \\
\verb|A3: a = 2*c by ABIAN:def 1;| \\
\verb|B4: 4*c^2 |\foldedline{6}\verb| |\foldedline{7}\verb| .= 2*b^2 by A3,4_3_1,SQUARE_1:68;| \\
\verb| |\foldedline{8}\verb| |\foldedline{9}\verb|; then 2*c^2 = b^2 by REAL_1:9;| \\
\verb| |\foldedline{{10}}\verb|; then b is even by PYTHTRIP:2;| \\
\verb| |\foldedline{{11}}\verb|; |\foldedline{{12}}\verb|; |\foldedline{{13}}%
\verb|; hence contradiction by B5,INT_2:17;| \\
\verb|end;|
\end{quote}
Note that this still is basically the same structure
as the formal proof sketch,
although it looks much `messier'.
In this version the folded parts are all the same size, one line long:
\def\foldedline#1{$\,\ldots_{#1}$}
\begingroup
\begin{eqnarray*}
\mbox{\foldedline{\ 1}} & \equiv\, & \verb|B1: b <> 0| \\
\mbox{\foldedline{\ 2}} & \equiv\, & \verb|B2: sqrt 2 = a/b| \\
\mbox{\foldedline{\ 3}} & \equiv\, & \verb|B3: b^2 <> 0 by B1,SQUARE_1:73| \\
\mbox{\foldedline{\ 4}} & \equiv\, & \verb|2 = (a/b)^2 by B2,SQUARE_1:def 4| \\
\mbox{\foldedline{\ 5}} & \equiv\, & \verb| .= a^2/b^2 by SQUARE_1:69| \\
\mbox{\foldedline{\ 6}} & \equiv\, & \verb| = (2*2)*c^2| \\
\mbox{\foldedline{\ 7}} & \equiv\, & \verb| .= 2^2*c^2 by SQUARE_1:def 3| \\
\mbox{\foldedline{\ 8}} & \equiv\, & \verb|2*(2*c^2) = (2*2)*c^2 by AXIOMS:16| \\
\mbox{\foldedline{\ 9}} & \equiv\, & \verb| .= 2*b^2 by B4| \\
\mbox{\foldedline{{10}}} & \equiv\, & \verb|then b^2 is even by ABIAN:def 1| \\
\mbox{\foldedline{{11}}} & \equiv\, & \verb|then 2 divides a & 2 divides b by A2,Def2| \\
\mbox{\foldedline{{12}}} & \equiv\, & \verb|then B5: 2 divides a gcd b by INT_2:33| \\
\mbox{\foldedline{{13}}} & \equiv\, & \verb|a gcd b = 1 by A1,INT_2:def 4|
\end{eqnarray*}
\endgroup
A third way of folding is to keep the proof the way it is, but
to hide all labels and justifications:
\begin{quote}
\begin{verbatim}
theorem Th43: sqrt 2 is irrational
proof
assume sqrt 2 is rational;
consider a,b such that
b <> 0 and
sqrt 2 = a/b and
a,b are_relative_prime;
b^2 <> 0;
2 = (a/b)^2
.= a^2/b^2;
a^2 = 2*b^2;
a^2 is even;
a is even;
consider c such that
a = 2*c;
4*c^2 = (2*2)*c^2
.= 2^2*c^2
.= 2*b^2;
2*(2*c^2) = (2*2)*c^2
.= 2*b^2;
2*c^2 = b^2;
b^2 is even;
b is even;
2 divides a & 2 divides b;
2 divides a gcd b;
a gcd b = 1;
thus contradiction;
end;
\end{verbatim}
\end{quote}
This is rather long, but it is much more readable than the formalization with
the labels and justifications shown.
\section{Another example}\label{geomath}
We will now present a second example, taken from the linear algebra
part of a textbook \cite{gal:01}.
This textbook currently has not been published on paper yet,
but it is available on the WWW.
On p.~16, we find the lemma:
\begin{quote}
{\bf Lemma 2.1.}
{\em
Given a linearly independent family $(u_i)_{i\in I}$ of elements of a vector space $E$, if
$v\in E$ is not a linear combination of $(u_i)_{i\in I}$, then the family $(u_i)_{i\in I}\cup_k (v)$ obtained by adding
$v$ to the family $(u_i)_{i\in I}$ is linearly independent (where $k\not\in I$).
}
\medskip
{\em Proof.}
Assume that $\mu v + \sum_{i\in I} \lambda_i u_i = 0$, for any family $(\lambda_i)_{i\in I}$ of scalars in $K$. If $\mu\ne 0$,
then $\mu$ has an inverse (because $K$ is a field), and thus we have $v = -\sum_{i\in I} (\mu^{-1}\lambda_i) u_i$, showing
that $v$ is a linear combination of $(u_i)_{i\in I}$ and contradicting the hypothesis. Thus, $\mu = 0$. But
then, we have $\sum_{i\in I} \lambda_i u_i = 0$, and since the family $(u_i)_{i\in I}$ is linearly independent, we have
$\lambda_i = 0$ for all $i\in I$.
$\hfill\Box$
\end{quote}
The formal proof sketch that corresponds to this is:
\begin{quote}
\begin{verbatim}
theorem Lem21:
u is linearly-independent & not v in Lin(u) implies
u \/ {v} is linearly-independent
proof
assume u is linearly-independent & not v in Lin(u);
assume u \/ {v} is linearly-dependent;
consider m being Element of K,
l being Linear_Combination of u such that
m*v + Sum(l) = 0.E;
now
assume m <> 0.K;
v = -m"*Sum(l);
v in Lin(u);
thus contradiction;
end;
m = 0.K;
Sum(l) = 0.E;
Carrier(l) = {};
thus contradiction;
end;
\end{verbatim}
\end{quote}
To show the similarity between the two, here is the informal
English version next to the formulas from the formal
proof sketch:
\begin{center}
\begin{tabular}{rcl}
Assume that $\mu v + \sum_{i\in I} \lambda_i u_i = 0$\rlap{,}
&$\quad$& {\tt m*v + Sum(l) = 0.E}\\
for any family $(\lambda_i)_{i\in I}$ of scalars in $K$\rlap{.}\\
%&& {\tt l being }{\dots}\\
If $\mu\ne 0$\rlap{,}
&& {\tt m <> 0.K}\\
then $\mu$ has an inverse (because $K$ is a field)\rlap{,}\\
and thus we have
$v = -\sum_{i\in I} (\mu^{-1}\lambda_i) u_i$\rlap{,}
&& {\tt v = -m"*Sum(l)}\\
showing that $v$ is a linear combination of $(u_i)_{i\in I}$
&& {\tt v in Lin(u)}\\
and contradicting the hypothesis\rlap{.}
&& {\tt contradiction}\\
Thus, $\mu = 0$
&& {\tt m = 0.K}\\
But then, we have $\sum_{i\in I} \lambda_i u_i = 0$\rlap{,}
&& {\tt Sum(l) = 0.E}\\
and since the family $(u_i)_{i\in I}$ is linearly independent\rlap{,}\\
we have
$\lambda_i = 0$ for all $i\in I$\rlap{.}
&& {\tt Carrier(l) = }\verb|{}|
\end{tabular}
\end{center}
Here is the full formalization that one gets by completing the formal
proof sketch:
\begin{quote}
\verb|theorem|\\
\verb| u is linearly-independent & not v in Lin(u) implies|\\
\verb| u \/ {v} is linearly-independent|\\
\verb|proof|\\
\verb| assume|\\
\verb|A1: u is linearly-independent & not v in Lin(u);|\\
\verb| |\underbar{\tt{assume u {\char92}/ {\char123}v{\char125} is linearly-dependent;}}\\
\verb| then consider l' being Linear_Combination of u \/ {v}|\\
\verb| such that|\\
\verb|A2: Sum(l') = 0.E & Carrier(l') <> {} by VECTSP_7:def 1;|\\
\verb| consider m' being Linear_Combination of {v},|\\
\verb| l being Linear_Combination of u such that|\\
\verb|A3: l' = m' + l by Th2;|\\
\verb| set m = m'.v;|\\
\verb|A4: m*v + Sum(l) = Sum(m') + Sum(l) by VECTSP_6:43|\\
\verb| .= 0.E by A2,A3,VECTSP_6:77;|\\
\verb| now|\\
\verb| assume|\\
\verb|A5: m <> 0.K;|\\
\verb| m*v = -Sum(l) by A4,RLVECT_1:def 10;|\\
\verb| then v = m"*(-Sum(l)) by A5,VECTSP_1:67|\\
\verb| .= -m"*Sum(l) by VECTSP_1:69;|\\
\verb| then|\\
\verb|A6: v = (-m")*Sum(l) by VECTSP_1:68;|\\
\verb| Sum(l) in Lin(u) by VECTSP_7:12;|\\
\verb| |\underbar{\tt{then v in Lin(u) by A6,VECTSP\_4:29;}}\\
\verb| hence contradiction by A1;|\\
\verb| end;|\\
\verb| then|\\
\underbar{\tt{A7: m = 0.K;}}\\
\verb| Sum(l) = 0.E + Sum(l) by VECTSP_1:7|\\
\verb| .= 0.E by A4,A7,VECTSP_1:59;|\\
\verb| then|\\
\verb|A8: Carrier(l) = {} by A1,VECTSP_7:def 1;|\\
\verb| now|\\
\verb| let x be set;|\\
\verb|A9: Carrier(m') c= {v} by VECTSP_6:def 7;|\\
\verb| not v in Carrier(m') by A7,VECTSP_6:20;|\\
\verb| hence not x in Carrier(m') by A9,TARSKI:def 1;|\\
\verb| end;|\\
\verb| then Carrier(m') = {} by BOOLE:def 1;|\\
\verb| then Carrier(l) \/ Carrier(m') = {} by A8;|\\
\verb| then Carrier(l') c= {} by A3,VECTSP_6:51;|\\
\verb| hence contradiction by A2,BOOLE:30;|\\
\verb|end;|
\end{quote}
The steps that have been underlined in this proof can be
omitted (as pointed out by the \verb|relinfer| tool).
When one omits them, and then again extracts the formal
proof sketch, one gets:
\begin{quote}
\verb|theorem Lem21:|\\
\verb| u is linearly-independent & not v in Lin(u) implies|\\
\verb| u \/ {v} is linearly-independent|\\
\verb|proof|\\
\verb| assume u is linearly-independent & not v in Lin(u);|\\
\verb| given l' being Linear_Combination of u \/ {v} such that|\\
\verb| Sum(l') = 0.E & Carrier(l') <> {};|\\
\verb| consider m' being Linear_Combination of {v},|\\
\verb| l being Linear_Combination of u such that|\\
\verb| l' = m' + l;|\\
\verb| set m = m'.v;|\\
\verb| m*v + Sum(l) = 0.E;|\\
\verb| now|\\
\verb| assume m <> 0.K;|\\
\verb| v = -m"*Sum(l);|\\
\verb| thus contradiction;|\\
\verb| end;|\\
\verb| Sum(l) = 0.E;|\\
\verb| Carrier(l) = {};|\\
\verb| thus contradiction;|\\
\verb|end;|
\end{quote}
This is clearly less readable than the first
version of the formal proof sketch.
When one does the experiment with HOL Light's \verb|MESON_TAC|
for this example,
one discovers that HOL Light is not even able to do the steps
that Mizar can do.
The reason for this is that the typing of the objects in this
proof is quite involved, and it is too complicated
to discover the necessary deductions
to get the necessary typing judgments by first order proof search.
The two steps in this example which are
of the `algebraic problem' type, are:
\begin{eqnarray*}
\mu v + \sum\lambda = 0 \;\land\; \mu\ne 0 &\;\vdash\;& v = -\mu^{-1}\sum\lambda\\
\mu v + \sum\lambda = 0 \;\land\; \mu = 0 &\;\vdash\;& \sum\lambda = 0
\end{eqnarray*}
These may seem trivial, but Mizar is not powerful enough to do either one
of them in one step.
Also, note that
these are not algebraic problems about numbers, but about abstract
entities like elements of an arbitrary field, vectors in an arbitrary
vector space, and `linear combinations of vectors'.
\section{Conclusion}
\subsection{Discussion}
We presented the notion of {\em formal proof sketch\/} and
looked at some possibilities to use this to make a better
interface for presentations of formalizations.
The main things that one should consider are:
\begin{itemize}
\item The dual window approach from Section~\ref{dual}.
\item The third variant of the folding interface from Section~\ref{folding},
where the labels and justifications can be hidden.
\end{itemize}
To get a `better' proof checker one should:
\begin{itemize}
\item Study algebraic decision procedures
as discussed in Section~\ref{algebra}.
\end{itemize}
\subsection{Future work}
We want to investigate the existing algebraic decision procedures (like for
instance in the ICS system \cite{fil:owr:rue:sha:01}) to find out
how well they can do the algebraic problems from Section~\ref{algebra}.
\subsection{Acknowledgments}
Thanks to Josef Urban for his translation of the proof obligations
in a Mizar article to TPTP format.
Thanks to Dan Synek for the example from Section~\ref{geomath}.
Thanks to Henk Barendregt for encouraging remarks.
%\bibliographystyle{plain}
%\bibliography{frk}
\begin{thebibliography}{1}
\bibitem{fil:owr:rue:sha:01}
Jean-Christophe Filli\^{a}tre, Sam Owre, Harald Rue\ss, and {N.} Shankar.
\newblock {ICS:} integrated canonizer and solver.
\newblock To be presented at {CAV'2001}, 2001.
\bibitem{gal:01}
Jean Gallier.
\newblock {\em Basics of Algebra and Analysis For Computer Science}.
\newblock University of Pennsylvania, 2001.
\newblock Published at:\hfill\break URL:
\verb||.
\bibitem{har:wri:60}
G.H. Hardy and E.M. Wright.
\newblock {\em An Introduction to the Theory of Numbers}.
\newblock Clarendon Press, Oxford, fourth edition, 1960.
\bibitem{har:00}
John Harrison.
\newblock {\em The HOL Light manual (1.1)}, 2000.
\newblock \hfill\break URL:
\verb||.
\bibitem{muz:93}
M.~Muzalewski.
\newblock {\em An Outline of PC Mizar}.
\newblock Fondation Philippe le Hodey, Brussels, 1993.
\newblock \hfill\break URL:
\verb||.
\bibitem{ned:01}
Rob Nederpelt.
\newblock {Weak Type Theory, a formal language for mathematics}.
\newblock Draft version, July 2001.
\bibitem{wie:99:1}
F.~Wiedijk.
\newblock {Mizar: An Impression}.
\newblock \hfill\break URL:
\verb||, 1999.
\end{thebibliography}
\appendix
\section{The smallest first order problem from Section \ref{meson}}
We will now show an example of the problems that we gave to \verb|MESON_TAC|
in Section \ref{meson}.
It is the smallest of these first order problems, which is step number 3
in the formal proof sketch.
That problem is (where the variable \verb|a| has type
\verb|Integer|):
\begin{center}
\begin{tabular}{c}
\verb|a^2 is even|\\\noalign{\smallskip}
\verb|for i being Integer holds i is even iff i^2 is even|\\\noalign{\smallskip}
\hline\noalign{\smallskip}
\verb|a is even|\\
\end{tabular}
\end{center}
The corresponding problem that we gave to \verb|MESON_TAC| looks much more
complicated:
\begin{flushleft}\footnotesize
\verb|v1_abian (k5_square_1 c1) /\|\\
\verb|(!U:V. v1_int_1 U|\\
\verb| ==> ~(v1_abian U /\ ~v1_abian (k5_square_1 U)) /\|\\
\verb| ~(v1_abian (k5_square_1 U) /\ ~v1_abian U)) /\|\\
\verb|v1_int_1 c1 /\|\\
\verb|v1_int_1 c2 /\|\\
\verb|(!U. m1_subset_1 U k1_arytm ==> m1_subset_1 (k5_square_1 U) k1_arytm) /\|\toolong\\
\verb|(!U. m1_subset_1 U k5_ordinal2 ==> m1_subset_1 (k5_square_1 U) k5_ordinal2) /\|\toolong\\
\verb|(!U. v1_int_1 U ==> m1_subset_1 (k5_square_1 U) k5_ordinal2) /\|\\
\verb|(!U. v1_int_1 U ==> v1_arytm U) /\|\\
\verb|(!U V W.|\\
\verb| (~v1_subset_1 U /\ ~v1_subset_1 V /\ m1_subset_1 V (k1_zfmisc_1 U)) /\|\toolong\\
\verb| m1_subset_1 W V|\\
\verb| ==> m1_subset_1 W U) /\|\\
\verb|m1_subset_1 k5_ordinal2 (k1_zfmisc_1 k1_arytm) /\|\\
\verb|(!U. m1_subset_1 U k5_ordinal2|\\
\verb| ==> v1_ordinal1 U /\|\\
\verb| v2_ordinal1 U /\|\\
\verb| v3_ordinal1 U /\|\\
\verb| v4_ordinal2 U /\|\\
\verb| v1_arytm U /\|\\
\verb| v1_int_1 U) /\|\\
\verb|(!U. m1_subset_1 U k1_arytm ==> v1_arytm U) /\|\\
\verb|(!U. v1_arytm U ==> v1_arytm (k5_square_1 U)) /\|\\
\verb|~v1_subset_1 k1_arytm /\|\\
\verb|~v1_subset_1 k5_ordinal2 /\|\\
\verb|(!U. v4_ordinal2 U ==> v1_int_1 U) /\|\\
\verb|(!U. v4_ordinal2 U ==> v1_arytm U) /\|\\
\verb|(!U V. r2_hidden U V = m1_subset_1 U V /\ ~v1_subset_1 V) /\|\\
\verb|(!U V. r1_tarski U V = m1_subset_1 U (k1_zfmisc_1 V)) /\|\\
\verb|(!U V. v1_subset_1 U /\ ~(U = V) ==> ~v1_subset_1 V) /\|\\
\verb|(!U. r1_tarski U U) /\|\\
\verb|(!U. v3_ordinal1 U ==> r1_tarski U U) /\|\\
\verb|(!U V. v3_ordinal1 U /\ v3_ordinal1 V ==> r1_tarski U V \/ r1_tarski V U) /\|\toolong\\
\verb|(!U V. r2_hidden U V ==> ~r2_hidden V U) /\|\\
\verb|(!U V W.|\\
\verb| r2_hidden U V /\ m1_subset_1 V (k1_zfmisc_1 W)|\\
\verb| ==> m1_subset_1 U W /\ ~v1_subset_1 W)|\\
\verb|==> v1_abian c1|
\end{flushleft}
The reason for this is that we use \verb|MESON_TAC| as an untyped
prover (the HOL type system is not powerful enough to accommodate
the Mizar type system), so all relevant typing judgments have to be given as
first order sentences.
The syntax that is used here does not use Mizar notation, but gives
each `constructor' with a code.
These codes translate back to the original Mizar notation according
to the following table:
\begin{center}
\begin{tabular}{lcl}
\verb|k1_zfmisc_1| &$\qquad$& \verb|bool| \\
\verb|k5_ordinal2| && \verb|NAT| \\
\verb|k1_arytm| && \verb|REAL| \\
\verb|k5_square_1| && \verb|^2| \\
\verb|r2_hidden| && \verb|in| \\
\verb|r1_tarski| && \verb|c=| \\
\verb|m1_subset_1| && \verb|Element| \\
\verb|v1_subset_1| && \verb|empty| \\
\verb|v1_ordinal1| && \verb|epsilon-transitive| \\
\verb|v2_ordinal1| && \verb|epsilon-connected| \\
\verb|v3_ordinal1| && \verb|ordinal| \\
\verb|v4_ordinal2| && \verb|natural| \\
\verb|v1_int_1| && \verb|integer| \\
\verb|v1_arytm| && \verb|real| \\
\verb|v1_abian| && \verb|even|
\end{tabular}
\end{center}
We now transform the HOL problem back to Mizar using this translation.
Note the following Mizar type equivalences:
\begin{eqnarray*}
\verb|Nat| &\equiv& \verb|Element of NAT|\\
\verb|Integer| &\equiv& \verb|integer set|\\
\verb|Real| &\equiv& \verb|Element of REAL|\\
\verb|Subset of X| &\equiv& \verb|Element of bool X|
\end{eqnarray*}
The problem that we gave to \verb|MESON_TAC|
is in Mizar notation:
\begin{center}\footnotesize
\begin{tabular}{c}
\verb|a^2 is even|\\\noalign{\medskip}
\verb|for i being integer set holds i is even iff i^2 is even|\\\noalign{\medskip}
\verb|a is integer|\\\noalign{\medskip}
\verb|b is integer|\\\noalign{\medskip}
\verb|for x being Element of REAL holds x^2 is Element of REAL|\\\noalign{\medskip}
\verb|for n being Element of NAT holds n^2 is Element of NAT|\\\noalign{\medskip}
\verb|for a being integer set holds a^2 is Element of NAT|\\\noalign{\medskip}
\verb|for IT being integer set holds IT is real|\\\noalign{\medskip}
\verb|for D being non empty set, X being non empty Element of bool D,|\\
\verb|IT being Element of X holds IT is Element of D|\\\noalign{\medskip}
\verb|NAT is Element of bool REAL|\\\noalign{\medskip}
\verb|for IT being Element of NAT holds IT is epsilon-transitive|\\
\verb|epsilon-connected ordinal natural real integer|\\\noalign{\medskip}
\verb|for IT being Element of REAL holds IT is real|\\\noalign{\medskip}
\verb|for x being real set holds x^2 is real|\\\noalign{\medskip}
\verb|REAL is non empty|\\\noalign{\medskip}
\verb|NAT is non empty|\\\noalign{\medskip}
\verb|for IT being natural set holds IT is integer|\\\noalign{\medskip}
\verb|for IT being natural set holds IT is real|\\\noalign{\medskip}
\verb|for U,V being set holds U in V iff (U is Element of V & V is non empty)|\\\noalign{\medskip}
\verb|for U,V being set holds U c= V iff U is Element of bool V|\\\noalign{\medskip}
\verb|for U,V being set st U is empty & U <> V holds V is non empty|\\\noalign{\medskip}
\verb|for U being set holds U c= U|\\\noalign{\medskip}
\verb|for U being ordinal set holds U c= U|\\\noalign{\medskip}
\verb|for U being ordinal set, V being ordinal set holds U c= V or V c= U|\\\noalign{\medskip}
\verb|for U being set, V being set st U in V holds not V in U|\\\noalign{\medskip}
\verb|for U,V,W being set st U in V & V is Element of bool W holds|\\
\verb|U is Element of W & W is non empty|\\\noalign{\medskip}
\hline\noalign{\medskip}
\verb|a is even|
\end{tabular}
\end{center}
\end{document}