% (find-angg "LATEX/2010-1-MD-prova-VS2.tex")
% (find-angg "LATEX/2010-1-MD-prova-VS.tex")
% (find-angg "LATEX/2010-1-MD-exercs-P4.tex")
% (find-dvipage "~/LATEX/2010-1-MD-exercs-P4.dvi")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010-1-MD-prova-VS2.tex && latex    2010-1-MD-prova-VS2.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010-1-MD-prova-VS2.tex && pdflatex 2010-1-MD-prova-VS2.tex"))
% (eev "cd ~/LATEX/ && Scp 2010-1-MD-prova-VS2.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2010-1-MD-prova-VS2.dvi"))
% (find-dvipage "~/LATEX/2010-1-MD-prova-VS2.dvi")
% (find-pspage  "~/LATEX/2010-1-MD-prova-VS2.pdf")
% (find-pspage  "~/LATEX/2010-1-MD-prova-VS2.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2010-1-MD-prova-VS2.ps 2010-1-MD-prova-VS2.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2010-1-MD-prova-VS2.ps 2010-1-MD-prova-VS2.dvi && ps2pdf 2010-1-MD-prova-VS2.ps 2010-1-MD-prova-VS2.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage  "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2010-1-MD-prova-VS2.pdf" (ee-twupfile "LATEX/2010-1-MD-prova-VS2.pdf") 'over)
% (ee-cp "~/LATEX/2010-1-MD-prova-VS2.pdf" (ee-twusfile "LATEX/2010-1-MD-prova-VS2.pdf") 'over)
% (find-twusfile     "LATEX/" "2010-1-MD-prova-VS2")
% http://angg.twu.net/LATEX/2010-1-MD-prova-VS2.pdf

\documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
\usepackage{edrx08}       % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty"  -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex   % (find-dn4ex "edrxheadfoot.tex")
\begin{document}

\input 2010-1-MD-prova-VS2.dnt

%
% (eedn4-51-bounded)

%Index of the slides:
%\msk
% To update the list of slides uncomment this line:
%\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")

{\setlength{\parindent}{0em}
\par Matemática Discreta - Prova Suplementar Extra (VS2)
\par PURO-UFF - 2010.1
\par 28/julho/2010
\par Prof: Eduardo Ochs
}

\bsk

\def\Pontos#1{{\color{blue}(Total: #1 pontos).}}
\def\pontos#1{{\color{blue}(#1 pontos)}}
\def\pontos#1{}

\def\Zten{\Z_{10}}
\def\BB#1#2{B_#1 \to B_#2}
\def\ren{\text{ren}}
\def\ren{\text{re}}
\def\ren{Ð{re}}
\def\re{\text{re}}
\def\re{Ð{re}}
\def\Foo#1{Ð{Foo}_{#1}}

Seja $\Zten = \{0,1,2,3,4,5,6,7,8,9\}$, e seja $B \subseteq \Zten$.
Vou abreviar ``$nÝB$'' por $B_n$; por exemplo, $B_2 \to B_3$ vai ser
uma abreviação para $2ÝB \to 3ÝB$. Além disso, vou abreviar como (i),
(ii), (iii), (iv) as proposições abaixo:

(i): $3ÝB$ (ou, abreviando: $B_3$).

(ii): $(\BB03) ´ (\BB14) ´ (\BB25) ´ (\BB36) ´ (\BB47) ´ (\BB58) ´ (\BB69)$.

(iii): $B_6´B_7 \to B_2´B_0$.

(iv): $B_4$.

\msk

Para cada escolha de $B \subseteq \Zten$ --- e repare que há
$2^{10}=1024$ escolhas possíveis --- cada uma das proposições (i),
(ii), (iii) vai ser ou verdadeira ou falsa. Além disso, dentre estes
1024 valores possíveis para $B$, 512 obedecem a condição (i),
$5·4·4=80$ obedecem a condição (ii), e $2·4·4=32$ obedecem (i)$´$(ii);
mas o que vai nos interessar agora não vai ser contar `$B$'s e sim
provar proposições sobre $B$ {\sl usando um certo sistema dedutivo}.

\msk

Se (i) e (ii) são verdade então $9ÝB$. Podemos escrever uma prova
disto em Português assim:

Como (ii) é verdade, então $\BB36$; por (i) sabemos que $B_3$ é
verdade, então $B_6$ é verdade. Mas (ii) também nos diz que $\BB69$;
como tínhamos descoberto que $B_6$ é verdade, concluímos que $B_9$ é
verdade --- ou seja, que $9ÝB$, como queríamos demonstrar.

No nosso sistema dedutivo esta prova vai ser representada por esta
\'arvore:

%:
%:  (i)      (ii)
%:  ---\ren  -----´E
%:  B_3      \BB36    (ii)
%:  --------------MP  -----´E
%:       B_6          \BB69
%:       ------------------MP
%:              B_9
%:
%:              ^B9
%:
$$\ded{B9}$$

O {\sl significado} desta árvore é o seguinte. Cada barra indica a
aplicação de uma das regras de dedução permitidas; à direita da barra
pomos o nome da regra, acima da barra pomos as ``hipóteses'' da regra
--- que são proposições que já sabemos que são verdadeiras --- e
abaixo da barra pomos a ``conclusão'' da regra.

As regras do nosso primeiro sistema dedutivo (``DN1'' --- ``dedução
natural, versão 1'') vão ser só estas:
%:
%:  P_1´\ldots´P_n     P_1 \ldots P_n
%:  --------------´E   --------------´I
%:       P_k           P_1´\ldots´P_n
%:
%:       ^andE         ^andI
%:
%:  P  P->Q      P
%:  -------MP    -\ren
%:     Q         P'
%:
%:     ^MP       ^ren
%:
$$\ded{andE} \qquad \ded{andI}$$
$$\ded{MP} \qquad \ded{ren}$$
%
onde $nÝ\{1,2,\ldots\}$ e $kÝ\{1,\ldots,n\}$. Aqui está um exemplo de
uma dedução em DN1 sem a regra $\re$:
%:
%:  Q´P    Q´P
%:  ---´E  ---´E
%:   P      Q
%:   --------´I
%:     P´Q       P´Q->R
%:     ----------------MP
%:            R
%:
%:            ^QPR
%:
$$\ded{QPR}$$

Ela mostra como ``deduzir'' que $R$ é verdade a partir das hipóteses
$Q´P$ e $P´Q \to R$... mas repare que isto é o ``significado'' desta
\'arvore, e, como vimos no curso e na lista de exercícios, ela também
pode ser vista como um objeto matemático abstrato:

{\bf Definição.} Uma {\sl dedução} de $\bb$ a partir de $\aa_1,
\ldots, \aa_n$ no sistema DNn é uma árvore na qual a ``raiz'' é $\bb$,
todas as proposições que aparecem nas ``folhas'' pertencem ao conjunto
$\{\aa_1, \ldots, \aa_n\}$, e cada barra é de uma das formas
permitidas no sistema DNn (cada barra é uma aplicação de uma das
regras do sistema DNn).

\msk

A regra $\re$ (``reescrita'') é especial --- você raramente vai
encontrá-la definida explicitamente nos livros... ela diz que podemos
deduzir $P'$ a partir de $P$ se $P$ e $P'$ só diferem por
``definições''. {\sl Vamos discutir isto no quadro antes da prova
  começar.}

\msk

Dizemos que uma regra de dedução é {\sl válida} se toda vez que as
suas hipóteses forem verdadeiras a sua conclusão também é verdadeira.
Por exemplo, a regra
%:
%:   P
%:  ---\Foo1
%:  P´Q
%:
%:  ^Foo1
%:
$$\ded{Foo1}$$
%
não é válida: se $P$ for $¦V$ e $Q$ for $¦F$ então ela ``nos permite
deduzir algo falso a partir de hipótese verdadeiras''.

{\sl Num sistema dedutivo no qual todas as regras são válidas,
  qualquer dedução com hipóteses verdadeiras tem conclusão
  verdadeira.} Todas as provas feitas em Português no Scheinerman
correspondem a deduções num certo sistema dedutivo (que infelizmente o
Scheinerman nunca apresenta de modo suficientemente explícito); as
regras deste sistema dedutivo são exatamente os 25 ``esquemas de
prova'' que ele lista na p.525.

\bsk

\noindent {\bf (1)} \Pontos{4.0} Digamos que o conjunto $B$ obedece as
condições (i), (ii), (iii), (iv). Encontre uma {\sl prova formal}, no
sistema dedutivo DN1, de que $2ÝB$ --- ou seja, uma dedução no sistema
DN1, com ``$2ÝB$'' na raiz e obedecendo todas as outras propriedades
discutidas acima.

\bsk

\noindent {\bf (2)} \Pontos{4.0} Para cada uma das regras abaixo,

%:
%:   Q            P         P->Q       P->Q
%:  ----\Foo2   ----\Foo3   ----\Foo4  ------\Foo5
%:  P->Q        P->Q        Q->P       ¬Q->¬P
%:
%:  ^Foo2       ^Foo3       ^Foo4      ^Foo5
%:
%:  ¬P  P->Q        P->Q  ¬Q
%:  --------\Foo6   --------\Foo7
%:     ¬Q             ¬P
%:
%:     ^Foo6          ^Foo7
%:
%:  P(4)         ÎnÝ\N.P(n)
%:  ----\Foo8    ----------\Foo9
%:  ÎnÝ\N.P(n)      P(4)
%:
%:  ^Foo8          ^Foo9
%:
%:  P(4)         ýnÝ\N.P(n)
%:  ----\Foo{10} ----------\Foo{11}
%:  ýnÝ\N.P(n)      P(4)
%:
%:  ^Foo10          ^Foo11
%:
%:  P'´P''  P'´P''->Q'´Q''
%:  ----------------------\Foo{12}
%:          Q'´Q''
%:
%:          ^Foo12
%:
%:  P´P'  P´(P'->Q)          P  (P->Q)´Q'
%:  -------------\Foo{13}    ----------\Foo{14}
%:        Q                     Q´Q'
%:
%:        ^Foo13                ^Foo14
%:
%:  a,b,cÝ\N  b<c          a,b,cÝ\Z   b\le"c
%:  -------------\Foo{15}  -----------------\Foo{16}
%:      ab<ac                   ab<ac
%:
%:      ^Foo15                  ^Foo16
%:
%:
$$\ded{Foo2} \qquad \ded{Foo3} \qquad \ded{Foo4} \qquad \ded{Foo5}$$
$$\ded{Foo6} \qquad \ded{Foo7}$$
$$\ded{Foo8} \qquad \ded{Foo9}$$
$$\ded{Foo10} \qquad \ded{Foo11}$$
$$\ded{Foo12}$$
$$\ded{Foo13} \qquad \ded{Foo14}$$
$$\ded{Foo15} \qquad \ded{Foo16}$$

Diga se ela é válida ou não, e justifique. {\sl Se você não tiver
  certeza da sua resposta de um item, ou se você não souber
  justificá-la direito, deixe-a em branco ou risque-a --- cada
  resposta errada ou com justificativa ruim anula uma certa.}


\bsk

\noindent {\bf (3)} \Pontos{2.0} Uma das perguntas da P2 era ``prove
ou refute: $ýnÝ\N. n<3^n$''. O esboço de resposta dela no gabarito era
uma árvore um pouco maior que esta aqui:
%
%\bsk
%:<=\le 
%:
%:                                  0<3^n
%:                                 -------
%:                                 0<2·3^n
%:                                ---------
%:                     n<3^n      3^n<3·3^n
%:                   ---------    ------------
%:                   n+1<3^n+1    3^n+1<=3·3^n
%:                   -------------------------
%:                       n+1<3^{n+1}
%:
%:                       ^nn
%:
$$\ded{nn}$$

Cada uma destas barras é uma aplicação de uma regra válida, só que a
\'arvore não diz {\sl qual} regra...

Encontre uma ``justificativa'' (isto é, uma regra geral --- inspire-se
nas regras $\Foo{15}$ e $\Foo{16}$ da questão anterior) para cada uma
das barras desta árvore.



\newpage

{\bf Mini-gabarito (incompleto):}

1)
%:
%:   (i)       (ii)       (iv)    (ii)
%:   ---\re  --------´E   ---   --------´E
%:   B_3     B_3->B_6     B_4   B_4->B_7
%:   ----------------MP   --------------MP
%:        B_6                 B_7             (iv)
%:        -----------------------´I      ----------------\re
%:              B_6´B_7                  B_6´B_7->B_2´B_0
%:              -----------------------------------------MP
%:                    B_2´B_0
%:                    -------´E
%:                      B_2
%:                      ---\re
%:                      2ÝB
%:
%:                      ^gab-1
%:
$$\ded{gab-1}$$









%

\end{document}

% Local Variables:
% coding:           raw-text-unix
% ee-anchor-format: "«%s»"
% End:
