diff --git a/_proof-writing.qmd b/_proof-writing.qmd index 8b453f70a..bf52098dc 100644 --- a/_proof-writing.qmd +++ b/_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 >}} 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..b778e9f3a --- /dev/null +++ b/_subfiles/proof-writing/_exm-negate-conditional.qmd @@ -0,0 +1,15 @@ +:::{#exm-negate-conditional} +#### Negating "if prime, then odd" + + +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. + +::: diff --git a/_subfiles/proof-writing/_exm-substitution-logic.qmd b/_subfiles/proof-writing/_exm-substitution-logic.qmd new file mode 100644 index 000000000..a54c50ccc --- /dev/null +++ b/_subfiles/proof-writing/_exm-substitution-logic.qmd @@ -0,0 +1,15 @@ +:::{#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. + +::: + +:::