lysa/ru/chapters/2/2-more-logic.ltx

\s{Совмещаем не, и и или}\label{2.2-more-logic}

В предыдущей секции мы поверхностно взглянули на операторы $\implies$,
$\impliedby$, $\iff$, $\land$, $\lor$, и $\lnot$.

Я собираюсь представить лишь 2 новых правила в этой секции. Вот они:

\begin{itemize}
\item $\lnot\parens{\lnot A} \iff A$
\item $\lnot\parens{A \land B} \iff \parens{\lnot A} \lor \parens{\lnot B}$

  Интуитивно вы можете думать об этих законах следующее: оба $A$ и $B$ должны
  быть правдой чтобы $A \land B$ было правдой. Так образом, если одно из них
  правдой не является, все выражение – ложь. Сказать, что ``все выражение – ложь''
  можно так: $\lnot\parens{A \land B}$. Сказать ``одно из них – ложь'' так:
  $\parens{\lnot A} \lor \parens{\lnot B}$.
\end{itemize}

Последнее правило:

\[\lnot\parens{A \lor B} \iff \parens{\lnot A} \land \parens{\lnot B} \semicolon
\forall A,B\]


\begin{proof}
  Его можно вывести из последнего закона. Пусть $C = \lnot A$, и $D = \lnot B$.
  \[
  \begin{array}{rcll}
    \lnot\parens{A \land  B}                              & \iff & \parens{\lnot A} \lor \parens{\lnot B}                              & \semicolon \forall C,D \\
    \lnot\parens{\parens{\lnot C} \land \parens{\lnot D}} & \iff & C \lor D                                                            & \semicolon \forall C,D \\
    C \lor D                                              & \iff & \lnot\parens{\parens{\lnot C} \land \parens{\lnot D}}               & \semicolon \forall C,D \\
    \lnot\parens{C \lor D}                                & \iff & \lnot\parens{\lnot\parens{\parens{\lnot C} \land \parens{\lnot D}}} & \semicolon \forall C,D \\
    \lnot\parens{C \lor D}                                & \iff & \parens{\lnot C} \land \parens{\lnot D}                             & \semicolon \forall C,D \\
  \end{array}
  \]
\end{proof}

Так и что это все за чертовщина? Ну, это ваш первый
So what the hell is all that? Well, this is your first taste of a
\xti{mathematical proof}. Basically, we start with a set of rules which we know
are true (the \xti{laws} or \xti{axioms}). We build them together to form
\xti{theorems}. That little white box at the bottom right is to say ``okay,
here's where I'm done proving stuff.''

I will also use the acronym Q.E.D., which is short for ``quod erat
demonstrandum'', which is fancy-talk for ``I'm done proving stuff''.

This really is your second taste of proofs, provided you did the exercises for
\cref{2.1-basic-logic}. You may have seen the terms ``proof'' and ``Q.E.D''
thrown around a lot. Well, now you know what they mean --- hopefully.

\begin{ExcList}
  \Exercise{Show that
    $\parens{A \notiff B} \iff \parens{\parens{A \notimplies B} \lor \parens{B
        \notimplies A}}$}
  \Answer{Let's restate the problem.
    \[
    \parens{
      A \notiff B
    } \iff \parens{
      \parens{
        A \notimplies B
      } \lor \parens{
        B \notimplies A
      }
    }
    \]
    \[
    \lnot\parens{
      A \iff B
    } \iff \parens{
      \lnot\parens{
        A \implies B
      } \lor \lnot\parens{
        B \implies A
      }
    }
    \]
    \[
    \lnot\parens{
      A \iff B
    }
    \iff
    \lnot
    \parens{
      \parens{
        A \implies B
      }
      \land
      \parens{
        B \implies A
      }
    }
    \]
    \[
    \lnot\parens{
      A \iff B
    }
    \iff
    \lnot
    \parens{
      A \iff B
    }
    \]
    Q.E.D.
  }
\end{ExcList}