% (find-angg "LATEX/2018-2-MD-demonstracoes.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2018-2-MD-demonstracoes.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2018-2-MD-demonstracoes.pdf"))
% (defun e () (interactive) (find-LATEX "2018-2-MD-demonstracoes.tex"))
% (defun u () (interactive) (find-latex-upload-links "2018-2-MD-demonstracoes"))
% (find-xpdfpage "~/LATEX/2018-2-MD-demonstracoes.pdf")
% (find-sh0 "cp -v  ~/LATEX/2018-2-MD-demonstracoes.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2018-2-MD-demonstracoes.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2018-2-MD-demonstracoes.pdf
%               file:///tmp/2018-2-MD-demonstracoes.pdf
%           file:///tmp/pen/2018-2-MD-demonstracoes.pdf
% http://angg.twu.net/LATEX/2018-2-MD-demonstracoes.pdf
\documentclass[oneside]{article}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{color}                % (find-LATEX "edrx15.sty" "colors")
\usepackage{colorweb}             % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof}   % For derivation trees ("%:" lines)
%\input diagxy        % For 2D diagrams ("%D" lines)
%\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
\catcode`\^^J=10                      % (find-es "luatex" "spurious-omega")
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")
\def\expr#1{\directlua{output(tostring(#1))}}
\def\eval#1{\directlua{#1}}
%
\usepackage{edrx15}               % (find-angg "LATEX/edrx15.sty")
\input edrxaccents.tex            % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-dn4ex "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
% (find-angg ".emacs.papers" "latexgeom")
% (find-latexgeomtext "total={6.5in,8.75in},")
\usepackage[%total={6.5in,4in},
            %textwidth=4in,  paperwidth=4.5in,
            %textheight=5in, paperheight=4.5in,
            a4paper,
            top=1.5in, left=1.5in%, includefoot
           ]{geometry}
%
\begin{document}

\catcode`\^^J=10

\def\V{\mathbf{V}}
\def\F{\mathbf{F}}
\def\Par  {\mathsf{par}}
\def\Impar{\mathsf{impar}}


\section{Duas demonstrações comentadas}

A VR e a VS vão vir com uma folha extra com dicas, e essas dicas vão
incluir as duas demonstrações abaixo, mas sem os comentários em
português.

\subsection{Uma demonstração que usa as duas regras do `$∃$'}

\def\smr#1{}
\def\smr#1{\hbox to 0pt{ ($#1$)\hss}}

\begin{minipage}[t]{25em}
\par 1) Suponha $a∈\Z$
\par 2) Suponha $\Impar(a)$
\par 3) Então $\Impar(a)$
\par 4) Então $∃b∈\Z.2b+1=a$ \hfill (Por 3, def)
\par 5) Suponha $b∈\Z,2b+1=a$
\par 6) Então $\begin{array}[t]{rcl}
               a^2 &=& (2b+1)^2 \\
                   &=& 4b^2 + 4b + 1 \\
                   &=& 2(b^2+2b) + 1 \\
               \end{array}$
\par 7) Então $2b^2+2b∈\Z∧2(b^2+2b)+1=a^2$
\par 8) Então $∃c∈\Z.2c+1=a^2$ \quad ($c:=2b^2+2b$) \hfill\smr{∃F}
\par 9) Então $\Impar(a^2)$
\par 10) Então $\Impar(a^2)$ \hfill (Usa 4, fecha 5)\smr{∃D}
\par 11) Então $\Impar(a)→\Impar(a^2)$ \hfill (fecha 2)
\par 12) Então $∀a∈\Z.\Impar(a)→\Impar(a^2)$ \hfill (fecha 1)\smr{∀D}
\end{minipage}

\bsk

A linha 3 corresponde a esta proposição,

3) $a∈\Z, \Impar(a) ⊢ \Impar(a)$

que é bem fácil de provar em LK (tente!).

\ssk

Na linha 4 nós usamos a justificativa ``completa'': o ``def'' quer
dizer ``por definição'', que no caso é pela definição de $\Impar$, que
é: Para $x∈\Z$, \; $\Impar(x) := ∃a∈\Z.2a+1=x$ (veja os quadros de
15/agosto), mas muitas vezes vamos omitir a justificativa, ou parte
dela. E lembre que vimos, nas aulas em que lemos as páginas 14 e 15 do
livro da Judith Gersting, que podemos mudar os nomes de variáveis
ligadas: $(∃a∈\Z.2a+1=x) = (∃b∈\Z.2b+1=x)$.

\ssk

A linha 5 adiciona ``$b∈\Z,2b+1=a$'' ao contexto pra gente poder
mencionar a variável $b$ nas linhas seguintes. Isto foi discutido nos
quadros de 22/agosto a 4/setembro, principalmente na parte sobre ``O
erro mais comum''.

\ssk

A linha 6 é uma ``prova álgebrica'' (veja a p.27 do Scheinerman).

\ssk

A passagem da linha 7 para a linha 8 (vamos escrever isto como
``$7→8$'' daqui por diante) usa a regra fácil para o `$∃$', que no
Scheinerman aparece como ``Esquema de prova 7: afirmações
existenciais'', na p.65.

% (find-scheinermanpage (+ 19 65) "Esquema de prova 7: afirmações existenciais")

\msk

A passagem $9→10$ usa a linha 4, que corresponde à proposição:

$a∈\Z, \Impar(a) ⊢ ∃b∈\Z.2b+1=a$,

para deletar as hipóteses $b∈\Z,2b+1=a$ do contexto da linha 9; a
linha 9 é:

$a∈\Z, \Impar(a), b∈\Z, 2b+1=a ⊢ \Impar(a^2)$,

e a linha 10 é:

$a∈\Z, \Impar(a) ⊢ \Impar(a^2)$.

A passagem $9→10$ usa a ``regra difícil para o `$∃$'\,'', que pode ser
escrita assim em LK:
%:
%:  Γ⊢∃y∈B.P   Γ,y∈B,P⊢Q
%:  --------------------------(∃D)
%:             Γ⊢Q
%:
%:             ^ex-D
%:
$$\pu\ded{ex-D}$$
%
mas ela só é aplicável se a variável $y$ não está livre na proposição
$Q$.

\newpage

A passagem $10→11$ fica assim em LK (caso particular e versão geral):
%:
%:   a∈\Z,\Impar(a)⊢\Impar(a^2)    Γ,P⊢Q
%:   --------------------------    -----
%:   a∈\Z⊢\Impar(a)→\Impar(a^2)    Γ⊢P→Q
%:
%:   ^imp1                         ^imp2
%:
$$\pu \ded{imp1} \qquad \ded{imp2}$$

A passagem $11→12$ fica assim (caso particular e versão geral):
%:
%:   a∈\Z⊢\Impar(a)→\Impar(a^2)        Γ,y∈B⊢P
%:   --------------------------(∀D)    -------(∀D)
%:   ⊢∀a∈\Z.\Impar(a)→\Impar(a^2)      Γ⊢∀y∈B.P
%:
%:   ^fa1                              ^fa2
%:
$$\pu \ded{fa1} \qquad \ded{fa2}$$


\subsection{Uma demonstração com lemas e indução}

% (find-scheinermanpage (+ 19 15) "Lema")

\begin{minipage}[t]{33em}
\par 1) Lema: $∀a∈\Z.\Par(a)→\Impar(a+1)$
\par 2) Lema: $∀a∈\Z.\Impar(a)→\Par(a+1)$
\par 3) Suponha $n∈\N$
\par 4) Então $n∈\Z$
\par 5) Então $\Par(n)→\Impar(n+1)$   \hfill (Por 1, com $a:=n$)\smr{∀F}
\par 6) Então $\Impar(n)→\Par(n+1)$   \hfill (Por 2, com $a:=n$)\smr{∀F}
\par 7) Então $\Par(n)∨\Impar(n)→\Par(n+1)∨\Impar(n+1)$  \hfill (Por 5 e 6)
\par 8) Então $∀n∈\N.\Par(n)∨\Impar(n)→\Par(n+1)∨\Impar(n+1)$ \hfill (Fecha 4)\smr{∀D}
\par 9) Lema: $\Par(0)$
\par 10) Então $\Par(0)∨\Impar(0)$
\par 11) Então $∀n∈\N.\Par(n)∨\Impar(n)$  \hfill (Por 10 e 8)\smr{Ind}
\end{minipage}

\msk

O capítulo 1 do Scheinerman menciona ``lemas'' na p.15, mas nós não
usamos lemas de forma muito explícita nos quadros do curso. As linhas
``Lema:'' da demonstração podem ser entendidas ou como linhas
``Então'' cuja justificativa, se fosse escrita explicitamente, seria
``isto é uma cópia de uma proposição que já provamos na página tal'',
ou como uma linha ``Suponha'' mencionando uma proposição que vamos
provar depois.

\msk

A linha 5 usa a regra fácil do `$∀$', que é assim em LK:
%:
%:  Γ⊢∀y∈B.P  Γ⊢t∈B
%:  ---------------(∀F)
%:     Γ⊢P[y:=t]
%:
%:     ^faf
%:
$$\pu\ded{faf}$$

Repare que
%
$$(∀F)\subst{Γ:= \\ y:=a \\ B:=\Z \\ P:=\Par(a)→\Impar(a+1) \\ t:=n}$$
%
dá exatamente a passagem de 1 e 4 para 5.

\msk

A passagem de 5 e 6 para 7 usa a idéia de que ``todas as regras
admissíveis são válidas'' que discutimos na última aula do curso, em
que pouquíssima gente veio (12/dezembro). Nós vimos em sala como
verificar que uma certa regra era admissivel usando uma tabela com uma
linha para cada caso, e dá pra fazer o mesmo pra esta regra aqui (mas
a tabela ficaria grande):
%:
%:  Γ⊢A→B  Γ⊢C→D
%:  ------------(Ad1)
%:    Γ⊢A∨C→D∨B
%:
%:    ^Ad1
%:
$$\pu\ded{Ad1}$$
%
Repare que
%
$$(Ad1)\subst{Γ:=n∈\N \\ A:=\Par(n) \\ B:=\Impar(n+1) \\ C:=\Impar(n) \\ D:=\Par(n+1)}$$
%
dá exatamente a passagem de 5 e 6 para 7.

A passagem de 9 para 10 usa uma regra admissível bem fácil (qual?
Exercício!), e a passagem de 10 e 8 para 11 usa indução --- mas não as
induções que provam equivalências de séries de números, que eu avisei
que cairiam na P2! Lembre de fazer os exercícios 21.2 e 21.3 da p.193
do Scheinerman para treinar o tipo de indução que vai cair na P2!

% (find-scheinermanpage (+ 19 177)  "21. Indução")
% (find-scheinermanpage (+ 19 181)   "Esquema de prova 17: indução")
% (find-scheinermanpage (+ 19 187)   "Esquema de prova 18: indução forte")
% (find-scheinermanpage (+ 19 192)   "Exercícios")
% (find-scheinermanpage (+ 19 193)   "(mais exercícios)")



\newpage

%:   Δ⊢Γ          Δ⊢Γ       
%:  -----(WL-)   -----(WR-)  
%:  Δ,A⊢Γ        Δ⊢Γ,A      
%:                          
%:  ^WL-         ^WR-        
%:
%:   Δ,Γ⊢Σ          Δ⊢Γ,Σ       
%:  -----(WL)    -----(WR)  
%:  Δ,A,Γ⊢Σ      Δ⊢Γ,A,Σ      
%:                          
%:  ^WL          ^WR        
%:
%:  Δ,A,B,Γ⊢Σ       Δ⊢Γ,A,B,Σ       
%:  ---------(PL)   ---------(PR)  
%:  Δ,B,A,Γ⊢Σ       Δ⊢Γ,B,A,Σ
%:                          
%:     ^PL             ^PR        
%:
%:  Δ,A,A⊢Γ         Δ⊢Γ,A,A       
%:  -------(CL-)     -------(CR-)   
%:   Δ,A⊢Γ           Δ⊢Γ,A        
%:
%:    ^CL-             ^CR-
%:
%:  Δ,A,A,Γ⊢Σ         Δ⊢Γ,A,A,Σ       
%:  -------(CL)     -------(CR)   
%:   Δ,A,Γ⊢Σ           Δ⊢Γ,A,Σ        
%:
%:    ^CL               ^CR
%:
\pu


% (find-wikiseqpage 5)

%:
%:  Γ⊢Δ,A∧B          Γ⊢Δ,A∧B          Γ,A∧B⊢Δ       Γ⊢A,Δ   Σ⊢B,Π
%:  -------(R∧_1)    -------(R∧_2)    -------(L∧)   -------------(R∧)
%:   Γ⊢Δ,A            Γ⊢Δ,B           Γ,A,B⊢Δ        Γ,Σ⊢A∧B,Δ,Π
%:                                  
%:   ^Rand1           ^Rand2           ^Land          ^Rand          
%:
%:
%:  Γ,A∨B⊢Δ          Γ,A∨B⊢Δ          Γ⊢A∨B,Δ       Γ,A⊢Δ   Σ,B⊢Π    
%:  -------(L∨_1)    -------(L∨_2)    -------(R∨)   -------------(L∨)
%:   Γ,A⊢Δ            Γ,B⊢Δ           Γ⊢A,B,Δ        Γ,Σ,A∨B⊢Δ,Π     
%:                                                                   
%:   ^Lor1            ^Lor2            ^Ror           ^Lor
%:
%:
\pu

%:           Γ⊢Δ,A  A,Σ⊢Π
%:  ---(I)   ------------(Cut)
%:  A⊢A        Γ,Σ⊢Δ,Π
%:
%:  ^I          ^Cut
%:
\pu

%:
%:   Γ⊢A,Δ   Σ,B⊢Π         Γ⊢A,Δ   Σ⊢B,Π
%:   --------------(→L)    -------------(→R)    
%:   Γ,Σ,A→B⊢Δ,Π             Γ⊢A→B,Δ       
%:
%:   ^toL                     ^toR
%:
\pu

%:
%:   Γ⊢A,Δ        Γ,A⊢Δ        
%:   -----(¬L)    -----(¬R)    
%:   Γ,¬A⊢Δ       Γ⊢¬A,Δ       
%:
%:   ^notL        ^notR
%:
\pu


% (find-wikiseqpage 8)
%:
%:    Γ,P[y:=t]⊢Δ           Γ⊢P,Δ       
%:    -----------(∀L)     -----------(∀R)^*
%:    Γ,∀y.P⊢Δ            Γ⊢∀y.P,Δ        
%:                                          
%:    ^faL                  ^faR              
%:
%:
%:       Γ,P⊢Δ            Γ⊢P[y:=t],Δ             
%:    -----------(∃L)^*   -----------(∃R)
%:    Γ,∃y.P⊢Δ            Γ⊢∃y.P,Δ          
%:                                            
%:    ^exL                  ^exR              
%:
\pu



\fbox{
\begin{tabular}{l}
Regras estruturais: \\
weakening, permutation, contraction \\
\\
$\begin{array}{ccc}
 \ded{WL-} && \ded{WR-} \\ \\
 \ded{WL}  && \ded{WR} \\ \\
 \ded{PL}  && \ded{PR} \\ \\
 \ded{CL-} && \ded{CR-} \\ \\
 \ded{CL}  && \ded{CR} \\ \\
 \end{array}
$ \\
\end{tabular}
}
%
\fbox{
\begin{tabular}{l}
Identidade e cut:
\\
$\begin{array}{ccc}
 \ded{I} \\ \\
 \ded{Cut} \\
 \end{array}
$ \\
\end{tabular}
}


\ssk

\fbox{
\begin{tabular}{l}
Regras lógicas pro $∧$: \\
\\
$\begin{array}{c}
\ded{Rand1} \\ \\
\ded{Rand2} \\ \\
\ded{Land} \\ \\
\ded{Rand} \\
\end{array}
$
\end{tabular}
}
%
%\quad
%
\fbox{
\begin{tabular}{l}
Regras lógicas pro $∨$: \\
\\
$\begin{array}{c}
\ded{Lor1} \\ \\
\ded{Lor2} \\ \\
\ded{Ror} \\ \\
\ded{Lor} \\
\end{array}
$
\end{tabular}
}

\ssk

\fbox{
\begin{tabular}{l}
Regras lógicas pro $→$: \\
\\
$\begin{array}{c}
\ded{toL} \\ \\
\ded{toR} \\
\end{array}
$
\end{tabular}
}
%
%\quad
%
\fbox{
\begin{tabular}{l}
Regras lógicas pro $¬$: \\
\\
$\begin{array}{c}
\ded{notL} \\ \\
\ded{notR} \\
\end{array}
$
\end{tabular}
}

\ssk

\fbox{
\begin{tabular}{l}
Regras lógicas para o $∀$: \\
\\
$\begin{array}{ccc}
 \ded{faR}  \\ \\
 \ded{faL} \\
 \end{array}
$ \\
\end{tabular}
}
\fbox{
\begin{tabular}{l}
Regras lógicas para o $∃$: \\
\\
$\begin{array}{ccc}
 \ded{exR}  \\ \\
 \ded{exL} \\
 \end{array}
$ \\
\end{tabular}
}

\ssk

Nas regras $(∀R)^*$ e $(∃L)^*$ o `${}^*$' quer dizer que o $y$ não
pode

aparecer como variável livre em $Γ$ ou $Δ$.





\end{document}

% Local Variables:
% coding: utf-8-unix
% End:
