\documentclass[runningheads]{llncs}
\usepackage{amssymb}
\usepackage{url}

\def\id#1{\mbox{\sc #1}}
\def\VAR{\id{var}}
\def\TERM{{\cal T}}
\def\FORM{{\cal F}}
\def\PROOF{{\cal P}}
\def\CONT{{\cal C}}
\def\JUDG{{\cal J}}
\def\DC{{\cal DC}}
\def\xx#1{{\rm\textsf{#1}}}
\def\xT{\xx{T}}
\def\xD{\xx{D}}
\def\xP{\xx{P}}
\def\xxx#1{^{\mbox{\rm\scriptsize #1}}}
\def\xxT{\xxx\xT}
\def\xxD{\xxx\xD}
\def\xxP{\xxx\xP}
\def\xverb#1{\mbox{\it #1\/}}
\def\ok{\xverb{wf}}
\def\wf{\;\xverb{wf}}
\def\FV{\xverb{FV}}
\def\gen#1{\mbox{\sf #1\/}}
\def\raa{\gen{raa}}
\def\refl{\gen{refl}}
\def\sym{\gen{sym}}
\def\trans{\gen{trans}}
\def\eqfun{\gen{eqfun}}
\def\eqpred{\gen{eqpred}}
\def\IFTRUE{\gen{if{}true}}
\def\IFFALSE{\gen{if{}false}}
\def\implies{\,\Rightarrow\,}
\def\iff{\leftrightarrow}
\def\and{,\;}
\def\namerule#1{({\it #1\/})}
\def\rulex#1#2{\frac{\displaystyle\strut #1}{\displaystyle\strut #2}}
\def\rulexn#1#2#3{\makebox[0pt][r]{\hss\namerule{#1}$\;\;$}\frac{\displaystyle\strut #2}{\displaystyle\strut #3}}
\def\rulexnc#1#2#3#4{\makebox[0pt][r]{\hss\namerule{#1}$\;\;$}\frac{\displaystyle\strut #2}{\displaystyle\strut #3}\mrlap{#4}}
\def\mrlap#1{\makebox[0pt][l]{$\displaystyle\;\;#1$\hss}}
\def\rulexn#1#2#3{\mbox{\namerule{#1}}\;\frac{\displaystyle\strut #2}{\displaystyle\strut #3}}
\def\rulexnc#1#2#3#4{\mbox{\namerule{#1}}\;\frac{\displaystyle\strut #2}{\displaystyle\strut #3}\mrlap{#4}}
\def\mrlap#1{{\displaystyle\;#1}}
\def\infer{\,\vdash}
\def\sep{.\,}
\def\text#1{\mbox{#1}}
\def\IF{\mbox{\sf{if }}}
\def\THEN{\mbox{\sf{ then }}}
\def\ELSE{\mbox{\sf{ else }}}
\def\pow{{\cal P}}
\def\tick{}
\def\alt{\mathrel{|}}
\def\lmarg#1{\leqno{\hbox{\normalsize\hspace{-2em}$#1$:}}}
\let\phi=\varphi

\begin{document}

\title{First order logic with domain conditions}
\author{Freek Wiedijk and Jan Zwanenburg}
\institute{Department of Computer Science,
  University of Nijmegen \\
  Toernooiveld 1,
  6525 ED Nijmegen,
  The Netherlands}
\maketitle

\begin{abstract}
This paper addresses the crucial issue in the design of a proof development system of
how to deal with {\em partial functions\/}
and the related question of how to treat {\em undefined terms}.
Often the problem is avoided by artificially making all functions total.
However, that does not correspond to the practice of everyday mathematics.

In type theory partial functions are modeled by giving functions extra arguments which are
{\em proof objects}.
In that case it will not be possible to apply functions outside their domain.
However, having proofs as first class objects
has the disadvantage that it will be unfamiliar to most mathematicians.
Also many proof tools (like the theorem prover Otter) will not be usable for such a logic.
Finally expressions get difficult to read because of
these proof objects.

The PVS system solves the problem of partial functions differently.
PVS generates {\em type-correctness conditions\/} (TCCs) for statements in its language.
These are proof obligations that have to be satisfied `on the side' to show that statements are well-formed.

We propose a TCC-like approach for the treatment of partial functions
in type theory.
We add {\em domain conditions\/} (DCs) to classical first-order logic
and show the equivalence with
a first order system that treats partial functions
in the style of type theory.
\end{abstract}


\section{Introduction}

\subsection{Problem.}

Until a few decades ago mathematics was something that was done in human heads, on the blackboard or on paper.
Only since the seventies have systems been developed that verify mathematics with the computer.
The first of these was the Automath system from the Netherlands.
Other early systems of this kind were the Mizar system \cite{muz:93} from Poland
and the LCF system from the UK.
Recently this kind of system has become widely used (mostly because of applications in computer science).
Currently the most popular is the PVS system \cite{owr:rus:sha:92}
from a US company called SRI International.
Other contemporary systems of this kind are ACL2 \cite{kau:man:moo:00}, IMPS \cite{gut:tha:93} and NuPRL \cite{con:all:bro:cle:cre:har:how:kno:men:pan:sas:smi:86} from the US,
HOL \cite{gor:mel:93} and Isabelle \cite{nip:pau:wen:02} from the UK and Germany, and the Coq system
\cite{coq:02} from France.
This last system is an implementation of an approach to formalizing mathematics
called {\em type theory}.

This paper addresses the question of how to treat partial functions in formal mathematics.
The prototypical example of a partial function is division:
the quotient
$1/0$
is problematic because $0$ is outside the domain of the division function.
Formal systems have to take a position on how to deal with this kind of expression.

A traditional way to model partial functions in logic is by using {\em relations}.
A statement about division is then interpreted as a statement about a ternary predicate $\mbox{\sf div\_eq}$,
that satisfies the equivalence:
$$\mbox{\sf div\_eq}(x,y,z) \;\Longleftrightarrow\; y\ne 0 \,\land\, x/y = z$$
However when translating statements this way, they become an order of magnitude larger than
the original.
Therefore, for actual implementations of formal systems it is not attractive.

In \cite{har:95:1}, John Harrison enumerated the four main approaches to partial functions
that one actually encounters in proof checkers:
\begin{quote}\em
\begin{enumerate}
\label{list}
\item Resolutely give each partial function a convenient value on points
outside its domain.
\item Give each partial function some arbitrary value outside its domain.
\item Encode the domain of the partial function in its type and make its
application to arguments outside that domain a type error.
\item Have a true logic of partial terms.
\end{enumerate}
\end{quote}
In the first case one would define $1/0 = 0$, in the second case $1/0$
would be some real number but one would not be able to prove which one it is, in the third case $1/0$ would be
a type error, and in the last case $1/0$ would be an allowed expression but it would not denote anything (and one would be able to prove so).

In the systems listed above,
ACL2 uses the first approach, HOL, Isabelle and Mizar use a mixture of
the first and second approaches, Coq, NuPRL and PVS use the third approach, and IMPS uses the fourth approach.

In this paper we explore a variant of Harrison's approach number 3.
Although we do present a system of our own, it is not a `logic of partial terms'.
It does not allow one to write $1/0$ or any other undefined term
and there is no way to state whether a term is defined (because it always is).

The approach that we present here is inspired by type theory, but our logic actually is one-sorted,
so the variables of our logic all have the same `type'.
It is easy to generalize our approach to a many-sorted logic.
We restricted ourselves to the one-sorted case for simplicity.

The problem that we address in this paper is how to be able to follow approach number 3, while still doing the proofs in
the ordinary first order predicate logic with total functions.

There are two reasons why it is worthwhile not to have to give up first order logic:
\begin{itemize}
\item First order logic is the best known logic.
Users of a proof checker will understand the system better if the logic is ordinary first order logic.
\item There is much technology for first order logic.
For instance there are many theorem provers for it.
The best known of these is Otter \cite{wos:96}, but there are many more.
They even compete in first order theorem prover competitions like the
CADE system competition.
It is valuable to be able to use this technology in a proof checker.
\end{itemize}

\subsection{Approach.}
We will introduce three logical systems, called system {\xT}, system {\xD} and system {\xP}.
The names of those systems are abbreviations of `total', `domain' and `partial'.
These systems are:
\begin{itemize}
\item[] {\em System {\xT}}.
Ordinary first order logic with total functions.
\item[] {\em System {\xD}}.
Exactly the same logic as system {\xT},
but in this system undefined expressions are not allowed.
This means that all functions have to have the arguments inside their domain.
\item[] {\em System {\xP}}.
A system in type theoretical style.
Extra arguments which are proof objects ensure that it is not possible to
write an undefined term.
\end{itemize}
Systems {\xT} and {\xD} have exactly the same set of expressions: only the derivations of both systems differ.
System {\xP} has a different set of expressions, because it also has expressions for proof terms.

(For technical reasons we have an `{\sf if-then-else}' construction in all three systems.
Therefore system {\xT} is not {\em really\/} ordinary first order logic, because it has something extra.
However this {\sf if-then-else} should not be considered to be an essential extension to the system.
It should be considered `syntactic sugar'.
We do not treat the relation between the systems with and without the {\sf if-then-else} in this
paper.
However we expect it to be unproblematic.)

Then for system {\xT} we introduce a notion of {\em domain conditions}.
This is a set of proof obligations that has to be satisfied to ensure that functions
are not applied outside their domain.
For example the domain conditions of division are such that:\label{dc-example-1}
$$\DC({1\over x-1} - {1\over x+1} = {2\over x^2-1}) =
  \{ \infer x-1\ne 0,\, \infer x+1\ne 0,\, \infer x^2-1\ne 0 \}$$
Now the main theorem that we prove consists of Propositions \ref{P-to-T} and \ref{T-to-P} below.
Together these state that:
\begin{quote}\em
A statement together with its domain conditions are provable in system {\xT} iff
that statement is provable in system {\xP}.
\end{quote}
This means that we can morally imagine ourselves as being in system {\xP}, while doing our proofs
and the presentation of the statements in system {\xT}, as long as we also prove the domain conditions.

The relation between the three systems is outlined in the following diagram:
\begin{center}
\begin{picture}(104,96)
%\put(0,0){\framebox(104,96){}}
\put(12,12){\makebox(0,0){\xT}}
\put(12,32){\makebox(0,0){$\cap$}}
\put(12,52){\makebox(0,0){\xD}}
\put(92,52){\makebox(0,0){\xP}}
\put(92,64){\line(0,1){7}}
\put(92,71){\line(-1,0){80}}
\put(12,71){\vector(0,-1){8}}
\put(52,85){\makebox(0,0){$|\cdot|$}}
\put(24,12){\line(1,0){7}}
\put(31,12){\line(0,1){40}}
\put(31,52){\vector(-1,0){8}}
\put(41,30){\makebox(0,0){*}}
\end{picture}
\end{center}
The $|\cdot|$ operation is called {\em erasure} (it is defined in Section \ref{section:erasure}).
It erases all proof terms from the expressions.
The $*$ operation is an auxiliary operation (as defined in Section \ref{section:star}) involved in the proof of the main theorem.
It lifts a {\xT} proof to a {\xD} analogue.

\subsection{Related work.}
There are many logics of partial terms, like Scott's E-logic \cite{sco:79,tro:dal:88}
and Beeson's LPT \cite{bee:85}.
See \cite{kup:94} for an overview of the field.
However our approach is not a logic of partial terms
because we do not allow undefined terms.
We think that $1/0$ should be {\em illegal}, and not just an undefined but legal expression.

Our paper integrates the type theoretical way to model partial functions
with the PVS approach of having correctness conditions on the side.
The type theoretical approach of having proof terms as an argument
to model partial functions
already dates from the Automath project (see \cite{ned:geu:vri:94} page 710).
For a discussion of type-correctness conditions in PVS, see \cite{sha:owr:99}.

The approach that we propose here is similar to the one implemented in the LAMBDA system
of Fourman \cite{fin:fou:lon:97},
where each function $f$ has an associated domain predicate \texttt{DOM'$f$}.
However there is a difference in spirit:
the LAMBDA system follows approach number 2
from the list on page \pageref{list},\footnote{%
\cite{fin:fou:lon:97}, p.~86:
`we regard a function application $f(x)$ as \emph{always defined}, but if $x$ is outside the intended domain of $f$, we will not be able to prove anything about its value.'}
while we follow approach number 3.
This is also apparent from the fact that in \cite{fin:fou:lon:97} the $\DC$ operation (called $<\!\!\!< \, >\!\!\!>$ there) only appears in axioms corresponding to function definitions, while in our approach it takes a much more central position.
%Also, the meta-theory of \cite{fin:fou:lon:97} is quite different from ours:
%they use a set-theoretic semantics, while we use proof theory.


\section{Examples}\label{section:examples}

We will now list some examples of partial functions and show how they are treated in the systems {\xT} and {\xP}.
Some of these functions occur in a proof of the fundamental
theorem of algebra in the Coq system \cite{geu:wie:zwa:00}.
The experiences we had in this `FTA project' was one of the motivations to write this paper.
\begin{itemize}
\item {\em Division}.
In system {\xT} the division operator
$x/y$
gets a domain condition that has to be proved to show that the expression is well-formed:
$$\DC(x/y) = \{ \infer y\ne 0 \}$$
In system {\xP} division becomes a ternary function:
$$\mbox{\sf div}(x,y,\alpha)$$
having three arguments $x$, $y$ and $\alpha$,
where $\alpha$ is a proof that $y\ne 0$.

This is an example of the general pattern.
In system {\xP}
all partial functions get one extra `domain' argument.
Therefore, in system {\xP} a function application
$f(x_1,\ldots,x_n)$
becomes
$f(x_1,\ldots,x_n,\alpha)$,
where $\alpha$ is a proof of $D_f(x_1,\ldots,x_n)$
with the predicate
$D_f$ representing the {\em domain\/} of the function $f$.

\item {\em Square root}. The domain condition of the real square root in system {\xT} is
$\DC(\!\sqrt{x}) = \{ \infer x\ge 0 \}$.
Again, in system {\xP} the square root function
$\mbox{\sf sqrt}(x,\alpha)$
has an extra argument,
where $\alpha$ is a proof of $x\ge 0$.

\item {\em Limit of a sequence}.
The domain conditions of the limit operation are in system {\xT}:
$$DC\big(\lim_{n\to\infty} a_n\big) = \{ \infer \mbox{the sequence $(a_n)$ converges} \,\}$$
In system {\xP} the limit operation becomes
$\mbox{\sf lim}(a,\alpha)$
where $a$ is a sequence and where $\alpha$ is a proof
that that sequence converges.

The natural way to express the limit operation in type theory is not first order, because the $a$ argument
is a function.
But the theory we present here is first order.
This means that this example should be considered in the context of set theory
(like in the Mizar system)
where one can talk about functions using a first order language.

\item {\em Function application in set theory}.
Set theory is untyped.
When one defines function application in it, it becomes a partial operation.
In set theory in the style of system {\xT}, function application would get the domain condition:
$$\DC(f(a)) = \{ \infer \mbox{$f$ is a function} \land a\in\mbox{\sf dom}\,f \}$$
Note that the $\mbox{\sf dom}$ function that occurs in this condition has a domain condition as well:\label{dc-example-2}
$$\DC(\mbox{\sf dom}\,f) = \{ \infer \mbox{$f$ is a relation} \}$$
In system {\xP} function application becomes ternary,
$\mbox{\sf apply}(f,a,\alpha)$,
where $\alpha$ is a proof of
`$\mbox{$f$ is a function} \land a\in\mbox{\sf dom}\,f$'.

\end{itemize}


\section{System {\xT}}\label{section:T}

We will now define the first of our three systems,
namely first order predicate logic
extended with an {\sf if-then-else} operation.

To define our systems we fix a signature with finitely many constant, function and predicate symbols:
\begin{itemize}
\item constant symbols $c_1,\ldots,c_k$
\item function symbols $f_1,\ldots,f_n$ with arities $a_1,\ldots,a_n$
\item predicate symbols $P_1,\ldots,P_m$ with arities $r_1,\ldots,r_m$
\end{itemize}
We also have variables:
\begin{itemize}
\item term variables $x_0,x_1,x_2,\ldots$
\item proof variables $h_0,h_1,h_2,\ldots$
\end{itemize}
(System {\xT} and {\xD} will only use term variables, but system {\xP} will also need proof variables.)

For each function symbol $f$ of arity $a$ there is a designated predicate symbol
$D_f$ (which is one of the $P_i$'s) that also has arity $a$.
$D_f$ is the predicate that represents the {\em domain\/} of the function $f$.
Note that this $D_f$ is not an extra-logical abbreviation of a formula:
it is a predicate {\em symbol}.

Constants could have been avoided by considering them to be nullary functions.
However in that case our main result (Proposition \ref{T-to-P} on page \pageref{T-to-P}) would not have been true.%
\footnote{This is shown by the following (pathological) case:
one function symbol $f$ of arity 0 with $D_f() \iff \bot$
and $\phi \equiv \exists x\sep \top$.
This $\phi$ can be derived in the {\xT}
system using witness $f()$, but it cannot be derived in the {\xP} system.
This shows that it is essential for our theory to have constants
$c_i$ without domain conditions.}

\medskip\noindent
System {\xT} has four kinds of expressions: terms, formulas, contexts and judgments.
These expressions are defined inductively as the smallest sets
$\TERM$, $\FORM$, $\CONT$ and $\JUDG$ satisfying:
\begin{eqnarray*}
\TERM & ::= &
  x_i \alt
  c_i \alt
  f_i(\TERM,\ldots,\TERM) \alt 
  (\IF \FORM \THEN \TERM \ELSE \TERM) \\
\FORM & ::= &
  \bot \alt
  P_i(\TERM,\ldots,\TERM) \alt
  \TERM=\TERM \alt
  (\FORM\to\FORM) \alt
  (\forall x_i\sep \FORM) \\
\CONT & ::= &
  \epsilon \alt
  \CONT,\,x_i \alt
  \CONT,\,\FORM \\
\JUDG & ::= &
  \CONT\infer\ok \alt
  \CONT\infer \TERM\wf \alt
  \CONT\infer \FORM\wf \alt
  \CONT\infer \FORM
\end{eqnarray*}
%
The four kinds of judgments mean respectively that the context is well-formed, that a term is well-formed,
that a formula is well-formed and that a formula is provable.

Finally, system {\xT} has the following set of derivation rules:
{\small
$$\rulexn{$\epsilon$-wf}{}{\epsilon\infer\ok}
\quad
\rulexn{decl-wf}{\Gamma\infer\ok}{\Gamma,\,x_i\infer\ok} %{x_i\not\in\Gamma}
\quad
\rulexn{assum-wf}{\Gamma\infer\phi\wf}{\Gamma,\,\phi\infer\ok}
\lmarg{\CONT}$$
$$\rulexnc{var-wf}{\Gamma\infer\ok}{\Gamma\infer x_i\wf}{x_i\in\Gamma}
\quad
\rulexn{const-wf}{\Gamma\infer\ok}{\Gamma\infer c_i\wf}
\lmarg{\TERM}$$
$$\rulexn{fun-wf}{\Gamma\infer t_1\wf \quad \cdots \quad \Gamma\infer t_{a_i}\wf\quad \Gamma\infer\ok}
  {\Gamma\infer f_i(t_1,\ldots,t_{a_i})\wf}$$
$$\rulexn{if-wf}{\Gamma\infer \phi\wf \quad \Gamma\infer t\wf \quad 
                        \Gamma\infer u\wf}
                       {\Gamma\infer (\IF\phi\THEN t
                                             \ELSE u)\wf}$$
$$\rulexn{$\bot$-wf}{\Gamma\infer\ok}{\Gamma\infer\bot\wf}
\quad
\rulexn{pred-wf}{\Gamma\infer t_1\wf \quad \cdots \quad \Gamma\infer t_{r_i}\wf \quad \Gamma\infer \ok}
  {\Gamma\infer P_i(t_1,\ldots,t_{r_i})\wf}
\lmarg{\FORM}$$
$$\rulexn{$\to$-wf}{\Gamma\infer\phi\wf\quad \Gamma\infer\psi\wf}
  {\Gamma\infer(\phi\to \psi)\wf}
\quad
\rulexn{$\forall$-wf}{\Gamma,\,x_i\infer\phi\wf}{\Gamma\infer(\forall x_i\sep \phi)\wf}$$
$$\rulexnc{assum}{\Gamma\infer\ok}{\Gamma\infer \phi}
               {\phi\in\Gamma}
\quad
\rulexn{raa}{\Gamma\infer \neg\neg\phi}
  {\Gamma\infer\phi}
\lmarg{\PROOF}$$
$$\rulexn{$\to$-I}{\Gamma,\,\phi\infer \psi}
      {\Gamma\infer(\phi\to \psi)}
\quad
\rulexn{$\to$-E}{\Gamma\infer (\phi\to \psi) \quad
 \Gamma\infer\phi}{\Gamma\infer\psi}$$
$$\rulexn{$\forall$-I}{\Gamma,\,x_i\infer \phi}
  {\Gamma\infer(\forall x_i\sep \phi)}
\quad
\rulexn{$\forall$-E}{\Gamma\infer (\forall x_i\sep \phi) \quad 
                \Gamma\infer t\wf}
               {\Gamma\infer\phi[x_i:=t]}$$
$$\rulexn{refl}{\Gamma\infer t\wf}{\Gamma\infer t=t}
\quad
\rulexn{sym}{\Gamma\infer t=u}
               {\Gamma\infer u=t}
\quad
\rulexn{trans}{\Gamma\infer t=u \quad \Gamma\infer u=v}
               {\Gamma\infer t=v}$$
$$\rulexn{$=$-fun}{\Gamma\infer t_1=t'_1 \quad \cdots \quad
                \Gamma\infer t_{a_i}=t'_{a_i} \quad \Gamma\infer \ok}
              {\Gamma\infer f_i(t_1,\ldots, t_{a_i}) = 
                             f_i(t'_1,\ldots, t'_{a_i})}$$
$$\rulexn{$=$-pred}{\Gamma\infer t_1=t'_1 \quad \cdots \quad
          \Gamma\infer t_{r_i}=t'_{r_i} \quad \Gamma\infer \ok}
               {\Gamma\infer
                             P_i(t_1,\ldots, t_{r_i}) \to
                             P_i(t'_1,\ldots, t'_{r_i})}$$
$$\rulexn{$=$-if-true}{\Gamma\infer \phi \quad \Gamma\infer t\wf \quad 
                            \Gamma\infer u\wf}
                       {\Gamma\infer
    (\IF\phi\THEN t \ELSE u)=t}$$
$$\rulexn{$=$-if-false}{\Gamma\infer \neg\phi \quad \Gamma\infer t\wf \quad 
                            \Gamma\infer u\wf}
                       {\Gamma\infer
    (\IF\phi\THEN t \ELSE u)=u}$$
}

\noindent
We identify expressions that are $\alpha$-equivalent.
Therefore we assume in these rules the Barendregt convention:
all variable names are as different as possible.

Logical operations have to be read as abbreviations from $\bot$, $\to$ and $\forall$:
\begin{eqnarray*}
\neg\phi &\equiv& \phi\to\bot\\
\phi\lor\psi &\equiv& \neg\phi\to\psi\\
\phi\land\psi &\equiv& \neg(\phi\to\neg\psi)\\
\phi\iff\psi &\equiv& (\phi\to\psi) \land (\psi\to\phi)
\end{eqnarray*}

\noindent
Some remarks about system {\xT}:
\begin{itemize}
\item
Our presentation of first order logic is slightly non-standard in that we have variables in the contexts that bind the
free variables in the terms and formulas.
Instead of `$x\ne 0 \infer 1/x\ne 0$' we write `$x,\, x\ne 0 \infer 1/x\ne 0$'.
We do this for aesthetic reasons.
It causes many well-formedness rules, but these are all trivial.
In system {\xT} well-formedness just means that all free variables occur in the context.
\item
The condition $\Gamma\infer\ok$ in the rules {\em fun-wf}, {\em pred-wf}, {\em $=$-fun\/}
and {\em $=$-pred\/} is needed for the case that $a_i = 0$ or $r_i = 0$.

\item
By symmetry of equality we can derive from rule {\em $=$-pred\/} the analogue rule with
equivalence instead of implication:
$$\rulexn{$=$-pred-iff}{\Gamma\infer t_1=t'_1 \quad \cdots \quad
          \Gamma\infer t_{r_i}=t'_{r_i} \quad \Gamma\infer \ok}
               {\Gamma\infer
                             P_i(t_1,\ldots, t_{r_i}) \iff
                             P_i(t'_1,\ldots, t'_{r_i})}$$
\item
It is possible to replace the rules {\em sym}, {\em trans}, {\em $=$-fun\/}
and {\em $=$-pred\/} by just one {\em substitution\/} rule:
$$\rulexn{$=$-subst}{\Gamma\infer t=u \quad \Gamma\infer\phi[x:=t]}
               {\Gamma\infer\phi[x:=u]}$$
However this rule does not generalize to systems {\xD} and {\xP}.
The term $t$ might satisfy domain conditions that $u$ does not.
\end{itemize}

\noindent
Our systems are non-standard because they have an {\sf if-then-else} construction,
which corresponds to the mathematical practice of definition by cases.
For example one can write
`$\IF x\ne 0 \THEN 1/x \ELSE 0$' as an expression.
The {\sf if-then-else} operator occurs in all three systems, {\xT}, {\xD} and {\xP}.

We would have preferred not to have this construction in our systems.
In that case system {\xT} would really have been ordinary first order logic.
However we need to have this construction to keep our definitions and proofs manageable.
We have tried to develop the theory without it, but it became too complex.

We believe that the {\sf if-then-else} is not essential to the systems.
The theorem to be proved for this is conservativity of the extended system over
the basic system:
\begin{quote}\em
If a judgment $\Gamma\infer\phi$ does not contain any {\sf if-then-else}s, then it is provable in
the system with {\sf if-then-else} iff it is provable in the system without {\sf if-then-else}.
\end{quote}
However we will not prove this theorem in this paper.

The {\sf if-then-else}s can be eliminated systematically from a formula by
replacing
$P[(\IF \phi \THEN t \ELSE u)]$
by
$(\phi\to P[t]) \land (\neg\phi\to P[u])$.
%The $t$ and $u$ might themselves contain {\sf if-then-else}s as well, so this
%elimination has to be iterated.
As an example
$(\IF x\ne 0 \THEN 1/x \ELSE 0)\cdot x = 1$
then becomes
$(x\ne 0 \to (1/x)\cdot x = 1) \land (x=0 \to 0\cdot x = 1)$.


\section{System {\xD}}\label{section:D}

The expressions of system {\xD} are exactly the same as the expressions of system {\xT}.
Only the set of rules is different.
We show the rules that differ from the corresponding rules in system
{\xT}:
\par\vspace{-\medskipamount}
{\small
$$\rulexn{fun-wf}{\Gamma\infer D_{f_i}(t_1,\ldots,t_{a_i})}
  {\Gamma\infer f_i(t_1,\ldots,t_{a_i})\wf}
\quad
\rulexn{if-wf}{\Gamma,\,\phi \infer t\wf \quad 
                        \Gamma,\,\neg\phi \infer u\wf}
                       {\Gamma\infer (\IF\phi\THEN t
                                             \ELSE u)\wf}
\lmarg{\TERM}$$
$$\rulexn{$\to$-wf}{\Gamma,\,\phi\infer\psi\wf}
  {\Gamma\infer(\phi\to \psi)\wf}
\lmarg{\FORM}$$
$$\rulexn{$=$-fun}{\begin{array}{c}
                \Gamma\infer t_1=t'_1 \quad \cdots \quad
                \Gamma\infer t_{a_i}=t'_{a_i} \\
                \Gamma\infer D_{f_i}(t_1,\ldots,t_{a_i}) \quad 
                \Gamma\infer D_{f_i}(t'_1,\ldots,t'_{a_i})
                \end{array}}
              {\Gamma\infer f_i(t_1,\ldots, t_{a_i}) = 
                             f_i(t'_1,\ldots, t'_{a_i})}
\lmarg{\PROOF}$$
$$\rulexn{$=$-if-true}{\Gamma\infer \phi \quad 
                        \Gamma,\,\phi \infer t\wf \quad 
                        \Gamma,\,\neg\phi \infer u\wf}
                       {\Gamma\infer
    (\IF\phi\THEN t \ELSE u)=t}$$
$$\rulexn{$=$-if-false}{\Gamma\infer \neg\phi \quad 
                        \Gamma,\,\phi \infer t\wf \quad 
                        \Gamma,\,\neg\phi \infer u\wf}
                       {\Gamma\infer
    (\IF\phi\THEN t \ELSE u)=u}$$
}

\noindent
The essential differences between systems {\xT} and {\xD} are the rules {\em fun-wf} and {\em $=$-fun}.
In system {\xD} you are only allowed to apply a function if you can prove that the
arguments are in its domain.

The other differences are not essential:
rules {\em if-wf}, {\em $\to$-wf}, {\em $=$-if-true\/} and {\em $=$-if-false}
in system {\xT} could have been the same as in system {\xD}.
(But not the other way around:
in system {\xD} these rules have to be the way they are.)
However we have chosen to use in system {\xT} the simpler variants of those rules.
The slight differences between systems {\xT} and {\xD} in this respect do not cause any problems in the proofs below.


\section{System {\xP}}\label{section:P}

The expressions of system {\xP} follow the same basic structure as the expressions of system {\xT} and {\xD}.
However there is an extra kind of expression $\PROOF$, for proof terms.
\begin{eqnarray*}
\TERM & ::= &
  x_i \alt
  c_i \alt
  f_i(\TERM,\ldots,\TERM,\PROOF) \alt
  (\IF\FORM\THEN \lambda h_i\sep \TERM \ELSE \lambda h_j\sep \TERM) \\
\FORM & ::= &
  \bot \alt
  P_i(\TERM,\ldots,\TERM) \alt
  \TERM=\TERM \alt
  (\Pi h_i:\FORM\sep \FORM) \alt
  (\forall x_i\sep \FORM) \\
\PROOF & ::= &
  h_i \alt
  (\lambda h_i:\FORM\sep \PROOF) \alt
  (\PROOF\PROOF) \alt
  (\lambda x_i\sep \PROOF) \alt
  (\PROOF \TERM) \\&& \alt
  \raa(\PROOF) \alt
  \refl(\TERM) \alt
  \sym(\PROOF) \alt
  \trans(\PROOF,\PROOF) \\&& \alt
  \eqfun(\PROOF,\ldots \PROOF,\PROOF,\PROOF) \alt
  \eqpred(i,\PROOF,\ldots \PROOF) \\&& \alt
  \IFTRUE(\PROOF,\lambda h_i\sep \TERM,\lambda h_j\sep \TERM) \alt
  \IFFALSE(\PROOF,\lambda h_i\sep \TERM,\lambda h_j\sep \TERM) \\
\CONT & ::= &
  \epsilon \alt
  \CONT,\,x_i \alt
  \CONT,\,h_i:\FORM \\
\JUDG & ::= &
  \CONT\infer\ok \alt
  \CONT\infer \TERM\wf \alt
  \CONT\infer\FORM\wf \alt
  \CONT\infer\PROOF:\FORM
\end{eqnarray*}
%
Here are the rules for system {\xP}.
They exactly parallel the rules for system {\xD}.
{\small
$$\rulexn{$\epsilon$-wf}{}{\epsilon\infer\ok}
\quad
\rulexn{decl-wf}{\Gamma\infer\ok}{\Gamma,\,x_i\infer\ok} %{x_i\not\in\Gamma}
\quad
\rulexn{assum-wf}{\Gamma\infer\phi\wf}{\Gamma,\,h_i:\phi\infer\ok}
                %{h_i\not\in\Gamma}
\lmarg{\CONT}$$
$$\rulexnc{var-wf}{\Gamma\infer\ok}{\Gamma\infer x_i\wf}{x_i\in\Gamma}
\quad
\rulexn{const-wf}{\Gamma\infer\ok}{\Gamma\infer c_i\wf}
\lmarg{\TERM}$$
$$\rulexn{fun-wf}{\Gamma\infer\alpha:D_{f_i}(t_1,\ldots,t_{a_i})}
  {\Gamma\infer f_i(t_1,\ldots,t_{a_i},\alpha)\wf}
\quad
\rulexn{if-wf}{\Gamma,\,h_i:\phi \infer t\wf \quad 
                        \Gamma,\,h_j:\neg\phi \infer u\wf}
                       {\Gamma\infer (\IF\phi\THEN \lambda h_i\sep t
                                             \ELSE \lambda h_j\sep u)\wf}$$
$$\rulexn{$\bot$-wf}{\Gamma\infer\ok}{\Gamma\infer\bot\wf}
\quad
\rulexn{pred-wf}{\Gamma\infer t_1\wf \quad \cdots \quad \Gamma\infer t_{r_i}\wf \quad \Gamma\infer \ok}
  {\Gamma\infer P_i(t_1,\ldots,t_{r_i})\wf}
\lmarg{\FORM}$$
$$\rulexn{$\Pi$-wf}{\Gamma,\,h_i:\phi\infer\psi\wf}
  {\Gamma\infer(\Pi h_i:\phi\sep \psi)\wf}
\quad
\rulexn{$\forall$-wf}{\Gamma,\,x_i\infer\phi\wf}{\Gamma\infer(\forall x_i\sep \phi)\wf}$$
$$\rulexnc{assum}{\Gamma\infer\ok}{\Gamma\infer h_i:\phi}
               {h_i:\phi\in\Gamma}
\quad
\rulexn{raa}{\Gamma\infer\alpha:\neg\neg\phi}
  {\Gamma\infer\raa(\alpha):\phi}
\lmarg{\PROOF}$$
$$\rulexn{$\Pi$-I}{\Gamma,\,h_i:\phi\infer\alpha:\psi}
      {\Gamma\infer(\lambda h_i:\phi\sep \alpha):(\Pi h_i:\phi\sep \psi)}
\quad
\rulexn{$\Pi$-E}{\Gamma\infer\alpha:(\Pi h_i:\phi\sep \psi) \quad
 \Gamma\infer\beta:\phi}{\Gamma\infer(\alpha\beta):\psi[h_i:=\beta]}$$
$$\rulexn{$\forall$-I}{\Gamma,\,x_i\infer\alpha:\phi}
  {\Gamma\infer(\lambda x_i\sep \alpha):(\forall x_i\sep \phi)}
\quad
\rulexn{$\forall$-E}{\Gamma\infer\alpha:(\forall x_i\sep \phi) \quad 
                \Gamma\infer t\wf}
               {\Gamma\infer(\alpha t):\phi[x_i:=t]}$$
$$\rulexn{refl}{\Gamma\infer t\wf}{\Gamma\infer\refl(t):t=t}
\quad
\rulexn{sym}{\Gamma\infer \alpha:t=u}
               {\Gamma\infer \sym(\alpha):u=t}$$
$$\rulexn{trans}{\Gamma\infer \alpha:t=u \quad \Gamma\infer \beta:u=v}
               {\Gamma\infer \trans(\alpha,\beta):t=v}$$
$$\rulexn{$=$-fun}{\begin{array}{c}
                \Gamma\infer \alpha_1:t_1=t'_1 \quad \cdots \quad
                \Gamma\infer \alpha_{a_i} : t_{a_i}=t'_{a_i} \\
                \Gamma\infer \beta:D_{f_i}(t_1,\ldots,t_{a_i}) \quad 
                \Gamma\infer \beta':D_{f_i}(t'_1,\ldots,t'_{a_i})
                \end{array}}
              {\Gamma\infer \eqfun(\alpha_1,\ldots \alpha_{a_i},\beta,\beta')
                           : f_i(t_1,\ldots, t_{a_i},\beta) = 
                             f_i(t'_1,\ldots, t'_{a_i},\beta')}$$
$$\rulexn{$=$-pred}{\Gamma\infer \alpha_1:t_1=t'_1 \quad \cdots \quad
          \Gamma\infer \alpha_{r_i} : t_{r_i}=t'_{r_i} \quad \Gamma\infer \ok}
               {\Gamma\infer \eqpred(i,\alpha_1,\ldots \alpha_{r_i}):
                             P_i(t_1,\ldots, t_{r_i}) \to
                             P_i(t'_1,\ldots, t'_{r_i})}$$
$$\rulexn{$=$-if-true}{\Gamma\infer \alpha : \phi \quad 
                        \Gamma,\,h_i:\phi \infer t\wf \quad 
                        \Gamma,\,h_j:\neg\phi \infer u\wf}
                       {\Gamma\infer
  \IFTRUE(\alpha,\lambda h_i\sep t,\lambda h_j\sep u) :
    (\IF\phi\THEN \lambda h_i\sep t
                            \ELSE \lambda h_j\sep u)=t[h_i:=\alpha]}$$
$$\rulexn{$=$-if-false}{\Gamma\infer \alpha : \neg\phi \quad 
                        \Gamma,\,h_i:\phi \infer t\wf \quad 
                        \Gamma,\,h_j:\neg\phi \infer u\wf}
                       {\Gamma\infer
  \IFFALSE(\alpha,\lambda h_i\sep t,\lambda h_j\sep u) :
    (\IF\phi\THEN \lambda h_i\sep t
                            \ELSE \lambda h_j\sep u)=u[h_j:=\alpha]}$$
}

\noindent
We will write $\Gamma\infer\phi$ if for some $\alpha$ we can derive that $\Gamma\infer\alpha:\phi$.
If $h_i$ does not occur in $\psi$ we write $\phi\to\psi$ for $\Pi h_i:\phi\sep\psi$ like before.

The expressions for the {\sf if-then-else} bind two proof variables:
one for the {\sf then} branch and one for the {\sf else} branch.
This is indicated by putting $\lambda$s in the {\sf if-then-else}, $\IFFALSE$ and $\IFTRUE$ expressions.
These $\lambda$s should not be confused with the $\lambda$-expressions that occur in the proof terms
of an implication or universally quantified formula,
which are introduced by the {\em $\Pi$-I\/} and {\em $\forall$-I\/} rules.

System {\xP} does not have a conversion rule.
Without a conversion rule the system does not satisfy the property of subject
reduction.
We do not think a conversion rule is relevant for our application.
We expect that adding a conversion rule will not affect the results from this paper.

Proof terms only occur as the final arguments of functions.


\section{Some properties of derivations}\label{section:properties}

The systems {\xT}, {\xD} and {\xP} are well behaved.
All three systems satisfy the following four propositions
(where ${\cal X}$ is
anything that can occur after a $\infer$):

\begin{proposition}
$\Gamma,\Gamma'\infer{\cal X}$ then with a shorter derivation $\Gamma\infer\ok$
\end{proposition}

\begin{proposition}
$\Gamma,\,\phi,\,\Gamma'\infer{\cal X}$ then with a shorter derivation $\Gamma\infer\phi\wf$
\end{proposition}

\begin{proposition}
$\Gamma\infer\phi$ implies $\Gamma\infer\phi\wf$.
\end{proposition}

\begin{proposition}[weakening]
$\Gamma\infer{\cal X}$ and $\Gamma,\Gamma'\infer\ok$ imply $\Gamma,\Gamma'\infer{\cal X}$.
\end{proposition}


\section{The domain conditions}\label{section:DC}

We now define the domain conditions of an expression.
For each system {\xT} expression (term, formula, judgment),
its domain conditions are a set of judgments that
state that in the expression no function is applied outside its domain.

Domain conditions are defined relative to a context $\Gamma$ which we put as a subscript
to the $\DC$ symbol.
\begin{itemize}
\item[\tick]\strut $\DC_{\Gamma} : \TERM\xxT \to \pow(\JUDG\xxT)$
\begin{itemize}
\item[]\strut $\DC_\Gamma(x_i) = \DC_\Gamma(c_i) = \emptyset$
\item[]\strut $\DC_\Gamma(f_i(t_1,\ldots,t_{a_i})) = \DC_\Gamma(t_1)\cup\ldots\cup\DC_\Gamma(t_{a_i})\cup
  \big\{\Gamma\infer\xxT D_{f_i}(t_1,\ldots,t_{a_i})\big\}\hspace{-1em}$
\item[]\strut $\DC_\Gamma(\IF \phi \THEN t \ELSE u) =
  \DC_\Gamma(\phi)\cup\DC_{\Gamma,\phi}(t)\cup\DC_{\Gamma,\neg\phi}(u)$
\end{itemize}
\item[\tick]\strut $\DC_{\Gamma} : \FORM\xxT \to \pow(\JUDG\xxT)$
\begin{itemize}
\item[]\strut $\DC_\Gamma(\bot) = \emptyset$
\item[]\strut $\DC_\Gamma(P_i(t_1,\ldots,t_{r_i})) =
  \DC_\Gamma(t_1)\cup\ldots\cup\DC_\Gamma(t_{r_i})$
\item[]\strut $\DC_\Gamma(t=u) = \DC(t)\cup\DC(u)$
\item[]\strut $\DC_\Gamma(\phi\to\psi) =
  \DC_\Gamma(\phi)\cup\DC_{\Gamma,\phi}(\psi)$
\item[]\strut $\DC_\Gamma(\forall x_i\sep\phi) = \DC_{\Gamma,x_i}(\phi)$
\end{itemize}
\item[\tick]\strut $\DC : \CONT\xxT \to \pow(\JUDG\xxT)$
\begin{itemize}
\item[]\strut $\DC(\epsilon) = \emptyset$
\item[]\strut $\DC(\Gamma,\,x_i) = \DC(\Gamma)$
\item[]\strut $\DC(\Gamma,\,\phi) = \DC(\Gamma)\cup\DC_\Gamma(\phi)$
\end{itemize}
\end{itemize}
Domain conditions are asymmetric in some of the propositional connectives.
Therefore, although system {\xT} is just first order logic,
the domain conditions do not respect logical equivalence.
For instance:
$$\DC(\phi\land\psi) \ne \DC(\psi\land\phi)$$
In the first case
$\phi\land\psi \equiv \neg(\phi\to\neg\psi)$
and we can use $\phi$ for proving the domain conditions of $\psi$,
while in the second case
$\psi\land\phi \equiv \neg(\psi\to\neg\phi)$
so in that case we can {\em not\/} use $\phi$ for the domain conditions of $\psi$.
As an example the domain conditions of
$(x\ne 0) \land P[1/x]$
might be provable
because we can use $x\ne 0$ to prove the domain conditions of $P[1/x]$,
but the domain conditions of
$P[1/x] \land (x\ne 0)$
might not be provable because in that case we have to prove the domain conditions
of $P[1/x]$ without the benefit of $x\ne 0$.
In this sense the $\land$ connective in system {\xT} behaves like the
\verb|&&| operator of the C programming language.

\medskip\noindent
The predicate symbol $D_f$ is a {\em symbol\/} that {\em represents\/} the domain of the function $f$.
To give this symbol a meaning we have to have an equivalence in the context.
For instance
$D_/(x,y)$
is the definedness predicate of the division.
It should be equivalent to $y\ne 0$.
This means that we have to imagine that we are reasoning in a context:
$$\Gamma \equiv \ldots,\,\mbox{\em theory of division including \/}\,\forall x,y\sep(D_/(x,y)\iff y\ne 0),\,\ldots$$
The domain condition for division is:
$\DC(x/y) = \{ \infer D_/(x,y) \}$.
This domain condition is equivalent to $y\ne 0$ in the proper context but it is not identical to it.
(So actually in
the examples on pages \pageref{dc-example-1}--\pageref{dc-example-2}
we were not completely correct.
We `cheated' there for the sake of the presentation.)


\section{The erasure: from {\xP} to {\xT}}\label{section:erasure}

The erasure operation $|\cdot|$ erases all proof terms from expressions.
It maps system {\xP} expressions to system {\xT}.
In such an erased expression all domain conditions hold.
This is the easy direction of our main result.
\begin{itemize}
\item[\tick]\strut $|\cdot| : \TERM\xxP \to \TERM\xxT$
\begin{itemize}
\item[]\strut $|x_i| = x_i \quad |c_i| = c_i$
\item[]\strut $|f_i(t_1,\ldots,t_{a_i},\alpha)| = f_i(|t_1|,\ldots,|t_{a_i}|)$
\item[]\strut $|(\IF\phi\THEN \lambda h_i\sep t \ELSE \lambda h_j\sep u)| =
  (\IF |\phi| \THEN |t| \ELSE |u|)$
\end{itemize}
\item[\tick]\strut $|\cdot| : \FORM\xxP \to \FORM\xxT$
\begin{itemize}
\item[]\strut $|\bot| = \bot$
\item[]\strut $|P_i(t_1,\ldots,t_{r_i})| = P_i(|t_1|,\ldots,|t_{r_i}|)$
\item[]\strut $|t=u| = |t|=|u|$
\item[]\strut $|(\Pi h_i:\phi\sep \psi)| = (|\phi|\to|\psi|)$
\item[]\strut $|(\forall x_i\sep \phi)| = (\forall x_i\sep |\phi|)$
\end{itemize}
\item[\tick]\strut $|\cdot| : \CONT\xxP \to \CONT\xxT$
\begin{itemize}
\item[]\strut $|\epsilon| = \epsilon$
\item[]\strut $|\Gamma,\,x_i| = |\Gamma|,\,x_i$
\item[]\strut $|\Gamma,\,h_i:\phi| = |\Gamma|,\,|\phi|$
\end{itemize}
\end{itemize}

\begin{proposition}\label{erasure-subst}
~\begin{itemize}
\item[] $|t[x_i:=u]| \equiv |t|[x_i:=|u|]$.
\item[] $|\phi[x_i:=u]| \equiv |\phi|[x_i:=|u|]$.
\item[] $|t[h_i:=\alpha]| \equiv |t|$.
\item[] $|\phi[h_i:=\alpha]| \equiv |\phi|$.
\end{itemize}
\end{proposition}
\begin{proof}
Simultaneous induction on the structure of $t$ and $\phi$.
\end{proof}

\begin{proposition}[from {\xP} to {\xD}]\label{P-to-D}
~\begin{itemize}
\item[] $\Gamma\infer\xxP \ok$ implies $|\Gamma|\infer\xxD \ok$.
\item[] $\Gamma\infer\xxP t\wf$ implies $|\Gamma|\infer\xxD |t|\wf$.
\item[] $\Gamma\infer\xxP \phi\wf$ implies $|\Gamma|\infer\xxD |\phi|\wf$.
\item[] $\Gamma\infer\xxP \phi$ implies $|\Gamma|\infer\xxD |\phi|$.
\end{itemize}
\end{proposition}
\begin{proof}
Simultaneous induction on the size of the derivation in system {\xP}.
\end{proof}

\begin{proposition}\label{strengthen-wf}
~\begin{itemize}
\item[] $\Gamma,\,\phi\infer\xxT t\wf$ implies $\Gamma\infer\xxT t\wf$.
\item[] $\Gamma,\,\phi\infer\xxT \psi\wf$ implies $\Gamma\infer\xxT \psi\wf$.
\end{itemize}
\end{proposition}
\begin{proof}
Well-formedness in system {\xT} just checks whether all free variables are in the context.
Removing assumptions from the context does not affect that.
\end{proof}

\begin{proposition}[from {\xD} to {\xT}]\label{D-to-T}
~\begin{itemize}
\item[] $\Gamma\infer\xxD \ok$ implies $\Gamma\infer\xxT \ok$
  and $\DC(\Gamma)$.
\item[] $\Gamma\infer\xxD t\wf$ implies $\Gamma\infer\xxT t\wf$
  and $\DC(\Gamma)$ and $\DC_\Gamma(t)$.
\item[] $\Gamma\infer\xxD \phi\wf$ implies $\Gamma\infer\xxT \phi\wf$
  and $\DC(\Gamma)$ and $\DC_\Gamma(\phi)$.
\item[] $\Gamma\infer\xxD \phi$ implies $\Gamma\infer\xxT \phi$
  and $\DC(\Gamma)$ and $\DC_\Gamma(\phi)$.
\end{itemize}
\end{proposition}
\begin{proof}
Simultaneous induction on the size of the derivation in system {\xD} using Proposition \ref{strengthen-wf}
for the {\it $\to$-wf}, {\it if-wf}, {\it $=$-if-true\/} and {\it $=$-if-false\/} rules.
\end{proof}

\begin{proposition}[main correspondence theorem from {\xP} to {\xT}]\label{P-to-T}
$\Gamma\infer\xxP \phi$ implies $|\Gamma|\infer\xxT |\phi|$
  and $\DC(|\Gamma|)$ and $\DC_{|\Gamma|}(|\phi|)$.
\end{proposition}
\begin{proof}
Propositions \ref{P-to-D} and \ref{D-to-T} combined.
\end{proof}


\section{The * operation: from {\xT} to {\xD}}\label{section:star}

Consider a statement for which the domain conditions hold.
A system {\xT} proof of this statement and a system {\xD} proof of the same statement
are different things.
In the first case, although the domain conditions of the statement are satisfied, the {\em proof\/} might violate some domain conditions
(for instance, it might reason about $1/0$ as a number).
But in the second case the domain conditions have to hold {\em in all steps} of the proof.
We will show that despite this difference
these two kinds of provability are equivalent (this is Proposition \ref{T-to-D-2} below).
For this we will use the $*$ operation.

The $*$ operation maps system {\xT} to system {\xD}.
It makes the partial functions total by setting them to the constant $c_1$ outside their domain.
Then system {\xT} proofs are interpreted in system {\xD} as talking about these `extended' functions.
\begin{itemize}
\item[\tick] $\cdot^* : \TERM\xxT \to \TERM\xxD$
\begin{itemize}
\item[] ${x_i}^* = x_i \quad {c_i}^* = c_i$
\item[] ${f_i(t_1,\ldots,t_{a_i})}^* =
  (\IF D_{f_i}({t_1}^*,\ldots,{t_{a_i}}^*) \THEN f_i({t_1}^*,\ldots,{t_{a_i}}^*) \ELSE c_1)$
\item[] ${(\IF\phi\THEN t \ELSE u)}^* =
  (\IF {\phi}^* \THEN {t}^* \ELSE {u}^*)$
\end{itemize}
\item[\tick] $\cdot^* : \FORM\xxT \to \FORM\xxD$
\begin{itemize}
\item[] ${\bot}^* = \bot$
\item[] ${P_i(t_1,\ldots,t_{r_i})}^* = P_i({t_1}^*,\ldots,{t_{r_i}}^*)$
\item[] ${(t=u)}^* = t^*=u^*$
\item[] ${(\phi\to \psi)}^* = ({\phi}^*\to{\psi}^*)$
\item[] ${(\forall x_i\sep \phi)}^* = (\forall x_i\sep {\phi}^*)$
\end{itemize}
\item[\tick] $\cdot^* : \CONT\xxT \to \CONT\xxD$
\begin{itemize}
\item[] ${\epsilon}^* = \epsilon$
\item[] ${(\Gamma,\,x_i)}^* = {\Gamma}^*,\,x_i$
\item[] ${(\Gamma,\,\phi)}^* = {\Gamma}^*,\,{\phi}^*$
\end{itemize}
\end{itemize}

\begin{proposition}\label{D-eq-1a}
~\begin{itemize}
\item[] $\Gamma\infer\xxD t\wf$ implies $\Gamma\infer\xxD t=t^*$.
\item[] $\Gamma\infer\xxD \phi\wf$ implies $\Gamma\infer\xxD \phi\iff\phi^*$.
\end{itemize}
\end{proposition}
\begin{proof}
Simultaneous induction on the structure of $t$ and $\phi$.
\end{proof}

\begin{proposition}\label{D-eq-2a}
$\Gamma\infer\xxD \ok$ implies that $\Gamma\infer\xxD \phi$ iff $\Gamma^*\infer\xxD \phi$.
\end{proposition}
\begin{proof}
Induction on the structure of $\Gamma$ using the second part of Proposition \ref{D-eq-1a}.
\end{proof}

\begin{proposition}\label{T-to-D-1}
~\begin{itemize}
\item[] $\Gamma\infer\xxT \ok$ implies $\Gamma^*\infer\xxD \ok$.
\item[] $\Gamma\infer\xxT t\wf$ implies $\Gamma^*\infer\xxD t^* \wf$.
\item[] $\Gamma\infer\xxT \phi\wf$ implies $\Gamma^*\infer\xxD \phi^*\wf$.
\item[] $\Gamma\infer\xxT \phi$ implies $\Gamma^*\infer\xxD \phi^*$.
\end{itemize}
\end{proposition}
\begin{proof}
Simultaneous induction on the size of the derivation in system {\xT}
using the previous two propositions.
\end{proof}

\begin{proposition}\label{D-eq-1}
~\begin{itemize}
\item[] $\Gamma\infer\xxD\ok$ and $\DC_\Gamma(t)$ imply $\Gamma\infer\xxD t=t^*$.
\item[] $\Gamma\infer\xxD\ok$ and $\DC_\Gamma(\phi)$ imply $\Gamma\infer\xxD \phi\iff\phi^*$.
\end{itemize}
\end{proposition}
\begin{proof}
Simultaneous induction on the structure of $t$ and $\phi$.
\end{proof}

\begin{proposition}\label{D-eq-2}
$\DC(\Gamma)$ implies that $\Gamma\infer\xxD \phi$ iff $\Gamma^*\infer\xxD \phi$.
\end{proposition}
\begin{proof}
Induction on the structure of $\Gamma$ using the second part of Proposition \ref{D-eq-1}.
\end{proof}

\begin{proposition}\label{T-to-D-2}
$\DC(\Gamma)$ and $\DC_\Gamma(\phi)$ and $\Gamma\infer\xxT \phi$ imply $\Gamma\infer\xxD \phi$.
\end{proposition}
\begin{proof}
Assume $\DC(\Gamma)$, $\DC_\Gamma(\phi)$ and $\Gamma\infer\xxT \phi$.
Then $\Gamma^*\infer\xxD \phi^*$ by Proposition \ref{T-to-D-1} and
then $\Gamma\infer\xxD \phi^*$ by Proposition \ref{D-eq-2} and
therefore $\Gamma\infer\xxD \phi$ by the second part of Proposition \ref{D-eq-1}.
\end{proof}


\section{From {\xD} to {\xP}}\label{section:D-to-P}

In the previous section we got from {\xT} to {\xD}.
Now we show how to get from {\xD} to {\xP}.
To `fill in' the proof objects in a system {\xD} proof we need a property called {\em proof irrelevance}.
It says that a {\xP} expression does not change its meaning
if we replace proof terms in it with
different proofs of the same statements.
This is stated `locally' in the {\em $=$-fun\/} rule of system {\xP}:
$$\rulex{\begin{array}{c}
                \Gamma\infer t_1=t'_1 \quad \cdots \quad
                \Gamma\infer t_{a_i}=t'_{a_i} \\
                \Gamma\infer \beta:D_{f_i}(t_1,\ldots,t_{a_i}) \quad 
                \Gamma\infer \beta':D_{f_i}(t'_1,\ldots,t'_{a_i})
                \end{array}}
              {\Gamma\infer f_i(t_1,\ldots, t_{a_i},\beta) = 
                             f_i(t'_1,\ldots, t'_{a_i},\beta')}$$
The two terms are equal despite the proof terms $\beta$ and $\beta'$ being different.
But the property of proof irrelevance is also true `globally':

\begin{proposition}[proof irrelevance]\label{P-eq}
~\begin{itemize}
\item[] $\Gamma \infer\xxP t \wf$ and $\Gamma \infer\xxP t' \wf$ and $|t|\equiv |t'|$ imply $\Gamma \infer\xxP t=t'$.
\item[] $\Gamma \infer\xxP \phi \wf$ and $\Gamma \infer\xxP \phi' \wf$ and $|\phi|\equiv |\phi'|$ imply $\Gamma \infer\xxP \phi\iff\phi'$.
\end{itemize}
\end{proposition}
\begin{proof}
Simultaneous induction on the size of $|t|$ and $|\phi|$ using Proposition
\ref{erasure-subst} and the
{\it $=$-fun}, {\it $=$-pred}, {\it $=$-if-true\/} and {\it $=$-if-false\/} rules.
\end{proof}

\noindent
Once we have proof irrelevance, getting a system {\xP} derivation from a system {\xD} derivation is straightforward.
Together with the earlier propositions this then allows us to prove the main result of this paper.

\begin{proposition}\label{D-to-P}
If $\Gamma\infer\xxP \ok$ then:
\begin{itemize}
\item[] $|\Gamma|\infer\xxD t'\wf$ imply that there exists a $t$ with $|t|\equiv t'$ such that $\Gamma\infer\xxP t\wf$.
\item[] $|\Gamma|\infer\xxD \phi'\wf$ imply that there exists a $\phi$ with $|\phi|\equiv\phi'$ such that $\Gamma\infer\xxP \phi\wf$.
\item[] $|\Gamma|\infer\xxD \phi'$ imply that there exists a $\phi$ with $|\phi|\equiv\phi'$ such that $\Gamma\infer\xxP \phi$.
\end{itemize}
\end{proposition}
\begin{proof}
Simultaneous induction on the size of the derivation in system {\xD} using Propositions
\ref{erasure-subst} and \ref{P-eq}.
\end{proof}

\begin{proposition}[main correspondence theorem from {\xT} to {\xP}]\label{T-to-P}
$\Gamma\infer\xxP \ok$ and $|\Gamma|\infer\xxT \phi'$ and $\DC_{|\Gamma|}(\phi')$ imply that there exists a $\phi$ with $|\phi|\equiv\phi'$ such that $\Gamma\infer\xxP \phi$.
\end{proposition}
\begin{proof}
Assume $\Gamma\infer\xxP\ok$, $|\Gamma|\infer\xxT\phi'$ and $\DC_{|\Gamma|}(\phi')$.
Then $\DC(|\Gamma|)$ by Proposition \ref{P-to-T} and
then $|\Gamma|\infer\xxD \phi'$ by Proposition \ref{T-to-D-2} and
therefore there exists a suitable $\phi$ by Proposition \ref{D-to-P}.
\end{proof}

\begin{proposition}[corollary]\label{T-to-P-2}
$\Gamma'\infer\xxT\phi'$ and $\DC(\Gamma')$ and $\DC_{\Gamma'}(\phi')$ imply
that there exist $\Gamma$ and $\phi$ with $|\Gamma|\equiv\Gamma'$ and $|\phi|\equiv\phi'$
such that $\Gamma\infer\xxP\phi$.
\end{proposition}
\begin{proof}
$\Gamma'\infer\xxD\phi'$ by Proposition \ref{T-to-D-2}, from which $\Gamma'\infer\xxD\ok$.
Then $\Gamma'\infer\xxD\ok$ implies that there exists a $\Gamma$ with $|\Gamma|\equiv\Gamma'$ such that $\Gamma\infer\xxP\ok$, by induction on the structure of $\Gamma'$
using Proposition \ref{D-to-P}.
Finally we get $\phi$ from Proposition \ref{T-to-P}.
\end{proof}


\section{Conclusion}

The main things left to be done are:
\begin{enumerate}
\item
Prove the systems with {\sf if-then-else} conservative over the same systems without this construction.

\item
Build a proof assistant that implements the approach of reasoning
in system~{\xT} with domain conditions, to study how well it works in practice.

\item
Investigate whether the theory from this paper extends to higher order logic.

\end{enumerate}


\paragraph{Acknowledgments.}
Thanks to Herman Geuvers, Paula Severi and Venanzio Cap\-retta for stimulating discussions.
Thanks to Gilles Barthe for the idea of how to fit this paper in 16 pages.
Thanks to the anonymous referees for valuable comments.

{
\hbadness=1776

\begin{thebibliography}{10}

\bibitem{bee:85}
M.J. Beeson.
\newblock {\em Foundations of constructive mathematics}.
\newblock Springer-Verlag, 1985.

\bibitem{con:all:bro:cle:cre:har:how:kno:men:pan:sas:smi:86}
Robert~L. Constable, Stuart~F. Allen, H.M. Bromley, W.R. Cleaveland, J.F.
  Cremer, R.W. Harper, Douglas~J. Howe, T.B. Knoblock, N.P. Mendler,
  P.~Panangaden, James~T. Sasaki, and Scott~F. Smith.
\newblock {\em Implementing Mathematics with the {N}uprl Development System}.
\newblock Prentice-Hall, NJ, 1986.

\bibitem{fin:fou:lon:97}
Simon Finn, Michael Fourman, and John Longley.
\newblock {Partial Functions in a Total Setting}.
\newblock {\em Journal of Automated Reasoning}, 18:85--104, 1997.

\bibitem{geu:wie:zwa:00}
H.~Geuvers, F.~Wiedijk, and J.~Zwanenburg.
\newblock {Equational Reasoning via Partial Reflection}.
\newblock In {\em Theorem Proving in Higher Order Logics, 13th International
  Conference, TPHOLs 2000}, volume 1869 of {\em LNCS}, pages 162--178, Berlin,
  Heidelberg, New York, 2000. Springer Verlag.

\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{gut:tha:93}
J.D. Guttman and F.J. Thayer.
\newblock {IMPS: An Interactive Mathematical Proof System}.
\newblock {\em Journal of Automated Reasoning}, 11:213--248, 1993.

\bibitem{har:95:1}
John Harrison.
\newblock {Re: Undefined terms}.
\newblock Message \url{<"swan.cl.cam.:266770:950519095422"@cl.cam.ac.uk>} as
  sent to the QED mailing list,
  \url{<http://www.ftp.cl.cam.ac.uk/ftp/hvg/qed-project-archive/03xx/0380>},
  1995.

\bibitem{kau:man:moo:00}
Matt Kaufmann, Panagiotis Manolios, and J.~Strother Moore.
\newblock {\em Computer-Aided Reasoning: An Approach}.
\newblock Kluwer Academic Publishers, Boston, 2000.

\bibitem{kup:94}
J.~Kuper.
\newblock {\em Partiality in Logic and Computation -- Aspects of
  Undefinedness}.
\newblock PhD thesis, University of Twente, Dept INF, Enschede, The
  Netherlands, 1994.

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

\bibitem{ned:geu:vri:94}
R.P. Nederpelt, J.H. Geuvers, and R.C. de~Vrijer.
\newblock {\em Selected Papers on Automath}, volume 133 of {\em Studies in
  Logic and the Foundations of Mathematics}.
\newblock Elsevier Science, Amsterdam, 1994.

\bibitem{nip:pau:wen:02}
T.~Nipkow, L.C. Paulson, and M.~Wenzel.
\newblock {\em Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  volume 2283 of {\em LNCS}.
\newblock Springer, 2002.

\bibitem{owr:rus:sha:92}
S.~Owre, J.~Rushby, and N.~Shankar.
\newblock {PVS: A prototype verification system}.
\newblock In D.~Kapur, editor, {\em 11th International Conference on Automated
  Deduction (CADE)}, volume 607 of {\em LNAI}, pages 748--752, Berlin,
  Heidelberg, New York, 1992. Springer-Verlag.

\bibitem{sco:79}
D.S. Scott.
\newblock {Identity and existence in intuitionistic logic}.
\newblock In M.P. Fourman, C.J. Mulvey, and D.S. Scott, editors, {\em
  Applications of Sheaves}, volume 753 of {\em Lecture Notes in Mathematics},
  pages 660--696, Berlin, 1979. Springer-Verlag.

\bibitem{sha:owr:99}
Natarajan Shankar and Sam Owre.
\newblock {Principles and Pragmatics of Subtyping in {PVS}}.
\newblock In Didier Bert, Christine Choppy, and Peter Mosses, editors, {\em
  {Recent Trends in Algebraic Development Techniques, {WADT '99}}}, volume 1827
  of {\em LNCS}, pages 37--52, Toulouse, France, September 1999.
  Springer-Verlag.

\bibitem{coq:02}
{The Coq Development Team}.
\newblock {\em The Coq Proof Assistant Reference Manual}, 2002.
\newblock
  \url{<ftp://ftp.inria.fr/INRIA/coq/current/doc/Reference-}\penalty100%
  \url{Manual-}\penalty100\url{all.ps.gz>}.

\bibitem{tro:dal:88}
A.~Troelstra and D.~van Dalen.
\newblock {\em Constructivism in Mathematics, an Introduction, Vols.~1-2},
  volume 121 and 123 of {\em Studies in Logic and The Foundations of
  Mathematics}.
\newblock North-Holland, 1988.

\bibitem{wos:96}
L.~Wos.
\newblock {\em The Automation of Reasoning: An Experimenter's Notebook with
  Otter Tutorial}.
\newblock Academic Press, New York, 1996.

\end{thebibliography}
}

\end{document}