Add tautology, contradiction and double negation to Proof Writing

_proof-writing.qmd

@@ -92,6 +92,38 @@ The symbols for [logical entailment](#def-logical-entailment) are listed under
 
 {{< slidebreak >}}
 
+{{< include mds/_subfiles/proof-writing/_def-tautology.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_exm-tautology.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_def-contradiction.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_exm-contradiction.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_thm-equivalence-iff.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_exm-equivalence-iff.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_thm-double-negation.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_exm-double-negation.qmd >}}
+
+{{< slidebreak >}}
+
 {{< include mds/_subfiles/proof-writing/_def-quantifier.qmd >}}
 
 {{< slidebreak >}}
@@ -269,6 +301,10 @@ Let's save $\rightarrow$ (`\rightarrow`) for [convergence](algebra.qmd#def-conve
 
 {{< slidebreak >}}
 
+{{< include mds/_subfiles/proof-writing/_thm-contradiction-works.qmd >}}
+
+{{< slidebreak >}}
+
 {{< include mds/_subfiles/proof-writing/_exm-proof-by-contradiction-truth-table.qmd >}}
 
 

_subfiles/proof-writing/_def-contradiction.qmd

@@ -0,0 +1,7 @@
+:::{#def-contradiction}
+#### Contradiction
+
+A **contradiction** is a [proposition](#def-proposition)
+that is false in every row of its [truth table](#def-truth-table).
+
+:::

_subfiles/proof-writing/_def-tautology.qmd

@@ -0,0 +1,7 @@
+:::{#def-tautology}
+#### Tautology
+
+A **tautology** is a [proposition](#def-proposition)
+that is true in every row of its [truth table](#def-truth-table).
+
+:::

_subfiles/proof-writing/_exm-contradiction.qmd

@@ -0,0 +1,16 @@
+:::{#exm-contradiction}
+#### $P \land \neg P$ is a contradiction
+<!-- no-figure: the truth table is the display -->
+
+By the definitions of [and](#def-and) and [not](#def-not),
+the [truth table](#def-truth-table) of $P \land \neg P$ is:
+
+| $P$ | $\neg P$ | $P \land \neg P$ |
+|:---:|:--------:|:----------------:|
+| T   | F        | F                |
+| F   | T        | F                |
+
+The last column is false in every row,
+so $P \land \neg P$ is a [contradiction](#def-contradiction).
+
+:::

_subfiles/proof-writing/_exm-double-negation.qmd

@@ -0,0 +1,11 @@
+:::{#exm-double-negation}
+#### Removing a double negation
+<!-- no-figure: a one-line rewording; nothing to plot -->
+
+Let $P$ be the [proposition](#def-proposition) "$7$ is [odd](number-systems.qmd#def-odd)".
+Then $\neg \neg P$ is "it is not the case that $7$ is not odd".
+By [double negation](#thm-double-negation),
+$\neg \neg P$ says the same thing as $P$:
+$7$ is odd.
+
+:::

_subfiles/proof-writing/_exm-equivalence-iff.qmd

@@ -0,0 +1,21 @@
+:::{#exm-equivalence-iff}
+#### A tautological biconditional
+<!-- no-figure: the truth table is the display -->
+
+@exm-logically-equivalent showed that
+$P \Rightarrow Q$ and $\neg P \lor Q$ are [logically equivalent](#def-logically-equivalent).
+Adding a column for the biconditional to its [truth table](#def-truth-table)
+gives:
+
+| $P$ | $Q$ | $\neg P \lor Q$ | $P \Rightarrow Q$ | $(P \Rightarrow Q) \Leftrightarrow (\neg P \lor Q)$ |
+|:---:|:---:|:---------------:|:-----------------:|:---------------------------------------------------:|
+| T   | T   | T               | T                 | T                                                   |
+| T   | F   | F               | F                 | T                                                   |
+| F   | T   | T               | T                 | T                                                   |
+| F   | F   | T               | T                 | T                                                   |
+
+The last column is true in every row,
+so the biconditional is a [tautology](#def-tautology),
+as [equivalence as a tautological biconditional](#thm-equivalence-iff) says it must be.
+
+:::

_subfiles/proof-writing/_exm-tautology.qmd

@@ -0,0 +1,16 @@
+:::{#exm-tautology}
+#### $P \lor \neg P$ is a tautology
+<!-- no-figure: the truth table is the display -->
+
+By the definitions of [or](#def-or) and [not](#def-not),
+the [truth table](#def-truth-table) of $P \lor \neg P$ is:
+
+| $P$ | $\neg P$ | $P \lor \neg P$ |
+|:---:|:--------:|:---------------:|
+| T   | F        | T               |
+| F   | T        | T               |
+
+The last column is true in every row,
+so $P \lor \neg P$ is a [tautology](#def-tautology).
+
+:::

_subfiles/proof-writing/_thm-contradiction-works.qmd

@@ -0,0 +1,36 @@
+:::{#thm-contradiction-works}
+#### Why a proof by contradiction works
+
+For [propositions](#def-proposition) $P$ and $C$,
+
+$$
+P \equiv \paren{\neg P \Rightarrow (C \land \neg C)}.
+$$
+
+:::
+
+::: {.content-hidden when-format="revealjs"}
+
+::: proof
+
+By the definitions of [and](#def-and) and [not](#def-not),
+$C \land \neg C$ is false in every row,
+so it is a [contradiction](#def-contradiction).
+So, by the definition of [implies](#def-implies),
+$\neg P \Rightarrow (C \land \neg C)$ is true exactly in the rows
+where $\neg P$ is false,
+which are the rows where $P$ is true:
+
+| $P$ | $C$ | $\neg P$ | $C \land \neg C$ | $\neg P \Rightarrow (C \land \neg C)$ |
+|:---:|:---:|:---:|:---:|:---:|
+| T | T | F | F | T |
+| T | F | F | F | T |
+| F | T | T | F | F |
+| F | F | T | F | F |
+
+The first and last columns match in every row,
+so the two are [logically equivalent](#def-logically-equivalent).
+
+:::
+
+:::

_subfiles/proof-writing/_thm-double-negation.qmd

@@ -0,0 +1,28 @@
+:::{#thm-double-negation}
+#### Double negation
+
+For a [proposition](#def-proposition) $P$,
+
+$$
+\neg \neg P \equiv P.
+$$
+
+:::
+
+::: {.content-hidden when-format="revealjs"}
+
+::: proof
+
+By the definition of [not](#def-not), the [truth table](#def-truth-table) is:
+
+| $P$ | $\neg P$ | $\neg \neg P$ |
+|:---:|:---:|:---:|
+| T | F | T |
+| F | T | F |
+
+The first and last columns match in both rows,
+so the two sides are [logically equivalent](#def-logically-equivalent).
+
+:::
+
+:::

_subfiles/proof-writing/_thm-equivalence-iff.qmd

@@ -0,0 +1,23 @@
+:::{#thm-equivalence-iff}
+#### Equivalence is a tautological biconditional
+
+For [propositions](#def-proposition) $A$ and $B$,
+$A$ and $B$ are [logically equivalent](#def-logically-equivalent)
+exactly when $A \Leftrightarrow B$ is a [tautology](#def-tautology).
+
+:::
+
+::: {.content-hidden when-format="revealjs"}
+
+::: proof
+
+By the definition of [if and only if](#def-iff),
+$A \Leftrightarrow B$ is true in a row of the [truth table](#def-truth-table)
+exactly when $A$ and $B$ have the same truth value in that row. <!-- check-term-links: allow -->
+So $A \Leftrightarrow B$ is true in every row
+exactly when $A$ and $B$ have the same truth value in every row,
+which is the definition of $A \equiv B$.
+
+:::
+
+:::