Add the distributive laws and negating a conditional to Proof Writing

_proof-writing.qmd

@@ -148,6 +148,38 @@ The symbols for [logical entailment](#def-logical-entailment) are listed under
 
 {{< slidebreak >}}
 
+{{< include mds/_subfiles/proof-writing/_thm-distributive.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_exm-distributive.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_thm-substitution-logic.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_exm-substitution-logic.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_thm-negate-conditional.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_exm-negate-conditional.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_cor-conditional-as-or.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_exm-conditional-as-or.qmd >}}
+
+{{< slidebreak >}}
+
 {{< include mds/_subfiles/proof-writing/_def-quantifier.qmd >}}
 
 {{< slidebreak >}}

_subfiles/proof-writing/_cor-conditional-as-or.qmd

@@ -0,0 +1,28 @@
+:::{#cor-conditional-as-or}
+#### A conditional without the arrow
+
+For [propositions](#def-proposition) $P$ and $Q$,
+
+$$
+(P \Rightarrow Q) \equiv (\neg P \lor Q).
+$$
+
+:::
+
+::: {.content-hidden when-format="revealjs"}
+
+::: proof
+
+1. By [double negation](#thm-double-negation),
+   $P \Rightarrow Q \equiv \neg \neg (P \Rightarrow Q)$.
+2. By [negating a conditional](#thm-negate-conditional)
+   and [replacing a part by an equivalent part](#thm-substitution-logic),
+   $\neg \neg (P \Rightarrow Q) \equiv \neg (P \land \neg Q)$.
+3. By the first of [De Morgan's laws](#thm-de-morgan-logic),
+   $\neg (P \land \neg Q) \equiv \neg P \lor \neg \neg Q$.
+4. By double negation and replacing a part by an equivalent part again,
+   $\neg P \lor \neg \neg Q \equiv \neg P \lor Q$.
+
+:::
+
+:::

_subfiles/proof-writing/_exm-conditional-as-or.qmd

@@ -0,0 +1,11 @@
+:::{#exm-conditional-as-or}
+#### "If ..., then ..." as "or"
+<!-- no-figure: a rewording of one sentence; nothing to plot -->
+
+Let $n$ be an [integer](number-systems.qmd#def-integers).
+By [a conditional without the arrow](#cor-conditional-as-or),
+"if $n > 2$, then $n^2 > 4$"
+says the same thing as
+"$n \le 2$, or $n^2 > 4$".
+
+:::

_subfiles/proof-writing/_exm-distributive.qmd

@@ -0,0 +1,13 @@
+:::{#exm-distributive}
+#### Distributing "and" over "or"
+<!-- no-figure: a rewording of one sentence; nothing to plot -->
+
+Let $n$ be an [integer](number-systems.qmd#def-integers).
+"$n$ is [even](number-systems.qmd#def-even-odd), and $n > 0$ or $n < 0$"
+has the form $A \land (B \lor C)$.
+By the first [distributive law](#thm-distributive),
+it says the same thing as
+"$n$ is even and $n > 0$, or $n$ is even and $n < 0$",
+which has the form $(A \land B) \lor (A \land C)$.
+
+:::

_subfiles/proof-writing/_exm-negate-conditional.qmd

@@ -0,0 +1,15 @@
+:::{#exm-negate-conditional}
+#### Negating "if prime, then odd"
+<!-- no-figure: a rewording of one sentence; nothing to plot -->
+
+Let $n$ be an [integer](number-systems.qmd#def-integers),
+let $P$ be "$n$ is [prime](number-systems.qmd#def-prime)",
+and let $Q$ be "$n$ is [odd](number-systems.qmd#def-odd)".
+By [negating a conditional](#thm-negate-conditional),
+the [negation](#def-not) of $P \Rightarrow Q$
+is $P \land \neg Q$:
+"$n$ is prime, and $n$ is not odd".
+For $n = 2$, the negation is true,
+so the conditional is false.
+
+:::

_subfiles/proof-writing/_exm-substitution-logic.qmd

@@ -0,0 +1,15 @@
+:::{#exm-substitution-logic}
+#### Simplifying part of a proposition
+<!-- no-figure: a one-line rewriting; nothing to plot -->
+
+By [double negation](#thm-double-negation),
+$\neg \neg Q \equiv Q$.
+Take $F$ to be $\neg P \lor \neg \neg Q$,
+with $A = \neg \neg Q$ and $B = Q$.
+By [replacing a part by an equivalent part](#thm-substitution-logic),
+
+$$
+\neg P \lor \neg \neg Q \equiv \neg P \lor Q.
+$$
+
+:::

_subfiles/proof-writing/_thm-distributive.qmd

@@ -0,0 +1,51 @@
+:::{#thm-distributive}
+#### Distributive laws for propositions
+
+For [propositions](#def-proposition) $A$, $B$ and $C$:
+
+$$
+\ba
+A \land (B \lor C) &\equiv (A \land B) \lor (A \land C) \\
+A \lor (B \land C) &\equiv (A \lor B) \land (A \lor C)
+\ea
+$$
+
+:::
+
+::: {.content-hidden when-format="revealjs"}
+
+::: proof
+
+By the definitions of [and](#def-and) and [or](#def-or),
+the [truth table](#def-truth-table) for the first law is:
+
+| $A$ | $B$ | $C$ | $A \land (B \lor C)$ | $(A \land B) \lor (A \land C)$ |
+|:---:|:---:|:---:|:---:|:---:|
+| T | T | T | T | T |
+| T | T | F | T | T |
+| T | F | T | T | T |
+| T | F | F | F | F |
+| F | T | T | F | F |
+| F | T | F | F | F |
+| F | F | T | F | F |
+| F | F | F | F | F |
+
+and for the second law:
+
+| $A$ | $B$ | $C$ | $A \lor (B \land C)$ | $(A \lor B) \land (A \lor C)$ |
+|:---:|:---:|:---:|:---:|:---:|
+| T | T | T | T | T |
+| T | T | F | T | T |
+| T | F | T | T | T |
+| T | F | F | T | T |
+| F | T | T | T | T |
+| F | T | F | F | F |
+| F | F | T | F | F |
+| F | F | F | F | F |
+
+In each table the last two columns match in every row,
+so each law is a [logical equivalence](#def-logically-equivalent).
+
+:::
+
+:::

_subfiles/proof-writing/_thm-negate-conditional.qmd

@@ -0,0 +1,27 @@
+:::{#thm-negate-conditional}
+#### Negating a conditional
+
+For [propositions](#def-proposition) $P$ and $Q$,
+
+$$
+\neg (P \Rightarrow Q) \equiv P \land \neg Q.
+$$
+
+:::
+
+::: {.content-hidden when-format="revealjs"}
+
+::: proof
+
+By the definition of [implies](#def-implies),
+$P \Rightarrow Q$ is false
+exactly when $P$ is true and $Q$ is false.
+So $\neg (P \Rightarrow Q)$ is true exactly in that row of the [truth table](#def-truth-table).
+By the definition of [and](#def-and),
+$P \land \neg Q$ is true
+exactly when $P$ is true and $\neg Q$ is true.
+That is the same row.
+
+:::
+
+:::

_subfiles/proof-writing/_thm-substitution-logic.qmd

@@ -0,0 +1,27 @@
+:::{#thm-substitution-logic}
+#### Replacing a part by an equivalent part
+
+Let $A$ and $B$ be [logically equivalent](#def-logically-equivalent) [propositions](#def-proposition).
+Let $F$ be a [proposition](#def-proposition) built from $A$ and other propositions
+with [logical connectives](#def-logical-connective),
+and let $F'$ be $F$ with $A$ replaced by $B$.
+Then $F \equiv F'$.
+
+:::
+
+::: {.content-hidden when-format="revealjs"}
+
+::: proof
+
+The truth value of $F$ in a row of its [truth table](#def-truth-table) <!-- check-term-links: allow -->
+is computed from the truth values of its parts in that row, <!-- check-term-links: allow -->
+using the truth table of each connective.
+$F'$ is computed the same way,
+except that $B$ takes the place of $A$.
+$A$ and $B$ have the same truth value in every row, <!-- check-term-links: allow -->
+so each step of the computation gives the same value for $F'$ as for $F$.
+So $F$ and $F'$ have the same truth value in every row. <!-- check-term-links: allow -->
+
+:::
+
+:::