\documentclass[a4paper,12pt,landscape,brazil]{article}
\newcommand{\ultimamodificacao}{15 de agosto de 2008}
\usepackage[latin1]{inputenc}
\usepackage[brazil]{babel}
\usepackage{epsfig,graphicx,color,latexsym,alltt,calc,ifthen,slides,hyperref} 

\newcounter{conta}
\begin{document}

\setbackgroundcolor{white}
\settextcolor{blue}
\setslidetitlecolor{red}
\setbordercolor{red}

\setedition{slides.sty}
\newincluder{fulledition}
\setincluder{fulledition}{true}

\sffamily 
\bfseries 
\mathversion{bold}
%\Hugesize
%\Hugefont

\title{Dedu\c{c}\~ao}
\author{Newton Jos\'e Vieira}
\lhead{Automa\c c\~ao de Sistemas de Infer\^encia}
\rhead{UFMG}
\lfoot{\copyright 2008 Newton Jos\'e Vieira}
%\rfoot{rsb}
\organization{UFMG}
\date{\ultimamodificacao}
\titlepage
\pagenumbering{arabic}

\newslide{Substitui\c{c}\~ao}

\begin{itemize}
 \item $\alpha_x^t$: f\'ormula obtida substituindo-se, na f\'ormula $\alpha$, toda vari\'avel \textcolor{red}{livre}
       $x$ pelo termo $t$ (se $\alpha$ n\~ao tem vari\'avel livre, $\alpha_x^t=\alpha$).
 \item Tal substitui\c c\~ao s\'o pode acontecer se $x$ n\~ao aparece no escopo de algum quantificador
       com vari\'avel que ocorra em $t$; \\
       Exemplo: em $\textcolor{black}{\exists x p(x,y)}$, $\textcolor{black}{y}$ n\~ao pode ser substitu\'{\i}da
       por $\textcolor{black}{x}$, nem por $\textcolor{black}{f(x)}$ etc., pois o quantificador $\exists$
       menciona $\textcolor{black}{x}$.
\end{itemize}

\vspace*{7mm}
Exemplo:

Seja a f\'ormula $\gamma=\textcolor{black}{\exists y p(y,x)\vee\forall x\neg q(x,z)}$
\begin{itemize}
 \item $\gamma_{\textcolor{black}{x}}^{\textcolor{black}{g(A,z})}=\textcolor{black}{\exists y p(y,g(A,z))\wedge\forall x\neg q(x,z)}$
 \item $\textcolor{black}{x}$ n\~ao pode ser substu\'{\i}da por $\textcolor{black}{g(A,y)}$ em $\gamma$.
 \item A ocorr\^encia de $\textcolor{black}{z}$ em $\gamma$ pode ser substitu\'{\i}da por qualquer
       termo $t$ que n\~ao tenha a ocorr\^encia da vari\'avel $\textcolor{black}{x}$.
\end{itemize}


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

\end{document}
\newslide{Um exemplo inicial}

A regra de {\em elimina\c c\~ao do quantificador universal\/} (EU) \'e:
       \begin{center}
        \begin{tabular}{cc}
         & $\forall x\alpha$ \\ \cline{2-2}
         & $\alpha_x^t$
        \end{tabular}
        $x$ \'e substitu\'{\i}vel por $t$ em $\alpha$
       \end{center}

\exemplo{
Segue uma dedu\c c\~ao que mostra que:
 \[\{\forall x(\mbox{\em homem\/}(x)\rightarrow\mbox{\em mortal\/}(x)),
  \mbox{\em homem\/}(\mbox{\em S\'ocrates\/})\}\vdash\mbox{\em mortal\/}(\mbox{\em S\'ocrates\/})\mbox{:}\]
\begin{tabbing}
 xxxx\= x. \=$\mbox{\em homem\/}(\mbox{\em S\a'ocrates\/})\rightarrow
                    \mbox{\em mortal\/}(\mbox{\em S\a'ocrates\/}))$ \ \=x \kill
 \> 1. \>$\forall x(\mbox{\em homem\/}(x)\rightarrow\mbox{\em mortal\/}(x))$ \> (H) \\
 \> 2. \>$\mbox{\em homem\/}(\mbox{\em S\a'ocrates\/})$ \> (H) \\
 \> 3. \>$\mbox{\em homem\/}(\mbox{\em S\a'ocrates\/})\rightarrow
                    \mbox{\em mortal\/}(\mbox{\em S\a'ocrates\/}))$ \> (EU 1) \\
 \> 4. \>$\mbox{\em mortal\/}(\mbox{\em S\a'ocrates\/})$ \> (MP 3,2) \\
\end{tabbing} \fim
}
%--------- fim do exemplo -------------


Seja $x$ uma vari\'avel que n\~ao ocorra livre em nenhuma f\'ormula do conjunto $H$.
A regra regra de {\em introdu\c c\~ao do quantificador universal\/} (IU) \'e:
       \begin{center}
        \begin{tabular}{cc}
         & $H\vdash \alpha$ \\ \cline{2-2}
         & $H\vdash \forall x \alpha_a^x$
        \end{tabular} $x$ n\~ao ocorre livre em $H$.
       \end{center}
Nesta regra apoia-se uma estat\'egia muito importante para se tentar
provar uma afirmativa da forma $\forall x \alpha$: Supor que $z$ (uma
vari\'avel {\em nova\/}, n\~ao usada para outro
fim\footnote{Essa vari\'avel pode ser a pr\'opria vari\'avel $x$, desde que
ela n\~ao esteja sendo usada para outro prop\'osito.}) denota um elemento
arbitr\'ario do universo e, em seguida, provar $\alpha_x^z$. Se conseguir,
pode concluir $\forall x \alpha$. 

\exemplo{
Segue uma dedu\c c\~ao que mostra que:
 \[\{\forall x(p(x)\rightarrow q(x)),\forall x \neg q(x)\}\vdash\forall x\neg p(x)\mbox{:}\]
\begin{tabbing}
 xxxx\= x. \=$\forall x(p(x)\rightarrow q(x))$ \ \=x \kill
 \> 1. \>$\forall x(p(x)\rightarrow q(x))$ \> (H) \\
 \> 2. \>$\forall x \neg q(x)$ \> (H) \\
 \> 3. \>$p(x)\rightarrow q(x)$ \> (EU 1) \\
 \> 4. \>$\neg q(x)$ \> (EU 2) \\
 \> 5. \>$\neg p(x)$ \> (MT 3,4) \\
 \> 6. \>$\forall x\neg p(x)$ \> (IU 5) \\
\end{tabbing} \fim
}
%--------- fim do exemplo -------------

O quantificador existencial pode ser introduzido mediante a regra
IE:
       \begin{center}
        \begin{tabular}{cc}
         & $\alpha_x^t$ \\ \cline{2-2}
         & $\exists x \alpha$
        \end{tabular}
       \end{center}
Uma estrat\'egia baseada nesta regra seria: para provar que $\exists\alpha$,
basta provar $\alpha_x^t$.

Por outro lado, a elimina\c c\~ao de quantificador existencial pode acontecer
durante a prova de uma afirmativa $\beta$ segundo a regra EE, a seguir.
Seja $z$ uma vari\'avel {\em nova\/}, que n\~ao apare\c ca em $H$, nem em
$\alpha$ nem em $\beta$. Ent\~ao:
       \begin{center}
        \begin{tabular}{cc}
         & $H\vdash \exists x \alpha$ \\
         & $H\cup\{\alpha_x^z\}\vdash \beta$ \\ \cline{2-2}
         & $H\vdash \beta$
        \end{tabular} $z$ n\~ao ocorre em $H$, $\exists x \alpha$, nem em $\beta$.
       \end{center}
Ou seja, pode-se ``representar'', em certo trecho de uma demonstra\c c\~ao,
um $x$ que exista, mediante uma vari\'avel livre $z$ usada apenas para este
prop\'osito. Observe que nem as hip\'oteses, nem a f\'ormula existencial,
nem a afirmativa que se deduz podem ter refer\^encias livres a $z$.

A seguir, o \emph{sistema do tipo Hilbert} apresentado para l\'ogica proposicional no cap\'{\i}tulo
anterior ser\'a complementado, tamb\'em apenas para dar um exemplo de sistema dedutivo correto e
completo para a l\'ogica de predicados de primeira ordem.\footnote{Este sistema dedutivo foi
tomado emprestado de Mendelson, E. \emph{Introduction to Mathematical Logic}, 3rd edition,
Wadsworth \& Brooks/Cole, 1987, p\'agina 56.} Repete-se, aqui, os esquemas de axiomas Ax1, Ax2 e Ax3
e a regra {\em modus ponens}.
\begin{itemize}
 \item Se $\alpha$, $\beta$ e $\gamma$ s\~ao f\'ormulas, ent\~ao s\~ao
       axiomas:
       \begin{enumerate}
        \item[Ax1:] $\alpha\rightarrow(\beta\rightarrow\alpha)$
        \item[Ax2:] $(\alpha\rightarrow(\beta\rightarrow\gamma))\rightarrow
               ((\alpha\rightarrow\beta)\rightarrow(\alpha\rightarrow\gamma))$
        \item[Ax3:] $(\neg\beta\rightarrow\neg\alpha)\rightarrow[(\neg\beta
               \rightarrow\alpha)\rightarrow\beta]$
        \item[Ax4:] $\forall x\alpha\rightarrow\alpha_x^t$ se $x$ \'e substitu\'{\i}vel por $t$ em $\alpha$
        \item[Ax5:] $\forall x(\alpha\rightarrow\beta)\rightarrow(\alpha\rightarrow\forall x\beta)$
                    se n\~ao h\'a cont\'em ocorr\^encia livre de $x$ em $\alpha$
       \end{enumerate}
 \item Regras de infer\^encia:
       \begin{enumerate}
        \item[MP:] {\em modus ponens}:

                   \begin{tabular}{cc}
                    & $\alpha\;\; \alpha\rightarrow\beta$ \\ \cline{2-2}
                    & $\beta$
                   \end{tabular}
        \item[GN:] {\em generaliza\c{c}\~ao}:

                   \begin{tabular}{cc}
                    & $\alpha$ \\ \cline{2-2}
                    & $\forall \alpha$
                   \end{tabular}
       \end{enumerate}
\end{itemize}
Este sistema dedutivo aproveitar o fato de que o conjunto de conectivos $\{\rightarrow,\neg,\forall\}$ \'e completo
para l\'ogica de primeira ordem.

\exemplo{ Uma dedu\c{c}\~ao usando o sistema dedutivo acima:
\begin{tabbing}
 xxxx\= 4. $\forall x(p(x)\rightarrow q(x))\rightarrow (p(x)\rightarrow q(x))$xx \=\kill
 \> 1. $\forall x(p(x)\rightarrow q(x))$ \> (H) \\
 \> 2. $\forall x\,p(x)$ \> (H) \\
 \> 3. $\forall x(p(x)\rightarrow q(x))\rightarrow (p(x)\rightarrow q(x))$ \> (Ax4) \\
 \> 4. $p(x)\rightarrow q(x)$ \> (MP 1,3) \\
 \> 5. $\forall p(x)\rightarrow p(x)$ \> (Ax4) \\
 \> 6. $p(x)$ \> (MP 2,5) \\
 \> 7. $q(x)$ \> (MP 4,6) \\
 \> 8. $\forall x\,q(x)$ \> (GN 7)
\end{tabbing}
Tem-se, portanto, que $\{\forall x(p(x)\rightarrow q(x)),\forall x\,p(x)\}\models \forall x\,q(x)$. \fim
}
%--------- fim do exemplo -------------



Como todo sistema dedutivo do tipo Hilbert, esse tem interesse principalmente te\'orico,
n\~ao sendo adequado para servir de base para processamento em computadores nem utiliza\c{c}\~ao
por seres humanos em demonstra\c{c}\~oes.

Para este \'ultimo prop\'osito o tipo de sistema dedutivo mais adequado \'e o de dedu\c{c}\~ao natural. Al\'em das
regras j\'a mostradas no cap\'{\i}tulo anterior para os conectivos proposicionais, tem-se as seguintes regras
relativas aos quantificadores:
\begin{itemize}
 \item Conectivo $\forall$:
       \begin{itemize}
        \item Introdu\c{c}\~ao (I$\forall$):
              \begin{center}
               \fbox{\parbox[t]{.9cm}{\hspace*{.5mm}$x_0$\\ \hspace*{5mm}$\vdots$\\ \hspace*{3.4mm}$\alpha_x^{x_0}$}} \\
               \rule{1.2cm}{0.2mm} \\
               $\forall x\alpha$
              \end{center}
        \item Elimina\c{c}\~ao (E$\forall$):
              \begin{center}
               \begin{tabular}{c}
               $\forall x\alpha$ \\ \cline{1-1}
               $\alpha_x^t$
               \end{tabular}
              \end{center}
       \end{itemize}
 \item Conectivo $\exists$:
       \begin{itemize}
        \item Introdu\c{c}\~ao (E$\exists$):
              \begin{center}
               \begin{tabular}{c}
               $\alpha_x^t$ \\ \cline{1-1}
               $\exists x\,\alpha$
               \end{tabular}
              \end{center}
        \item Elimina\c{c}\~ao (I$\exists$):
              \begin{center}
               $\exists x\,\alpha$\hspace*{3mm}\fbox{\parbox[b]{11.4mm}{\hspace*{.5mm}$x_0 \;\;\alpha_x^{x_0}$\\
                \hspace*{7mm}$\vdots$\\
                \hspace*{6mm}$\beta$}} \\
               \rule{3cm}{0.2mm} \\
               $\beta$
              \end{center}
       \end{itemize}
\end{itemize}

\exemplo{ A seguinte dedu\c{c}\~ao no sistema de dedu\c{c}\~ao natural prova que
        $\{\forall x(p(x)\rightarrow q(x)),\exists x\,p(x)\}\models \exists x\,q(x)$:
\begin{flushleft}
\begin{tabular}{lll}
\hspace*{1.5mm}& 1. $\forall x(p(x)\rightarrow q(x))$ & (H) \\
 & 2. $\exists x\,p(x)$ & (H) \\ \cline{2-3}
 & \multicolumn{1}{|l}{3. $p(x_0)$} & \multicolumn{1}{l|}{(suposi\c{c}\~ao/$x_0$)} \\
 & \multicolumn{1}{|l}{4. $p(x_0)\rightarrow q(x_0)$} & \multicolumn{1}{l|}{(E$\forall$ 1)} \\
 & \multicolumn{1}{|l}{5. $q(x_0)$} & \multicolumn{1}{l|}{(E$\rightarrow$ 3,4)}  \\
 & \multicolumn{1}{|l}{6. $\exists x\,q(x)$} & \multicolumn{1}{l|}{(I$\exists$ 5)}  \\  \cline{2-3}
 & 6. $\exists x\,q(x)$ & (E$\exists$ 2,3---6)
\end{tabular}
\end{flushleft}
 \fim
}
%--------- fim do exemplo -------------


Exemplos de estrat\'egias de prova relacionadas com os quantificadores, normalmente empregadas
em demonstra\c{c}\~oes informais, juntamente com regras de infer\^encia que as justificam, est\~ao
mostrados a seguir.

\vspace*{4mm}
\noindent{\bf\large Prova de uma afirmativa universal}
\begin{itemize}
 \item Regra de infer\^encia: I$\forall$.
 \item Estrat\'egia: para deduzir $\forall \alpha$, supor um elemento $x_0$ arbitr\'ario e provar
      $\alpha_x^{x_0}$.
\end{itemize}

\vspace*{4mm}
\noindent{\bf\large Prova por constru\c{c}\~ao}
\begin{itemize}
 \item Regra de infer\^encia: I$\exists$.
 \item Estrat\'egia: para deduzir $\exists x\,\alpha$, provar $\alpha_x^t$, para um certo termo $t$.
\end{itemize}

Segue uma complementa\c{c}\~ao dos sistemas de tableaux para tratamento dos quantificadores.
O termo $t$ pode ser qualquer termo da linguagem, mas a constante $a$ tem que ser \emph{nova}, isto \'e,
uma ainda n\~ao utilizada.
No tableau com f\'ormulas marcadas, as regras de infer\^encia faltantes s\~ao:
\begin{enumerate}
 \item Conectivo $\forall$:
 
       \mbox{\setlength{\unitlength}{1mm}
        \begin{picture}(100,10.6)
         \put(30,7.6){\makebox(0,0)[l]{$s\!:\forall x\,\alpha$}}
         \put(30,4.9){\line(1,0){10}}
         \put(30,2){\makebox(0,0)[l]{$s\!:\alpha_x^t$}}

         \put(60,7.6){\makebox(0,0)[l]{$f\!:\forall x\,\alpha$}}
         \put(60,4.9){\line(1,0){10}}
         \put(60,2){\makebox(0,0)[l]{$f\!:\alpha_x^a$}}
        \end{picture}
       }
       
 \item Conectivo $\exists$:

       \mbox{\setlength{\unitlength}{1mm}
        \begin{picture}(100,10.6)
         \put(30,7.6){\makebox(0,0)[l]{$s\!:\exists x\,\alpha$}}
         \put(30,4.9){\line(1,0){10}}
         \put(30,2){\makebox(0,0)[l]{$s\!:\alpha_x^a$}}

         \put(60,7.6){\makebox(0,0)[l]{$f\!:\exists x\,\alpha$}}
         \put(60,4.9){\line(1,0){10}}
         \put(60,2){\makebox(0,0)[l]{$f\!:\alpha_x^t$}}
        \end{picture}
       }
\end{enumerate}

\exemplo{ \label{etpo}
Segue um tableau que prova que
$\forall x\,(p(x)\rightarrow q(x))\rightarrow(\forall x\,p(x)\rightarrow\forall x\,q(x))$ \'e
v\'alida:

       \mbox{\setlength{\unitlength}{1mm}
        \begin{picture}(100,55.5)
         \put(30,51.5){\makebox(0,0)[l]{1. $f\!:\forall x\,(p(x)\rightarrow q(x))\rightarrow(\forall x\,p(x)\rightarrow\forall x\,q(x))$}}
         \put(30,47){\makebox(0,0)[l]{2. $s\!:\forall x\,(p(x)\rightarrow q(x))$ [1]}}
         \put(30,42.5){\makebox(0,0)[l]{3. $f\!:\forall x\,p(x)\rightarrow\forall x\,q(x)$ [1]}}
         \put(30,38){\makebox(0,0)[l]{4. $s\!:\forall x\,p(x)$ [3]}}
         \put(30,33.5){\makebox(0,0)[l]{5. $f\!:\forall x\,q(x)$ [3]}}
         \put(30,29){\makebox(0,0)[l]{6. $f\!:q(C)$ [5]}}
         \put(30,24.5){\makebox(0,0)[l]{7. $s\!:p(C)$ [4]}}
         \put(30,20){\makebox(0,0)[l]{8. $s\!:p(C)\rightarrow q(C)$ [2]}}

         \put(40,18){\line(-2,-1){20}}
         \put(40,18){\line(2,-1){20}}
         \put(10,5){\makebox(0,0)[l]{9. $f\!:p(C)$ [8]}}
         \put(20,2){\makebox(0,0){\sf X}}

         \put(50,5){\makebox(0,0)[l]{10. $s\!:q(C)$ [8]}}
         \put(60,2){\makebox(0,0){\sf X}}
        \end{picture}
       }

 \fim
}
%--------- fim do exemplo -------------


Para tableaux com f\'ormulas n\~ao marcadas, as regras de infer\^encia faltantes s\~ao:
\begin{enumerate}
 \item Conectivo $\forall$:
 
       \mbox{\setlength{\unitlength}{1mm}
        \begin{picture}(100,10.6)
         \put(30,7.6){\makebox(0,0)[l]{$\forall x\,\alpha$}}
         \put(30,4.9){\line(1,0){10}}
         \put(30,2){\makebox(0,0)[l]{$\alpha_x^t$}}

         \put(60,7.6){\makebox(0,0)[l]{$\neg\forall x\,\alpha$}}
         \put(60,4.9){\line(1,0){10}}
         \put(60,2){\makebox(0,0)[l]{$\neg\alpha_x^a$}}
        \end{picture}
       }
       
 \item Conectivo $\exists$:

       \mbox{\setlength{\unitlength}{1mm}
        \begin{picture}(100,10.6)
         \put(30,7.6){\makebox(0,0)[l]{$\exists x\,\alpha$}}
         \put(30,4.9){\line(1,0){10}}
         \put(30,2){\makebox(0,0)[l]{$\alpha_x^a$}}

         \put(60,7.6){\makebox(0,0)[l]{$\neg\exists x\,\alpha$}}
         \put(60,4.9){\line(1,0){10}}
         \put(60,2){\makebox(0,0)[l]{$\neg\alpha_x^t$}}
        \end{picture}
       }
\end{enumerate}


\exemplo{
Segue um tableau com f\'ormulas n\~ao marcadas que prova que a mesma f\'ormula do Exemplo~\ref{etpo},
$\forall x\,(p(x)\rightarrow q(x))\rightarrow(\forall x\,p(x)\rightarrow\forall x\,q(x))$, \'e
v\'alida:

       \mbox{\setlength{\unitlength}{1mm}
        \begin{picture}(100,55.5)
         \put(30,51.5){\makebox(0,0)[l]{1. $\neg\forall x\,(p(x)\rightarrow q(x))\rightarrow(\forall x\,p(x)\rightarrow\forall x\,q(x))$}}
         \put(30,47){\makebox(0,0)[l]{2. $\forall x\,(p(x)\rightarrow q(x))$ [1]}}
         \put(30,42.5){\makebox(0,0)[l]{3. $\neg\forall x\,p(x)\rightarrow\forall x\,q(x)$ [1]}}
         \put(30,38){\makebox(0,0)[l]{4. $\forall x\,p(x)$ [3]}}
         \put(30,33.5){\makebox(0,0)[l]{5. $\neg\forall x\,q(x)$ [3]}}
         \put(30,29){\makebox(0,0)[l]{6. $\neg q(C)$ [5]}}
         \put(30,24.5){\makebox(0,0)[l]{7. $p(C)$ [4]}}
         \put(30,20){\makebox(0,0)[l]{8. $p(C)\rightarrow q(C)$ [2]}}

         \put(40,18){\line(-2,-1){20}}
         \put(40,18){\line(2,-1){20}}
         \put(10,5){\makebox(0,0)[l]{9. $\neg p(C)$ [8]}}
         \put(20,2){\makebox(0,0){\sf X}}

         \put(50,5){\makebox(0,0)[l]{10. $q(C)$ [8]}}
         \put(60,2){\makebox(0,0){\sf X}}
        \end{picture}
       }
 \fim
}
%--------- fim do exemplo -------------

\`As vezes, a partir de um tableau n\~ao fechado para uma f\'ormula $\neg\alpha$, pode-se recuperar
um modelo que satisfaz $\neg\alpha$, sendo assim, um modelo que falseia $\alpha$, mostrando porque
$\alpha$ n\~ao \'e v\'alida. Segue um exempplo.

\exemplo{
Segue um tableau n\~ao fechado para
$\neg[\exists x\,(p(x)\wedge\exists x\, q(x)\rightarrow\exists x\,(p(x)\wedge q(x))]$:

       \mbox{\setlength{\unitlength}{1mm}
        \begin{picture}(100,75.5)
         \put(30,71.5){\makebox(0,0)[l]{1. $\neg[\exists x\,(p(x)\wedge\exists x\, q(x)\rightarrow\exists x\,(p(x)\wedge q(x))]$}}
         \put(30,67){\makebox(0,0)[l]{2. $\exists x\,p(x)\wedge\exists x\, q(x)$ [1]}}
         \put(30,62.5){\makebox(0,0)[l]{3. $\neg\exists x(p(x)\wedge q(x))$ [1]}}
         \put(30,58){\makebox(0,0)[l]{4. $\exists\,p(x)$ [2]}}
         \put(30,53.5){\makebox(0,0)[l]{5. $\exists x\,q(x)$ [2]}}
         \put(30,49){\makebox(0,0)[l]{6. $p(C_1)$ [4]}}
         \put(30,44.5){\makebox(0,0)[l]{7. $q(C_2)$ [5]}}
         \put(30,40){\makebox(0,0)[l]{8. $\neg(p(C_1)\wedge q(C_1))$ [3]}}
         \put(30,35.5){\makebox(0,0)[l]{9. $\neg(p(C_2)\wedge q(C_2))$ [3]}}

         \put(40,33.5){\line(-2,-1){20}}
         \put(40,33.5){\line(2,-1){20}}
         \put(10,20.5){\makebox(0,0)[l]{10. $\neg p(C_1)$ [8]}}
         \put(20,17.5){\makebox(0,0){\sf X}}

         \put(50,20.5){\makebox(0,0)[l]{13. $\neg q(C_1)$ [8]}}
         \put(60,18.5){\line(-1,-1){10}}
         \put(60,18.5){\line(1,-1){10}}
         \put(35,5.5){\makebox(0,0)[l]{11. $\neg p(C_2)$ [9]}}
         \put(65,5.5){\makebox(0,0)[l]{12. $\neg q(C_2)$ [9]}}
         \put(70,2.5){\makebox(0,0){\sf X}}
        \end{picture}
       }
 \fim
}
%--------- fim do exemplo -------------

\lastpage

\end{document}
