From 037ea0f76794741e1b15eb407bfc3d7dbd0f82d0 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Fri, 17 May 2024 10:45:50 -0600 Subject: [PATCH] Propositional and predicate logic notes. --- .../plugins/obsidian-to-anki-plugin/data.json | 26 +- notes/_journal/2024-05-17.md | 11 + notes/_journal/{ => 2024-05}/2024-05-15.md | 3 +- notes/_journal/2024-05/2024-05-16.md | 12 + notes/abstract-data-types/index.md | 2 +- notes/c17/strings.md | 2 +- notes/encoding/integer.md | 6 +- notes/{programming => logic}/equiv-trans.md | 169 +------ notes/logic/pred-logic.md | 92 ++++ notes/logic/prop-logic.md | 413 ++++++++++++++++++ notes/logic/propositional.md | 232 ---------- notes/programming/pred-trans.md | 91 +++- notes/set/axioms.md | 34 +- notes/set/index.md | 65 +++ 14 files changed, 742 insertions(+), 416 deletions(-) create mode 100644 notes/_journal/2024-05-17.md rename notes/_journal/{ => 2024-05}/2024-05-15.md (69%) create mode 100644 notes/_journal/2024-05/2024-05-16.md rename notes/{programming => logic}/equiv-trans.md (69%) create mode 100644 notes/logic/pred-logic.md create mode 100644 notes/logic/prop-logic.md delete mode 100644 notes/logic/propositional.md diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index 5a61207..9c18e66 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -166,7 +166,7 @@ "_journal/2024-02-02.md": "a3b222daee8a50bce4cbac699efc7180", "_journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb", "_journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970", - "logic/equiv-trans.md": "63515dfd471653bc0c8bc4eca66ccaf8", + "logic/equiv-trans.md": "454cfcfac3a220868b3e7c4a4fd9462c", "_journal/2024-02-07.md": "8d81cd56a3b33883a7706d32e77b5889", "algorithms/loop-invariants.md": "cbefc346842c21a6cce5c5edce451eb2", "algorithms/loop-invariant.md": "3b390e720f3b2a98e611b49a0bb1f5a9", @@ -239,7 +239,7 @@ "_journal/2024-02/2024-02-21.md": "f423137ae550eb958378750d1f5e98c7", "_journal/2024-02-23.md": "219ce9ad15a8733edd476c97628b71fd", "_journal/2024-02/2024-02-22.md": "312e55d57868026f6e80f7989a889c2b", - "c17/strings.md": "8f23005c9f8e25c72e2ac6b74b6afd7e", + "c17/strings.md": "192fe7fe4e321262dcd9ad2a1d322d8e", "c17/index.md": "78576ee41d0185df82c59999142f4edb", "c17/escape-sequences.md": "a8b99070336878b4e8c11e9e4525a500", "c17/declarations.md": "65d2faaf8cc50878ad80126109e98b1f", @@ -258,7 +258,7 @@ "filesystems/cas.md": "d41c0d2e943adecbadd10a03fd1e4274", "git/objects.md": "8c1da67ac3f568624c3f9623eb2133e1", "git/index.md": "ca842957bda479dfa1170ae85f2f37b8", - "encoding/integer.md": "2ab21152b9468f547ebee496e03bc410", + "encoding/integer.md": "17387c74064bc738c4b4929ab37a0f56", "_journal/2024-02-29.md": "f610f3caed659c1de3eed5f226cab508", "_journal/2024-02/2024-02-28.md": "7489377c014a2ff3c535d581961b5b82", "_journal/2024-03-01.md": "a532486279190b0c12954966cbf8c3fe", @@ -307,7 +307,7 @@ "_journal/2024-03-18.md": "8479f07f63136a4e16c9cd07dbf2f27f", "_journal/2024-03/2024-03-17.md": "23f9672f5c93a6de52099b1b86834e8b", "set/directed-graph.md": "b4b8ad1be634a0a808af125fe8577a53", - "set/index.md": "f2e907b2643cd4e5023169dcd96ca828", + "set/index.md": "fd0afffa094e47aace1ec89428218eec", "set/graphs.md": "4bbcea8f5711b1ae26ed0026a4a69800", "_journal/2024-03-19.md": "a0807691819725bf44c0262405e97cbb", "_journal/2024-03/2024-03-18.md": "63c3c843fc6cfc2cd289ac8b7b108391", @@ -395,7 +395,7 @@ "_journal/2024-04/2024-04-28.md": "b34a9fe3bccb1f224b96ca00e78ad061", "programming/assertions.md": "d663ab31fc7e7296b6636edbffe9d8c7", "programming/text-sub.md": "4ffcaf134858b478ffc3087b58026ee8", - "programming/equiv-trans.md": "77b02845208902d55d3048bc05584d6e", + "programming/equiv-trans.md": "c165edfa15a2628d60ae3dfd839df170", "programming/index.md": "bb082325e269a95236aa6aff9307fe59", "_journal/2024-04-30.md": "369f98b9d91de89cc1f4f581bc530c0d", "_journal/2024-04/2024-04-29.md": "b4fa2fd62e1b4fe34c1f71dc1e9f5b0b", @@ -407,7 +407,7 @@ "data-structures/heaps.md": "a0289574930328d422b9b53047936274", "data-structures/index.md": "2605977fad54956b5dc2d8dda9be2b10", "abstract-data-types/priority-queues.md": "d3dad736cb05c47bdc93c52a3a4af083", - "abstract-data-types/index.md": "6b110b20393c561497629ca4c3e09472", + "abstract-data-types/index.md": "ff6dbecefeec918a1def38af4999fc51", "_journal/2024-05-04.md": "679934dc63ded49503d573b8d2046e5d", "_journal/2024-05/2024-05-03.md": "be21fe4d9c1c24f74a74d06d07f8e90b", "_journal/2024-05/2024-05-02.md": "d7d6ba7e065d807986f0bd77281c0bb1", @@ -430,13 +430,19 @@ "_journal/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b", "_journal/2024-05/2024-05-12.md": "ca9f3996272152ef89924bb328efd365", "git/remotes.md": "2208e34b3195b6f1ec041024a66fb38b", - "programming/pred-trans.md": "241dc727a7a1cb5c899e5ddc7abb92fb", - "set/axioms.md": "8459540f07443284f80e8fb112c69d0a", + "programming/pred-trans.md": "736e2c6e89494c8f5a2a7998aa905fdd", + "set/axioms.md": "063955bf19c703e9ad23be2aee4f1ab7", "_journal/2024-05-14.md": "f6ece1d6c178d57875786f87345343c5", "_journal/2024-05/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b", "x86-64/registers.md": "be5e22ceb14084c34f446dd91702477b", - "_journal/2024-05-15.md": "17e60d1515be44ac4121eb86060ec4dd", - "_journal/2024-05/2024-05-14.md": "f6ece1d6c178d57875786f87345343c5" + "_journal/2024-05-15.md": "4e6a7e6df32e93f0d8a56bc76613d908", + "_journal/2024-05/2024-05-14.md": "f6ece1d6c178d57875786f87345343c5", + "_journal/2024-05-16.md": "580c7ec61ec56be92fa8d6affcf0a5f6", + "_journal/2024-05/2024-05-15.md": "4e6a7e6df32e93f0d8a56bc76613d908", + "logic/pred-logic.md": "c23c3da8756ac0ef17b9710a67440d84", + "logic/prop-logic.md": "4d45544452791470458cfb08656e16c1", + "_journal/2024-05-17.md": "4bada636652a610967c4ce51deb2ff43", + "_journal/2024-05/2024-05-16.md": "9fdfadc3f9ea6a4418fd0e7066d6b10c" }, "fields_dict": { "Basic": [ diff --git a/notes/_journal/2024-05-17.md b/notes/_journal/2024-05-17.md new file mode 100644 index 0000000..d3996cd --- /dev/null +++ b/notes/_journal/2024-05-17.md @@ -0,0 +1,11 @@ +--- +title: "2024-05-17" +--- + +- [x] Anki Flashcards +- [x] KoL +- [ ] Sheet Music (10 min.) +- [ ] Go (1 Life & Death Problem) +- [ ] Korean (Read 1 Story) + +* Exploration of the law of [[pred-trans#Distributivity of Conjunction|Distributivity of Conjunction]]. \ No newline at end of file diff --git a/notes/_journal/2024-05-15.md b/notes/_journal/2024-05/2024-05-15.md similarity index 69% rename from notes/_journal/2024-05-15.md rename to notes/_journal/2024-05/2024-05-15.md index f273943..bf21804 100644 --- a/notes/_journal/2024-05-15.md +++ b/notes/_journal/2024-05/2024-05-15.md @@ -8,4 +8,5 @@ title: "2024-05-15" - [ ] Go (1 Life & Death Problem) - [ ] Korean (Read 1 Story) -* Finished MOV instruction class practice problems in "Computer Systems: A Programmer's Perspective". Also notes on `leaq`. \ No newline at end of file +* Finished MOV instruction class practice problems in "Computer Systems: A Programmer's Perspective". Also notes on `leaq`. +* Notes on different set notations. \ No newline at end of file diff --git a/notes/_journal/2024-05/2024-05-16.md b/notes/_journal/2024-05/2024-05-16.md new file mode 100644 index 0000000..468ba70 --- /dev/null +++ b/notes/_journal/2024-05/2024-05-16.md @@ -0,0 +1,12 @@ +--- +title: "2024-05-16" +--- + +- [x] Anki Flashcards +- [x] KoL +- [ ] Sheet Music (10 min.) +- [ ] Go (1 Life & Death Problem) +- [ ] Korean (Read 1 Story) + +* Refine the distinction between propositions/predicates and their state representations. +* Additional notes on the first few set theory axioms. \ No newline at end of file diff --git a/notes/abstract-data-types/index.md b/notes/abstract-data-types/index.md index eafdadf..2ba1764 100644 --- a/notes/abstract-data-types/index.md +++ b/notes/abstract-data-types/index.md @@ -13,7 +13,7 @@ An **abstract data type** (ADT) is a mathematical model for data types, defined %%ANKI Basic What is an ADT an acronym for? -Back: **A**bstract **D**ata **T**type. +Back: **A**bstract **D**ata **T**ype. Reference: “Abstract Data Type.” In _Wikipedia_, March 18, 2024. [https://en.wikipedia.org/w/index.php?title=Abstract_data_type&oldid=1214359576](https://en.wikipedia.org/w/index.php?title=Abstract_data_type&oldid=1214359576). END%% diff --git a/notes/c17/strings.md b/notes/c17/strings.md index 716b795..b349fc4 100644 --- a/notes/c17/strings.md +++ b/notes/c17/strings.md @@ -232,7 +232,7 @@ END%% %%ANKI Basic How do the `+` and `␣` `printf` flags relate to one another? -Back: Both prepend a character to positive signed-numeric types. +Back: Both prepend a character to positively signed-numeric types. Reference: “Printf,” in *Wikipedia*, January 18, 2024, [https://en.wikipedia.org/w/index.php?title=Printf&oldid=1196716962](https://en.wikipedia.org/w/index.php?title=Printf&oldid=1196716962). Tags: printf diff --git a/notes/encoding/integer.md b/notes/encoding/integer.md index 80acaa2..ad4fed8 100644 --- a/notes/encoding/integer.md +++ b/notes/encoding/integer.md @@ -1054,7 +1054,7 @@ END%% %%ANKI Basic How do you detect whether unsigned addition $s \coloneqq x +_w^u y$ overflowed? -Back: Overflow occurs if and only if $s < x$. +Back: Overflow occurs if and only if $s < x$ (or $s < y$). Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. END%% @@ -1299,8 +1299,8 @@ END%% %%ANKI Basic -Which two's-complement integer is its own additive inverse? -Back: $TMin$ +Which two's-complement integers are their own additive inverse? +Back: $TMin$ and $0$. Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. END%% diff --git a/notes/programming/equiv-trans.md b/notes/logic/equiv-trans.md similarity index 69% rename from notes/programming/equiv-trans.md rename to notes/logic/equiv-trans.md index 1a20b73..cfd593b 100644 --- a/notes/programming/equiv-trans.md +++ b/notes/logic/equiv-trans.md @@ -10,7 +10,9 @@ tags: ## Overview -**Equivalence-transformation** refers to a class of calculi for [[propositional|propositional logic]] derived from negation ($\neg$), conjunction ($\land$), disjunction ($\lor$), implication ($\Rightarrow$), and equality ($=$). Gries covers two in "The Science of Programming": a system of evaluation and a formal system. The system of evaluation mirrors how a computer processes instructions, at least in an abstract sense. The formal system serves as a theoretical framework for reasoning about propositions and their transformations without resorting to "lower-level" operations like substitution. +**Equivalence-transformation** refers to a class of calculi for [[prop-logic|propositional logic]] derived from negation ($\neg$), conjunction ($\land$), disjunction ($\lor$), implication ($\Rightarrow$), and equality ($=$). + +Gries covers two in "The Science of Programming": a system of evaluation and a formal system. The system of evaluation mirrors how a computer processes instructions, at least in an abstract sense. The formal system serves as a theoretical framework for reasoning about propositions and their transformations without resorting to "lower-level" operations like substitution. %%ANKI Basic @@ -20,14 +22,6 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in END%% -%%ANKI -Basic -What are constant propositions? -Back: Propositions that contain only constants as operands. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - %%ANKI Cloze Gries replaces logical operator {$\Leftrightarrow$} in favor of {$=$}. @@ -35,27 +29,6 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in END%% -%%ANKI -Basic -How does Lean define propositional equality? -Back: Expressions `a` and `b` are propositionally equal iff `a = b` is true. -Reference: Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. -Tags: lean - -END%% - -%%ANKI -Basic -How does Lean define `propext`? -Back: -```lean -axiom propext {a b : Prop} : (a ↔ b) → (a = b) -``` -Reference: Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. -Tags: lean - -END%% - %%ANKI Basic What Lean theorem justifies Gries' choice of $=$ over $\Leftrightarrow$? @@ -65,142 +38,6 @@ Tags: lean END%% -%%ANKI -Basic -Is $(b \land c)$ well-defined in $\{(b, T), (c, F)\}$? -Back: Yes. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Is $(b \lor d)$ well-defined in $\{(b, T), (c, F)\}$? -Back: No. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What proposition represents states $\{(b, T)\}$ and $\{(c, F)\}$? -Back: $b \lor \neg c$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What set of states does $a \land b$ represent? -Back: The set containing just state $\{(a, T), (b, T)\}$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is sloppy about phrase "the states in $b \lor \neg c$"? -Back: $b \lor \neg c$ is not a set but a representation of a set (of states). -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the weakest proposition? -Back: $T$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What set of states does $T$ represent? -Back: The set of all states. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the strongest proposition? -Back: $F$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What set of states does $F$ represent? -Back: The set of no states. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What does a proposition *represent*? -Back: The set of states in which it is true. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -When is $p$ stronger than $q$? -Back: When $p \Rightarrow q$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -If $p \Rightarrow q$, which of $p$ or $q$ is considered stronger? -Back: $p$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -When is $p$ weaker than $q$? -Back: When $q \Rightarrow p$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -If $p \Rightarrow q$, which of $p$ or $q$ is considered weaker? -Back: $q$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -A proposition is well-defined with respect to what? -Back: A state to evaluate against. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Why is $b \land c$ stronger than $b \lor c$? -Back: The former represents a subset of the states the latter represents. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is a state? -Back: A function mapping identifiers to values. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - %%ANKI Basic What are the two calculi Gries describes equivalence-transformation with? diff --git a/notes/logic/pred-logic.md b/notes/logic/pred-logic.md new file mode 100644 index 0000000..96c92e3 --- /dev/null +++ b/notes/logic/pred-logic.md @@ -0,0 +1,92 @@ +--- +title: Predicate Logic +TARGET DECK: Obsidian::STEM +FILE TAGS: logic::predicate +tags: + - logic + - predicate +--- + +## Overview + +A branch of logic that uses quantified variables over non-logical objects. A **predicate** is a sentence with some number of free variables. A predicate with free variables "plugged in" is a [[prop-logic|proposition]]. + +%%ANKI +Cloze +{Predicate} logic is also known as {first}-order logic. +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +What is a predicate? +Back: A sentence with some number of free variables. +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +What distinguishes a predicate from a proposition? +Back: A proposition does not contain free variables. +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +How are propositions defined in terms of predicates? +Back: A proposition is a predicate with $0$ free variables. +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +Why is "$3 + x = 12$" *not* a proposition? +Back: Because $x$ is a variable. +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +## Sets + +A **state** is a function that maps identifiers to values. A predicate can be equivalently seen as a representation of the set of states in which it is true. + +%%ANKI +Basic +Is $(i \geq 0)$ well-defined in $\{(i, -10)\}$? +Back: Yes. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Is $(i \geq 0)$ well-defined in $\{(j, -10)\}$? +Back: No. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What predicate represents states $\{(i, 0), (i, 2), (i, 4), \ldots\}$? +Back: $i \geq 0$ is even. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is sloppy about phrase "the states in $i + j = 0$"? +Back: $i + j = 0$ is not a set but a representation of a set (of states). +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +## Bibliography + +* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +* Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). \ No newline at end of file diff --git a/notes/logic/prop-logic.md b/notes/logic/prop-logic.md new file mode 100644 index 0000000..eccfcbb --- /dev/null +++ b/notes/logic/prop-logic.md @@ -0,0 +1,413 @@ +--- +title: Propositional Logic +TARGET DECK: Obsidian::STEM +FILE TAGS: logic::propositional +tags: + - logic + - propositional +--- + +## Overview + +A branch of logic derived from negation ($\neg$), conjunction ($\land$), disjunction ($\lor$), implication ($\Rightarrow$), and biconditionals ($\Leftrightarrow$). A **proposition** is a sentence that can be assigned a truth or false value. + +%%ANKI +Cloze +{Propositional} logic is also known as {zeroth}-order logic. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What are the basic propositional logical operators? +Back: $\neg$, $\land$, $\lor$, $\Rightarrow$, and $\Leftrightarrow$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is a proposition? +Back: A declarative sentence which is either true or false. +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +What two categories do propositions fall within? +Back: Atomic and molecular propositions. +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +What is an atomic proposition? +Back: One that cannot be broken up into smaller propositions. +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +What is a molecular proposition? +Back: One that can be broken up into smaller propositions. +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Cloze +A {molecular} proposition can be broken up into {atomic} propositions. +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +What distinguishes a sentence from a proposition? +Back: The latter has an associated truth value. +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +What are constant propositions? +Back: Propositions that contain only constants as operands. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How does Lean define propositional equality? +Back: Expressions `a` and `b` are propositionally equal iff `a = b` is true. +Reference: Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. +Tags: lean + +END%% + +%%ANKI +Basic +How does Lean define `propext`? +Back: +```lean +axiom propext {a b : Prop} : (a ↔ b) → (a = b) +``` +Reference: Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. +Tags: lean + +END%% + +## Implication + +Implication is denoted as $\Rightarrow$. It has truth table + +$p$ | $q$ | $p \Rightarrow q$ +--- | --- | ----------------- +$T$ | $T$ | $T$ +$T$ | $F$ | $F$ +$F$ | $T$ | $T$ +$F$ | $F$ | $T$ + +Implication has a few "equivalent" English expressions that are commonly used. +Given propositions $P$ and $Q$, we have the following equivalences: + +* $P$ if $Q$ +* $P$ only if $Q$ +* $P$ is necessary for $Q$ +* $P$ is sufficient for $Q$ + +%%ANKI +Basic +What name is given to operand $a$ in $a \Rightarrow b$? +Back: The antecedent +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What name is given to operand $b$ in $a \Rightarrow b$? +Back: The consequent +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How does "$P$ if $Q$" translate with $\Rightarrow$? +Back: $Q \Rightarrow P$ +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +How does "$P$ only if $Q$" translate with $\Rightarrow$? +Back: $P \Rightarrow Q$ +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +How does "$P$ is necessary for $Q$" translate with $\Rightarrow$? +Back: $Q \Rightarrow P$ +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +How does "$P$ is sufficient for $Q$" translate with $\Rightarrow$? +Back: $P \Rightarrow Q$ +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +Which of *if* or *only if* map to *necessary*? +Back: *if* +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +Which of *if* or *only if* map to *sufficient*? +Back: *only if* +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +Which logical operator maps to "if and only if"? +Back: $\Leftrightarrow$ +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +Which logical operator maps to "necessary and sufficient"? +Back: $\Leftrightarrow$ +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +What is the converse of $P \Rightarrow Q$? +Back: $Q \Rightarrow P$ +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +When is implication equivalent to its converse? +Back: It's indeterminate. +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +What is the contrapositive of $P \Rightarrow Q$? +Back: $\neg Q \Rightarrow \neg P$ +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +When is implication equivalent to its contrapositive? +Back: They are always equivalent. +Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + +END%% + +%%ANKI +Basic +Given propositions $p$ and $q$, $p \Leftrightarrow q$ is equivalent to the conjunction of what two expressions? +Back: $p \Rightarrow q$ and $q \Rightarrow p$. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +END%% + +## Sets + +A **state** is a function that maps identifiers to $T$ or $F$. A proposition can be equivalently seen as a representation of the set of states in which it is true. + +%%ANKI +Basic +What is a state? +Back: A function mapping identifiers to values. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Is $(b \land c)$ well-defined in $\{(b, T), (c, F)\}$? +Back: Yes. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Is $(b \lor d)$ well-defined in $\{(b, T), (c, F)\}$? +Back: No. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +A proposition is well-defined with respect to what? +Back: A state to evaluate against. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What proposition represents states $\{(b, T), (c, T)\}$ and $\{(b, F), (c, F)\}$? +Back: $(b \land c) \lor (\neg b \land \neg c)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What set of states does proposition $a \land b$ represent? +Back: $\{\{(a, T), (b, T)\}\}$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What set of states does proposition $a \lor b$ represent? +Back: $\{\{(a, T), (b, T)\}, \{(a, T), (b, F)\}, \{(a, F), (b, T)\}\}$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is sloppy about phrase "the states in $b \lor \neg c$"? +Back: $b \lor \neg c$ is not a set but a representation of a set (of states). +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the weakest proposition? +Back: $T$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What set of states does $T$ represent? +Back: The set of all states. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the strongest proposition? +Back: $F$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What set of states does $F$ represent? +Back: The set of no states. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does a proposition *represent*? +Back: The set of states in which it is true. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +When is $p$ stronger than $q$? +Back: When $p \Rightarrow q$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +If $p \Rightarrow q$, which of $p$ or $q$ is considered stronger? +Back: $p$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +When is $p$ weaker than $q$? +Back: When $q \Rightarrow p$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +If $p \Rightarrow q$, which of $p$ or $q$ is considered weaker? +Back: $q$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Why is $b \land c$ stronger than $b \lor c$? +Back: The former represents a subset of the states the latter represents. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given sets $a$ and $b$, $a = b$ is equivalent to the conjunction of what two expressions? +Back: $a \subseteq b$ and $b \subseteq a$. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +END%% + +%%ANKI +Cloze +{$a \Rightarrow b$} is to propositional logic as {$a \subseteq b$} is to sets. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +END%% + +%%ANKI +Cloze +{$a \Leftrightarrow b$} is to propositional logic as {$a = b$} is to sets. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +END%% + +## Bibliography + +* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +* Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). \ No newline at end of file diff --git a/notes/logic/propositional.md b/notes/logic/propositional.md deleted file mode 100644 index f560dd6..0000000 --- a/notes/logic/propositional.md +++ /dev/null @@ -1,232 +0,0 @@ ---- -title: Propositional Logic -TARGET DECK: Obsidian::STEM -FILE TAGS: logic::propositional -tags: - - logic - - propositional ---- - -## Overview - -A branch of logic derived from negation ($\neg$), conjunction ($\land$), disjunction ($\lor$), implication ($\Rightarrow$), and biconditionals ($\Leftrightarrow$). There exists a hierarchy of terms used to describe a string of English: - -* A **sentence** is any grammatical string of words. -* A **predicate** is a sentence with free variables. -* A **statement** is a sentence that can be assigned a truth or false value. - * A predicate with free variables "plugged in" is a statement. - -%%ANKI -Basic -What are the basic propositional logical operators? -Back: $\neg$, $\land$, $\lor$, $\Rightarrow$, and $\Leftrightarrow$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is a propositional statement? -Back: A declarative sentence which is either true or false. -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -What two categories do propositional statements fall within? -Back: Atomic and molecular statements. -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -What is an atomic statement? -Back: One that cannot be broken up into smaller statements. -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -What is a molecular statement? -Back: One that can be broken up into smaller statements. -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Cloze -A {molecular} statement can be broken up into {atomic} statements. -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -What distinguishes a sentence from a statement? -Back: The latter is a sentence that can be derived a truth value. -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -What distinguishes a predicate from a statement? -Back: A statement does not contain free variables. -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -How are statements defined in terms of predicates? -Back: A statement is a predicate with $0$ free variables. -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -Why is "$3 + x = 12$" *not* a statement? -Back: Because $x$ is a variable. -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -## Implication - -Implication is denoted as $\Rightarrow$. It has truth table - -$p$ | $q$ | $p \Rightarrow q$ ---- | --- | ----------------- -$T$ | $T$ | $T$ -$T$ | $F$ | $F$ -$F$ | $T$ | $T$ -$F$ | $F$ | $T$ - -Implication has a few "equivalent" English expressions that are commonly used. -Given propositions $P$ and $Q$, we have the following equivalences: - -* $P$ if $Q$ -* $P$ only if $Q$ -* $P$ is necessary for $Q$ -* $P$ is sufficient for $Q$ - -%%ANKI -Basic -What name is given to operand $a$ in $a \Rightarrow b$? -Back: The antecedent -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What name is given to operand $b$ in $a \Rightarrow b$? -Back: The consequent -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How does "$P$ if $Q$" translate with $\Rightarrow$? -Back: $Q \Rightarrow P$ -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -How does "$P$ only if $Q$" translate with $\Rightarrow$? -Back: $P \Rightarrow Q$ -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -How does "$P$ is necessary for $Q$" translate with $\Rightarrow$? -Back: $Q \Rightarrow P$ -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -How does "$P$ is sufficient for $Q$" translate with $\Rightarrow$? -Back: $P \Rightarrow Q$ -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -Which of *if* or *only if* map to *necessary*? -Back: *if* -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -Which of *if* or *only if* map to *sufficient*? -Back: *only if* -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -Which logical operator maps to "if and only if"? -Back: $\Leftrightarrow$ -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -Which logical operator maps to "necessary and sufficient"? -Back: $\Leftrightarrow$ -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -What is the converse of $P \Rightarrow Q$? -Back: $Q \Rightarrow P$ -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -When is implication equivalent to its converse? -Back: It's indeterminate. -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -What is the contrapositive of $P \Rightarrow Q$? -Back: $\neg Q \Rightarrow \neg P$ -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -%%ANKI -Basic -When is implication equivalent to its contrapositive? -Back: They are always equivalent. -Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). - -END%% - -## Bibliography - -* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. -* Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). diff --git a/notes/programming/pred-trans.md b/notes/programming/pred-trans.md index db318de..9df7802 100644 --- a/notes/programming/pred-trans.md +++ b/notes/programming/pred-trans.md @@ -200,7 +200,7 @@ END%% %%ANKI Basic Given command $S$ and predicate $R$, what kind of mathematical object is $wp(S, R)$? -Back: A set (of states). +Back: A predicate, i.e. a set of states. Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. END%% @@ -253,6 +253,95 @@ Reference: Reference: Gries, David. *The Science of Programming*. Texts and Mon END%% +### Law of the Excluded Miracle + +Given any command $S$, $$wp(S, F) = F$$ + +%%ANKI +Basic +Given command $S$, what does $wp(S, F)$ evaluate to? +Back: The empty set. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does the Law of the Excluded Miracle state? +Back: For any command $S$, $wp(S, F) = F$. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What name is given to identity $wp(S, F) = F$? +Back: The Law of the Excluded Miracle. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Explain why the Law of the Excluded Miracle holds true. +Back: No state satisfies $F$ so no precondition can either. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Why is the Law of the Excluded Miracle named the way it is? +Back: It would indeed be a miracle if execution could terminate in no state. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +### Distributivity of Conjunction + +Given command $S$ and predicates $Q$ and $R$, $$wp(S, Q \land R) = wp(S, Q) \land wp(S, R)$$ + +%%ANKI +Basic +What does Distributivity of Conjunction state? +Back: Given command $S$ and predicates $Q$ and $R$, $wp(S, Q \land R) = wp(S, Q) \land wp(S, R)$. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +END%% + +%%ANKI +Cloze +Distributivity of Conjunction states {$wp(S, Q \land R)$} $=$ {$wp(S, Q) \land wp(S, R)$}. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +END%% + +%%ANKI +Basic +In Gries's exposition, is Distributivity of Conjunction taken as an axiom or a theorem? +Back: An axiom. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +END%% + +%%ANKI +Basic +Does $wp(S, Q) \land wp(S, R) \Rightarrow wp(S, Q \land R)$ hold when $S$ is nondeterministic? +Back: Yes. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +END%% + +%%ANKI +Basic +Does $wp(S, Q \land R) \Rightarrow wp(S, Q) \land wp(S, R)$ hold when $S$ is nondeterministic? +Back: Yes. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +END%% + +%%ANKI +Basic +What does it mean for command $S$ to be nondeterministic? +Back: Execution may not be the same even if begun in the same state. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +END%% + ## Bibliography * Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. \ No newline at end of file diff --git a/notes/set/axioms.md b/notes/set/axioms.md index 26c6150..732a875 100644 --- a/notes/set/axioms.md +++ b/notes/set/axioms.md @@ -97,6 +97,14 @@ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Pre END%% +%%ANKI +Basic +How is the empty set defined using set-builder notation? +Back: $\{x \mid x \neq x\}$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + ## Pairing Axiom For any sets $u$ and $v$, there exists a set having as members just $u$ and $v$: $$\forall u, \forall v, \exists B, \forall x, (x \in B \Leftrightarrow x = u \lor x = v)$$ @@ -165,6 +173,14 @@ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Pre END%% +%%ANKI +Basic +How is the pair set $\{u, v\}$ defined using set-builder notation? +Back: $\{x \mid x = u \lor x = v\}$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + ## Union Axiom ### Preliminary Form @@ -205,12 +221,20 @@ END%% %%ANKI Basic -What two set theory axioms proves existence of e.g. $\{x_1, x_2, x_3\}$? +What two set theory axioms prove existence of e.g. $\{x_1, x_2, x_3\}$? Back: The pairing axiom and union axiom. Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). END%% +%%ANKI +Basic +How is the union of set $a$ and $b$ defined using set-builder notation? +Back: $\{x \mid x \in a \lor x \in b\}$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + ## Power Set Axiom For any set $a$, there is a set whose members are exactly the subsets of $a$: $$\forall a, \exists B, \forall x, (x \in B \Leftrightarrow x \subseteq a)$$ @@ -255,6 +279,14 @@ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Pre END%% +%%ANKI +Basic +How is the power set of set $a$ defined using set-builder notation? +Back: $\{x \mid x \subseteq a\}$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + ## Bibliography * Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). \ No newline at end of file diff --git a/notes/set/index.md b/notes/set/index.md index ae817a8..c0e5eb7 100644 --- a/notes/set/index.md +++ b/notes/set/index.md @@ -70,6 +70,71 @@ Tags: adt::dynamic_set END%% +%%ANKI +Basic +Define the set of prime numbers less than $10$ using abstraction. +Back: $\{x \mid x < 10 \land x \text{ is prime}\}$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Define the set of prime numbers less than $5$ using set-builder notation. +Back: $\{x \mid x < 5 \land x \text{ is prime}\}$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Define the set of prime numbers less than $5$ using roster notation. +Back: $\{2, 3\}$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Define the set of prime numbers less than $5$ using abstraction. +Back: $\{x \mid x < 5 \land x \text{ is prime}\}$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What term describes the expression to the right of $\mid$ in set-builder notation? +Back: The entrance requirement. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What term refers to $\_\_\; x\; \_\_$ in $\{x \mid \_\_\; x\; \_\_\}$? +Back: The entrance requirement. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +The term "entrance requirement" refers to what kind of set notation? +Back: Set-builder/abstraction. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What name is given to set notation in which members are explicitly listed? +Back: Roster notation. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + ## Bibliography +* Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). * Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). \ No newline at end of file