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

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


Note that $\Pi\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.

% \begin{Lemma}
% \label{le:part-imm}
% \mbox{}
% \ben
% \item
% If $\GG\prv \vM\in \|\mnot \vN\|$ then $\gna\sn\mnotd (q\ \vN) \imm \neg q\ \vM$
% \item
% If $\GG\prv \vM\not\in \| \mnot \vN\|$ then $\gna\fn\mnotd (q\ \vN) \nimm \neg q\ \vM$.
% \enen
% \end{Lemma}
% \begin{proof}
% \mbox{}
% \ben
% \item
% Apply $I^{\prv} \And$ and $I^{\prv}_{\pix}$.
% \item
% Apply $I^{\prv} \And$ and $I^{\nprv}_{\pix}$.
% \enen
% \end{proof}

\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 $\SM ::  \ga\fpp G$ then $\SP :: \gna\snp ( G)$.
\item
If for all well-typed  substitutions $\q$ 
such that $dom(\q) = var(def(Q))$, 
$\IM :: \ga\fpp \q (def(Q)) \nimm Q$, then
% there is a substitution $\q$ such that $dom(\q) = var(def(\neg Q))$ and
$\IP :: \gna\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{}{\ga\fpp\top\nimm Q}{\not\imm\top}$$
As, for all $\q$ $\q\top=\top$.  Then $\mnotd (\top) = \perp$ and
$$ \IP = \ianc{}{\gna\sn\perp\imm \neg Q}{\imm\perp}$$
\itc
$$ \IM = \ianc{\ga\vd\vN \neq \vM}{\ga\fpp (q\ \vN \If G)\nimm q\ \vM}\not\imm{\Imp^1}$$
As, for all $\q$ $\q\vN=\vN$. Now, $\vN \neq \vM$ trivially entails
$\cdot\prv \vM\not\in\| \vN\|$. 
By term exhaustivity (\ref{le:part}) $\cdot\prv \vM\in \|\mnot (\vN)\|$.
Thus there is a $\sigma$ such that $\vM=\sigma\vec{S}$ for
$\vec{S}\in\mnot(\vN)$. Thus by rule $\Pi(\BAnd_{\vec{S}\in\mnot(\vN)} q\
\vec{S}\If \top)\imm q\ \vM$ and finally $\ga\sn\mnotd(q\ \vN\If
G)\imm q\ \vM$.
\itc 
$$\IM = \ibnc{\ga\spp \vN\eqd\vM }{\foq \fpp G}{\foq\ga\fpp ( q\ \vN\If G)
\nimm q\ \vM} {\not\imm{\Imp_2}}$$
By IH $\snp (G)$ and $\ga\sn\neg q\ \vN\imm \neg q\ \vM$.  Thus, by rule 
$\imm\Imp$ we have: $\gna\sn \neg q\ \vN \If \mnotg (G)\imm \neg q\ \vM$ 
and rule $\nprv{\And_2}$ yields $\gna\sn(\mnotd (q\ \vN)\And \neg q\ \vN 
\If \mnotg (G))\imm \neg q\ \vM$ which, by definition of $\mnotd$, is 
equivalent to $\gna\sn \mnotd(q\ \vN\If G) \imm \neg q\ \vM$.
\itc 
$$ \IM = \ianc{\foq\ga\fpp \q D_{i}\nimm Q}{\foq\ga\fpp \q(D_{1}\tensor 
D_{2})\nimm Q}{ \not\imm\tensor_i}$$
For $i = 1 \mbox{ or } 2$.  By IH $2$ $\gna\sn \mnotd (D_{i})\imm \neg Q$ 
and by rule $\nprv{\And_i}$ we infer $\gna\sn \mnotd (D_{1})\And 
\mnotd(D_{2})\imm \neg Q$ which, by definition of $\mnotd$, is 
equivalent to $\gna\sn \mnotd (D_{1}\tensor D_{2})\imm \neg Q$.
\itc 
$$\IM = \ibnc{\foq\ga\fpp\q D_{1}\nimm Q}{\foq \ga\fpp\q D_{2}\nimm Q}
{\foq\ga\fpp\q( D_{1}\And D_{2})\nimm Q}{\not\imm\And}$$
By IH $2$ $\gna\sn \mnotd (D_{1})\imm \neg Q$ and $\gna\sn\mnotd 
(D_{2})\imm \neg Q$, hence, by rule $\imm\tensor$ we infer $ 
\gna\sn\mnotd (D_{1})\tensor \mnotd(D_{2})\imm \neg Q$ which, by 
definition of $\mnotd$, is equivalent to $ \gna\sn\mnotd (D_{1}\And 
D_{2})\imm \neg Q$.
% \itc
% $$\IM = \ianc{\ga\fpp q\ \vN\nimm Q}{\ga\fpp ( q\ \vN\If G) \nimm Q}{\not\imm{\Imp_1}}$$
% By IH $\gna\sn\mnotd (q\ \vN) \imm \neg Q$ and by rule 
% $\nprv{\And_1}$ we have $\gna\sn(\mnotd (q\ \vN)\And \neg q\ \vN \If 
% \mnotg (G))\imm \neg Q$ which, by definition of $\mnotd$, is 
% equivalent to $\gna\sn \mnotd(q\ \vN\If G) \imm \neg Q$.

\itc
$$\IM = 
\ianc{\mbox{for all } \q \ga\fpp [t/x]\cdot\q D \nimm Q}{\foq\ga\fpp\q\PIXA D \nimm Q}{\not\imm\Pi}$$
By IH $2$ $\gna\sn\mnotd ( D)\imm \neg Q$, which, by definition of $\mnotd$, is equivalent to 
$\gna\sn\mnotd (\PIXA D)\imm \neg Q$.
\itc
$$\SM = \ianc{ \foq\ga\sp\q def(Q) \imm Q}{\ga\sp Q}{\vd{ {\rm 
atm}}}$$
By IH $2$ $\ga\snp def(\neg Q) \imm \neg Q$ which entails $\ga\snp (Q)$.
\itc 
$$\SM = \ianc{\ga\fp G_1\quad\ga\fp G_{2}}{\ga\fp 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{\ga\fp G_i}{\ga\fp 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
$$ \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}

%%%%%%%%%
