From 2fd3d89ebe67436896b70f491f5a7f3932f6338e Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 16:49:35 +0000 Subject: [PATCH 1/2] Add the distributive laws and negating a conditional 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. They were in #596 until its review asked for an example after each result, which took that PR past the size cap. Each result here now has an example. The substitution theorem now states its claim exactly: a proposition F built from A with connectives, and F' with A replaced by B. Long "when" clauses in the negated-conditional proof are split onto their own lines. Part of #453. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox --- _proof-writing.qmd | 32 ++++++++++++ .../proof-writing/_cor-conditional-as-or.qmd | 28 ++++++++++ .../proof-writing/_exm-conditional-as-or.qmd | 11 ++++ _subfiles/proof-writing/_exm-distributive.qmd | 13 +++++ .../proof-writing/_exm-negate-conditional.qmd | 14 +++++ .../proof-writing/_exm-substitution-logic.qmd | 14 +++++ _subfiles/proof-writing/_thm-distributive.qmd | 51 +++++++++++++++++++ .../proof-writing/_thm-negate-conditional.qmd | 27 ++++++++++ .../proof-writing/_thm-substitution-logic.qmd | 27 ++++++++++ 9 files changed, 217 insertions(+) create mode 100644 _subfiles/proof-writing/_cor-conditional-as-or.qmd create mode 100644 _subfiles/proof-writing/_exm-conditional-as-or.qmd create mode 100644 _subfiles/proof-writing/_exm-distributive.qmd create mode 100644 _subfiles/proof-writing/_exm-negate-conditional.qmd create mode 100644 _subfiles/proof-writing/_exm-substitution-logic.qmd create mode 100644 _subfiles/proof-writing/_thm-distributive.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..4ff783eed 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/_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 >}} 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/_exm-conditional-as-or.qmd b/_subfiles/proof-writing/_exm-conditional-as-or.qmd new file mode 100644 index 000000000..942363643 --- /dev/null +++ b/_subfiles/proof-writing/_exm-conditional-as-or.qmd @@ -0,0 +1,11 @@ +:::{#exm-conditional-as-or} +#### "If ..., then ..." as "or" + + +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$". + +::: diff --git a/_subfiles/proof-writing/_exm-distributive.qmd b/_subfiles/proof-writing/_exm-distributive.qmd new file mode 100644 index 000000000..072a59dda --- /dev/null +++ b/_subfiles/proof-writing/_exm-distributive.qmd @@ -0,0 +1,13 @@ +:::{#exm-distributive} +#### Distributing "and" over "or" + + +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)$. + +::: diff --git a/_subfiles/proof-writing/_exm-negate-conditional.qmd b/_subfiles/proof-writing/_exm-negate-conditional.qmd new file mode 100644 index 000000000..4ba23c267 --- /dev/null +++ b/_subfiles/proof-writing/_exm-negate-conditional.qmd @@ -0,0 +1,14 @@ +:::{#exm-negate-conditional} +#### Negating "if prime, then odd" + + +Let $n$ be an [integer](number-systems.qmd#def-integers), +and let $P$ be "$n$ is [prime](number-systems.qmd#def-prime)" +and $Q$ be "$n$ is [odd](number-systems.qmd#def-odd)". +By [negating a conditional](#thm-negate-conditional), +the negation of "if $n$ is prime, then $n$ is odd" +is "$n$ is prime, and $n$ is not odd". +For $n = 2$, the negation is true, +so the conditional is false. + +::: diff --git a/_subfiles/proof-writing/_exm-substitution-logic.qmd b/_subfiles/proof-writing/_exm-substitution-logic.qmd new file mode 100644 index 000000000..c988339b1 --- /dev/null +++ b/_subfiles/proof-writing/_exm-substitution-logic.qmd @@ -0,0 +1,14 @@ +:::{#exm-substitution-logic} +#### Simplifying part of a proposition + + +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. +$$ + +::: 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-negate-conditional.qmd b/_subfiles/proof-writing/_thm-negate-conditional.qmd new file mode 100644 index 000000000..356188211 --- /dev/null +++ b/_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. + +::: + +::: diff --git a/_subfiles/proof-writing/_thm-substitution-logic.qmd b/_subfiles/proof-writing/_thm-substitution-logic.qmd new file mode 100644 index 000000000..494959f19 --- /dev/null +++ b/_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) +is computed from the truth values of its parts in that row, +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, +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. + +::: + +::: From 10c44566de91bc885f446345c34f1046a88be6f0 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 17:47:58 +0000 Subject: [PATCH 2/2] Split the substitution example's setup sentence onto two lines Review suggestion on #599: one line for F and one for A and B. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox --- _subfiles/proof-writing/_exm-substitution-logic.qmd | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/_subfiles/proof-writing/_exm-substitution-logic.qmd b/_subfiles/proof-writing/_exm-substitution-logic.qmd index c988339b1..a54c50ccc 100644 --- a/_subfiles/proof-writing/_exm-substitution-logic.qmd +++ b/_subfiles/proof-writing/_exm-substitution-logic.qmd @@ -4,7 +4,8 @@ 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$. +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), $$