Resumo das Regras para a Dedução Natural
Material de aula da disciplina MAC0239 - Introdução à Lógica e Verificação de Programas (Agosto de 2015)
\documentclass{article}
\usepackage[portuguese]{babel}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{parskip}
\usepackage[colorinlistoftodos]{todonotes}
\usepackage{logicproof}
\usepackage{tabularx}
\PassOptionsToPackage{hyphens}{url}\usepackage{hyperref}
\usepackage[a4paper, total={7.5in, 10in}]{geometry}
\hypersetup{
colorlinks = true,
urlcolor = blue,
linkcolor = blue,
citecolor = red
}
% -----------------------------------------------------------------------------
% -----------------------------------------------------------------------------
\title{Resumo das Regras para a Dedução Natural}
\author{MAC0239 -- Introdução à Lógica e Verificação de Programas}
\date{Agosto de 2015}
\begin{document}
\maketitle
\section{Tabela de regras básicas}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Primeira parte da tabela
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{center}
\large
\begin{tabularx}{\textwidth}{ |>{\hsize=.2\hsize}X | >{\hsize=.4\hsize}X | >{\hsize=.4\hsize}X| }
\cline{2-3}
\multicolumn{1}{r|}{} & \begin{center}Introdução\end{center} & \begin{center}Eliminação\end{center} \\
\hline
\begin{center}
Regras para a conjunção ($\land$)
\end{center}
&
\begin{center}
\Huge
$\dfrac{\phi \quad \psi}{\phi \land \psi}$
\large
$\land{i}$
\end{center}
&
\begin{center}
\Huge
$\dfrac{\phi \land \psi}{\phi}$
\Large
$\land{e_1}$
\vspace{1em}
\Huge
$\dfrac{\phi \land \psi}{\psi}$
\Large
$\land{e_2}$
\end{center}
\\
\hline
\begin{center}
Regras para a dupla negação ($\lnot\lnot$)
\end{center}
&
\begin{center}
\Huge
$\dfrac{\phi}{\lnot\lnot\phi}$
\Large
$\lnot\lnot{i}$
\end{center}
&
\begin{center}
\Huge
$\dfrac{\lnot\lnot\phi}{\phi}$
\Large
$\lnot\lnot{e}$
\end{center}
\\
\hline
\begin{center}
Regras para o condicional ($\to$)
\end{center}
&
\begin{center}
\Huge
$\dfrac{\boxed{\begin{array}{c}
\phi \\
\vdots \\
\psi
\end{array}}}{\phi \to \psi}$
\Large
$\to{i}$
\end{center}
&
\begin{center}
\Huge
$\dfrac{\phi \quad \phi \to \psi}{\psi}$
\Large
$\to{e}$
\vspace{0.5em}
\begin{minipage}[][][c]{\hsize}
\todo[inline]{\textbf{\textit{modus ponens}} \newline {\small método (\textit{modus}) que afirma (\textit{ponens}) o consequente}}
\end{minipage}
\vspace{1em}
\Huge
$\dfrac{\phi \to \psi \quad \lnot\psi}{\lnot\phi}$
\Large
$MT$
\vspace{0.5em}
\begin{minipage}[][][c]{\hsize}
\todo[inline]{\textbf{\textit{modus tollens}} \newline {\small método (\textit{modus}) que nega (\textit{tollens}) o antecedente}}
\end{minipage}
\end{center}
\\
\hline
\end{tabularx}
\end{center}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Segunda parte da tabela
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\pagebreak
\begin{center}
\large
\begin{tabularx}{\textwidth}{ |>{\hsize=.2\hsize}X | >{\hsize=.4\hsize}X | >{\hsize=.4\hsize}X| }
\cline{2-3}
\multicolumn{1}{r|}{} & \begin{center}Introdução\end{center} & \begin{center}Eliminação\end{center} \\
\hline
\begin{center}
Regras para a disjunção ($\lor$)
\end{center}
&
\begin{center}
\Huge
$\dfrac{\phi}{\phi \lor \psi}$
\large
$\lor{i_1}$
\vspace{1em}
\Huge
$\dfrac{\psi}{\phi \lor \psi}$
\large
$\lor{i_2}$
\end{center}
&
\begin{center}
\Huge
$\dfrac{\begin{array}{c} \\ \\ \phi \lor \psi \end{array} \quad \boxed{\begin{array}{c}
\phi \\
\vdots \\
\chi
\end{array}} ~ \boxed{\begin{array}{c}
\psi \\
\vdots \\
\chi
\end{array}}}{\chi}$
\Large
$\lor{e}$
\end{center}
\\
\hline
\begin{center}
Regras para a contradição ($\bot$)
\end{center}
&
\begin{center}
\begin{minipage}[][][c]{\hsize}
\todo[inline,color=green!40,size=\Large]{Não há regra de introdução para $\bot$}
\end{minipage}
\end{center}
&
\begin{center}
\Huge
$\dfrac{\bot}{\phi}$
\Large
$\bot{e}$
\end{center}
\\
\hline
\begin{center}
Regras para a negação ($\lnot$)
\end{center}
&
\begin{center}
\Huge
$\dfrac{\boxed{\begin{array}{c}
\phi \\
\vdots \\
\bot
\end{array}}}{\lnot\phi}$
\Large
$\lnot{i}$
\end{center}
&
\begin{center}
\Huge
$\dfrac{\phi \quad \lnot\phi}{\bot}$
\Large
$\lnot{e}$
\end{center}
\\
\hline
\end{tabularx}
\end{center}
\section{Tabela de regras deduzidas}
\begin{center}
\large
\begin{tabularx}{\textwidth}{ |>{\hsize=.2\hsize}X | >{\hsize=.8\hsize}X| }
\hline
\begin{center}
Regra para a demonstração por absurdo ($DPA$)
\end{center}
&
\begin{center}
\Huge
$\dfrac{\boxed{\begin{array}{c}
\lnot\phi \\
\vdots \\
\bot
\end{array}}}{\phi}$
\Large
$DPA$
\end{center}
\\
\hline
\begin{center}
Regra da lei do terceiro excluído ($LTE$)
\end{center}
&
\begin{center}
\Huge
$\dfrac{}{\phi \lor \lnot\phi}$
\Large
$LTE$
\end{center}
\\
\hline
\end{tabularx}
\end{center}
\section{Observações importantes}
\begin{enumerate}
\item As regras \underline{\textit{modus tollens}} ($MT$) e \underline{introdução da dupla negação} ($\lnot\lnot{i}$) também podem ser consideradas como regras deduzíveis a partir das demais regras básicas.
\item Há também a regra (básica) de cópia (indicada apenas por $copie$) que permite copiar qualquer fórmula $\phi$ anteriormente utilizada em uma demonstração, contanto que ela não esteja em um bloco de hipóteses temporárias já fechado.
\end{enumerate}
\end{document}