|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (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: