% \newcommand{\fpp}{\nprv_{\PP}}
% \newcommand{\fnp}{\nprv_{\PM}\mnotg }
% \newcommand{\fn}{\nprv_{\PM}}
% \newcommand{\fp}{\nprv_{\cP}}
\renewcommand{\ga}{ } %change!
\renewcommand{\gna}{ }%change!

\section{Exhaustivity in Horn Logic}
\label{sec:exhau}

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


\begin{figure}
\label{fig:sf}
\[
\begin{array}{c}
% |-
 \ianc{}{\ga\sp\top}{\vd\top}\qquad\ianc{}{\gna\fp \perp}{{\nprv}_\perp}\vsk
% top and bot
\ianc{\vM = \vN}{\ga\sp \vM \eqd \vN}{{\prv\eqd}}\qquad
\ianc{\vM \not = \vN}{\ga\fp \vM \eqd \vN}{{\nprv\eqd}}\vsk
\ianc{\vM \not = \vN}{\ga\sp \vM \neqd \vN}{{\prv\neqd}}\qquad
\ianc{\vM  = \vN}{\ga\fp \vM \neqd \vN}{{\nprv\neqd}}\vsk
\ibnc{\ga\sp G_1}{\ga\sp G_{2}}{\ga\sp G_{1}\And G_{2}}{{\prv}_\And}
\qquad
\ibnc{\ga\fp G_1}{\ga\fp G_{2}}{\ga\fp G_{1}\Or G_{2}}{{\nprv}_\Or}
\vsk
\ianc{\ga\sp G_i}{\ga\sp G_{1}\Or G_{2}}{{\prv\Or_i}}
\qquad
\ianc{\ga\fp G_i}{\ga\fp G_{1}\And G_{2}}{{\nprv\And_i}}
% \qquad i\in 1\ \mbox{or} \ 2
\vsk
\ianc{ \GG\sp def(Q) \imm Q}{\ga\sp Q}{{ {\rm atm}}}
\qquad
\ianc{ \GG\fp def(Q) \nimm Q}{\ga\fp Q}{{\nprv {\rm atm}}}\vsk
% HORN --> HHF
% \ianc{\GG;\cD\And D \sp G}{\ga\sp D \Imp G}{{\prv} \Imp}
% \qquad
% \ianc{\GG;\cD\And D \fp G}{\ga\fp D \Imp G}{{\nprv} \Imp}
% \vsk
% \ianc{(\GG,y\oftp A);\cD\sp[y/x]G}{\ga\sp \PIXA G}{{\prv} \Pi}
% \qquad
% \ianc{(\GG,y\oftp A);\cD\fp[y/x]G}{\ga\fp \PIXA G}{{\nprv} \Pi}
\end{array}
\]
\caption{Provability and Denial}
\end{figure}

\begin{figure}
\label{fig:imm}
\[
\begin{array}{c}
% immediate >>
\ianc{}{\GG\sp\perp\imm  Q}{\imm\perp}\qquad
\ianc{}{\GG\fp \top\nimm Q}{\nprv \top}\vsk
%\ianc{\vN = \vM}{\GG\sp q\ \vN \imm q\ \vM}{\imm{\rm atm}}\qquad
%\ianc{\vN \neq \vM}{\GG\fp q\ \vN \nimm q\ \vM}{\not\imm{\rm atm}}\vsk
\ibnc{\mbox{for some $\GG\vd t\hastype A$}}{ \GG\sp  [t/x]D \imm
  Q}{\GG\sp \PIXA D \imm Q}{\imm\Pi}\qquad
\ibnc{\mbox{for all $\GG\vd t\hastype A$} }{ \GG\fp [t/x]D \nimm
  Q}{\GG\fp \PIXA D \nimm Q}{\not\imm\Pi}\vsk
\ianc{\GG\sp D_{i}\imm Q}{\GG\sp D_{1}\And D_{2}\imm Q}{\imm{\And_i}}\qquad
\ianc{\GG\fp D_{i}\nimm Q}{\GG\sp D_{1}\tensor D_{2}\nimm Q}{\not\imm{\tensor_i}}\vsk
\ibnc{\GG\sp D_{1}\imm Q}{ \GG\sp D_{2}\imm Q}{\GG\sp D_{1}\tensor D_{2}\imm 
Q}{\imm\tensor}\qquad
\ibnc{\GG\fp D_{1}\nimm Q}{\GG\fp D_{2}\nimm Q}{\GG\fp D_{1}\And D_{2}\nimm
Q}{\not\imm\And}\vsk
\ibnc{\GG\sp\vd\vN\eqd\vM}{\ga\sp G}{ \GG\sp (G\Imp q\  \vN) \imm q\ \vM}{\imm\Imp}
\vsk
\ianc{\GG\fp \vN\eqd\vM}{\GG\fp (G\Imp q\ \vN) \nimm q\ \vM}{\not\imm{\Imp_1}}
\qquad
\ibnc{\GG\fp \vN\neqd\vM}{\fp G} {\GG\fp (G\Imp q\ \vN) \nimm q\ \vM}{\not\imm{\Imp_2}}
% to avoid dependency pos-neg 
% \ianc{\GG\sp Q'\imm Q\quad\sp G}{ \GG\sp (G\Imp Q') \imm Q}{\imm\Imp}
% \vsk
% \ianc{\GG\fp Q'\nimm Q}{ \GG\fp (G\Imp Q') \nimm Q}{\not\imm{\Imp_1}}
% \qquad
% \ianc{\GG\sp Q'\imm Q\quad\fp G} { \GG\fp (G\Imp Q') \nimm Q}{\not\imm{\Imp_2}}
\end{array}
\]
\caption{Immediate Entailment and its Complement}
\end{figure}


Note that $\Pi\not\imm$ is a peseudo-rule, given the metalinguistic
extensional universal quantification on all terms.


% Note that in the above rules denial depends on provability, while this 
% is not the case for the system in Figure \ref{fig:sf}. Still they make 
% the main proof easier.

We use $\gna\snp (G)$ for $\gna\vd\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$.

\newcommand{\foq}{\mbox{\textrm{for all }} \q\,}

\begin{Proposition}[Exhaustivity]
If $\ga\fpp G$ then $ \gna\snp (G)$.
\end{Proposition}
\begin{proof}
We generalize this to:
\ben
\item
If for all well-typed  substitutions $\q$   $\SM ::  \ga\fpp \q G$ then $\SP :: \gna\snp (G)$.
\item
If for all $\q$
%such that $dom(\q) = var(def(Q))$, 
$\IM :: \GG\fpp \q (def(Q)) \nimm Q$, then
% there is a substitution $\q$ such that $dom(\q) = var(def(\neg Q))$ and
$\IP :: \GG\sn  (def(\neg Q)) \imm \neg Q$.
\enen
The proof is by mutual induction on the structure of $\SM$ and $\IM$.
% the structure of the judgments in \ref{fig:sf}
\bit
\itc 
$$\IM = \ianc{}{\GG\fpp\top\nimm Q}{\not\imm\top}$$
As, for all $\q$ $\q\top=\top$.  Then $\mnotd (\top) = \perp$ and
$$ \IP = \ianc{}{\GG\sn\perp\imm \neg Q}{\imm\perp}$$
\itc
$$ \IM = \ianc{\foq\ga\fpp\q\vN \eqd \vM}{\foq\ga\fpp \q(q\ \vN \If
  G)\nimm q\ \vM}{\not\imm\Imp^1}$$
\btab
 $\foq\ga\fpp\q\vN \eqd \vM$\bv
$\foq \q\vN \neq \vM$\br\\
$\cdot\prv \vM\not\in\| \vN\|$\` Trivially\\
 $\cdot\prv \vM\in \|\mnot (\vN)\|$\` By term exhaustivity (\ref{le:part})\\
$\vM=\sigma\vec{S}$ for some $\sigma$ and
$\vec{S}\in\mnot(\vN)$\` By definition of $\|\_\|$\\
$\GG\sn\Pi(\BAnd_{\vec{S}\in\mnot(\vN)} q\
\vec{S}\If \top)\imm q\ \vM$\br\\
$\GG\sn(\Pi(\BAnd_{\vec{S}\in\mnot(\vN)} q\
\vec{S}\If \top)\And \neg q\ \vM \If \mnotg(G))\imm q\ \vM$\br\\
 $\GG\sn\mnotd(q\ \vN\If G)\imm q\ \vM$\br
\etab
\itc 
$$\IM = \ibnc{\foq\ga\fpp \q\vN\neqd\vM }{\foq \ga\fpp G}{\foq\ga\fpp \q( q\ \vN\If G)
\nimm q\ \vM} {\not\imm{\Imp_2}}$$
\btab
$\foq\ga\fpp \q\vN\neqd\vM $\bv
$\ga\sn \vN\eqd \vM$\bi $2$\\
$\foq \ga\fpp G$\bv
$\gna\snp (G)$\bi $2$\\
$\GG\sn \neg q\ \vN \If \mnotg (G)\imm \neg q\ \vM$ \br\\
$\GG\sn(\Pi(\BAnd_{\vec{S}\in\mnot(\vN)} q\
\vec{S}\If \top)\And \neg q\ \vM \If \mnotg(G))\imm q\ \vM$\br\\
%$\gna\sn(\mnotd (q\ \vN\If\top)\And \neg q\ \vN 
%\If \mnotg (G))\imm \neg q\ \vM$\br\\
$\GG\sn \mnotd(q\ \vN\If G) \imm \neg q\ \vM$\br
\etab
\itc 
$$ \IM = \ianc{\foq\GG\fpp \q D_{i}\nimm Q}{\foq\GG\fpp \q(D_{1}\tensor 
D_{2})\nimm Q}{ \not\imm\tensor_i}$$
For $i = 1 \mbox{ or } 2$.  By IH $2$ $\GG\sn \mnotd (D_{i})\imm \neg Q$ 
and by rule $\nprv{\And_i}$ we infer $\GG\sn \mnotd (D_{1})\And 
\mnotd(D_{2})\imm \neg Q$ which, by definition of $\mnotd$, is 
equivalent to $\GG\sn \mnotd (D_{1}\tensor D_{2})\imm \neg Q$.
\itc 
$$\IM = \ibnc{\foq\GG\fpp\q D_{1}\nimm Q}{\foq \GG\fpp\q D_{2}\nimm Q}
{\foq\GG\fpp\q( D_{1}\And D_{2})\nimm Q}{\not\imm\And}$$
By IH $2$ $\GG\sn \mnotd (D_{1})\imm \neg Q$ and $\GG\sn\mnotd 
(D_{2})\imm \neg Q$, hence, by rule $\imm\tensor$ we infer $ 
\GG\sn\mnotd (D_{1})\tensor \mnotd(D_{2})\imm \neg Q$ which, by 
definition of $\mnotd$, is equivalent to $ \GG\sn\mnotd (D_{1}\And 
D_{2})\imm \neg Q$.
% \itc
% $$\IM = \ianc{\GG\fpp q\ \vN\nimm Q}{\GG\fpp ( q\ \vN\If G) \nimm Q}{\not\imm{\Imp_1}}$$
% By IH $\GG\sn\mnotd (q\ \vN) \imm \neg Q$ and by rule 
% $\nprv{\And_1}$ we have $\GG\sn(\mnotd (q\ \vN)\And \neg q\ \vN \If 
% \mnotg (G))\imm \neg Q$ which, by definition of $\mnotd$, is 
% equivalent to $\GG\sn \mnotd(q\ \vN\If G) \imm \neg Q$.

\itc
$$\IM = 
\ianc{\mbox{for all $t$, } \q \GG\fpp [t/x]\cdot\q D \nimm Q}{\foq\GG\fpp\q\PIXA D \nimm Q}{\not\imm\Pi}$$
By IH $2$ $\GG\sn\mnotd ( D)\imm \neg Q$, which, by definition of $\mnotd$, is equivalent to 
$\GG\sn\mnotd (\PIXA D)\imm \neg Q$.


\itc
$$\SM = \ianc{ \foq\GG\fpp\q def(Q) \imm Q}{\foq\ga\fpp\q Q}{\vd{ {\rm 
atm}}}$$
By IH $2$ $\GG\sn def(\neg Q) \imm \neg Q$ which entails $\ga\snp (Q)$.

\itc
$$\SM=\ianc{}{\foq\ga\fpp\bot}{\vd\bot}$$
Then $\ga\snp (\bot)$
\itc 
$$\SM = \ibnc{\foq\ga\fp \q G_1}{\foq\ga\fp \q G_{2}}{\foq\ga\fp \q(G_{1}\Or
G_{2})}{\nprv\Or}$$
By IH $1$, $ \ga\snp (G_{1})$ and $\ga\snp (G_{2})$ which implies $\ga\sn 
\mnotg (G_{1})\And \mnotg (G_{2})$, which is equivalent, by definition 
of $\mnotg$, $to \ga\snp (G_{1} \Or G_{2})$.
\itc 
$$\SM =
\ianc{\foq\ga\fp\q G_i}{\foq\ga\fp\q( G_{1}\And G_{2})}{\nprv{\And_i}}$$
For $i=1 \mbox{ or } 2$.  By IH $1$ $ \ga\snp (G_{i})$ which implies 
$\ga\sn \mnotg (G_{1})\Or \mnotg (G_{2})$, which is equivalent, by 
definition of $\mnotg$, to $ \ga\snp (G_{1} \And G_{2})$.
\itc (dis)equations: delayed to unification logic
% $$ \SM =
% \ianc{\vM \not = \vN}{\ga\fpp \vM \eqd \vN}{\nprv{\eqd}}$$
% Then $\ga\sn  \vM \neqd \vN$ and $\ga\sn\mnotg( \vM \eqd \vN)$.
% \itc
% $$ \SM =
% \ianc{\vM  = \vN}{\ga\fpp \vM \neqd \vN}{\nprv{\neqd}}$$
% Then $\ga\sn\vM \eqd \vN$ and $\ga\sn\mnotg( \vM \neqd \vN)$.
\enit
\end{proof}
\end{document}


% ------------------------

\begin{Proposition}[Disjointness]
If $\ga\spp G$ then $\gna\fnp ( G)$.
\end{Proposition}
\begin{proof} We generalize this to:
\ben
\item
If $\SP ::  \ga\spp G$ then $\SM :: \gna\fnp ( G)$
\item
If there is a substitution $\sigma$ such that 
$dom(\sigma)=var(def(Q))$ and 
$\IP :: \ga\spp \sigma (def(Q)) \imm Q$ then 
for all substitutions $\q$ such that $dom(\q)=var(def(\neg Q)),\  \IM :: 
\gna\fn \q (def(\neg Q)) \nimm \neg Q$.
\enen
The proof is by induction on the structure of $\SP$ and $\IM$\footnote{since 
substitutions are needed only in the $\Pi$ case we for now suppress mention to 
them in the other cases}.
\bit
\itc 
$$\IP = \ianc{}{\ga\spp\perp\imm Q}{\imm\perp}$$
Then $\mnotd (\perp) = \top$ and
 $$ \IM = \ianc{}{\gna\fn\top\nimm \neg Q}{\not\imm\top}$$
\itc
$$ \IP = \ianc{\ga\vN = \vM}{\ga\spp q\ \vN \imm q\ \vM}{\imm{\rm atm}}$$
From $\vN = \vM$ we infer $\GG\prv \vM\in\| \vN\|$. By the term partition 
Lemma (\ref{le:part}) $\GG\prv \vM\not\in \|\mnot \vN\|$. By Lemma 
\ref{le:part-imm} $\gna\fn\mnotd (q\ \vN) \nimm\neg q\ \vM$.
\itc
$$ \IP = \ianc{\ga\spp D_{i}\imm Q}{\ga\spp D_{1}\And D_{2}\imm Q}{\nprv{\And_i}}$$
For $i = 1 \mbox{ or } 2$.  By IH $\gna\fn\mnot D_{i}\nimm \neg Q$ and by rule 
$I^{\nprv}_{\tensor_i}$ we infer $\gna\fn\mnotd (D_{1})\tensor \mnot(D_{2})\nimm \neg Q$
which, by definition of $\mnotd$, is equivalent to  $\gna\fn\mnotd (D_{1}\And D_{2})\nimm \neg Q$.
\itc 
$$\IP = \ianc{\ga\spp D_{1}\imm Q\quad D_{2}\imm Q}{\ga\spp D_{1}\tensor D_{2}\imm 
Q}{\imm\tensor}$$
 By IH $\gna\fn\mnotd (D_{1})\nimm \neg Q$ and 
$\gna\fn\mnotd (D_{2})\nimm \neg Q$, hence, by rule $I^{\nprv}_\And$ we infer
$\gna\fn \mnotd (D_{1})\And\mnotd(D_{2})\nimm \neg Q$
which, by definition of $\mnotd$, is equivalent to  $\gna\fn \mnotd (D_{1}\tensor D_{2})\nimm \neg Q$. 
\itc
$$\IP = \ianc{\ga\spp q\ \vN\imm Q \quad \spp G}{ \ga\spp (q\ \vN \If G) \imm 
Q}{\imm\Imp} $$
By IH $\gna\fn\mnotd (q\ \vN) \nimm \neg Q$ and $\fnp (G)$.  Rule 
$\not\imm{\Imp_1}$ yields $\neg q\ \vN \If \mnotg (G)\nimm Q$: finally 
by rule $I^{\nprv}_\And$ we have $\gna\fn(\mnotd (q\ \vN)\And \neg q\ \vN \If 
\mnotg (G))\nimm Q$ which is equivalent to $\gna\fn \mnotd(q\ \vN\If 
G)\nimm \neg Q$.
\itc
$$\IP = 
\ianc{ \ga\spp [t/x]D \imm Q}{\ga\spp \PIXA D \imm Q}{\imm\Pi}$$
By IH for all $\q$ such that $\gna\fn\mnotd (\q D)\nimm \neg Q$, 
hence by Lemma \ref{le:clo-imm}, $\gna\fnp\pix (\mnotd(D))\nimm\neg 
Q$ which, by definition of $\mnotd$, is equivalent to $\gna\fn\mnotd 
(\Pi x:A.D)\nimm \neg Q$.
\itc
$$\SP =
\ianc{ \ga\sp def(Q) \imm Q}{\ga\sp Q}{\vd{ {\rm atm}}}$$
By IH $\gna\fn def(\neg Q) \nimm \neg Q$  which entails $\ga\fnp (Q)$. 
\item 
Case:
$$\SP = \ianc{\ga\sp G_1\quad\ga\sp G_{2}}{\ga\sp G_{1}\And 
G_{2}}{\vd\And}$$
By IH, $ \ga\fnp(G_{1})$ and $\ga\fnp (G_{2})$ which implies $\ga\fn 
\mnotd (G_{1}) \Or \mnotd(G_{2})$ which, by definition of $\mnotg$, 
is equivalent to $ \ga\fnp (G_{1} \And G_{2})$.
\itc 
$$\SP = \ianc{\ga\sp G_i}{\ga\sp G_{1}\Or G_{2}}{\vd{\Or_i}}
$$
For $i=1 \mbox{ or } 2$.  By IH, $ \ga\fnp (G_{i})$ which implies 
$\ga\fn \mnotd (G_{1}) \And \mnotd(G_{2})$ which, by definition of 
$\mnotg$, is equivalent to $ \ga\fnp (G_{1} \Or G_{2})$.
\itc
$$ \SP =
\ianc{\vM = \vN}{\ga\spp \vM \eqd \vN}{\vd{\eqd}}$$
Then $\ga\fn  \vM \neqd \vN$ and $\ga\fn\mnotg( \vM \eqd \vN)$.
\itc
$$ \SP =
\ianc{\vM \not = \vN}{\ga\spp \vM \neqd \vN}{\nprv{\eqd}}$$
Then $\ga\fn  \vM \eqd \vN$ and $\ga\sn\mnotg( \vM \neqd \vN)$.
\enit
\end{proof}

%%%%%%%%%
