
\section{Exclusivity in Horn Logic}
\label{sec:temp}

Uniform proofs judgments:
\[
\begin{array}{ll}
\sp G & \mbox{Program $\cP$ uniformly entails $G$}\\
\sp D \imm Q & \mbox{Clause  $D$ immediately entails atom $Q$ under 
$\cP$}
\end{array}
\]

\begin{figure}[htbp]
\label{fig:sf}
\[
\begin{array}{c}
% |-
% \ianc{}{}\ga\sp\top}{\top}\qquad\ianc{}{\gna\fp \perp}{S^{\nvd}_\perp}\vsk
% ADD top and bot to G's ????
\ianc{\vM = \vN}{\ga\sp \vM \eqd \vN}{\vd \eqd}\qquad
\ianc{\vM \not = \vN}{\ga\sp \vM \neqd \vN}{ \vd \neqd}\vsk
\ibnc{\ga\sp G_1}{\ga\sp G_{2}}{\ga\sp G_{1}\And G_{2}}{ \vd\And}
\vsk
\ianc{\ga\sp G_1}{\ga\sp G_{1}\Or G_{2}}{ \vd \Or_1}
\qquad
\ianc{\ga\sp G_1}{\ga\sp G_{1}\Or G_{2}}{ \vd \Or_2}
\vsk
\ibnc{D\in\cP}{ \ga\sp D \imm Q}{\ga\sp Q}{ \vd  {\rm atm}}\vsk
% \ianc{ \cP,G_{1}\vd_{u} G_{2}}{\cP\vd_{u} G_{1}\Imp G_{2}}{ \vd\Imp}
% \qquad
% \ianc{\cP\vd_{u} [a/x]G}{\cP\vd_{u}\Pi x. G}{ \vd\Pi^{*}}\vsk 

% immediate >>
\ianc{}{\ga\sp\perp_q\imm  Q}{\imm\perp}\qquad \mbox{\textrm{no rule for
     }} \top_q\vsk
%\ianc{\vN = \vM}{\ga\sp q\ \vN \imm q\ \vM}{\imm \rm atm}}\qquad
\ianc{\mbox{for some $t\oftp A$} \ \ga\sp  [t/x]D \imm Q}{\ga\sp
  \PIXA D \imm Q}{\imm\Pi}\vsk
\ianc{\ga\sp D_{1}\imm Q}{\ga\sp D_{1}\And D_{2}\imm
  Q}{\imm \And_1}\qquad
\ianc{\ga\sp D_{2}\imm Q}{\ga\sp D_{1}\And D_{2}\imm
  Q}{\imm \And_2}
\vsk
\ibnc{\ga\sp D_{1}\imm Q}{ \ga\sp D_{2}\imm Q}{\ga\sp D_{1}\tensor
  D_{2}\imm Q}{\imm\tensor}\vsk
%\ianc{\sp G}{ \ga\sp (G\Imp Q) \imm Q}{\imm\Imp}
%\vsk
\ibnc{\ga\sp \vN\eqd\vM}{\ga\sp G}{\ga\sp (G\Imp q\ \vN) \imm q\ \vM}{\imm \Imp}
\end{array}
\]
\caption{Provability  in Horn logic without existentials}
\end{figure}

We use $\gna\snp (G)$ for $\mnotg(G) = G'$ and $\gna\sn G'$; 
similarly $\gna\sn\mnotd (D)\imm\neg Q$ for $\mnotd(D) = D'$ and $\gna\sn D'\imm\neg
Q$.

\begin{Theorem}[Exclusivity] It is not the case that both
$\ga\spp G$ and $ \gna\snp (G)$.
\end{Theorem}
\begin{proof}
We generalize this to:
\ben
\item
It is not the case that there is $\SP ::  \ga\spp G$ and there is $\SM :: \gna\snp ( G)$.
\item
 It is not the case that there are
proofs $\IP,\IM$, a well-typed substitution $\q$ and clause $D$ such that
$\IP :: \ga\spp \q D \imm Q$ and
$\IM :: \gna\sn\mnotd(D) \imm \neg Q$.
\enen
We proceed by mutual induction on the structure of $\IP,\IM$ and $\SP,\SM$,
by assuming the existence of the latter and deriving the absurdum. Fix
a generic $\q$:
\bit
\itc
$\q\top_Q=\top_Q$ and $\mnotd(\top_Q)=\perp_Q$:
$$\IM=\ianc{}{\perp_Q\imm \neg Q}{\imm At}$$
But there is no proof of $Q$ from $\top_Q$.
\itc
$$\IP=\ianc{\ga\spp G}{\ga\spp (q\ \vM\If G)\imm q\ \vM}{\imm\Imp}$$
and
$\IM$ ends in $\gna\sn \mnotd (q\ \vM\If G)\imm \neg q\
\vM$, where $\q\vM=\vM$.
\btab
$\ga\spp G$\bv
% $\gna\sn (\neg q\ \vM_1\If \mnotg(G))\imm \neg q\ \vM_2$\br\\
$\gna\sn \BAnd_{\vN\in
        \cdot\vd\mnot(\vM)}\Pi( \neg (q\ \vN)\If \top) \And  \neg (q\ \vM)\If
      \mnotg(G)\imm \neg q\ \vM$\\
\br\\
\etab
\bit
\item[Subcase right]
\btab
$\gna\sn\neg (q\ \vM)\If
      \mnotg(G)\imm \neg q\ \vM$\br\\
$\gna\snp (G)$\br\\
$\perp$\bi $2$\\
\etab
\item[Subcase left]
\btab
$\gna\sn \BAnd_{\vN\in
        \cdot\vd\mnot(\vM)}\Pi( \neg (q\ \vN)\If \top)\imm\neg q\
      \vM$\br\\
$\sigma(\neg q\ \vN)\If\top_q\imm \neg q\ \vM$\` for some $\sigma$ and
some $\vN\in\mnot(\vM)$ By rule\\
$\sigma\vN\eqd\vM$ and thus $\vM\in\|\vN\|$\br\\
$\perp$\` By the Partition Lemma
\etab
\enit
\itc %imm\tensor
$$\IP= \ibnc{\ga\sp\q D_{1}\imm Q}{\ga\sp\q D_{2}\imm Q}{\ga\sp\q (D_{1}\tensor
  D_{2})\imm Q}{\imm\tensor}$$
and $\IM$ ends in $\gna\sn\mnotd (D_{1}\tensor
  D_{2})\imm \neg Q$
\btab
 $\ga\spp \q D_1\imm Q$ \bv
$\ga\spp \q D_2\imm Q$\bv
$\gna\sn \mnotd (D_1)\And\mnotd (D_2)\imm\neg Q$\br\\
$\gna\sn \mnotd (D_i)\imm\neg Q$\br\\
$\perp$\bi $2$
\etab
\itc%And
$$\IP= \ianc{\ga\sp\q D_{i}\imm Q}{\ga\sp\q (D_{1}\And
  D_{2})\imm Q}{\imm\And}$$
and $\IM$ ends in $\gna\sn\mnotd (D_{1}\And
  D_{2})\imm \neg Q$
\btab
 $\ga\spp \q D_i\imm Q$ \bv
$\gna\sn \mnotd (D_1)\imm\neg Q$\br\\
$\gna\sn \mnotd (D_2)\imm\neg Q$\br\\
$\perp$\bi $2$
\etab
\itc %\Pi imm
$$\IP= \ibnc{%\GG\vd t\hastype A
}{ \ga\spp ([t/x]\cdot \q) D \imm Q}{\ga\spp\q\PI
 { x}{A}D \imm Q}{\imm\Pi}$$
and $\IM$ ends in $\mnotd(\PI{x}{A}D)\imm\neg Q$.
\btab
$\ga\spp ([t/x]\cdot\q) D\imm Q$\bv
$\gna\sn \mnotd(D)\imm\neg Q$\br\\
$\perp$\bi $2$\\
\etab

%start \vd G
\itc
$$\SP=\ibnc{D\in\cP^+}{ \ga\spp D \imm Q}{\ga\spp Q}{ \vd  {\rm atm}}$$
and $\SM$ ends in $\gna\snp (Q)$
\btab
$\ga\spp D\imm Q$\bv
$\ga\spp \q D\imm Q$\` for some $\q$\\
$\gna\sn\neg Q$\br\\
$\gna\sn\mnotd  (D)\imm \neg Q$\br\\
$\perp$\bi $2$
\etab
%And
\itc
$$\SP=\ibnc{\ga\spp G_1}{\ga\spp G_{2}}{\ga\spp G_{1}\And G_{2}}
{ \vd\And}$$
and $\SM$ ends in $\gna\snp (G_1\And G_2)$
\btab
 $\ga\spp G_1$\bv
 $\ga\spp G_2$\bv
 $\gna\sn\mnotg(G_1)\Or\mnotg(G_2)$\br\\
 $\gna\snp(G_i)$\br\\
$\perp$\bi $1$
\etab
%Or
\itc
$$\SP=\ianc{\ga\spp G_i}{\ga\spp G_{1}\Or G_{2}}
{ \vd\Or}$$
and $\SM$ ends in $\gna\snp (G_1\Or G_2)$
\btab
$\gna\sn\mnotg(G_1)\And\mnotg(G_2)$\br\\
 $\gna\snp (G_1)$\bv
 $\gna\snp (G_2)$\bv
 $\ga\spp G_i$\br\\
$\perp$\bi $1$
\etab
\itc The (dis)equality case follows from the decidability of the $=$
 judgment to be detailed later in the unification logic judgment.
\enit% main bit
\end{proof}

