From b6efdf1ebc031b9d7048e6dea230884be85f8ff4 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 3 Nov 2026 16:38:02 +0000
Subject: [PATCH 1/2] Add laws of propositional logic to Proof Writing

mcs (CSCI 201) defines these general results locally. Moving them here,
one block per subfile, lets mcs include them instead of keeping its own
copies, per the mds/mcs consolidation plan. Each block keeps its mcs id,
so no link in mcs breaks when it switches to the include.

Adds tautology, contradiction, equivalence as a tautological
biconditional, double negation, the distributive laws, replacing a part
by an equivalent part, negating a conditional, the conditional as an or,
and why a proof by contradiction works. The last proof is a full truth
table rather than mcs's pointer to an exercise solution.

Part of #453.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox
---
 _proof-writing.qmd                            | 36 +++++++++++++
 .../proof-writing/_cor-conditional-as-or.qmd  | 28 ++++++++++
 .../proof-writing/_def-contradiction.qmd      |  7 +++
 _subfiles/proof-writing/_def-tautology.qmd    |  7 +++
 .../_thm-contradiction-works.qmd              | 35 +++++++++++++
 _subfiles/proof-writing/_thm-distributive.qmd | 51 +++++++++++++++++++
 .../proof-writing/_thm-double-negation.qmd    | 28 ++++++++++
 .../proof-writing/_thm-equivalence-iff.qmd    | 23 +++++++++
 .../proof-writing/_thm-negate-conditional.qmd | 25 +++++++++
 .../proof-writing/_thm-substitution-logic.qmd | 22 ++++++++
 10 files changed, 262 insertions(+)
 create mode 100644 _subfiles/proof-writing/_cor-conditional-as-or.qmd
 create mode 100644 _subfiles/proof-writing/_def-contradiction.qmd
 create mode 100644 _subfiles/proof-writing/_def-tautology.qmd
 create mode 100644 _subfiles/proof-writing/_thm-contradiction-works.qmd
 create mode 100644 _subfiles/proof-writing/_thm-distributive.qmd
 create mode 100644 _subfiles/proof-writing/_thm-double-negation.qmd
 create mode 100644 _subfiles/proof-writing/_thm-equivalence-iff.qmd
 create mode 100644 _subfiles/proof-writing/_thm-negate-conditional.qmd
 create mode 100644 _subfiles/proof-writing/_thm-substitution-logic.qmd

diff --git a/_proof-writing.qmd b/_proof-writing.qmd
index ef7c4aff8..430587707 100644
--- a/_proof-writing.qmd
+++ b/_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/_def-contradiction.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_thm-equivalence-iff.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_thm-double-negation.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_thm-distributive.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_thm-substitution-logic.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_thm-negate-conditional.qmd >}}
+
+{{< slidebreak >}}
+
+{{< include mds/_subfiles/proof-writing/_cor-conditional-as-or.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 >}}
 
 
diff --git a/_subfiles/proof-writing/_cor-conditional-as-or.qmd b/_subfiles/proof-writing/_cor-conditional-as-or.qmd
new file mode 100644
index 000000000..7ae899114
--- /dev/null
+++ b/_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$.
+
+:::
+
+:::
diff --git a/_subfiles/proof-writing/_def-contradiction.qmd b/_subfiles/proof-writing/_def-contradiction.qmd
new file mode 100644
index 000000000..56fe32b76
--- /dev/null
+++ b/_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).
+
+:::
diff --git a/_subfiles/proof-writing/_def-tautology.qmd b/_subfiles/proof-writing/_def-tautology.qmd
new file mode 100644
index 000000000..cf5767cc2
--- /dev/null
+++ b/_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).
+
+:::
diff --git a/_subfiles/proof-writing/_thm-contradiction-works.qmd b/_subfiles/proof-writing/_thm-contradiction-works.qmd
new file mode 100644
index 000000000..b2d8bbb25
--- /dev/null
+++ b/_subfiles/proof-writing/_thm-contradiction-works.qmd
@@ -0,0 +1,35 @@
+:::{#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).
+
+:::
+
+:::
diff --git a/_subfiles/proof-writing/_thm-distributive.qmd b/_subfiles/proof-writing/_thm-distributive.qmd
new file mode 100644
index 000000000..94a1c44c7
--- /dev/null
+++ b/_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).
+
+:::
+
+:::
diff --git a/_subfiles/proof-writing/_thm-double-negation.qmd b/_subfiles/proof-writing/_thm-double-negation.qmd
new file mode 100644
index 000000000..9fdbd081c
--- /dev/null
+++ b/_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).
+
+:::
+
+:::
diff --git a/_subfiles/proof-writing/_thm-equivalence-iff.qmd b/_subfiles/proof-writing/_thm-equivalence-iff.qmd
new file mode 100644
index 000000000..b2b4c25da
--- /dev/null
+++ b/_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$.
+
+:::
+
+:::
diff --git a/_subfiles/proof-writing/_thm-negate-conditional.qmd b/_subfiles/proof-writing/_thm-negate-conditional.qmd
new file mode 100644
index 000000000..5258f9610
--- /dev/null
+++ b/_subfiles/proof-writing/_thm-negate-conditional.qmd
@@ -0,0 +1,25 @@
+:::{#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,
+which is the same row.
+
+:::
+
+:::
diff --git a/_subfiles/proof-writing/_thm-substitution-logic.qmd b/_subfiles/proof-writing/_thm-substitution-logic.qmd
new file mode 100644
index 000000000..c04666daf
--- /dev/null
+++ b/_subfiles/proof-writing/_thm-substitution-logic.qmd
@@ -0,0 +1,22 @@
+:::{#thm-substitution-logic}
+#### Replacing a part by an equivalent part
+
+Let $A$ and $B$ be [logically equivalent](#def-logically-equivalent) [propositions](#def-proposition).
+Replacing $A$ by $B$ inside a larger [proposition](#def-proposition)
+gives a proposition logically equivalent to the larger one.
+In particular, $\neg A \equiv \neg B$.
+
+:::
+
+::: {.content-hidden when-format="revealjs"}
+
+::: proof
+
+Whether the larger [proposition](#def-proposition) is true in a row of its [truth table](#def-truth-table)
+depends only on whether $A$ is true in that row, not on how $A$ is written.
+$A$ and $B$ are true in the same rows,
+so the two larger [propositions](#def-proposition) are true in the same rows too.
+
+:::
+
+:::

From 68e9c4194ca28ad8bec611d1013c9ccd7fa6de4d Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 3 Nov 2026 16:48:15 +0000
Subject: [PATCH 2/2] Add examples and narrow #596 to the first four logic laws

The review of #596 asked for an example after each new definition and
result, as the rest of the Proof Writing page has. This adds one each
for tautology, contradiction, equivalence as a tautological
biconditional and double negation, and splits a long "where" clause in
the contradiction proof onto its own line.

Adding those examples takes the PR past the size cap, so the
distributive laws, the substitution theorem, negating a conditional
and the conditional as an or move to their own PR, with examples of
their own.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox
---
 _proof-writing.qmd                            | 14 ++---
 .../proof-writing/_cor-conditional-as-or.qmd  | 28 ----------
 .../proof-writing/_exm-contradiction.qmd      | 16 ++++++
 .../proof-writing/_exm-double-negation.qmd    | 11 ++++
 .../proof-writing/_exm-equivalence-iff.qmd    | 21 ++++++++
 _subfiles/proof-writing/_exm-tautology.qmd    | 16 ++++++
 .../_thm-contradiction-works.qmd              |  3 +-
 _subfiles/proof-writing/_thm-distributive.qmd | 51 -------------------
 .../proof-writing/_thm-negate-conditional.qmd | 25 ---------
 .../proof-writing/_thm-substitution-logic.qmd | 22 --------
 10 files changed, 73 insertions(+), 134 deletions(-)
 delete mode 100644 _subfiles/proof-writing/_cor-conditional-as-or.qmd
 create mode 100644 _subfiles/proof-writing/_exm-contradiction.qmd
 create mode 100644 _subfiles/proof-writing/_exm-double-negation.qmd
 create mode 100644 _subfiles/proof-writing/_exm-equivalence-iff.qmd
 create mode 100644 _subfiles/proof-writing/_exm-tautology.qmd
 delete mode 100644 _subfiles/proof-writing/_thm-distributive.qmd
 delete mode 100644 _subfiles/proof-writing/_thm-negate-conditional.qmd
 delete mode 100644 _subfiles/proof-writing/_thm-substitution-logic.qmd

diff --git a/_proof-writing.qmd b/_proof-writing.qmd
index 430587707..f0310c5e1 100644
--- a/_proof-writing.qmd
+++ b/_proof-writing.qmd
@@ -96,31 +96,31 @@ The symbols for [logical entailment](#def-logical-entailment) are listed under
 
 {{< slidebreak >}}
 
-{{< include mds/_subfiles/proof-writing/_def-contradiction.qmd >}}
+{{< include mds/_subfiles/proof-writing/_exm-tautology.qmd >}}
 
 {{< slidebreak >}}
 
-{{< include mds/_subfiles/proof-writing/_thm-equivalence-iff.qmd >}}
+{{< include mds/_subfiles/proof-writing/_def-contradiction.qmd >}}
 
 {{< slidebreak >}}
 
-{{< include mds/_subfiles/proof-writing/_thm-double-negation.qmd >}}
+{{< include mds/_subfiles/proof-writing/_exm-contradiction.qmd >}}
 
 {{< slidebreak >}}
 
-{{< include mds/_subfiles/proof-writing/_thm-distributive.qmd >}}
+{{< include mds/_subfiles/proof-writing/_thm-equivalence-iff.qmd >}}
 
 {{< slidebreak >}}
 
-{{< include mds/_subfiles/proof-writing/_thm-substitution-logic.qmd >}}
+{{< include mds/_subfiles/proof-writing/_exm-equivalence-iff.qmd >}}
 
 {{< slidebreak >}}
 
-{{< include mds/_subfiles/proof-writing/_thm-negate-conditional.qmd >}}
+{{< include mds/_subfiles/proof-writing/_thm-double-negation.qmd >}}
 
 {{< slidebreak >}}
 
-{{< include mds/_subfiles/proof-writing/_cor-conditional-as-or.qmd >}}
+{{< include mds/_subfiles/proof-writing/_exm-double-negation.qmd >}}
 
 {{< slidebreak >}}
 
diff --git a/_subfiles/proof-writing/_cor-conditional-as-or.qmd b/_subfiles/proof-writing/_cor-conditional-as-or.qmd
deleted file mode 100644
index 7ae899114..000000000
--- a/_subfiles/proof-writing/_cor-conditional-as-or.qmd
+++ /dev/null
@@ -1,28 +0,0 @@
-:::{#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$.
-
-:::
-
-:::
diff --git a/_subfiles/proof-writing/_exm-contradiction.qmd b/_subfiles/proof-writing/_exm-contradiction.qmd
new file mode 100644
index 000000000..09d72269a
--- /dev/null
+++ b/_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).
+
+:::
diff --git a/_subfiles/proof-writing/_exm-double-negation.qmd b/_subfiles/proof-writing/_exm-double-negation.qmd
new file mode 100644
index 000000000..327a1de38
--- /dev/null
+++ b/_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.
+
+:::
diff --git a/_subfiles/proof-writing/_exm-equivalence-iff.qmd b/_subfiles/proof-writing/_exm-equivalence-iff.qmd
new file mode 100644
index 000000000..7075aa51f
--- /dev/null
+++ b/_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.
+
+:::
diff --git a/_subfiles/proof-writing/_exm-tautology.qmd b/_subfiles/proof-writing/_exm-tautology.qmd
new file mode 100644
index 000000000..ec4ffa4f1
--- /dev/null
+++ b/_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).
+
+:::
diff --git a/_subfiles/proof-writing/_thm-contradiction-works.qmd b/_subfiles/proof-writing/_thm-contradiction-works.qmd
index b2d8bbb25..1e2744f7b 100644
--- a/_subfiles/proof-writing/_thm-contradiction-works.qmd
+++ b/_subfiles/proof-writing/_thm-contradiction-works.qmd
@@ -17,7 +17,8 @@ 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,
+$\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)$ |
diff --git a/_subfiles/proof-writing/_thm-distributive.qmd b/_subfiles/proof-writing/_thm-distributive.qmd
deleted file mode 100644
index 94a1c44c7..000000000
--- a/_subfiles/proof-writing/_thm-distributive.qmd
+++ /dev/null
@@ -1,51 +0,0 @@
-:::{#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).
-
-:::
-
-:::
diff --git a/_subfiles/proof-writing/_thm-negate-conditional.qmd b/_subfiles/proof-writing/_thm-negate-conditional.qmd
deleted file mode 100644
index 5258f9610..000000000
--- a/_subfiles/proof-writing/_thm-negate-conditional.qmd
+++ /dev/null
@@ -1,25 +0,0 @@
-:::{#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,
-which is the same row.
-
-:::
-
-:::
diff --git a/_subfiles/proof-writing/_thm-substitution-logic.qmd b/_subfiles/proof-writing/_thm-substitution-logic.qmd
deleted file mode 100644
index c04666daf..000000000
--- a/_subfiles/proof-writing/_thm-substitution-logic.qmd
+++ /dev/null
@@ -1,22 +0,0 @@
-:::{#thm-substitution-logic}
-#### Replacing a part by an equivalent part
-
-Let $A$ and $B$ be [logically equivalent](#def-logically-equivalent) [propositions](#def-proposition).
-Replacing $A$ by $B$ inside a larger [proposition](#def-proposition)
-gives a proposition logically equivalent to the larger one.
-In particular, $\neg A \equiv \neg B$.
-
-:::
-
-::: {.content-hidden when-format="revealjs"}
-
-::: proof
-
-Whether the larger [proposition](#def-proposition) is true in a row of its [truth table](#def-truth-table)
-depends only on whether $A$ is true in that row, not on how $A$ is written.
-$A$ and $B$ are true in the same rows,
-so the two larger [propositions](#def-proposition) are true in the same rows too.
-
-:::
-
-:::