diff --git a/book/logical-structure/logical-equivalence.tex b/book/logical-structure/logical-equivalence.tex
index 38735be..4f6de88 100644
--- a/book/logical-structure/logical-equivalence.tex
+++ b/book/logical-structure/logical-equivalence.tex
@@ -1,125 +1,128 @@
 % !TeX root = ../../infdesc.tex
-\section{Logical equivalence}
+\section{Equivalencia lógica}
 \secbegin{secLogicalEquivalence}
 
-We motivate the content of this section with an example.
+Motivamos o conteúdo desta seção com um exemplo.
 
 \begin{example}
 \label{exNoEvenPrimeGreaterThanTwo}
-Consider the following two logical formulae, where $P$ denotes the set of all prime numbers.
+Considere as duas fórmulas lógicas a seguir, onde $P$ denota o conjunto de todos os números primos.
 \begin{enumerate}[(1)]
 \item $\forall n \in P,\, (n > 2 \Rightarrow [\exists k \in \mathbb{Z},\, n=2k+1])$;
 \item $\neg \exists n \in P,\, (n > 2 \wedge [\exists k \in \mathbb{Z},\, n=2k])$.
 \end{enumerate}
-The logical formula (1) translates to `every prime number greater than two is odd', and the logical formula (2) translates to `there does not exist an even prime number greater than two'. These statements are evidently \textit{equivalent}---they mean the same thing---but they suggest different proof strategies:
+A fórmula lógica (1) se traduz em “todo número primo maior que dois é ímpar”, e a fórmula lógica (2) se traduz em “não existe um número primo par maior que dois”. Estas afirmações são evidentemente \textit{equivalentes}---elas significam a mesma coisa---mas sugerem diferentes estratégias de prova:
 
 \begin{enumerate}[(1)]
-\item Fix a prime number $n$, assume that $n>2$, and then prove that $n = 2k+1$ for some $k \in \mathbb{Z}$.
-\item Assume that there is some prime number $n$ such that $n>2$ and $n=2k$ for some $k \in \mathbb{Z}$, and derive a contradiction.
+\item Corrija um número primo $n$, assuma que $n>2$, e então prove que $n = 2k+1$ para alguns $k \in \mathbb{Z}$.
+\item Suponha que exista um número primo $n$ de tal modo que $n>2$ e $n=2k$ para algum $k \in \mathbb{Z}$, e deduza a contradição.
 \end{enumerate}
 
-While statement (1) more directly translates the plain English statement `every prime number greater than two is odd', it is the proof strategy suggested by (2) that is easier to use. Indeed, if $n$ is a prime number such that $n>2$ and $n=2k$ for some $k \in \mathbb{Z}$, then $2$ is a divisor of $n$ other than $1$ and $n$ (since $1<2<n$), contradicting the assumption that $n$ is prime.
+Embora a afirmação (1) traduza mais diretamente a afirmação simples “todo número primo maior que dois é ímpar”, é a estratégia de prova sugerida por (2) que é mais fácil de usar. De fato, se $n$ é a número primo de tal modo que $n>2$ e $n=2k$ para $k \in \mathbb{Z}$, então $2$ é um divisor de $n$ diferente de $1$ e $n$ (desde que $1<2<n$), contradizendo afirmação que $n$ é primo.
 \end{example}
 
-The notion of \textit{logical equivalence}, captures precisely the sense in which the logical formulae in (1) and (2) in \Cref{exNoEvenPrimeGreaterThanTwo} `mean the same thing'. Being able to transform a logical formula into a different (but equivalent) form allows us to identify a wider range of feasible proof strategies.
+A noção de \textit{logical equivalence}, captura precisamente o sentido em que a fórmula lógica em (1) e (2) em \Cref{exNoEvenPrimeGreaterThanTwo} `significa a mesma coisa'. Ser capaz de transformar uma fórmula lógica numa forma diferente (mas equivalente) permite-nos identificar uma gama mais ampla de estratégias de prova viáveis.
 
 \begin{definition}
 \label{defLogicalEquivalence}
 \index{logical equivalence}
 \index{equivalence!logical}
 \nindex{logical equivalence}{$\equiv$}{logical equivalence}
-Let $p$ and $q$ be logical formulae. We say that $p$ and $q$ are \textbf{logically equivalent}, and write $p \equiv q$ \inlatex{equiv}\lindexmmc{equiv}{$\equiv$}, if $q$ can be derived from $p$ and $p$ can be derived from $q$.
+Seja $p$ e $q$ fórmulas lógicas. Nós dizemos que $p$ e $q$ são \textbf{logicalmente equivalente}, e escrevemos $p \equiv q$ \inlatex{equiv}\lindexmmc{equiv}{$\equiv$}, se $q$ pode ser derivado de $p$ e $p$ pode ser derivado de $q$.
 \end{definition}
 
-\subsection*{Logical equivalence of propositional formulae}
+\subsection*{Equivalencia lógica de fórmulas proposicionais}
 
-While \Cref{defLogicalEquivalence} defines logical equivalence between arbitrary logical formulae, we will start by focusing our attention on logical equivalence between \textit{propositional} formulae, like those we saw in \Cref{secPropositionalLogic}.
-
-First, let's look at a couple of examples of what proofs of logical equivalence might look like. Be warned---they're not very nice to read! But there is light at the end of the tunnel. After struggling through \Cref{exConjunctionDistributesOverDisjunction,exImplicationInTermsOfDisjunction} and \Cref{exPAndQImpliesRIffPImpliesRAndQImpliesR}, we will introduce a very quick and easy tool for proving propositional formulae are logically equivalent.
+Enquanto \Cref{defLogicalEquivalence} define equivalência lógica entre fórmulas lógicas arbitrárias, começaremos focando nossa atenção na equivalência lógica entre fórmulas \textit{proposicionais}, como vimos em \Cref{secPropositionalLogic}.
 
+Primeiro, vejamos alguns exemplos de como podem ser as provas de equivalência lógica. Esteja avisado: eles não são muito agradáveis ​​de ler! Mas há luz no fim do túnel. Depois de lutar \Cref{exConjunctionDistributesOverDisjunction,exImplicationInTermsOfDisjunction} e \Cref{exPAndQImpliesRIffPImpliesRAndQImpliesR},apresentaremos uma ferramenta muito rápida e fácil para provar que fórmulas proposicionais são logicamente equivalentes.
 \begin{example}
 \label{exConjunctionDistributesOverDisjunction}
-We demonstrate that $p \wedge (q \vee r) \equiv (p \wedge q) \vee (p \wedge r)$, where $p$, $q$ and $r$ are propositional variables.
+Nós demostramos que p∧(q∨r)≡(p∧q)∨(p∧r)p \wedge (q \vee r) \equiv (p \wedge q) \vee (p \wedge r), onde pp, qq and rr são variáveis proposicionais.
 
 \begin{itemize}
-\item First assume that $p \wedge (q \vee r)$ is true. Then $p$ is true and $q \vee r$ is true by definition of conjunction. By definition of disjunction, either $q$ is true or $r$ is true.
+\item Primeiro assuma que p∧(q∨r)p \wedge (q \vee r) é verdade. Então pp é verdade e q∨rq \vee r é verdade pela definição de conjunção. Pela definição de disjunção, qualquer qq é verdade ou rr é verdade.
 \begin{itemize}
-\item If $q$ is true, then $p \wedge q$ is true by definition of conjunction.
-\item If $r$ is true, then $p \wedge r$ is true by definition of conjunction.
+\item Se $q$ é verdade, então $p \wedge q$ é verdade pela definição de conjunção.
+\item Se $r$ é verdade, então $p \wedge r$ é verdade pela definição de conjunção.
 \end{itemize}
-In both cases we have that $(p \wedge q) \vee (p \wedge r)$ is true by definition of disjunction.
+Em ambos os casos nós temos que $(p \wedge q) \vee (p \wedge r)$ é verdade pela definição de conjunção.
 
-\item Now assume that $(p \wedge q) \vee (p \wedge r)$ is true. Then either $p \wedge q$ is true or $p \wedge r$ is true, by definition of disjunction.
+\item Agora assuma que $(p \wedge q) \vee (p \wedge r)$ é verdade. Então qualquer $p \wedge q$ is true or $p \wedge r$ é verdade, pela definição de disjunção.
 \begin{itemize}
-\item If $p \wedge q$ is true, then $p$ is true and $q$ is true by definition of conjunction.
-\item If $p \wedge r$ is true, then $p$ is true and $r$ is true by definition of conjunction.
+\item Se $p \wedge q$ é verdade, então $p$ é veradde e $q$ é verdadeiro pela definição de conjunção.
+\item If $p \wedge r$ é verdade, então $p$ é verrdade e $r$ é verdadeiro pela definição de conjunção.
 \end{itemize}
-In both cases we have that $p$ is true, and that $q \vee r$ is true by definition of disjunction. Hence $p \wedge (q \vee r)$ is true by definition of conjunction.
+Em ambos os casos nós temos que $p$ é verdade, e que $q \vee r$ é verdairo pela definição de disjunção. Por isso $p \wedge (q \vee r)$ é verdadeiro pela definição de conjunção.
 \end{itemize}
 
-Since we can derive $(p \wedge q) \vee (p \wedge r)$ from $p \wedge (q \vee r)$ and vice versa, it follows that
+Já que podemos derivar $(p \wedge q) \vee (p \wedge r)$ from $p \wedge (q \vee r)$ e vice-versa, segue que
 \[ p \wedge (q \vee r) \equiv (p \wedge q) \vee (p \wedge r)\]
-as required.
+como requerido.
 \end{example}
 
 \begin{example}
 \label{exImplicationInTermsOfDisjunction}
-We prove that $p \Rightarrow q \equiv (\neg p) \vee q$, where $p$, $q$ and $r$ are propositional variables.
+Nós provamos que $p \Rightarrow q \equiv (\neg p) \vee q$, onde $p$, $q$ e $r$ são variáveis ​​proposicionais.
 
 \begin{itemize}
-\item First assume that $p \Rightarrow q$ is true. By the law of excluded middle (\Cref{axLEM}), either $p$ is true or $\neg p$ is true---we derive $(\neg p) \vee q$ in each case.
+\item Primeiro assuma que $p \Rightarrow q$ é verdade. Pela lei do meio excluído (\Cref{axLEM}), qualquer $p$ é verdadeiro ou $\neg p$ é verdadeiro---nós derivamos $(\neg p) \vee q$ em cada caso.
 \begin{itemize}
-\item If $p$ is true, then since $p \Rightarrow q$ is true, it follows from \elimrule{\Rightarrow} that $q$ is true, and so $(\neg p) \vee q$ is true by \introrulesub{\vee}{2};
-\item If $\neg p$ is true, then $(\neg p) \vee q$ is true by \introrulesub{\vee}{1}.
+\item Se $p$ é verdade, então ja qué $p \Rightarrow q$ é verdade,segue de \elimrule{\Rightarrow} que $q$ é verdadeiro, e assim $(\neg p) \vee q$ é verdade por \introrulesub{\vee}{2};
+\item Se $\neg p$ é verdade, então $(\neg p) \vee q$ é verdadeiro por \introrulesub{\vee}{1}.
 \end{itemize}
-In both cases, we see that $(\neg p) \vee q$ is true.
+Em ambos os casos, nós vemos que$(\neg p) \vee q$ é verdade.
 
-\item Now assume that $(\neg p) \vee q$ is true. To prove that $p \Rightarrow q$ is true, it suffices by \introrule{\Rightarrow} to assume that $p$ is true and derive $q$. So assume $p$ is true. Since $(\neg p) \vee q$ is true, we have that either $\neg p$ is true or $q$ is true.
-\begin{itemize}
-\item If $\neg p$ is true, then we obtain a contradiction from the assumption that $p$ is true, and so $q$ is true by the principle of explosion (\Cref{axPrincipleOfExplosion}).
-\item If $q$ is true\dots{} well, then $q$ is true---there is nothing more to prove!
+\item Agora suponha que $(\neg p) \vee q$ seja verdadeiro. Para provar que $p \Rightarrow q$ é verdadeiro, basta por \introrule{\Rightarrow} assumir que $p$ é verdadeiro e derivar $q$. Portanto, suponha que $p$ seja verdadeiro. Como $(\neg p) \vee q$ é verdadeiro, temos que $\neg p$ é verdadeiro ou $q$ é verdadeiro.
+\begin{itemizar}
+\item Se $\neg p$ for verdadeiro, então obtemos uma contradição a partir da suposição de que $p$ é verdadeiro, e então $q$ é verdadeiro pelo princípio da explosão (\Cref{axPrincipleOfExplosion}).
+\item Se $q$ for verdadeiro\dots{} bem, então $q$ é verdadeiro --- não há mais nada a provar!
 \end{itemize}
-In both cases we have that $q$ is true. Hence $p \Rightarrow q$ is true.
+Em ambos os casos temos que $q$ é verdadeiro. Portanto, $p \Rightarrow q$ é verdadeiro.
 \end{itemize}
 
-We have derived $(\neg p) \vee q$ from $p \Rightarrow q$ and vice versa, and so the two formulae are logically equivalent.
+
+Nós derivamos $(\neg p) \vee q$ de $p \Rightarrow q$ e vice-versa, e então as duas fórmulas são logicamente equivalentes.
 \end{example}
 
 \begin{exercise}
 \label{exPAndQImpliesRIffPImpliesRAndQImpliesR}
-Let $p$, $q$ and $r$ be propositional variables. Prove that the propositional formula $(p \vee q) \Rightarrow r$ is logically equivalent to $(p \Rightarrow r) \wedge (q \Rightarrow r)$.
+Seja $p$, $q$ and $r$ ser variáveis ​​proposicionais. Prove que a fórmula proposicional $(p \vee q) \Rightarrow r$ é logicamente equivalente para $(p \Rightarrow r) \wedge (q \Rightarrow r)$.
 \end{exercise}
 
-Working through the derivations each time we want to prove logical equivalence can become cumbersome even for small examples like \Cref{exConjunctionDistributesOverDisjunction,exImplicationInTermsOfDisjunction} and \Cref{exPAndQImpliesRIffPImpliesRAndQImpliesR}.
+Trabalhar com as derivações cada vez que quisermos provar a equivalência lógica pode se tornar complicado mesmo para pequenos exemplos como\Cref{exConjunctionDistributesOverDisjunction,exImplicationInTermsOfDisjunction} and \Cref{exPAndQImpliesRIffPImpliesRAndQImpliesR}.
+
+
+O teorema a seguir reduz o problema de provar a equivalência lógica entre fórmulas \textit{proposicionais} à tarefa puramente algorítmica de verificar quando as fórmulas são verdadeiras e quando são falsas em uma lista (relativamente) pequena de casos. Iremos agilizar ainda mais esse processo usando \textit{tabelas verdade} (\Cref{defTruthTable})
 
-The following theorem reduces the problem of proving logical equivalence between \textit{propositional} formulae to the purely algorithmic task of checking when the formulae are true and when they are false in a (relatively) small list of cases. We will streamline this process even further using \textit{truth tables} (\Cref{defTruthTable}).
 
 \begin{theorem}
 \label{thmLogicalEquivalentIffSameTruthValues}
-Two propositional formulae are logically equivalent if and only if their truth values are the same under any assignment of truth values to their constituent propositional variables.
+Duas fórmulas proposicionais são logicamente equivalentes se e somente se seus valores verdade são os mesmos sob qualquer atribuição de valores verdade às suas variáveis ​​proposicionais constituintes.
 \end{theorem}
 
+
 \begin{cidea}
-A formal proof of this fact is slightly beyond our reach at this point, although we will be able to prove it formally by \textit{structural induction}, introduced in \Cref{secStructuralInduction}.
+Uma prova formal deste facto está um pouco fora do nosso alcance neste momento, embora possamos prová-lo formalmente através  \textit{structural induction}, introduzido em \Cref{secStructuralInduction}.
 
-The idea of the proof is that, since propositional formulae are built up from simpler propositional formulae using logical operators, the truth value of a more complex propositional formula is determined by the truth values of its simpler subformulae. If we keep `chasing' these subformulae, we end up with just propositional variables.
+A ideia da prova é que, uma vez que as fórmulas proposicionais são construídas a partir de fórmulas proposicionais mais simples usando operadores lógicos, o valor verdade de uma fórmula proposicional mais complexa é determinado pelos valores verdade das suas subfórmulas mais simples. Se continuarmos a “perseguir” estas subfórmulas, acabaremos apenas com variáveis ​​proposicionais.
 
-For example, the truth value of $(p \Rightarrow r) \wedge (q \Rightarrow r)$ is determined by the truth values of $p \Rightarrow r$ and $q \Rightarrow r$ according to the rules for the conjunction operator $\wedge$. In turn, the truth value of $p \Rightarrow r$ is determined by the truth values of $p$ and $r$ according to the implication operator $\Rightarrow$, and the truth value of $q \Rightarrow r$ is determined by the truth values of $q$ and $r$ according to the implication operator again. It follows that the truth value of the whole propositional formula $(p \Rightarrow r) \wedge (q \Rightarrow r)$ is determined by the truth values of $p,q,r$ according to the rules for $\wedge$ and $\Rightarrow$.
+Por examplo, o verdadeiro valor de $(p \Rightarrow r) \wedge (q \Rightarrow r)$ é determinado pelos valores verdadeiros de $p \Rightarrow r$ and $q \Rightarrow r$ de acordo com as regras para o operador de conjunção $\wedge$. Por sua vez, o valor de verdade de $p \Rightarrow r$ é determinado pelos valores de verdade de $p$ and $r$ de acordo com o operador de implicação $\Rightarrow$, e o valor verdadeiro de $q \Rightarrow r$ é determinado pelos valores de verdade de $q$ e $r$ de acordo com o operador de implicação novamente. Segue-se que o valor de verdade de toda a fórmula proposicional $(p \Rightarrow r) \wedge (q \Rightarrow r)$ é determinado pelos verdadeiros valores de $p,q,r$ de acordo com as regras de $\wedge$ and $\Rightarrow$.
 
-If some assignment of truth values to propositional variables makes one propositional formula true but another false, then it must be impossible to derive one from the other---otherwise we'd obtain a contradiction. Hence both propositional formulae must have the same truth values no matter what assignment of truth values is given to their constituent propositional variables.
+Se alguma atribuição de valores de verdade a variáveis ​​proposicionais torna uma fórmula proposicional verdadeira, mas outra falsa, então deve ser impossível derivar uma da outra – caso contrário, obteríamos uma contradição. Portanto, ambas as fórmulas proposicionais devem ter os mesmos valores de verdade, não importa qual atribuição de valores de verdade seja dada às suas variáveis ​​proposicionais constituintes.
 \end{cidea}
 
-We now develop a systematic way of checking the truth values of a propositional formula under each assignment of truth values to its constituent propositional variables.
+Desenvolvemos agora uma forma sistemática de verificar os valores verdade de uma fórmula proposicional sob cada atribuição de valores verdade às suas variáveis ​​proposicionais constituintes.
 
 \begin{definition}
 \label{defTruthTable}
 \index{truth table}
-The \textbf{truth table} of a propositional formula is the table with one row for each possible assignment of truth values to its constituent propositional variables, and one column for each subformula (including the propositional variables and the propositional formula itself). The entries of the truth table are the truth values of the subformulae.
+O \textbf{verdairo valor} de uma fórmula proposicional é a tabela com uma linha para cada atribuição possível de valores de verdade às suas variáveis ​​proposicionais constituintes e uma coluna para cada subfórmula (incluindo as variáveis ​​proposicionais e a própria fórmula proposicional). As entradas da tabela verdade são os valores verdade das subfórmulas.
 \end{definition}
 
 \begin{example}
 \label{exNegationConjunctionDisjunctionImplicationTruthTable}
-The following are the truth tables for $\neg p$, $p \wedge q$, $p \vee q$ and $p \Rightarrow q$.
+A seguir estão as tabelas verdade para $\neg p$, $p \wedge q$, $p \vee q$ and $p \Rightarrow q$.
 
 \begin{center}
 \begin{tabular}{c|c}
@@ -162,18 +165,17 @@ \subsection*{Logical equivalence of propositional formulae}
 \end{center}
 \end{example}
 
-In \Cref{exNegationConjunctionDisjunctionImplicationTruthTable} we have used the symbol \TT{} \inlatex{checkmark}\lindexmmc{checkmark}{$\checkmark$} to mean `true' and \FF{} \inlatex{times}\lindexmmc{times}{$\times$} to mean `false'. Some authors adopt other conventions, such as $T,F$ or $\top,\bot$ \inlatex{top,\textbackslash{}bot}\lindexmmc{top}{$\top$}\lindexmmc{bot}{$\bot$} or $1,0$ or $0,1$---the possibilites are endless!
+Em \Cref{exNegationConjunctionDisjunctionImplicationTruthTable} nós temos usedo o símbolo \TT{} \inlatex{checkmark}\lindexmmc{checkmark}{$\checkmark$} para significar `verdade' e \FF{} \inlatex{times}\lindexmmc{times}{$\times$} para significar `falso'. Alguns autores adotam outras convenções, tanto quanto $T,F$ or $\top,\bot$ \inlatex{top,\textbackslash{}bot}\lindexmmc{top}{$\top$}\lindexmmc{bot}{$\bot$} or $1,0$ or $0,1$---as posibilidades são infinitas!
 
 \begin{exercise}
-Use the definitions of $\wedge$, $\vee$ and $\Rightarrow$ to justify the truth tables in \Cref{exNegationConjunctionDisjunctionImplicationTruthTable}.
-\hintlabel{exJustifyBasicTruthTables}{Note that you may need to use the law of excluded middle (\Cref{axLEM}) and the principle of explosion (\Cref{axPrincipleOfExplosion}).}
+Use as definiçõe de $\wedge$, $\vee$ and $\Rightarrow$ para justificar as tabelas verdade em \Cref{exNegationConjunctionDisjunctionImplicationTruthTable}.
+\hintlabel{exJustifyBasicTruthTables}{Observe que você pode precisar usar a lei do meio excluído (\Cref{axLEM}) e o princípio da explosão (\Cref{axPrincipleOfExplosion}).}
 \end{exercise}
 
-The next example shows how the truth tables for the individual logical operators (as in \Cref{exNegationConjunctionDisjunctionImplicationTruthTable}) may be combined to form a truth table for a more complicated propositional formula that involves three propositional variables.
-
+O próximo exemplo mostra como as tabelas verdade para os operadores lógicos individuais (as in \Cref{exNegationConjunctionDisjunctionImplicationTruthTable}) podem ser combinadas para formar uma tabela verdade para uma fórmula proposicional mais complicada que envolve três variáveis ​​proposicionais.
 \begin{example}
 \label{exFirstExampleOfTruthTable}
-The following is the truth table for $(p \wedge q) \vee (p \wedge r)$.
+A seguir está a tabela verdade para $(p \wedge q) \vee (p \wedge r)$.
 \begin{center}
 \begin{tabular}{ccc|cc|c}
 $p$ & $q$ & $r$ & $p \wedge q$  & $p \wedge r$ & $(p \wedge q) \vee (p \wedge r)$\\ \hline
@@ -189,24 +191,25 @@ \subsection*{Logical equivalence of propositional formulae}
 \multicolumn{3}{c}{\begin{minipage}{40pt}\centering\scriptsize propositional\\ variables\end{minipage}} & \multicolumn{2}{c}{\begin{minipage}{40pt}\centering\scriptsize intermediate\\ subformulae\end{minipage}} & \multicolumn{1}{c}{\scriptsize main formula}
 \end{tabular}
 \end{center}
-Some comments about the construction of this truth table are pertinent:
+Alguns comentários sobre a construção desta tabela verdade são pertinentes:
+
 \begin{itemize}
-\item The propositional variables appear first. Since there are three of them, there are $2^3=8$ rows. The column for $p$ contains four \TT{}s followed by four \FF{}s; the column for $q$ contains two \TT{}s, two \FF{}s, and then repeats; and the column for $r$ contains one \TT{}, one \FF{}, and then repeats.
-\item The next group of columns are the next-most complicated subformulae. Each is constructed by looking at the relevant columns further to the left and comparing with the truth table for conjunction.
-\item The final column is the main formula itself, which again is constructed by looking at the relevant columns further to the left and comparing with the truth table for disjunction.
+\item As variáveis ​​proposicionais aparecem primeiro. Como são três, há $2^3=8$ linhas. A coluna para $p$ contém quatro \TT{}s seguida por quatro \FF{}s; a coluna para $q$ contém dois \TT{}s, two \FF{}s, e então repete; e a coluna para $r$ contém uma \TT{}, um \FF{}, e então repete.
+\item 
+O próximo grupo de colunas são as próximas subfórmulas mais complicadas. Cada uma é construída observando as colunas relevantes mais à esquerda e comparando com a tabela verdade da conjunção.
+\item A coluna final é a própria fórmula principal, que novamente é construída observando as colunas relevantes mais à esquerda e comparando com a tabela verdade para disjunção.
 \end{itemize}
-Our choices of where to put the vertical bars and what order to put the rows in were not the only choices that could have been made, but when constructing truth tables for more complex logical formulae, it is useful to develop a system and stick to it.
+Nossas escolhas sobre onde colocar as barras verticais e em que ordem colocar as linhas não foram as únicas escolhas que poderiam ter sido feitas, mas ao construir tabelas verdade para fórmulas lógicas mais complexas, é útil desenvolver um sistema e segui-lo.
 \end{example}
 
-Returning to \Cref{thmLogicalEquivalentIffSameTruthValues}, we obtain the following strategy for proving that two propositional formulae are logically equivalent.
-
+Returnando para \Cref{thmLogicalEquivalentIffSameTruthValues}, obtemos a seguinte estratégia para provar que duas fórmulas proposicionais são logicamente equivalentes.
 \begin{strategy}[Logical equivalence using truth tables]
 \label{strTruthTable}
-In order to prove that propositional formulae are logically equivalent, it suffices to show that they have identical columns in a truth table.
+Para provar que as fórmulas proposicionais são logicamente equivalentes, basta mostrar que elas têm colunas idênticas numa tabela verdade.
 \end{strategy}
 
 \begin{example}
-In \Cref{exConjunctionDistributesOverDisjunction} we proved that $p \wedge (q \vee r) \equiv (p \wedge q) \vee (p \wedge r)$. We prove this again using truth tables. First we construct the truth table for $p \wedge (q \vee r)$:
+Em \Cref{exConjunctionDistributesOverDisjunction} nós provamos que $p \wedge (q \vee r) \equiv (p \wedge q) \vee (p \wedge r)$. Provamos isso novamente usando tabelas verdade. Primeiro construímos a tabela verdade para $p \wedge (q \vee r)$:
 \begin{center}
 \begin{tabular}{ccc|c|c}
 $p$ & $q$ & $r$ & $q \vee r$ & $p \wedge (q \vee r)$ \\ \hline
@@ -220,10 +223,10 @@ \subsection*{Logical equivalence of propositional formulae}
 \FF & \FF & \FF & \FF & \FF
 \end{tabular}
 \end{center}
-Note that the column for $p \wedge (q \vee r)$ is identical to that of $(p \wedge q) \vee (p \wedge r)$ in \Cref{exFirstExampleOfTruthTable}. Hence the two formulae are logically equivalent.
+Observe que a coluna de $p \wedge (q \vee r)$ é idêntico ao de $(p \wedge q) \vee (p \wedge r)$ in \Cref{exFirstExampleOfTruthTable}. Portanto, as duas fórmulas são logicamente equivalentes.
 \end{example}
 
-To avoid having to write out two truth tables, it can be helpful to combine them into one. For example, the following truth table exhibits that $p \wedge (q \vee r)$ is logically equivalent to $(p \wedge q) \vee (p \wedge r)$:
+Para evitar ter que escrever duas tabelas verdade, pode ser útil combiná-las em uma. Por exemplo, a seguinte tabela verdade mostra que $p \wedge (q \vee r)$ é logicamente equivalente a $(p \wedge q) \vee (p \wedge r)$:
 
 \begin{center}
 \begin{tabular}{ccc||c|c||cc|c}
@@ -239,29 +242,29 @@ \subsection*{Logical equivalence of propositional formulae}
 \end{tabular}
 \end{center}
 
-In the following exercises, we use truth tables to repeat the proofs of logical equivalence from \Cref{exImplicationInTermsOfDisjunction} and \Cref{exPAndQImpliesRIffPImpliesRAndQImpliesR}.
+Nos exercícios a seguir, usamos tabelas verdade para repetir as provas de equivalência lógica de \Cref{exImplicationInTermsOfDisjunction} e \Cref{exPAndQImpliesRIffPImpliesRAndQImpliesR}.
 
 \begin{exercise}
 \label{exImplicationInTermsOfDisjunctionWithTruthTables}
-Use a truth table to prove that $p \Rightarrow q \equiv (\neg p) \vee q$.
+Use uma tabela verdade para provar que $p \Rightarrow q \equiv (\neg p) \vee q$.
 \end{exercise}
 
 \begin{exercise}
 \label{exPAndQImpliesRIffPImpliesRAndQImpliesRWithTruthTables}
-Let $p$, $q$ and $r$ be propositional variables. Use a truth table to prove that the propositional formula $(p \vee q) \Rightarrow r$ is logically equivalent to $(p \Rightarrow r) \wedge (q \Rightarrow r)$.
+Let $p$, $q$ and $r$ ser variáveis ​​proposicionais. Use uma tabela verdade para provar que a fórmula proposicional $(p \vee q) \Rightarrow r$ é logicamente equivalente a $(p \Rightarrow r) \wedge (q \Rightarrow r)$.
 \end{exercise}
 
 \subsection*{Some proof strategies}
 
-We are now in good shape to use logical equivalence to derive some more sophisticated proof strategies.
+Estamos agora em boa forma para usar a equivalência lógica para derivar algumas estratégias de prova mais sofisticadas.
 
 \begin{theorem}[Law of double negation]
 \label{thmDoubleNegation}
-Let $p$ be a propositional variable. Then $p \equiv \neg \neg p$.
+Seja $p$ uma variável proposicional. Então $p \equiv \neg \neg p$.
 \end{theorem}
 
 \begin{cproof}
-The proof is almost trivialised using truth tables. Indeed, consider the following truth table.
+A prova é quase banalizada usando tabelas verdade. Na verdade, considere a seguinte tabela verdade.
 \begin{center}
 \begin{tabular}{c|c|c}
 $p$ & $\neg p$ & $\neg \neg p$ \\ \hline
@@ -269,51 +272,51 @@ \subsection*{Some proof strategies}
 \FF & \TT & \FF
 \end{tabular}
 \end{center}
-The columns for $p$ and $\neg \neg p$ are identical, and so $p \equiv \neg \neg p$.
+A coluna para $p$ and $\neg \neg p$ são idênticas, e então $p \equiv \neg \neg p$.
 \end{cproof}
 
-The law of double negation is important because it suggests a second way that we can prove statements by contradiction. Indeed, it says that proving a proposition $p$ is equivalent to proving $\neg \neg p$, which amounts to assuming $\neg p$ and deriving a contradiction.
+A lei da dupla negação é importante porque sugere uma segunda maneira de provar afirmações por contradição. Na verdade, diz que provar uma proposição $p$ é equivalente a provar $\neg \neg p$,o que equivale a assumir $\neg p$ e derivando uma contradição.
 
-\begin{strategy}[Proof by contradiction (indirect version)]
+\begin{strategy}[Prova por contradição (versão indireta)]
 \label{strProofByContradictionIndirect}
-\index{contradiction!(indirect) proof by}
-\index{proof!by contradiction (indirect)}
-In order to prove a proposition $p$ is true, it suffices to assume that $p$ is false and derive a contradiction.
+\index{indireta!(contradição) provado por}
+\index{por contradição! prova (indireta)}
+Para provar que uma proposição $p$ é verdadeira, basta assumir que $p$ é falsa e derivar uma contradição.
 \end{strategy}
 
-At first sight, \Cref{strProofByContradictionIndirect} looks very similar to \Cref{strProvingNegationsDirect}, which we also termed \textit{proof by contradiction}. But there is an important difference between the two:
+À primeira vista, \Cref{strProofByContradictionIndirect} parece muito parecido com \Cref{strProvingNegationsDirect}, que também denominamos \textit{prova por contradição}. Mas há uma diferença importante entre os dois:
 \begin{itemize}
-\item \Cref{strProvingNegationsDirect} says that to prove that a proposition is \textit{false}, it suffices to assume that it is \textit{true} and derive a contradiction;
-\item \Cref{strProofByContradictionIndirect} says that to prove that a proposition is \textit{true}, it suffices to assume that it is \textit{false} and derive a contradiction.
+\item \Cref{strProvingNegationsDirect} diz que para provar que uma proposição é \textit{falso}, basta supor que é \textit{verdade} e derivar uma contradição;
+\item \Cref{strProofByContradictionIndirect} diz que para provar que uma proposição é \textit{true}, basta assumir que é \textit{falso} e derivar uma contradição.
 \end{itemize}
 
-The former is a \textit{direct} proof technique, since it arises directly from the definition of the negation operator; the latter is an \textit{indirect} proof technique, since it arises from a logical equivalence, namely the law of double negation.
+A primeira é uma técnica de prova \textit{direta}, pois surge diretamente da definição do operador de negação; a última é uma técnica de prova \textit{indireta}, uma vez que surge de uma equivalência lógica, nomeadamente a lei da dupla negação.
 
 \begin{example}
-We prove that if $a$, $b$ and $c$ are non-negative real numbers satisfying $a^2+b^2=c^2$, then $a+b \ge c$.
+Nós provamos que $a$, $b$ e $c$ são números reais não negativos satisfatórios $a^2+b^2=c^2$, then $a+b \ge c$.
 
-Indeed, let $a,b,c \in \mathbb{R}$ with $a,b,c \ge 0$, and assume that $a^2+b^2=c^2$. Towards a contradiction, assume that it is not the case that $a+b \ge c$. Then we must have $a+b < c$. But then
+Na verdade,se $a,b,c \in \mathbb{R}$ com $a,b,c \ge 0$, e assuma que $a^2+b^2=c^2$. Em direção a uma contradição, suponha que não seja o caso que $a+b \ge c$. Então devemos ter $a+b < c$. Mas então
 \[ (a+b)^2 = (a+b)(a+b) < (a+b) c < c \cdot c = c^2\]
-and so
+e então
 \[ c^2 > (a+b)^2 = a^2+2ab+b^2 = c^2+2ab \ge c^2\]
-This implies that $c^2 > c^2$, which is a contradiction. So it must be the case that $a + b \ge c$, as required.
+Isso implica que $c^2 > c^2$, o que é uma contradição. Portanto, deve ser o caso de $a + b \ge c$, conforme necessário.
 \end{example}
 
-The next proof strategy we derive concerns proving implications.
+A próxima estratégia de prova que derivamos diz respeito à prova de implicações.
 
 \begin{definition}
 \label{defContrapositive}
 \index{contrapositive}
-The \textbf{contrapositive} of a proposition of the form $p \Rightarrow q$ is the proposition $\neg q \Rightarrow \neg p$.
+O \textbf{contrapositivo} de uma proposição da forma $p \Rightarrow q$ é a proposta $\neg q \Rightarrow \neg p$.
 \end{definition}
 
-\begin{theorem}[Law of contraposition]
+\begin{theorem}[Lei da contraposição]
 \label{thmLawOfContraposition}
-Let $p$ and $q$ be propositional variables. Then $p \Rightarrow q \equiv (\neg q) \Rightarrow (\neg p)$.
+Se $p$ e $q$ são variáveis ​​proposicionais. Então $p \Rightarrow q \equiv (\neg q) \Rightarrow (\neg p)$.
 \end{theorem}
 
 \begin{cproof}
-We build the truth tables for $p \Rightarrow q$ and $(\neg q) \Rightarrow (\neg p)$.
+Construímos as tabelas verdade para $p \Rightarrow q$ e $(\neg q) \Rightarrow (\neg p)$.
 
 \begin{center}
 \begin{tabular}{cc||c||cc|c}
@@ -325,51 +328,52 @@ \subsection*{Some proof strategies}
 \end{tabular}
 \end{center}
 
-The columns for $p \Rightarrow q$ and $(\neg q) \Rightarrow (\neg p)$ are identical, so they are logically equivalent.
+As colunas para $p \Rightarrow q$ and $(\neg q) \Rightarrow (\neg p)$ são idênticos, portanto são logicamente equivalentes.
 \end{cproof}
 
-\Cref{thmLawOfContraposition} suggests the following proof strategy.
+\Cref{thmLawOfContraposition} sugere a seguinte estratégia de prova.
 
-\begin{strategy}[Proof by contraposition]
+\begin{strategy}[Prova por contraposição]
 \label{strProofByContraposition}
 \index{contraposition!proof by}
 \index{proof!by contraposition}
-In order to prove a proposition of the form $p \Rightarrow q$, it suffices to assume that $q$ is false and derive that $p$ is false.
+Para provar uma proposição da forma $p \Rightarrow q$, basta assumir que $q$ é falso e derivar que $p$ é falso.
 \end{strategy}
 
 \begin{example}
-Fix two natural numbers $m$ and $n$. We will prove that if $mn > 64$, then either $m>8$ or $n>8$.
+Fixe dois números naturais $m$ e $n$. Provaremos que se $mn > 64$, então $m>8$ ou $n>8$.
 
-By contraposition, it suffices to assume that it is \textit{not} the case that $m > 8$ or $n > 8$, and derive that it is not the case that $mn > 64$.
+Por contraposição, basta assumir que \textit{não} é o caso de $m > 8$ ou $n > 8$, e derivar que não é o caso de $mn > 64$.
 
-So assume that neither $m>8$ nor $n>8$. Then $m \le 8$ and $n \le 8$, so that $mn \le 64$, as required.
+Portanto, suponha que nem $m>8$ nem $n>8$. Então $m \le 8$ e $n \le 8$, de modo que $mn \le 64$, conforme necessário.
 \end{example}
 
 \begin{exercise}
-Use the law of contraposition to prove that $p \Leftrightarrow q \equiv (p \Rightarrow q) \wedge ((\neg p) \Rightarrow (\neg q))$, and use the proof technique that this equivalence suggests to prove that an integer is even if and only if its square is even.
+Use a lei da contraposição para provar que $p \Leftrightarrow q \equiv (p \Rightarrow q) \wedge ((\neg p) \Rightarrow (\neg q))$, e use a técnica de prova que esta equivalência sugere para provar que um número inteiro é par se e somente se seu quadrado for par.
 \hintlabel{exIntegerEvenIffSquareEven}{%
-Express this statement as $\forall n \in \mathbb{Z},\, (n \text{ is even}) \Leftrightarrow (n^2 \text{ is even})$, and note that the negation of `$x$ is even' is `$x$ is odd'.
+Expresse esta afirmação como $\forall n \in \mathbb{Z},\, (n \text{ is even}) \Leftrightarrow (n^2 \text{ is even})$, e observe que a negação de `$x$ é par' é `$x$ é ímpar'.
+
 }
 \end{exercise}
 
-It feels good to invoke impressive-sounding results like \textit{proof by contraposition}, but in practice, the logical equivalence between \textit{any} two different propositional formulae suggests a new proof technique, and not all of these techniques have names. And indeed, the proof strategy in the following exercise, while useful, has no slick-sounding name---at least, not one that would be widely understood.
+É bom invocar resultados que parecem impressionantes como \textit{prova por contraposição}, mas na prática, a equivalência lógica entre \textit{quaisquer} duas fórmulas proposicionais diferentes sugere uma nova técnica de prova, e nem todas estas técnicas têm nomes. E, de facto, a estratégia de prova no exercício seguinte, embora útil, não tem um nome que soe engenhoso – pelo menos, não um que possa ser amplamente compreendido.
 
 \begin{exercise}
-Prove that $p \vee q \equiv (\neg p) \Rightarrow q$. Use this logical equivalence to suggest a new strategy for proving propositions of the form $p \vee q$, and use this strategy to prove that if two integers sum to an even number, then either both integers are even or both are odd.
+Prove que p∨q≡(¬p)⇒qp \vee q \equiv (\neg p) \Rightarrow q. Use esta equivalência lógica para sugerir uma nova estratégia para provar proposições da forma p∨qp \vee q, e use esta estratégia para provar que se dois inteiros somam um número par, então ambos os inteiros são pares ou ambos são ímpares.
 \end{exercise}
 
 \subsection*{Negation}
 
-In pure mathematics it is common to ask whether or not a certain property holds of a mathematical object. For example, in \Cref{secCompletenessConvergence}, we will look at convergence of sequences of real numbers: to say that a sequence $x_0,x_1,x_2,\dots$ of real numbers \textit{converges}\label{pConvergencePreliminary} (\Cref{defConvergenceOfSequence}) is to say
+Na matemática pura é comum perguntar se uma determinada propriedade é válida ou não para um objeto matemático. Por exemplo, em \Cref{secCompletenessConvergence}, veremos a convergência de sequências de números reais: para dizer que uma sequência $x_0,x_1,x_2,\dots$ de números reais \textit{converge}\label{pConvergencePreliminary} ( \Cref{defConvergenceOfSequence}) quer dizer
 \[ \exists a \in \mathbb{R},\, \forall \varepsilon \in \mathbb{R},\, (\varepsilon > 0 \Rightarrow \exists N \in \mathbb{N},\, \forall n \in \mathbb{N},\, [n \ge N \Rightarrow |x_n-a| < \varepsilon])\]
-This is already a relatively complicated logical formula. But what if we wanted to prove that a sequence \textit{does not} converge? Simply assuming the logical formula above and deriving a contradiction might work sometimes, but it is not particularly enlightening.
+Esta já é uma fórmula lógica relativamente complicada. Mas e se quiséssemos provar que uma sequência \textit{não} converge? Simplesmente assumir a fórmula lógica acima e derivar uma contradição pode funcionar às vezes, mas não é particularmente esclarecedor.
 
-Our next goal is to develop a systematic method for negating complicated logical formulae. With this done, we will be able to negate the logical formula expressing `the sequence $x_0, x_1, x_2, \dots$ converges' as follows
+Nosso próximo objetivo é desenvolver um método sistemático para negar fórmulas lógicas complicadas. Feito isso, seremos capazes de negar a fórmula lógica que expressa “a sequência $x_0, x_1, x_2, \dots$ converges' do seguinte modo
 \[ \forall a \in \mathbb{R},\, \exists \varepsilon \in \mathbb{R},\, (\varepsilon > 0 \wedge \forall N \in \mathbb{N},\, \exists n \in \mathbb{N},\, [n \ge N \wedge |x_n-a| \ge \varepsilon])\]
 
-Granted, this is still a complicated expression, but when broken down element by element, it provides useful information about how it may be proved.
+É verdade que esta ainda é uma expressão complicada, mas quando decomposta elemento por elemento, fornece informações úteis sobre como pode ser provada.
 
-The rules for negating conjunctions and disjunctions are instances of \textit{de Morgan's laws}, which exhibit a kind of duality between $\wedge$ and $\vee$.
+As regras para negar conjunções e disjunções são exemplos de \textit{Leis de Morgan}, que apresentam uma espécie de dualidade entre $\wedge$ and $\vee$.
 
 \begin{theorem}[de Morgan's laws for logical operators]
 \label{thmDeMorganLogicalOperators}
@@ -382,7 +386,7 @@ \subsection*{Negation}
 \end{theorem}
 
 \begin{cproof}[of (a)]
-Consider the following truth table.
+Considere a seguinte tabela verdade.
 \begin{center}
 \begin{tabular}{cc||c|c||cc|c}
 $p$ & $q$ & $p \wedge q$ & $\neg (p \wedge q)$ & $\neg p$ & $\neg q$ & $(\neg p) \vee (\neg q)$ \\ \hline
@@ -392,26 +396,27 @@ \subsection*{Negation}
 \FF & \FF & \FF & \TT & \TT & \TT & \TT \\
 \end{tabular}
 \end{center}
-The columns for $\neg (p \wedge q)$ and $(\neg p) \vee (\neg q)$ are identical, so they are logically equivalent.
+As colunas para $\neg (p \wedge q)$ and $(\neg p) \vee (\neg q)$ are identical, so they are logically equivalent.
 \end{cproof}
 
 \begin{exercise}
-Prove \Cref{thmDeMorganLogicalOperators}(b) thrice: once using the definition of logical equivalence directly (like we did in \Cref{exConjunctionDistributesOverDisjunction,exImplicationInTermsOfDisjunction} and \Cref{exPAndQImpliesRIffPImpliesRAndQImpliesR}), once using a truth table, and once using part (a) together with the law of double negation.
+Prove \Cref{thmDeMorganLogicalOperators}(b) três vezes: uma vez usando a definição de equivalência lógica diretamente (como fizemos em \Cref{exConjunctionDistributesOverDisjunction,exImplicationInTermsOfDisjunction} e \Cref{exPAndQImpliesRIffPImpliesRAndQImpliesR}), uma vez usando uma tabela verdade e uma vez usando a parte (a) junto com a lei da dupla negação.
 \end{exercise}
 
 \begin{example}
-We often use de Morgan's laws for logical operators without thinking about it. For example to say that `neither $3$ nor $7$ is even' is equivalent to saying `$3$ is odd and $7$ is odd'. The former statement translates to
+
+Frequentemente usamos as leis de Morgan para operadores lógicos sem pensar nisso. Por exemplo, dizer que “nem $3$ nem $7$ são pares” é equivalente a dizer “$3$ é ímpar e $7$ é ímpar”. A afirmação anterior se traduz em
 \[ \neg [(3 \text{ is even}) \vee (7 \text{ is even})]\]
-while the second statement translates to
+enquanto a segunda afirmação se traduz em
 \[ [\neg (3 \text{ is even})] \wedge [\neg (7 \text{ is even})]\]
 \end{example}
 
 \begin{exercise}
 \label{exNegationOfImplication}
-Prove that $\neg (p \Rightarrow q) \equiv p \wedge (\neg q)$ twice, once using a truth table, and once using \Cref{exImplicationInTermsOfDisjunctionWithTruthTables} together with de Morgan's laws and the law of double negation.
+Prove que $\neg (p \Rightarrow q) \equiv p \wedge (\neg q)$ duas vezes, uma vez usando uma tabela verdade, e uma vez usando \Cref{exImplicationInTermsOfDisjunctionWithTruthTables} juntamente com as leis de de Morgan e a lei da dupla negação.
 \end{exercise}
 
-De Morgan's laws for logical operators generalise to statements about quantifiers, expressing a similar duality between $\forall$ and $\exists$ as we have between $\wedge$ and $\vee$.
+As leis de De Morgan para operadores lógicos generalizam-se para afirmações sobre quantificadores, expressando uma dualidade semelhante entre $\forall$ e $\exists$ como temos entre $\wedge$ e $\vee$.
 
 \begin{theorem}[de Morgan's laws for quantifiers]
 \label{thmDeMorganQuantifiers}
@@ -424,64 +429,64 @@ \subsection*{Negation}
 \end{theorem}
 
 \begin{cproof}
-Unfortunately, since these logical formulae involve quantifiers, we do not have truth tables at our disposal, so we must assume each formula and derive the other.
+Infelizmente, como essas fórmulas lógicas envolvem quantificadores, não temos tabelas verdade à nossa disposição, portanto devemos assumir cada fórmula e derivar a outra.
 
-We start by proving the equivalence in part (b), and then we derive (a) as a consequence.
+Começamos provando a equivalência na parte (b) e então derivamos (a) como consequência.
 
 \begin{itemize}
-\item Assume $\neg \exists x \in X,\, p(x)$. To prove $\forall x \in X,\, \neg p(x)$, fix some $x \in X$. If $p(x)$ were true, then we'd have $\exists x \in X,\, p(x)$, which contradicts our main assumption; so we have $\neg p(x)$. But then $\forall x \in X,\, \neg p(x)$ is true.
+\item Assuma $\neg \exists x \in X,\, p(x)$. Para provar $\forall x \in X,\, \neg p(x)$, fixe um $x \in X$. If $p(x)$ fossem verdadeiras, então teríamos $\exists x \in X,\, p(x)$, o que contradiz nossa suposição principal; então temos $\neg p(x)$. Mas então $\forall x \in X,\, \neg p(x)$ é verdadeiro.
 
-\item Assume $\forall x \in X,\, \neg p(x)$. For the sake of contradiction, assume $\exists x \in X,\, p(x)$ were true. Then we obtain some $a \in X$ for which $p(a)$ is true. But $\neg p(a)$ is true by the assumption that $\forall x \in X,\, \neg p(a)$, so we obtain a contradiction. Hence $\neg \exists x \in X,\, p(x)$ is true.
+\item Assuma $\forall x \in X,\, \neg p(x)$. Por uma questão de contradição, suponha $\exists x \in X,\, p(x)$ eram verdade. Então obtemos alguns $a \in X$ para qual $p(a)$ é verdade. Mas $\neg p(a)$ é verdade pela suposição de que $\forall x \in X,\, \neg p(a)$, então obtemos uma contradição. Por isso $\neg \exists x \in X,\, p(x)$ é verdade.
 \end{itemize}
 
-This proves that $\neg \exists x \in X,\, p(x) \equiv \forall x \in X,\, \neg p(x)$.
+Isto prova que $\neg \exists x \in X,\, p(x) \equiv \forall x \in X,\, \neg p(x)$.
 
 Now (a) follows from (b) using the law of double negation (\Cref{thmDoubleNegation}):
 \[ \exists x \in X,\, \neg p(x) \equiv \neg\neg \exists x \in X,\, \neg p(x) \overset{(b)}{\equiv} \neg \forall x \in X,\, \neg \neg p(x) \equiv \neg \forall x \in X,\, p(x)\]
 as required.
 \end{cproof}
 
-The proof strategy suggested by the logical equivalence in \Cref{thmDeMorganQuantifiers}(b) is so important that it has its own name.
+A estratégia de prova sugerida pela equivalência lógica em \Cref{thmDeMorganQuantifiers}(b) é tão importante que tem nome próprio.
 
 \begin{strategy}[Proof by counterexample]
 \label{strCounterexample}
 \index{counterexample}
 \index{proof!by counterexample}
-To prove that a proposition of the form $\forall x \in X,\, p(x)$ is false, it suffices to find a single element $a \in X$ such that $p(a)$ is false. The element $a$ is called a \textbf{counterexample} to the proposition $\forall x \in X,\, p(x)$.
+Para provar que uma proposição da forma $\forall x \in X,\, p(x)$ é falsa, basta encontrar um único elemento $a \in X$ de tal modo que $p(a)$ é falso. O elemento $a$ é chamado de \textbf{counterexample} para a proposta $\forall x \in X,\, p(x)$.
 \end{strategy}
 
 \begin{example}
-We prove by counterexample that not every integer is divisible by a prime number. Indeed, let $x = 1$. The only integral factors of $1$ are $1$ and $-1$, neither of which are prime, so that $1$ is not divisible by any primes.
+Provamos por contra-exemplo que nem todo número inteiro é divisível por um número primo. Na verdade, seja $x = 1$. Os únicos fatores integrais de $1$ são $1$ e $-1$, nenhum dos quais é primo, de modo que $1$ não é divisível por nenhum número primo.
 \end{example}
 
 \begin{exercise}
-Prove by counterexample that not every rational number can be expressed as $\dfrac{a}{b}$ where $a \in \mathbb{Z}$ is even and $b \in \mathbb{Z}$ is odd.
+Prove por contra-exemplo que nem todo número racional pode ser expresso como $\dfrac{a}{b}$ where $a \in \mathbb{Z}$ is even and $b \in \mathbb{Z}$ é ímpar.
 \hintlabel{exNotEveryRationalIsEvenDividedByOdd}{%
-Find a rational number all of whose representations as a ratio of two integers have an even denominator.
+Encontre um número racional cujas representações como razão de dois inteiros tenham um denominador par.
 }
 \end{exercise}
 
-We have now seen how to negate the logical operators $\neg$, $\wedge$, $\vee$ and $\Rightarrow$, as well as the quantifiers $\forall$ and $\exists$. 
+Vimos agora como negar os operadores lógicos $\neg$, $\wedge$, $\vee$ and $\Rightarrow$, bem como os quantificadores $\forall$ and $\exists$. 
 
 \begin{definition}
 \label{defMaximallyNegatedLogicalFormula}
 \index{negation!maximal}
 \index{logical formula!maximally negated}
-A logical formula is \textbf{maximally negated} if the only instances of the negation operator $\neg$ appear immediately before a predicate (or other proposition not involving logical operators or quantifiers).
+Uma fórmula lógica é \textbf{maximally negated} se as únicas instâncias do operador de negação $\neg$ aparecem imediatamente antes de um predicado (ou outra proposição que não envolva operadores lógicos ou quantificadores).
 \end{definition}
 
 \begin{example}
-The following propositional formula is maximally negated:
+A seguinte fórmula proposicional é negada ao máximo:
 \[ [p \wedge (q \Rightarrow (\neg r))] \Leftrightarrow (s \wedge (\neg t))\]
-Indeed, all instances of $\neg$ appear immediately before propositional variables.
+Na verdade, todas as instâncias de $\neg$ aparecem imediatamente antes das variáveis ​​proposicionais.
 
-However the following propositional formula is \textit{not} maximally negated:
+No entanto, a seguinte fórmula proposicional \textit{não} é negada ao máximo:
 \[ (\neg \neg q) \Rightarrow q\]
-Here the subformula $\neg \neg q$ contains a negation operator immediately before another negation operator ($\neg \neg q$). However by the law of double negation, this is equivalent to $q \Rightarrow q$, which is maximally negated trivially since there are no negation operators to speak of.
+Aqui a subfórmula $\neg \neg q$ contém um operador de negação imediatamente antes de outro operador de negação ($\neg \neg q$). No entanto, pela lei da dupla negação, isso é equivalente a $q \Rightarrow q$, que é negado ao máximo trivialmente, uma vez que não há operadores de negação dignos de menção.
 \end{example}
 
 \begin{exercise}
-Determine which of the following logical formulae are maximally negated.
+Determine quais das seguintes fórmulas lógicas são negadas ao máximo.
 \begin{enumerate}[(a)]
 \item $\forall x \in X,\, (\neg p(x)) \Rightarrow \forall y \in X, \neg (r(x,y) \wedge s(x,y))$;
 \item $\forall x \in X,\, (\neg p(x)) \Rightarrow \forall y \in X, (\neg r(x,y)) \vee (\neg s(x,y))$;
@@ -490,22 +495,22 @@ \subsection*{Negation}
 \end{enumerate}
 \end{exercise}
 
-The following theorem allows us to replace logical formulae by maximally negated ones, which in turn suggests proof strategies that we can use for proving that complicated-looking propositions are \textit{false}.
+O seguinte teorema permite-nos substituir fórmulas lógicas por fórmulas maximamente negadas, o que por sua vez sugere estratégias de prova que podemos usar para provar que proposições aparentemente complicadas são \textit{falsas}.
 
 \begin{theorem}
 \label{thmLogicalFormulaEquivalentToMaximallyNegated}
-Every logical formula (built using only the logical operators and quantifiers we have seen so far) is logically equivalent to a maximally negated logical formula.
+Cada fórmula lógica (construída usando apenas os operadores lógicos e quantificadores que vimos até agora) é logicamente equivalente a uma fórmula lógica negada ao máximo.
 \end{theorem}
 
 \begin{cidea}
-Much like \Cref{thmLogicalEquivalentIffSameTruthValues}, a precise proof of \Cref{thmLogicalFormulaEquivalentToMaximallyNegated} requires some form of induction argument, so instead we will give an idea of the proof.
+Muito parecido \Cref{thmLogicalEquivalentIffSameTruthValues}, uma prova precisa de \Cref{thmLogicalFormulaEquivalentToMaximallyNegated} requer alguma forma de argumento de indução, então em vez disso daremos uma ideia da prova.
 
-Every logical formula we have seen so far is built from predicates using the logical operators ${\wedge}, {\vee}, {\Rightarrow}$ and $\neg$ and the quantifiers $\forall$ and $\exists$---indeed, the logical operator $\Leftrightarrow$ was defined in terms of $\wedge$ and $\Rightarrow$, and the quantifier $\exists$ was defined in terms of the quantifiers $\forall$ and $\exists$ and the logical operators $\wedge$ and $\Rightarrow$.
+Cada fórmula lógica que vimos até agora é construída a partir de predicados usando os operadores lógicos ${\wedge}, {\vee}, {\Rightarrow}$ e $\neg$ e os quantificadores $\forall$ e $\exists$- --de fato, o operador lógico $\Leftrightarrow$ foi definido em termos de $\wedge$ e $\Rightarrow$, e o quantificador $\exists$ foi definido em termos dos quantificadores $\forall$ e $\exists$ e os operadores lógicos $\wedge$ e $\Rightarrow$.
 
-But the results in this section allow us to push negations `inside' each of these logical operators and quantifiers, as summarised in the following table.
+Mas os resultados desta seção nos permitem colocar negações “dentro” de cada um desses operadores lógicos e quantificadores, conforme resumido na tabela a seguir.
 \begin{center}
 \begin{tabular}{rcll}
-Negation outside & & Negation inside & Proof \\ \hline
+Negação fora & & Negação dentro & Prova \\ \hline
 $\neg (p \wedge q)$ &$\equiv$& $(\neg p) \vee (\neg q)$ & \Cref{thmDeMorganLogicalOperators}(a) \\
 $\neg (p \vee q)$ &$\equiv$& $(\neg p) \wedge (\neg q)$ &  \Cref{thmDeMorganLogicalOperators}(b) \\
 $\neg (p \Rightarrow q)$ &$\equiv$& $p \wedge (\neg q)$ & \Cref{exNegationOfImplication} \\
@@ -515,79 +520,79 @@ \subsection*{Negation}
 \end{tabular}
 \end{center}
 
-Repeatedly applying these rules to a logical formula eventually yields a logically equivalent, maximally negated logical formula.
+A aplicação repetida dessas regras a uma fórmula lógica eventualmente produz uma fórmula lógica logicamente equivalente e maximamente negada.
 \end{cidea}
 
 \begin{example}
-Recall the logical formula from page \pageref{pConvergencePreliminary} expressing the assertion that a sequence $x_0, x_1, x_2, \dots$ of real numbers converges:
+Lembre-se da fórmula lógica da página \pageref{pConvergencePreliminary} expressando a afirmação de que uma sequência $x_0, x_1, x_2, \dots$  \pageref{pConvergencePreliminary} dos números reais converge:
 \[ \exists a \in \mathbb{R},\, \forall \varepsilon \in \mathbb{R},\, (\varepsilon > 0 \Rightarrow \exists N \in \mathbb{N},\, \forall n \in \mathbb{N},\, [n \ge N \Rightarrow |x_n-a| < \varepsilon])\]
-We will maximally negate this to obtain a logical formula expressing the assertion that the sequence does not converge.
+Negaremos isso ao máximo para obter uma fórmula lógica que expresse a afirmação de que a sequência não converge.
 
-Let's start at the beginning. The negation of the formula we started with is:
+Vamos começar no início. A negação da fórmula com a qual começamos é:
 \[ \neg \exists a \in \mathbb{R},\, \forall \varepsilon \in \mathbb{R},\, (\varepsilon > 0 \Rightarrow \exists N \in \mathbb{N},\, \forall n \in \mathbb{N},\, [n \ge N \Rightarrow |x_n-a| < \varepsilon])\]
 %
-The key to maximally negating a logical formula is to ignore information that is not immediately relevant. Here, the expression that we are negating takes the form $\neg \exists a \in \mathbb{R},\, (\text{stuff})$. It doesn't matter what the `stuff' is just yet; all that matters is that we are negating an existentially quantified statement, and so de Morgan's laws for quantifiers tells us that this is logically equivalent to $\forall a \in \mathbb{R},\, \neg (\text{stuff})$. We apply this rule and just re-write the `stuff', to obtain:
+A chave para negar ao máximo uma fórmula lógica é ignorar informações que não são imediatamente relevantes. Aqui, a expressão que estamos negando assume a forma $\neg \exists a \in \mathbb{R},\, (\text{stuff})$. Não importa qual seja a “coisa” ainda; tudo o que importa é que estamos negando uma afirmação existencialmente quantificada e, portanto, as leis de Morgan para quantificadores nos dizem que isso é logicamente equivalente a $\forall a \in \mathbb{R},\, \neg (\text{stuff} )$. Aplicamos esta regra e apenas reescrevemos as `coisas', para obter:
 \[ \forall a \in \mathbb{R},\, \neg \forall \varepsilon \in \mathbb{R},\, (\varepsilon > 0 \Rightarrow \exists N \in \mathbb{N},\, \forall n \in \mathbb{N},\, [n \ge N \Rightarrow |x_n-a| < \varepsilon])\]
 %
-Now we are negating a universally quantified statement, $\neg \forall \varepsilon \in \mathbb{R},\, (\text{stuff})$ which, by de Morgan's laws for quantifiers, is equivalent to $\exists \varepsilon \in \mathbb{R},\, \neg (\text{stuff})$:
+Agora estamos negando uma afirmação universalmente quantificada, $\neg \forall \varepsilon \in \mathbb{R},\, (\text{stuff})$ que, pelas leis de Morgan para quantificadores, é equivalente a $\exists \varepsilon \in \mathbb{R},\, \neg (\text{stuff})$:
 \[ \forall a \in \mathbb{R},\, \exists \varepsilon \in \mathbb{R},\, \neg (\varepsilon > 0 \Rightarrow \exists N \in \mathbb{N},\, \forall n \in \mathbb{N},\, [n \ge N \Rightarrow |x_n-a| < \varepsilon])\]
 %
-At this point, the statement being negated is of the form $(\text{stuff}) \Rightarrow (\text{junk})$, which by \Cref{exNegationOfImplication} negates to $(\text{stuff}) \wedge \neg (\text{junk})$. Here, `stuff' is $\varepsilon > 0$ and `junk' is $\exists N \in \mathbb{N}, \forall n \in \mathbb{N},\, [n \ge N \Rightarrow |x_n - a| < \varepsilon]$. So performing this negation yields:
+Neste ponto, a afirmação que está sendo negada tem a forma $(\text{stuff}) \Rightarrow (\text{junk})$, which by \Cref{exNegationOfImplication} negates to $(\text{stuff}) \wedge \neg (\text{junk})$. Aqui, `coisas' são $\varepsilon > 0$ e `porcarias' são $\exists N \in \mathbb{N}, \forall n \in \mathbb{N},\, [n \ge N \Rightarrow |x_n - a| < \varepsilon]$. So performing this negation yields:
 \[ \forall a \in \mathbb{R},\, \exists \varepsilon \in \mathbb{R},\, (\varepsilon > 0 \wedge \neg \exists N \in \mathbb{N},\, \forall n \in \mathbb{N},\, [n \ge N \Rightarrow |x_n-a| < \varepsilon])\]
 %
-Now we are negating an existentially quantified formula again, so using de Morgan's laws for quantifiers gives:
+Agora estamos negando novamente uma fórmula existencialmente quantificada, então usar as leis de Morgan para quantificadores dá:
 \[ \forall a \in \mathbb{R},\, \exists \varepsilon \in \mathbb{R},\, (\varepsilon > 0 \wedge \forall N \in \mathbb{N},\, \neg \forall n \in \mathbb{N},\, [n \ge N \Rightarrow |x_n-a| < \varepsilon])\]
 %
-The formula being negated here is univerally quantified, so using de Morgan's laws for quantifiers \textit{again} gives:
+A fórmula que está sendo negada aqui é quantificada universalmente, então usar as leis de Morgan para quantificadores \textit{novamente} dá:
 \[ \forall a \in \mathbb{R},\, \exists \varepsilon \in \mathbb{R},\, (\varepsilon > 0 \wedge \forall N \in \mathbb{N},\, \exists n \in \mathbb{N},\, \neg [n \ge N \Rightarrow |x_n-a| < \varepsilon])\]
 %
-We're almost there! The statement being negated here is an implication, so applying the rule $\neg (p \Rightarrow q) \equiv p \wedge (\neg q)$ again yields:
+Estamos quase lá! A afirmação negada aqui é uma implicação, portanto, aplicando a regra $\neg (p \Rightarrow q) \equiv p \wedge (\neg q)$ again yields:
 \[ \forall a \in \mathbb{R},\, \exists \varepsilon \in \mathbb{R},\, (\varepsilon > 0 \wedge \forall N \in \mathbb{N},\, \exists n \in \mathbb{N},\, [n \ge N \wedge \neg (|x_n - a| < \varepsilon)])\]
 %
-At this point, strictly speaking, the formula is maximally negated, since the statement being negated does not involve any other logical operators or quantifiers. However, since $\neg (|x_n-a| < \varepsilon)$ is equivalent to $|x_n - a| \ge \varepsilon$, we can go one step further to obtain:
+Neste ponto, a rigor, a fórmula é negada ao máximo, uma vez que a afirmação que está sendo negada não envolve quaisquer outros operadores lógicos ou quantificadores. No entanto,desde que $\neg (|x_n-a| < \varepsilon)$ é equivalente a $|x_n - a| \ge \varepsilon$, podemos dar um passo adiante para obter:
 \[ \forall a \in \mathbb{R},\, \exists \varepsilon \in \mathbb{R},\, (\varepsilon > 0 \wedge \forall N \in \mathbb{N},\, \exists n \in \mathbb{N},\, [n \ge N \wedge |x_n - a| \ge \varepsilon])\]
 %
-This is as negated as we could ever dream of, and so we stop here.
+Isto é tão negado quanto poderíamos sonhar, e por isso paramos por aqui.
 \end{example}
 
 \begin{exercise}
-Find a maximally negated propositional formula that is logically equivalent to $\neg (p \Leftrightarrow q)$.
+Encontre uma fórmula proposicional maximamente negada que seja logicamente equivalente a $\neg (p \Leftrightarrow q)$.
 \hintlabel{exMaximallyNegateBiconditional}{%
-Start by expressing $\Leftrightarrow$ in terms of $\Rightarrow$ and $\wedge$, as in \Cref{defBiconditional}.
+Comece expressando $\Leftrightarrow$ in terms of $\Rightarrow$ and $\wedge$, as in \Cref{defBiconditional}.
 }
 \end{exercise}
 
 \begin{exercise}
-Maximally negate the following logical formula, then prove that it is true or prove that it is false.
+Negue ao máximo a seguinte fórmula lógica e, em seguida, prove que é verdadeira ou prove que é falsa.
 \[ \exists x \in \mathbb{R},\, [x > 1 \wedge (\forall y \in \mathbb{R},\, [x < y \Rightarrow x^2 \le y])]\]
 \end{exercise}
 
 \subsection*{Tautologies}
 
-The final concept that we introduce in this chapter is that of a \textit{tautology}, which can be thought of as the opposite of a contradiction. The word `tautology' has other implications when used colloquially, but in the context of symbolic logic it has a precise definition.
+O conceito final que introduzimos neste capítulo é o de uma \textit{tautologia}, que pode ser pensada como o oposto de uma contradição. A palavra “tautologia” tem outras implicações quando usada coloquialmente, mas no contexto da lógica simbólica tem uma definição precisa.
 
 \begin{definition}
 \label{defTautology}
 \index{tautology}
-A \textbf{tautology} is a proposition or logical formula that is true, no matter how truth values are assigned to its component propositional variables and predicates.
+Uma \textbf{tautologia} é uma proposição ou fórmula lógica que é verdadeira, não importa como os valores de verdade são atribuídos às suas variáveis ​​​​proposicionais e predicados componentes.
 \end{definition}
 
-The reason we are interested in tautologies is that tautologies can be used as assumptions at any point in a proof, for any reason.
+A razão pela qual estamos interessados ​​em tautologias é que as tautologias podem ser usadas como suposições em qualquer ponto de uma prova, por qualquer motivo.
 
 \begin{strategy}[Assuming tautologies]
-Let $p$ be a proposition. Any tautology may be assumed in any proof of $p$.
+Seja $p$ uma proposição. Qualquer tautologia pode ser assumida em qualquer prova de $p$.
 \end{strategy}
 
 \begin{example}
-The law of excluded middle (\Cref{axLEM}) says precisely that $p \vee (\neg p)$ is a tautology. This means that when proving any result, we may split into cases based on whether a proposition is true or false, just as we did in \Cref{propIfProductEvenThenSomeFactorEven}.
+A lei do terceiro excluído (\Cref{axLEM}) diz precisamente que $p \vee (\neg p)$ é uma tautologia. Isto significa que, ao provar qualquer resultado, podemos dividir em casos com base no facto de uma proposição ser verdadeira ou falsa, tal como fizemos em \Cref{propIfProductEvenThenSomeFactorEven}.
 \end{example}
 
 \begin{example}
-The formula $p \Rightarrow (q \Rightarrow p)$ is a tautology.
+S fórmula $p \Rightarrow (q \Rightarrow p)$ is a tautology.
 
-A direct proof of this fact is as follows. In order to prove $p \Rightarrow (q \Rightarrow p)$ is true, it suffices to assume $p$ and derive $q \Rightarrow p$. So assume $p$. Now in order to prove $q \Rightarrow p$, it suffices to assume $q$ and derive $p$. So assume $q$. But we're already assuming that $p$ is true! So $q \Rightarrow p$ is true, and hence $p \Rightarrow (q \Rightarrow p)$ is true.
+Uma prova direta deste fato é a seguinte. Para provar que $p \Rightarrow (q \Rightarrow p)$ é verdadeiro, basta assumir $p$ e derivar $q \Rightarrow p$. Então assuma $p$. Agora, para provar $q \Rightarrow p$, basta assumir $q$ e derivar $p$. Então assuma $q$. Mas já estamos assumindo que $p$ é verdade! Portanto, $q \Rightarrow p$ é verdadeiro e, portanto, $p \Rightarrow (q \Rightarrow p)$ é verdadeiro.
 
-A proof using truth tables is as follows:
+Uma prova usar tabelas verdade é o seguinte:
 \begin{center}
 \begin{tabular}{cc|c|c}
 $p$ & $q$ & $q \Rightarrow p$ & $p \Rightarrow (q \Rightarrow p)$ \\ \hline
@@ -597,12 +602,12 @@ \subsection*{Tautologies}
 \FF & \FF & \TT & \TT
 \end{tabular}
 \end{center}
-We see that $p \Rightarrow (q \Rightarrow p)$ is true regardless of the truth values of $p$ and $q$.
+Nós vemos que $p \Rightarrow (q \Rightarrow p)$ is true regardless of the truth values of $p$ and $q$.
 \end{example}
 
 \begin{exercise}
 \label{exTautologies}
-Prove that each of the following is a tautology:
+Prove que cada uma das afirmações a seguir é uma tautologia:
 \begin{enumerate}[(a)]
 \item $[(p \Rightarrow q) \wedge (q \Rightarrow r)] \Rightarrow (p \Rightarrow r)$;
 \item $[p \Rightarrow (q \Rightarrow r)] \Rightarrow [(p \Rightarrow q) \Rightarrow (p \Rightarrow r)]$;
@@ -610,77 +615,77 @@ \subsection*{Tautologies}
 \item $[\neg (p \wedge q)] \Leftrightarrow [(\neg p) \vee (\neg q)]$;
 \item $(\neg \forall x \in X,\, p(x)) \Leftrightarrow (\exists x \in X,\, \neg p(x))$.
 \end{enumerate}
-For each, try to interpret what it means, and how it might be useful in a proof.
+Para cada um, tente interpretar o que significa e como pode ser útil em uma prova.
 \end{exercise}
 
-You may have noticed parallels between de Morgan's laws for logical operators and quantifiers, and parts (d) and (e) of \Cref{exTautologies}, respectively. They almost seem to say the same thing, except that in \Cref{exTautologies} we used `$\Leftrightarrow$' and in \Cref{thmDeMorganLogicalOperators,thmDeMorganQuantifiers} we used `$\equiv$'. There is an important difference, though: if $p$ and $q$ are logical formulae, then $p \Rightarrow q$ is itself a logical formula, which we may study as a mathematical object in its own right. However, $p \equiv q$ is not a logical formula: it is an assertion \textit{about} logical formulae, namely that the logical formulae $p$ and $q$ are equivalent.
+Você deve ter notado paralelos entre as leis de Morgan para operadores lógicos e quantificadores e as partes (d) e (e) de \Cref{exTautologias}, respectivamente. Eles quase parecem dizer a mesma coisa, exceto que em \Cref{exTautologies} usamos `$\Leftrightarrow$' e em \Cref{thmDeMorganLogicalOperators,thmDeMorganQuantifiers} usamos `$\equiv$'. Porém, há uma diferença importante: se $p$ e $q$ são fórmulas lógicas, então $p \Rightarrow q$ é em si uma fórmula lógica, que podemos estudar como um objeto matemático por si só. No entanto, $p \equiv q$ não é uma fórmula lógica: é uma afirmação \textit{sobre} fórmulas lógicas, nomeadamente que as fórmulas lógicas $p$ e $q$ são equivalentes.
 
-There is, nonetheless, a close relationship between $\Leftrightarrow$ and $\equiv$---this relationship is summarised in the following theorem.
+Existe, no entanto, uma estreita relação entre $\Leftrightarrow$ and $\equiv$---esta relação é resumida no seguinte teorema.
 
 \begin{theorem}
 \label{thmTautologyAndDerivation}
-Let $p$ and $q$ be logical formulae.
+Seja $p$ e $q$ fórmulas lógicas.
 \begin{enumerate}[(a)]
-\item $q$ can be derived from $p$ if and only if $p \Rightarrow q$ is a tautology;
-\item $p \equiv q$ if and only if $p \Leftrightarrow q$ is a tautology.
+\item $q$ pode ser derivado de $p$ se e somente se $p \Rightarrow q$ is a tautology;
+\item $p \equiv q$ se e somente se $p \Leftrightarrow q$ for uma tautologia.
 \end{enumerate}
 \end{theorem}
 
 \begin{cproof}
-For (a), note that a derivation of $q$ from $p$ is sufficient to establish the truth of $p \Rightarrow q$ by the introduction rule for implication \introrule{\Rightarrow}, and so if $q$ can be derived from $p$, then $p \Rightarrow q$ is a tautology. Conversely, if $p \Rightarrow q$ is a tautology, then $q$ can be derived from $p$ using the elimination rule for implication \elimrule{\Rightarrow} together with the (tautological) assumption that $p \Rightarrow q$ is true.
+Para (a), observe que uma derivação de $q$ de $p$ é suficiente para estabelecer a verdade de $p \Rightarrow q$ pela regra de introdução para implicação \introrule{\Rightarrow}, e então se $q$ puder ser derivado de $p$, então $p \Rightarrow q$ é uma tautologia. Por outro lado, se $p \Rightarrow q$ é uma tautologia, então $q$ pode ser derivado de $p$ usando a regra de eliminação para implicação \elimrule{\Rightarrow} junto com a suposição (tautológica) de que $p \Rightarrow q$ é verdade.
 
-Now (b) follows from (a), since logical equivalence is defined in terms of derivation in each direction, and $\Leftrightarrow$ is simply the conjunction of two implications.
+Agora (b) segue de (a), uma vez que a equivalência lógica é definida em termos de derivação em cada direção, e $\Leftrightarrow$ é simplesmente a conjunção de duas implicações.
 \end{cproof}
 
-%\textit{Aaand breathe!} All this new notation can be overwhelming at first, but it will be worth it in the end. This chapter was all about teaching you a new language---new symbols, new terminology---because without it, our future pursuits will be impossible. If you're stuck now, then don't worry: you'll soon get the hang of it, especially when we start using this new language in context. You can, of course, refer back to the results in this chapter for reference at any point in the future.
+%\textit{Respire!} Toda essa nova notação pode ser cansativa no início, mas valerá a pena no final. Este capítulo foi sobre ensinar a você um novo idioma – novos símbolos, nova terminologia – porque sem ele, nossas atividades futuras serão impossíveis. Se você estiver travado agora, não se preocupe: em breve você pegará o jeito, especialmente quando começarmos a usar essa nova linguagem no contexto. Você pode, é claro, consultar os resultados deste capítulo para referência em qualquer momento no futuro.
+
 
 \begin{tldr}{secLogicalEquivalence}
 \subsubsection*{Logical equivalence}
 
 \begin{tldrlist}
 \tldritem{defLogicalEquivalence}
-Two logical formulae are \textit{logically equivalent} (written $\equiv$) if each can be derived from the other.
+Duas fórmulas lógicas são \textit{logicamente equivalentes} (escritas $\equiv$) se cada uma puder ser derivada da outra.
 
 \tldritem{defTruthTable}
-The \textit{truth table} of a propositional formula is a tabulation of its truth values under all assignments of truth values to its constituent propositional variables. Two propositional formulae are logically equivalent if and only if they have identical columns in a truth table.
+A \textit{tabela verdade} de uma fórmula proposicional é uma tabulação de seus valores verdade sob todas as atribuições de valores verdade às suas variáveis ​​proposicionais constituintes. Duas fórmulas proposicionais são logicamente equivalentes se e somente se tiverem colunas idênticas em uma tabela verdade.
 \end{tldrlist}
 
 \subsubsection*{Some specific logical equivalences}
 
 \begin{tldrlist}
 \tldritem{thmDoubleNegation}
-The double-negation of a proposition is equivalent to the original proposition. This gives rise to `indirect' proof by contradiction: in order to prove that a proposition $p$ is \textit{true}, assume $p$ is false and derive a contradiction.
+A dupla negação de uma proposição é equivalente à proposição original. Isto dá origem à prova `indireta' por contradição: para provar que uma proposição $p$ é \textit{verdadeira}, assuma que $p$ é falso e derive uma contradição.
 
 \tldritem{defContrapositive}
-The \textit{contrapositive} of an implication $p \Rightarrow q$ is the implication $(\neg q) \Rightarrow (\neg p)$. Every implication is equivalent to its contrapositive, so in order to prove $p \Rightarrow q$, it suffices to assume that $q$ is false, and derive that $p$ is false.
+A \textit{contrapositiva} de uma implicação $p \Rightarrow q$ é a implicação $(\neg q) \Rightarrow (\neg p)$. Toda implicação é equivalente à sua contrapositiva, portanto, para provar $p \Rightarrow q$, basta assumir que $q$ é falso e derivar que $p$ é falso.
 
 \tldritem{thmDeMorganLogicalOperators}
-De Morgan's laws for logical operators say that $\neg (p \wedge q) \equiv (\neg p) \vee (\neg q)$ and $\neg (p \vee q) \equiv (\neg p) \wedge (\neg q)$.
+As leis de De Morgan para operadores lógicos dizem que $\neg (p \wedge q) \equiv (\neg p) \vee (\neg q)$ and $\neg (p \vee q) \equiv (\neg p) \wedge (\neg q)$.
 
 \tldritem{exNegationOfImplication}
-The negation of $p \Rightarrow q$ is logically equivalent to $p \wedge (\neg q)$, so in order to prove that $p \Rightarrow q$ is \textit{false}, it suffices to prove that $p$ is true but $q$ is false.
+A negação de $p \Rightarrow q$ is logically equivalent to $p \wedge (\neg q)$, so in order to prove that $p \Rightarrow q$ is \textit{false}, basta provar que $p$ é verdadeiro, mas $q$ é falso.
 
 \tldritem{thmDeMorganQuantifiers}
-De Morgan's laws for quantifiers say that $\neg \forall x \in X,\, p(x) \equiv \exists x \in X,\, \neg p(x)$ and $\neg \exists x \in X,\, p(x) \equiv \forall x \in X,\, \neg p(x)$. The first of these suggests the strategy of \textit{proof by counterexample}.
+As leis de De Morgan para quantificadores dizem que $\neg \forall x \in X,\, p(x) \equiv \exists x \in X,\, \neg p(x)$ and $\neg \exists x \in X,\, p(x) \equiv \forall x \in X,\, \neg p(x)$. A primeira delas sugere a estratégia de \textit{proof by counterexample}.
 \end{tldrlist}
 
 \subsubsection*{Maximal negation}
 
 \begin{tldrlist}
 \tldritem{defMaximallyNegatedLogicalFormula}
-A logical formula is \textit{maximally negated} if it contains no negation operators (except, perhaps, immediately before a propositional variable or predicate).
+Uma fórmula lógica é \textit{maximamente negada} se não contém operadores de negação (exceto, talvez, imediatamente antes de uma variável ou predicado proposicional).
 
 \tldritem{thmLogicalFormulaEquivalentToMaximallyNegated}
-Every logical formula built using the logical operators and quantifiers in this section is logically equivalent to a maximally negated one.
+Cada fórmula lógica construída usando os operadores lógicos e quantificadores nesta seção é logicamente equivalente a uma fórmula maximamente negada.
 \end{tldrlist}
 
 \subsubsection*{Tautologies}
 
 \begin{tldrlist}
 \tldritem{defTautology}
-A \textit{tautology} is a logical formula that is true no matter what assignment of truth values is given to its constituent propositional variables or what values are substituted for its free variables. Tautologies can be invoked as assumptions at any point in a proof.
-
+Uma \textit{tautologia} é uma fórmula lógica que é verdadeira independentemente da atribuição de valores de verdade dada às suas variáveis ​​proposicionais constituintes ou de quais valores são substituídos por suas variáveis ​​livres. Tautologias podem ser invocadas como suposições em qualquer ponto de uma prova.
 \tldritem{thmTautologyAndDerivation}
-A proposition $p$ can be derived from a proposition $q$ if and only if $p \Rightarrow q$ is a tautology; and $p \equiv q$ if and only if $p \Leftrightarrow q$ is a tautology.
+Uma proposição pp pode ser derivada de uma proposição qq se e somente se p⇒qp \Rightarrow q for uma tautologia; e p≡qp \equiv q se e somente se p⇔qp \Leftrightarrow q for uma tautologia.
 \end{tldrlist}
-\end{tldr}
\ No newline at end of file
+\end{tldr}