\documentclass[runningheads,envcountsame,envcountsect,orivec]{llncs}
\usepackage{amssymb,url,alltt}
%\raggedbottom

\def\omit#1{}
\def\cases{::=}
\def\defs{\;:=\;}
\def\alt{\;|\;}
\def\star{\mathord{*}}
\def\wf{\mathord{\cdot}}
\def\key#1{\mbox{\sf #1}}
\def\pred#1{#1}
%\def\pred#1{\underline{#1}}
\def\xpred#1{is\char`\_#1}
\def\xxpred#1{\xpred{#1}\char`\_{\penalty 100}of}
\def\trans#1{|{#1}|}

\begin{document}

\title{Mizar's Soft Type System}
\author{Freek Wiedijk}
\institute{
Institute for Computing and Information Sciences \\
Radboud University Nijmegen \\
Toernooiveld 1, 6525 ED Nijmegen, The Netherlands}
\maketitle

\begin{abstract}
In Mizar, unlike in most other proof assistants,
the types are not part of the {foundations} of the
system.
Mizar is based on untyped set theory, which means
that in Mizar expressions are typed but the values of
those expressions are not.

In this paper we present the Mizar type system
as a collection of type inference rules.
We will interpret Mizar types as \emph{soft types},
by translating Mizar's type judgments into sequents of
untyped
first order predicate logic.
We will then prove that the Mizar type system is
\emph{correct} with respect to this translation
in the sense that each derivable type judgment translates
to a provable sequent.
\end{abstract}


\section{Introduction}

\subsection{Problem}

The activity of checking mathematical proofs for correctness
using a computer is called `{formalization of mathematics}'.
Systems for doing this are called proof assistants \cite{wie:06}.
There are three main classes of proof assistants:
the ones based on Church's \emph{higher order logic}
(e.g., HOL, Isabelle/HOL, ProofPower, and maybe also systems like PVS), the ones based on
Martin-L\"of's \emph{type theory} (e.g., Coq, NuPRL, Agda, Epigram), and the
proof assistants based on Cantor's \emph{set theory} (e.g., Mizar, Metamath, Isabelle/ZF, the B method).
These three `cultures' are quite different, and people from different
cultures sometimes find it hard to get a clear view on what people from
the other cultures are doing.
The primary aim of this paper is to make the set theoretical
system Mizar (and in particular its type system) more
understandable to people from the type theoretical
and higher order logic communities.

The Mizar proof assistant \cite{muz:93} has been in development in Bia\l ystok, Poland,
from the seventies until today, by a team led by Andrzej Trybulec.
The current version of the system is called PC Mizar and is at version 7.
It was originally released in 1989, and is still being actively developed.
The library of formalized mathematics that accompanies the Mizar system
is called MML (for Mizar Mathematical Library).
It is the largest library of formalized mathematics that is currently
in existence.
At the time of writing it consists of 1.9 million lines
of Mizar text, and is the collaborative work of almost two hundred people
(the so-called `Mizar authors.')
The large size of the MML library is partly a reflection of the fact that Mizar
only gives one moderate automation.
Also the Mizar library contains
quite a bit of rather obscure mathematics.
Still the Mizar library is
undoubtedly one of the most interesting libraries of formalized mathematics
in the world.
The MML contains a formalization of a graduate-level
textbook on the theory of continuous lattices,
which is being translated quite faithfully into the Mizar language.
(This project, which is being led by Grzegorz Bancerek, is currently two thirds finished.)

The Mizar system is based on first order predicate logic with on top of that a
slight extension of Zermelo-Fraenkel set theory (ZF).
To be precise: the \emph{system} only implements first order predicate logic
(together with `schematic' axioms and theorems\footnote{
Mizar's notation for set comprehension -- in the Mizar community called the `Fraenkel-operator' -- is a alternative version of this.
} -- to be able to deal with
the `replacement' axiom scheme of ZF -- and with a Hilbert choice operator
that is hard-wired into the way the system deals with underspecified functions),
but the MML \emph{library} is based on set theory (all of the 1.9 million of
lines are fully checked for correctness against only a handful of
set theoretical axioms.)
It is irrelevant for the rest of the paper exactly which set theory
the Mizar library is based on, but to be specific:
Mizar's set theory is called Tarski-Grothendieck set theory.
It is 
ZF set theory with one extra axiom added (where `$\sim$' means
that the two sets have the same cardinality):
$$
\begin{array}{l}
\forall N \exists M \big(N\in M \land {}
\\ \phantom{\forall N \exists M \big(}
\forall X \forall Y (X \in M \land Y \subseteq X \!\Rightarrow\! Y \in M) \land {} \\
\phantom{\forall N \exists M \big(}\forall X (X \in M \!\Rightarrow\! \exists Z (Z \in M \land \forall Y (Y \subseteq X \!\Rightarrow\! Y \in Z))) \land {} \\
\phantom{\forall N \exists M \big(}\forall X (X \subseteq M \!\Rightarrow\! X \sim M \lor X \in M)\big)
\end{array}
$$
This axiom states that there are arbitrarily large universes, or, in other
words, that there are arbitrarily large strongly inaccessible cardinals.
From it one can derive the Axiom of Choice (even without
that axiom being hard wired into the logic.)
I do not know why Mizar has selected exactly \emph{this} set theory for its foundation.
Maybe one of the reasons was that the universes are useful when one wants to do category theory.

Set theory in the style of Cantor, like ZF set theory or von Neumann-Bernays-G\"odel set theory (NBG), customarily is an \emph{untyped} theory.
Most often there is just one `sort', the sort of sets.
At most there will be two sorts, with the second sort being the sort of `proper classes'.
However, the Mizar system is a \emph{typed} system: it implements a type
system on top of its first order predicate logic.
And not only does it have a type system, its type system is very powerful,
and has many interesting features.
In particular: it does support \emph{dependent types}, which are \emph{very} useful
if one wants to formalize abstract mathematics.

This raises the question of what the type system of Mizar `means':
what the relation is between the typed version of set theory that
one gets in Mizar and the untyped set theories like ZF that one finds
in logic textbooks.
This is the question that this paper will address.

\subsection{Approach}

There are at least two ways in which to give an interpretation to Mizar's types:
\begin{enumerate}
\item
\label{approaches}
Either one interprets the types of Mizar as \emph{classes of sets}.
In that case the set theory of Mizar will be taken to be a set theory like NBG
set theory, where proper classes are first class objects.

In this approach the interpretation of the Mizar type `\texttt{Ring}'
will be the class of rings,
while the (dependent) type `\texttt{LeftMod} \texttt{of}' will be interpreted by the `class function' that maps each
element of this class of rings to the class of the left modules over it.
This interpretation of `\texttt{LeftMod} \texttt{of}' therefore maps \emph{each} element of a proper class to a \emph{different} proper class.

\item
Alternatively one can interpret the types of Mizar as \emph{predicates}\footnote{
More generally: a dependent type with $n$ parameters will be interpreted as an $n + 1$-ary predicate.
} that
the system will keep track of automatically.
This approach sometimes is called \emph{soft typing}\footnote{
This term originates in the programming languages community \cite{car:fag:91},
where it is used with a somewhat different meaning.
In that context it means that you statically type as much as possible, and insert run-time checks for what cannot be statically typed.
}, which is
the terminology that we will adopt for it in this paper.

In this approach each reference to the type `\texttt{Ring}' will
be interpreted as \emph{actually} being about a unary predicate `\texttt{\xpred{Ring}}',
while the type `\texttt{LeftMod} \texttt{of}' will be interpreted as 
\emph{actually} talking about a binary predicate `\texttt{\xxpred{LeftMod}}'.

\end{enumerate}

\noindent
In this paper we will focus on the second approach, and will not pursue the first possibility.
This second approach has the attractive property that it does not
need set theory.
It allows one to give a meaning to the types of typed first order
predicate logic (and even with types that are as powerful as the ones
that one find in Mizar), even in the case that the theory in that logic is not set theory.

Mizar uses types in various ways.
First, they annotate all variables that occur in a Mizar text:
both for bound variables in formulas and for variables in a proof\footnote{
Although in logic these are considered variables, in the Mizar community they are
often looked at as constants that are local to the proof.
In the Isabelle community these are called \emph{fixed variables}.
} there is a type.
For instance, one writes
$$\texttt{for n being Nat holds \dots}$$
when one universally quantifies over a variable \texttt{n} that has the type \texttt{Nat} (the type of natural numbers),
and one might write
$$\texttt{let n be Nat;}$$
if one is reasoning in a proof about a variable of type \texttt{Nat}.

But types also can be used to create a formula, that states that an expression has a certain type.
For instance one can write that
$$\texttt{i is Nat;}$$
Here the keyword `\texttt{is}' is put between a term and a type.
This specific example means that the value of the expression `\texttt{i}' (which for instance
could be a variable of type `\texttt{Integer}') satisfies
the defining property of the type `\texttt{Nat}', i.e., this states that
\texttt{i} is non-negative.

This second way of using types does not have a direct counterpart in most of the proof
assistants
from the higher order logic and type theory traditions.
There a type judgment is on a different level from the statements
that one reasons about:
in those systems type judgments are \emph{outside} the logic, while statements are
\emph{in} the logic.
But `soft types' cross this boundary.

Apart from using types for reasoning, Mizar also uses types to disambiguate
expressions that involve overloaded notation.
Although this feature is very useful (for instance in Mizar a notation like
$X + Y$
can mean many different things, depending on what the types of $X$ and $Y$ are)
we will not go into this use of Mizar types in this paper.

To reiterate: the interpretation that we give to Mizar types
will be to associate a `hidden' predicate which each type,
and to consider references to types to really be about these hidden predicates.
We will consider the Mizar type system as being an engine that automatically --
behind the scenes -- generates
statements involving those predicates.
For instance, if we call the predicate that corresponds to the `\texttt{Nat}'
type `\texttt{\xpred{Nat}}', then the three example lines of
Mizar on the previous page will be interpreted as being an abbreviation of:
$$\texttt{for n being set holds (\xpred{Nat}(n) implies \dots)}\vspace{-\smallskipamount}$$
$$\texttt{let n be set; assume \xpred{Nat}(n);}$$
$$\texttt{\xpred{Nat}(i)}$$
Now we have statements in single sorted predicate logic where all variables
are in the sort `\texttt{set}'.

\subsection{Related Work}

There already is a paper about the Mizar type system by
Grzegorz Bancerek \cite{ban:03}.
However, the presentation of the type system in that papers
is quite different from the one that is used here.
Also, the interpretation of the types in an `algebra of types' is closer
to the first approach that we mentioned on page \pageref{approaches}
than to the second
approach that we are pursuing here.
Andrzej Trybulec also has such an approach, using the notion
of what he calls \emph{dependent type algebras}.

The work of Ingo Dahn \cite{dah:98} and the work of Josef Urban \cite{urb:03,urb:03:1,urb:06} on translating Mizar into a form
that is digestible by first order theorem provers,
is based on the same interpretation of Mizar types as soft types that
we present in Section \ref{correctness}.
%
In the work of Josef Urban \cite{urb:06} also occurs the view of the
Mizar type checker in `logic programming' style, which is how
we interpreted our typing rules in Section \ref{rules}.

There are other theorem provers that use soft types as a way of pushing
the type system of first order predicate logic beyond the customary `many-sorted'
variant of first order predicate logic, where one only has a finite
number of types without any further structure.
For instance it is used in the SPASS first order theorem prover, see \cite{wei:99}.

Joe Hurd showed how to have a layer of soft typing on top of 
a higher order system \cite{hur:01}.
PVS also can be considered to be such a system.
However, in PVS the soft typing is not actually a separate \emph{layer}.

\subsection{Contribution}

The contribution of this paper is threefold:
\begin{itemize}
\item
It gives a \emph{presentation} of the Mizar type system
as a collection of type inference rules,
which is the style
that is standard in the type theoretical research community.
This presentation of the Mizar type system is new.

\item
It gives an \emph{interpretation} of Mizar's types by systematically
translating type judgments to sequents of untyped first order
predicate logic.
This interpretation was already implicitly present in the work of Ingo Dahn
and Josef Urban,
but the way it is made explicit in this paper,
and the focus that we have on interpreting it as the \emph{semantics}
of the Mizar type system, is new.

\item
It shows that this interpretation is \emph{correct}, in the sense
that for any type judgment that is generated by the Mizar type system,
the corresponding translation is provable.

\end{itemize}

\subsection{Outline}

The structure of this paper is as follows.
In Section \ref{judgments} we present the notation that we
will use for Mizar's type judgments.
In Section \ref{example} we give a non-trivial example of such a judgment,
which we both present in our notation and in the usual Mizar syntax.
In Section \ref{rules} we present the type inference rules of the Mizar
type system.
In Section \ref{correctness} we prove that these rules are correct
with respect to a translation into untyped logic.
Finally in Section \ref{conclusion} we conclude, and mention some questions
for further research.


\section{Judgments}\label{judgments}

In Mizar types have various uses.
In particular, they also play an important r\^ole in the logical language of the system,
because type judgments are one of the kinds of atomic formula.
However, from now on we will focus on the type system on its own, separately
from the logic.
That is, we will now just focus on the mechanism that ascribes types
to terms.\footnote{
This might seem to be a strong restriction.
In particular the reader might wonder how the type system fits in
with the underlying set theory.
(In fact, the Mizar type system is completely independent of
set theory.
The Mizar system
and its type theory can be used with \emph{any} first order theory.)

\looseness=-1
If one translates a Mizar formalization into standard `unsorted' first
order predicate
logic (as is done in \cite{urb:03}), then basically three kinds of statements
are involved.
First, there are the statements that actually occur in the
Mizar text, which are `translated' by relativizing all quantifiers
to the predicates that correspond to the types.
Second, there are the statement that give the definition of the
various predicates, functors, modes and attributes.
In the Mizar file these are implicitly given by the keywords `\texttt{means}' or \texttt{equals}'.
Third, there are the statements that originate in the
type system: the statements occurring in the
translations of the type judgments as described in Section~\ref{correctness}.
%
Apart from the statements of the second kind,
\emph{all} these statements have a proof in the Mizar file.

This means that although it might seem in Section~\ref{rules}
that one is allowed to arbitrarily build a Mizar context,
if one wants to have that context in an actual Mizar text, then
one will need to \emph{prove} the translation in the style of Section~\ref{correctness} of that context.
%(In Mizar these statements are called the `correctness conditions'.)
}
In the Mizar system, this is implemented in the part of the system
that is called {\small ANALYZER}.
(The logic is implemented in the part called {\small CHECKER}.\footnote{
Note that neither {\small ANALYZER} nor {\small CHECKER} has a small
`kernel', as is common in LCF-style systems.
To trust the Mizar system, one will need to trust the full code base.
})

We will now describe the syntax that we will use for Mizar type judgments.
The notation that we will use is specific to this paper.
It will make the typing rules of Section \ref{rules} much more compact
than if we had used the Mizar input syntax.
For a non-trivial example of a typing sequent, both in our syntax as
well as in the Mizar input syntax, see Section \ref{example}.

In our judgments we will have four kinds of variables.
Actually, three of the four kinds are not considered to be variables
in the Mizar system, but because we bind these symbols in the context
part of the judgments\footnote{
Actually, many of these variables will occur multiple times in the context,
because of the presence of redefinitions and clusters.
The first occurrence of the variable -- corresponding to its original 
introduction in the Mizar text -- is the binding one.
}
we will consider them to be variables of the
type judgment.
These kinds of variables are:
\begin{center}
\begin{tabular}{ccl}
$x$ &$\quad$& term variable \\
$f$ && `functor' = function symbol \\
$\alpha$ && `attributes' = type modifier \\
$M$ && `mode' = type symbol \\
\end{tabular}
\end{center}
\noindent
(The words `functor', `attributes\footnote{
Most systems do not have anything like the attributes of Mizar,
which are type modifiers that behave a bit like intersection types.
See Section \ref{example} below for an example that shows how attributes
are used.
In that example the type `\key{int}' of the integers
has attributes `\key{pos}' and `\key{neg}' that allow one to talk
about the positive and the negative
integers.  For example the type `\key{pos} \key{int}' contains
the positive integers.
The elements of that type are the objects that \emph{both} satisfy the
defining statement of the `\key{int}' type and that of the `\key{pos}' attribute.
}', `mode' and (below) `radix type' are Mizar-specific terminology.\footnote{
Words like `functor' and `radix' are used with quite different meanings
outside of the context of Mizar,
so our use of these words might be confusing.
Maybe `function symbol' or `operator' for `functor'
%(a contraction of `function' and `operator')
and `base type' for `radix type'
would be more appropriate.
However, we decided not to depart from standard
Mizar terminology.})

Apart from these variables, we will use one special symbol, the asterisk,
for the root type of Mizar, of which all other types are subtypes:
\begin{center}
\begin{tabular}{ccl}
\setbox0=\hbox{$M$}\hbox to \wd0{\hss$\star$\hss} &$\quad$& \rlap{the root type}\phantom{`functor' = function symbol}
\end{tabular}
\end{center}
\noindent
In Mizar input syntax this type is called
`\texttt{set}' because it is the type of all sets.
It also used to be called `\texttt{Any}'.
(In our interpretation of types
as unary predicates it corresponds to the predicate that is constantly
true.\footnote{
In the typing rules of Section~\ref{rules} the root type plays an essential
r\^ole.
One can only introduce new radix types to the context
if one already \emph{has} a type (which will be its supertype).
So without the root type the rules of Section~\ref{rules} would not work,
as there would not be a starting point for introducing types.
})

Mizar also has \emph{predicate symbols}, which are not treated
in this paper.
The reason for leaving them out is that although the arguments to
the predicates are typed,
the predicates will not play any part in generating the types.

Next, here is the grammar that gives the various notions that occur in our type judgments:
\begin{eqnarray*}
t &\cases& x \alt f(\vec{t}) \\
\noalign{\medskip}
R &\cases& \star \alt M(\vec{t}) \\
a &\cases& \alpha \alt \bar{\alpha} \\
T &\cases& \vec{a}\,R \\
\noalign{\medskip}
D &\cases& x : T \\
J &\cases& \wf \alt t : T \alt T \le T \alt \exists\, T \alt \alpha / T \\
\noalign{\medskip}
\Delta &\cases& \vec{D} \\
\Gamma &\cases& \overrightarrow{[\Delta](J)}
\end{eqnarray*}
\noindent
In this grammar $t$ are the \emph{terms},
$R$ are the \emph{radix types},
$a$ are the \emph{adjectives} (these are either an attribute $\alpha$
or the negation of an attribute $\bar{\alpha}$),
$T$ are the \emph{types},
$D$ are the \emph{declarations},
$J$ are the \emph{judgment elements},
and $\Delta$ and $\Gamma$ are the two parts of the context of a type judgment.
The full type judgments that we will derive with our typing rules will have the shape:
$$\Gamma; \Delta \vdash J$$
\noindent
In this judgement $\Gamma$ corresponds to the type information of
a series of Mizar definitions and registrations.
The `local context' $\Delta$ corresponds to the types of the variables
that have been introduced \emph{inside} a Mizar definition or proof.
We call $\Gamma$ the global context and $\Delta$ the local context of
the judgment.

In the grammar from this section we use vector notation.
For instance, an
expression like
$[\vec{x}:\vec{T}](f(\vec{x}):T')$ should
be read as $[x_1:T_1, \dots, x_n:T_n]\penalty-100(f(x_1,\dots,x_n):T')$.
Furthermore all expressions should only be considered `modulo $\alpha$-equivalence',
so $[x:T](f(x):T')$ and $[y:T](f(y):T')$ are really considered to be
the same.
Finally the `clusters of adjectives' $\vec{a}$ in front of a type
are considered only as sets.
In other words, the expression $\alpha_1 \bar{\alpha}_2$ is considered to be
equivalent to $\bar{\alpha}_2 \alpha_1$, $\alpha_1 \alpha_1 \bar{\alpha}_2$, $\alpha_1 \bar{\alpha}_2 \bar{\alpha}_2$, and so on.

The instances of the notion of judgment elements $J$ have the following
interpretations:
\begin{center}
\begin{tabular}{ccl}
$t:T$ &$\quad$& $t$ has type $T$ \\
$T_1 \le T_2$ && $T_1$ is a subtype of $T_2$ \\
$\exists\, T$ && $T$ is a non-empty type \\
$\alpha/T$ && $\alpha$ is an attribute of the type $T$
\end{tabular}
\end{center}
In Mizar input language $t:T$ is written as `$t$ \texttt{be} $T$' or
`$t$ \texttt{being} $T$', and $T_1 \le T_2$ is written as `$T_1$ \texttt{->} $T_2$'.

The centered dot `$\,\cdot\,$' is used if one just wants to state that a
context is well-formed.
(To indicate that a type $T$ is well-formed one either uses $T \le T$ or
$\exists\, T$, depending on whether one already knows that the type is non-empty
or not.)

\section{Example}\label{example}

We now present an example that demonstrates the various features
of the Mizar type system.
The following type judgment\footnote{
We put the first two judgment elements `$\key{int} \le \star$' and
`$\exists\,\key{int}$' on a single line,
as in the Mizar text it corresponds to a single definition.
} is derivable using the rules of Section~\ref{rules}:
$$
\begin{array}{c}
\key{int} \le \star,\;
\exists\,\key{int},\; \\
\key{pos}/\key{int},\; \\
\key{neg}/\key{int},\; \\
\key{pos}\;\key{int} \le \overline{\key{neg}}\;\key{int},\; \\
\exists\,\key{pos}\;\key{int},\; \\
\exists\,\overline{\key{pos}}\;\overline{\key{neg}}\;\key{int},\; \\
\key{z} : \key{int},\; \\
\key{z} : \overline{\key{neg}}\;\overline{\key{pos}}\;\key{int},\; \\
{}[n:\key{int}](\key{S}(n) : \key{int}),\; \\
{}[n:\key{int}](\key{P}(n) : \key{int}),\; \\
{}[n:\overline{\key{neg}}\;\key{int}](\key{S}(n) : \key{pos}\;\key{int}),\; \\
{}[n:\key{pos}\;\key{int}](\key{P}(n) : \overline{\key{neg}}\;\key{int}),\; \\
%\noalign{\smallskip}
{}[n:\overline{\key{neg}}\;\key{int}](\key{list}(n) \le \star),\;
{}[n:\overline{\key{neg}}\;\key{int}](\exists\,\key{list}(n)),\; \\
\key{nil} : \key{list}(\key{z}),\; \\
{}[n:\overline{\key{neg}}\;\key{int},\, x:\star,\, l:\key{list}(n)](\key{cons}(n,x,l) : \key{list}(\key{S}(n))),\; \\
{}[n:\key{pos}\;\key{int},\, l:\key{list}(n)](\key{car}(n,l) : \star), \\
{}[n:\key{pos}\;\key{int},\, l:\key{list}(n)](\key{cdr}(n,l) : \key{list}(\key{P}(n)))\\ ;\; \\
%\noalign{\smallskip}
x : \star \\
\vdash \\
\key{cdr}(\key{S}(\key{z}),\key{cons}(\key{z},x,\key{nil})) : \key{list}(\key{P}(\key{S}(\key{z})))
\end{array}
$$
\noindent
This example involves types \key{int} and \key{list} for integers and
lists, the latter being a dependent type with the length of the
list as the argument.
It has attributes \key{pos} and \key{neg} on the type of integers for positive and
negative integers.
Furthermore it has
functions \key{S} and \key{P} on the integers for successor and predecessor
and functions \key{nil}, \key{cons}, \key{car} and \key{cdr} for the lists.%
\footnote{
These are not the names that are used in the MML for these
notions.
There \key{int} is called \texttt{Integer}, \key{list} is called \texttt{FinSequence} (although the version that depends on the length of the list like in the example is called \texttt{Tuple}, and that type also depends on the set from which the elements are taken).
The attributes \key{pos} and \key{neg} are called \texttt{positive} and \texttt{negative},
and \key{nil}
is called \texttt{\char`\{\char`\}}.
The functions \key{S} and \key{P} do not exist in the MML, $\key{S}(n)$ is just written as $n + 1$ and $\key{P}(n)$ is just
$n - 1$.
The list functions do not exist either:
$\key{cons}(x,l)$ is written \texttt{<*$x$*>\char`\^$l$},
$\key{car}(l)$ is written \texttt{$l$.1}, and
$\key{cdr}(l)$ is written \texttt{$l$/\char`\^1}.

The name \texttt{neg} in the MML is not an attribute symbol
but a functor symbol, for intuitionistic negation.
}
The local context of the judgment is just the variable declaration $x : \star$,
and the statement of the judgment is that the term `$\key{cdr}(\key{S}(\key{z}),\key{cons}(\key{z},x,\key{nil}))$' has among its collection of types the type `$\key{list}(\key{P}(\key{S}(\key{z})))$'.

The judgment that we just presented has the shape
$$\Gamma; \Delta \vdash J$$
of which the part $\Gamma$ corresponds to a
series of definitions and registrations.
Here is what this $\Gamma$ looks like in Mizar syntax:
\begingroup
\small
\begin{alltt}
definition
 mode int -> set means \dots; existence \dots
end;\medskip
definition let n be int;
 attr n is pos means \dots
 attr n is neg means \dots
end;\medskip
registration
 cluster pos -> non neg int; coherence \dots
end;\medskip
registration
 cluster pos int; existence \dots
 cluster non pos non neg int; existence \dots
end;\medskip
definition
 func z -> int means \dots
end;\medskip
registration
 cluster z -> non neg non pos; coherence \dots
end;\medskip
definition let n be int;
 func S n -> int means \dots
 func P n -> int means \dots
end;\medskip
registration let n be non neg int;
 cluster S n -> pos; coherence \dots
end;\medskip
definition let n be pos int;
 redefine func P n -> non neg int; coherence \dots
end;\medskip
definition let n be non neg int;
 mode list of n -> set means \dots; existence \dots
end;\medskip
definition
 func nil -> list of z means \dots
end;\medskip
definition let n be non neg int; let x be set; let l be list of n;
 func cons(x,l) -> list of S n means \dots
end;\medskip
definition let n be pos int; let l be list of n;
 func car l -> set means \dots
end;\medskip
definition let n be pos int; let l be list of n;
 func cdr l -> list of P n means \dots
end;
\end{alltt}
%theorem for x being set holds cdr cons(x,nil) is list of P S z;
\endgroup
\noindent
For a version of these definitions that has been completed with statements
and proofs
in the place of the dots see \texttt{\char`\<}\url{http://www.cs.ru.nl/}\texttt{\char`\~}\url{freek/mizar/example.miz}\texttt{\char`\>} and
\texttt{\char`\<}\url{http://www.cs.ru.nl/}\texttt{\char`\~}\url{freek/mizar/example.voc}\texttt{\char`\>}.\footnote{
Note that from the point of view of the MML, this is a \emph{very} silly example as
it just defines a lot of stuff that is present already, only using different names.
}

Note that most of the items in this list of definitions and registrations
have proof obligations.
This means that they do not, like in the judgments that we show in this
paper, behave like assumptions, but that they really are statements that
are proved from the existing theory.
For example, the part of the context
$$
{}[n:\key{pos}\;\key{int}](\key{P}(n) : \overline{\key{neg}}\;\key{int}),\; \\
$$
that is the `redefinition' of the predecessor function
to give its value the more specific type `$\overline{\key{neg}}\;\key{int}$' when
it is known that the argument has the type `$\key{pos}\;\key{int}$'
is in the Mizar formalization written as
\begingroup
\small
\def\prooftag{$\langle\mbox{\rm proof steps}\rangle$}
\def\xdots{{\rm\dots}}
\begin{alltt}
definition
 let n be pos int;
 redefine func P n -> non neg int;
 coherence
 proof
  \xdots
  hence P n is non neg int by \xdots
 end;
end;
\end{alltt}
\endgroup
\noindent
where the `\texttt{P} \texttt{n}' in the \texttt{hence} line
refers to the earlier definition of the \key{P} function.
This means that the dots will have to be a proof that amounts to showing that from $n > 0$
it follows that $n - 1 \ge 0$.
Under the translation from Section \ref{correctness} this part of the
typing context turns into
$$\forall n \big(\pred{\key{pos}}(n) \land \pred{\key{int}}(n) \Rightarrow \neg \pred{\key{neg}}(\key{P}(n)) \land \pred{\key{int}}(\key{P}(n))\big)$$
and in a real Mizar formalization that statement will have to be proved.

Similarly the other definitions and registrations have appropriate proof
obligations
(the only judgment elements in the context of the example that do not have proof obligations are the attribute
definitions.)


\section{Rules}\label{rules}

We will now present the Mizar type system as a collection of typing rules.
These rules present a slightly simplified version of the Mizar type system:
\begin{itemize}
\item
There are no structure types.

Structure types are the `record types' of Mizar.
(For an interesting discussion of how structure types can
be understood in terms of the underlying set theoretical foundations of the Mizar system, see \cite{lee:rud:07}.)
\item
In the real Mizar system, symbols can be overloaded.
Here we suppose that all symbols have been sufficiently
disambiguated.
That is, the typing rules that we are presenting should only be
instantiated according to the Barendregt convention (variables should
never be `hidden' by later variables.)
\item
In the real Mizar type system, a redefinition takes priority over the definitions
that come before it in the context.
However, in this version of the type system the order of the definitions
is not taken into account when generating type judgments.
\item
When reasoning, the set of types of a Mizar expression will be closed
under available equalities.
For instance, if one of the statements that justifies the inference is
$n = n'$ and an expression has type $\key{list}(n)$, then it also will be
assigned type $\key{list}(n')$.
This kind of equality reasoning is not present in our
version of the Mizar type system.
\end{itemize}
\noindent
Note that a Mizar term generally does not have just one type
(for instance, every well typed expression will always \emph{also} have the
type $\star$),
and can even get a quite large collection of types.

One can consider these rules to be something like a `logic programming'
description of the Mizar type checker:
\medskip

$$
{
\over
; \vdash \wf
}
$$
$$
{
\Gamma; \Delta \vdash \vec{t} : \vec{T}[\vec{x} := \vec{t}]
\over
\Gamma; \Delta \vdash J[\vec{x} := \vec{t}]
}
\;
[\vec{x} : \vec{T}](J) \in \Gamma; \Delta
\qquad
{
\Gamma; \Delta \vdash \exists\, T
\over
\Gamma; \Delta, x : T \vdash \wf
}
$$

$$
{
\Gamma; \Delta \vdash \wf
\over
\Gamma; \Delta \vdash \star \le \star
}
\qquad
{
\Gamma; \Delta \vdash \wf
\over
\Gamma; \Delta \vdash \exists\,\star
}
$$

$$
{
\Gamma; \Delta \vdash T \le T'
\over
\Gamma; \Delta \vdash T \le T
}
\qquad
{
\Gamma; \Delta \vdash T \le T'
\quad
\Gamma; \Delta \vdash T' \le T''
\over
\Gamma; \Delta \vdash T \le T''
}
$$
$$
{
\Gamma; \Delta \vdash t : T
\quad
\Gamma; \Delta \vdash T \le T'
\over
\Gamma; \Delta \vdash t : T'
}
\qquad
{
\Gamma; \Delta \vdash T \le T'
\quad
\Gamma; \Delta \vdash \exists\, T
\over
\Gamma; \Delta \vdash \exists\, T'
}
$$

$$
{
\Gamma; \Delta \vdash \alpha / T
\over
\Gamma; \Delta \vdash \alpha T \le T
}
\qquad
{
\Gamma; \Delta \vdash \alpha / T
\over
\Gamma; \Delta \vdash \bar{\alpha} T \le T
}
$$
$$
{
\Gamma; \Delta \vdash T \le T'
\quad
\Gamma; \Delta \vdash a\, T' \le T'
\over
\Gamma; \Delta \vdash a\, T \le T
}
\qquad
{
\Gamma; \Delta \vdash T \le T'
\quad
\Gamma; \Delta \vdash a\, T' \le T'
\over
\Gamma; \Delta \vdash a\, T \le a\, T'
}
$$
$$
{
\Gamma; \Delta \vdash T \le a T'
\quad
\Gamma; \Delta \vdash T \le a' T'
\over
\Gamma; \Delta \vdash T \le a a' T'
}
$$
$$
{
\Gamma;\, \vec{x} : \vec{T} \vdash \exists\, T'
\over
\Gamma,\, [\vec{x} : \vec{T}](f(\vec{x}) : T');\, \vdash \wf
}
\; f \not\in \Gamma
\leqno{
\emph{functor definition:}
}
$$
$$
{
\Gamma;\, \vec{x} : \vec{T} \vdash \exists\, T'
\over
\Gamma,\, [\vec{x} : \vec{T}](M(\vec{x}) \le T'),\,
  [\vec{x} : \vec{T}](\exists\, M(\vec{x}));\, \vdash \wf
}
\; M \not\in \Gamma
\leqno{
\emph{mode definition:}
}
$$
$$
{
\Gamma; \Delta \vdash \exists\, T'
\over
\Gamma,\, [\Delta](\alpha / T');\, \vdash \wf
}
\; \alpha \not\in \Gamma
\leqno{
\emph{attribute definition:}
}
$$
$$
{
\Gamma; \Delta \vdash \vec{a}\, T' \le T'
\quad
\Gamma; \Delta \vdash \exists\, T'
\over
\Gamma,\, [\Delta](\exists\, \vec{a}\, T');\, \vdash \wf
}
\leqno{
\emph{existential cluster:}
}
$$
$$
{
\Gamma; \Delta \vdash \vec{a}\,T' \le T'
\quad
\Gamma; \Delta \vdash \vec{a}'\,T' \le T'
\over
\Gamma,\, [\Delta](\vec{a}\,T' \le \vec{a}'\,T');\, \vdash \wf
}
\leqno{
\emph{conditional cluster:}
}
$$
$$
{
\Gamma; \Delta \vdash t : T'
\quad
\Gamma; \Delta \vdash \vec{a}\,T' \le T'
\over
\Gamma,\, [\Delta](t : \vec{a}\,T');\, \vdash \wf
}
\leqno{
\emph{functorial cluster:}
}
$$
$$
{
\begin{array}{c}
\Gamma;\, \vec{x} : \vec{T} \vdash \exists\, T''
\quad
\Gamma;\, \vec{x} : \vec{T} \vdash T'' \le T''' \\
\Gamma;\, \vec{x}' : \vec{T}',\, \vec{x} : \vec{T} \vdash f(\vec{x}) : T'''
\end{array}
\over
\Gamma,\, [\vec{x}' : \vec{T}',\, \vec{x} : \vec{T}](f(\vec{x}) : T'');\, \vdash \wf
}
\leqno{
\emph{functor redefinition:}
}
$$
$$
{
\begin{array}{c}
\Gamma;\, \vec{x} : \vec{T} \vdash \exists\, T''
\quad
\Gamma;\, \vec{x} : \vec{T} \vdash T'' \le T''' \\
\Gamma;\, \vec{x}' : \vec{T}',\, \vec{x} : \vec{T} \vdash M(\vec{x}) \le T'''
\end{array}
\over
\Gamma,\, [\vec{x}' : \vec{T}',\, \vec{x} : \vec{T}](M(\vec{x}) : T'');\, \vdash \wf
}
\leqno{
\emph{mode redefinition:}
}
$$
\vspace{0\medskipamount}

\noindent
The side-conditions `$\dots \not\in \Gamma$' of the three
definition rules mean that
the symbol does not occur anywhere in the context $\Gamma$.
The `extra arguments' $\vec{x}'$ in the redefinition rules
and generally are the empty vector.

In Mizar the types of actual terms always have to be non-empty.\footnote{
There is no good mathematical reason for this restriction.
It \emph{does} lead to higher quality formalizations,
as the formalizer will need to think about whether the types are empty or not.
Also, it of course simplifies the implementation of the inference
checker.
On the other hand it sometimes leads to unnatural mode definitions
(like the infamous definition of `\texttt{Element} \texttt{of}').
}
This explains all the assumptions of the form $\exists\, T$ that
occur in these rules.
However, note that clusters sometimes involve types that
have not been shown to be non-empty.


\section{Correctness}\label{correctness}

We will now translate the typing judgments of our Mizar type system
into sequents of single sorted first order predicate logic.\footnote{
In fact the Mizar typing rules can be motivated from this translation.
The Mizar type system is designed to combine two opposite goals: to
have the system automatically infer as many type judgments as possible
for which the translation is provable; but on the other hand
to have a type system in which all typing judgments can be efficiently
inferred.
}
We will do this in two phases:

\begin{itemize}
\item
First we introduce an \emph{annotated} version of the Mizar type system,
in which all the attributes have explicit arguments.
This is exactly the same system that we already presented,
but each attribute $\alpha$ now gets a list of arguments.
These arguments are the arguments that determine the type
on which the attribute was defined.

The grammar of the judgments stays exactly like it was, except
that the rule for an adjective becomes:
\begin{eqnarray*}
a &\cases& \alpha(\vec{t}) \alt \bar{\alpha}(\vec{t})
\end{eqnarray*}
The derivation rules also stay all the same, apart from the rules
that explicitly involve an attribute symbol:
$$
{
\Gamma; \vec{x} : \vec{T} \vdash \exists\, T'
\over
\Gamma,\, [\vec{x} : \vec{T}](\alpha(\vec{x}) / T');\, \vdash \wf
}
\; \alpha \not\in \Gamma
%\leqno{
%\emph{attribute definition:}
%}
$$
$$
{
\Gamma; \Delta \vdash \alpha(\vec{t}) / T
\over
\Gamma; \Delta \vdash \alpha(\vec{t})\, T \le T
}
\qquad
{
\Gamma; \Delta \vdash \alpha(\vec{t}) / T
\over
\Gamma; \Delta \vdash \bar{\alpha}(\vec{t})\, T \le T
}
$$
\vspace{0\medskipamount}

\noindent
We now have the following theorem, that we present here without proof:
\begin{theorem}
For every derivable type judgment of the non-annotated version
of the Mizar type system,
there exists a corresponding type judgment of
the annotated version of the Mizar type system which
only differs in that after the attributes arguments have been added.)
\end{theorem}

\noindent
Note that the annotated version of the judgment is not always
unique.
This is the reason that the Mizar implementation
internally keeps track of these `hidden arguments' of the attributes.
(There has been discussion in the Mizar community about whether these
arguments maybe also should be allowed to be explicit.)
\medskip

\item
Now that we have annotated versions of the Mizar type judgments,
translating them into first order logic is easy.
We define a translation $\trans{\,\cdot\,}$ that maps our system
into first order logic:
\begin{eqnarray*}
\trans{*}(t) &\defs& \top \\
\trans{M(\vec{t}')}(t) &\defs& \pred{M}(t,\vec{t'}) \\
\trans{\alpha(\vec{t}')}(t) &\defs& \pred{\alpha}(t,\vec{t'}) \\
\trans{\bar{\alpha}(\vec{t}')}(t) &\defs& \neg\pred{\alpha}(t,\vec{t'}) \\
\trans{a_1 \dots a_n\, R}(t) &\defs& \trans{a_1}(t) \land \dots \land \trans{a_n}(t) \land \trans{R}(t) \\
\noalign{\medskip}
\trans{t : T} &\defs& \trans{T}(t) \\
\trans{T \le T'} &\defs& \forall x\, (\trans{T}(x) \Rightarrow \trans{T'}(x)) \\
\trans{\exists\, T} &\defs& \exists x\, (\trans{T}(x)) \\
\trans{\alpha / T} &\defs& \top \\
\noalign{\medskip}
\trans{[x_1 : T_1, \dots, x_n : T_n](J)} &\defs& \forall x_1 \dots \forall x_n (\trans{T_1}(x_1) \land \dots \land \trans{T_n}(x_n) \Rightarrow \trans{J}) \\
\trans{\overrightarrow{[\Delta](J)}; \overrightarrow{J'} \vdash J''} &\defs& \overrightarrow{\trans{[\Delta](J)}}, \overrightarrow{\trans{J'}} \vdash \trans{J''}
\end{eqnarray*}

\noindent
In the first order logic, we take the symbols for types and attributes
to be predicate symbols, where the arity as a predicate symbol is one
more than the original arity.
The idea is that if $T$ is a type, then $\trans{T}(t)$ corresponds to the
Mizar statement `$t\texttt{ is }T$'.
This explains the order that we chose for the arguments of the symbol
taken as a predicate.

(The translation of $\alpha / T$ as just `true' might be
unexpected.
One might expect the translation to be:
$$\trans{\alpha / T} := \forall x\, (\trans{\alpha}(x) \Rightarrow \trans{T}(x))$$
However, we decided not to do this, as it would be strange to
require $\trans{\alpha}(t)$ to imply $\trans{T}(t)$, but not
to require the same property for $\trans{\bar{\alpha}}(t)$
($\bar{\alpha}$ also being an adjective of $T$).
Our translation is
interpreting adjectives in the spirit of intersection types.\footnote{
It might be surprising that an attribute
can be given whatever radix type one likes.
This corresponds to the fact that in Mizar an attribute definition
does not need any proof (it does not have a `correctness condition'):
the defining statement of an attribute can be any formula, without
any restriction.
Note also that there is no such thing as an `attribute redefinition'.
})
\medskip

The following theorem now also is easy:
\begin{theorem}
If $\Gamma; \Delta \vdash J$ is a judgment of the annotated version
of the Mizar type system, then 
$\trans{\Gamma; \Delta \vdash J}$ is a provable sequent of first order
predicate logic.
\end{theorem}
\begin{proof}
Induction on the derivation of the judgment:
each rule
of the type system corresponds to a small derivation in first order logic.
\hfill$\Box$
\end{proof}

\end{itemize}


\section{Conclusion}\label{conclusion}

\subsection{Discussion}

One of the nicest things about interpreting the Mizar type system
as a system of \emph{soft} types, is that it shows that
the Mizar type system, with all its power, can easily be added
`on top' of any existing proof assistant.\footnote{
The work of Joe Hurd \cite{hur:01} already is a version of this
(although it of course does not implement the full Mizar type system.)
}
It is mainly a matter of defining selected predicates to take the r\^{o}le
of the types and then to:
\begin{itemize}
\item
Implement automatic inference of statements about these predicates
along the lines of the rules in Section \ref{rules}.
\item
Add a layer of parsing and pretty-printing to the system to have syntax
for the predicates as types.
In this layer the \emph{implicit arguments} that are common in
dependently typed systems can be implemented.
\end{itemize}
This way even the systems from the HOL family of proof assistants \cite{gor:mel:93}
can have dependent types!

In fact, even in systems like Coq that have a rather powerful type
system already, one often sees the tendency to use `soft' types
on top of the `hard' types that are already in the system.
For instance, in the C-CoRN library from Nijmegen, there is a formalization
of integration theory, where instead of using a type
for
continuous partial functions, there are lines in the development that
look like:
\begingroup
\small
\begin{alltt}
Variables a b : IR.
Hypothesis Hab : a [<=] b.
Variable F : PartIR.
Hypothesis contF : Continuous_I Hab F.
\end{alltt}
\endgroup
\noindent
and then the operation called `\texttt{Integral}' takes the predicate
`\texttt{contF}'
as one of its arguments.
Clearly this is a rough version of soft typing.

Similarly, a development of Galois theory by Georges Gonthier and Sean McLaughlin (developed in
the Microsoft/INRIA institute in Paris) is using a style of having
`soft types on top of Coq'.

\subsection{Future work}

There are various interesting questions that might be pursued as a continuation
of the research presented in this paper:
\begin{itemize}
\item
A type system really should be \emph{decidable}, but we have not
established this property for the type system that we presented here.
The implementation of the type system in the Mizar type checker
clearly seems to have this property,
but then the rules that we presented in this paper do not \emph{exactly} match
the type system as it is implemented in the actual system.

It is clear that a naive implementation of our version of the Mizar type system
will not work.
The redefinition:
\begin{center}
\small
\texttt{redefine mode Element of n -> Element of n + 1;}
\end{center}
(which is allowed in the actual Mizar system!) will with our version
of the typing rules give rise to infinite collections of types.\footnote{
We got this example from Josef Urban.
}
This example also shows that a direct Prolog-style implementation of
the rules from Section~\ref{rules} will not always terminate.
However, it is might be the case that a less naive algorithm than just
generating all possible types for an expression still can implement a type checker
for the typing rules from Section~\ref{rules}.
%
%More interesting might be to study how the typing rules
%should be adapted to exactly describe the type system as implemented in
%the real Mizar system.

\item
We have proved that the type system that we present in this paper
is \emph{correct}, but one also could consider the question of whether it is
\emph{complete}.
The theorem to be proved for this would be that if a sequent is
a translation of a typing judgment in our system of which the
context is already a correct context, and if
that sequent is provable in first order predicate logic, that then
in fact the typing judgment is derivable in the type system.

We have not yet tried to prove this property, but thus
far we do not know of a counter-example either.

\item
It might be interesting to make the rules that we presented
here more realistic, by for example adding structure types or equalities between
terms.
Maybe even more interesting would be to precisely analyze the differences between our version of the type system, and the corresponding fragment of the
type system the way it is implemented in the actual Mizar system.
The interesting question would be whether the differences might easily
be removed (either by adapting the typing rules, or by changing the implementation), or whether the differences are essential for giving the implementation
of the type checker a reasonable performance.

\end{itemize}

\paragraph{Acknowledgments.}
It will be clear that this paper was inspired by the papers
of Fairouz Kamareddine.
%
When I wrote this paper I had Herman Geuvers in mind as my
target audience:
I hope that this paper managed to communicate the Mizar type system to him.
%
Furthermore many thanks to Josef Urban, Makarius and the
anonymous referees of the TPHOLs conference for their helpful comments on a draft version of this paper.

%\bibliographystyle{plain}
%\bibliography{frk}

\begin{thebibliography}{10}

\bibitem{ban:03}
Grzegorz Bancerek.
\newblock {On the structure of Mizar types}.
\newblock {\em Electronic Notes in Theoretical Computer Science}, 85, 2003.

\bibitem{car:fag:91}
R.~Cartwright and M.~Fagan.
\newblock Soft typing.
\newblock In {\em Proceedings of the {SIGPLAN} '91 Conference on Programming
  Language Design and Implementation}, pages 278--292, 1991.

\bibitem{dah:98}
Ingo Dahn.
\newblock {Interpretation of a Mizar-Like Logic in First-Order Logic}.
\newblock In {\em {FTP} ({LNCS} Selection)}, pages 137--151, 1998.

\bibitem{gor:mel:93}
M.J.C. Gordon and T.F. Melham, editors.
\newblock {\em Introduction to HOL}.
\newblock Cambridge University Press, Cambridge, 1993.

\bibitem{hur:01}
Joe Hurd.
\newblock Predicate subtyping with predicate sets.
\newblock In Richard~J. Boulton and Paul~B. Jackson, editors, {\em 14th
  International Conference on Theorem Proving in Higher Order Logics: {TPHOLs}
  2001}, volume 2152 of {\em LNCS}, pages 265--280. Springer-Verlag, 2001.

\bibitem{lee:rud:07}
Gilbert Lee and Piotr Rudnicki.
\newblock {Alternative Aggregates in Mizar}, 2007.
\newblock {To be published in Mathematical Knowledge Management 2007.}

\bibitem{muz:93}
Micha{\l} Muzalewski.
\newblock {\em An Outline of PC Mizar}.
\newblock Fondation Philippe le Hodey, Brussels, 1993.
\newblock
  \url{<http://www.cs.ru.nl/}\texttt{\char`\~}\url{freek/mizar/mizarmanual.ps.%
gz>}.

\bibitem{urb:03:1}
Josef Urban.
\newblock {MPTP 0.1: System Description}.
\newblock {\em ENTCS}, 86(1), 2003.

\bibitem{urb:03}
Josef Urban.
\newblock {Translating {M}izar for First Order Theorem Provers}.
\newblock In {\em MKM}, volume 2594 of {\em Lecture Notes in Computer Science},
  pages 203--215. Springer, 2003.

\bibitem{urb:06}
Josef Urban.
\newblock {MoMM -- Fast Interreduction and Retrieval in Large Libraries of
  Formalized Mathematics}.
\newblock {\em International Journal on Artificial Intelligence Tools},
  15(1):109--130, 2006.

\bibitem{wei:99}
C.~Weidenbach.
\newblock {SPASS: Combining superposition, sorts and splitting}, 1999.

\bibitem{wie:06}
Freek Wiedijk, editor.
\newblock {\em {The Seventeen Provers of the World}}, volume 3600 of {\em
  LNCS}.
\newblock Springer, 2006.
\newblock With a foreword by Dana S.~Scott.

\end{thebibliography}

\end{document}