From 9c39cc2b49715767a1bd90778dc9ad4a90ac28c5 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Mon, 3 Jun 2024 07:55:29 -0600 Subject: [PATCH] Notes on equality and formal systems. --- .../plugins/obsidian-to-anki-plugin/data.json | 34 +- notes/_journal/{ => 2024-05}/2024-05-29.md | 0 notes/_journal/2024-05/2024-05-30.md | 11 + notes/_journal/2024-05/2024-05-31.md | 9 + notes/_journal/2024-06-03.md | 11 + notes/_journal/2024-06/2024-06-01.md | 9 + notes/_journal/2024-06/2024-06-02.md | 11 + notes/_templates/daily.md | 2 +- notes/algebra/set.md | 332 ++++++++++++++++++ notes/algorithms/order-growth.md | 4 +- notes/c17/strings.md | 4 +- notes/git/merge-conflicts.md | 2 +- notes/hashing/index.md | 2 +- notes/logic/equality.md | 15 + notes/programming/lambda-calculus.md | 63 +++- notes/programming/lean.md | 9 + notes/programming/pred-trans.md | 10 +- notes/set/classes.md | 2 +- notes/set/index.md | 58 ++- 19 files changed, 557 insertions(+), 31 deletions(-) rename notes/_journal/{ => 2024-05}/2024-05-29.md (100%) create mode 100644 notes/_journal/2024-05/2024-05-30.md create mode 100644 notes/_journal/2024-05/2024-05-31.md create mode 100644 notes/_journal/2024-06-03.md create mode 100644 notes/_journal/2024-06/2024-06-01.md create mode 100644 notes/_journal/2024-06/2024-06-02.md create mode 100644 notes/logic/equality.md create mode 100644 notes/programming/lean.md diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index 5d3e676..3d0fd6d 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -164,7 +164,7 @@ "posix/regexp.md": "887711b8fc64ca258d9987133ecf056c", "journal/2024-02-04.md": "e2b5678fc53d7284b71ed6820c02b954", "gawk/regexp.md": "d9229f1eabe1b99e965eecaa03bee86c", - "_templates/daily.md": "bfcd221502a23a285af100317b6ef127", + "_templates/daily.md": "36d0b695e8a955ff1d8e980154469e03", "_journal/2024-02-05.md": "f8505abd415c50fd97c81fd6153a6d4f", "_journal/2024-02-06.md": "1ea415f3c3f5be17f796b9a0d4df565f", "_journal/2024-02-04.md": "f77a3c5f3ce7969120f226738836dc92", @@ -177,7 +177,7 @@ "algorithms/loop-invariants.md": "cbefc346842c21a6cce5c5edce451eb2", "algorithms/loop-invariant.md": "3b390e720f3b2a98e611b49a0bb1f5a9", "algorithms/running-time.md": "5efc0791097d2c996f931c9046c95f65", - "algorithms/order-growth.md": "12bf6c10653912283921dcc46c7fa0f8", + "algorithms/order-growth.md": "4b03586ce9d75579f0a85be85445c1c4", "_journal/2024-02-08.md": "19092bdfe378f31e2774f20d6afbfbac", "algorithms/sorting/selection-sort.md": "73415c44d6f4429f43c366078fd4bf98", "algorithms/index 1.md": "6fada1f3d5d3af64687719eb465a5b97", @@ -245,7 +245,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": "192fe7fe4e321262dcd9ad2a1d322d8e", + "c17/strings.md": "c4da68e9280cda7bb5200382f83f6f6f", "c17/index.md": "78576ee41d0185df82c59999142f4edb", "c17/escape-sequences.md": "a8b99070336878b4e8c11e9e4525a500", "c17/declarations.md": "65d2faaf8cc50878ad80126109e98b1f", @@ -313,7 +313,7 @@ "_journal/2024-03-18.md": "8479f07f63136a4e16c9cd07dbf2f27f", "_journal/2024-03/2024-03-17.md": "23f9672f5c93a6de52099b1b86834e8b", "set/directed-graph.md": "b4b8ad1be634a0a808af125fe8577a53", - "set/index.md": "74b50d8ca249c4e99b22abd4adedb300", + "set/index.md": "55a80d53973af2c0343438346e2086b2", "set/graphs.md": "4bbcea8f5711b1ae26ed0026a4a69800", "_journal/2024-03-19.md": "a0807691819725bf44c0262405e97cbb", "_journal/2024-03/2024-03-18.md": "63c3c843fc6cfc2cd289ac8b7b108391", @@ -436,7 +436,7 @@ "_journal/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b", "_journal/2024-05/2024-05-12.md": "ca9f3996272152ef89924bb328efd365", "git/remotes.md": "2208e34b3195b6f1ec041024a66fb38b", - "programming/pred-trans.md": "6925b0be2de73c214df916a53e23fd5a", + "programming/pred-trans.md": "293806a24c2b9ef3fdb95ad74f9239b4", "set/axioms.md": "063955bf19c703e9ad23be2aee4f1ab7", "_journal/2024-05-14.md": "f6ece1d6c178d57875786f87345343c5", "_journal/2024-05/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b", @@ -451,8 +451,8 @@ "_journal/2024-05/2024-05-16.md": "9fdfadc3f9ea6a4418fd0e7066d6b10c", "_journal/2024-05-18.md": "c0b58b28f84b31cea91404f43b0ee40c", "hashing/direct-addressing.md": "87d1052ac7eae3061d88d011432cb693", - "hashing/index.md": "c870cf66e0224db58315ac0ba43b9cb1", - "set/classes.md": "18a09731868070e0c24a42bf0f582619", + "hashing/index.md": "8912a564ac1066de14044421fdc35b75", + "set/classes.md": "6776b4dc415021e0ef60b323b5c2d436", "_journal/2024-05-19.md": "fddd90fae08fab9bd83b0ef5d362c93a", "_journal/2024-05/2024-05-18.md": "c0b58b28f84b31cea91404f43b0ee40c", "_journal/2024-05/2024-05-17.md": "fb880d68077b655ede36d994554f3aba", @@ -466,7 +466,7 @@ "programming/λ-Calculus.md": "bf36bdaf85abffd171bb2087fb8228b2", "_journal/2024-05-23.md": "9d9106a68197adcee42cd19c69d2f840", "_journal/2024-05/2024-05-22.md": "3c29eec25f640183b0be365e7a023750", - "programming/lambda-calculus.md": "151797fa3c012f1971d6a33eeea19274", + "programming/lambda-calculus.md": "547bc98111e516fc70a415d91db7b3ff", "_journal/2024-05-25.md": "04e8e1cf4bfdbfb286effed40b09c900", "_journal/2024-05/2024-05-24.md": "86132f18c7a27ebc7a3e4a07f4867858", "_journal/2024-05/2024-05-23.md": "d0c98b484b1def3a9fd7262dcf2050ad", @@ -474,13 +474,25 @@ "_journal/2024-05/2024-05-25.md": "3e8a0061fa58a6e5c48d12800d1ab869", "_journal/2024-05-27.md": "b36636d10eab34380f17f288868df3ae", "_journal/2024-05/2024-05-26.md": "abe84b5beae74baa25501c818e64fc95", - "algebra/set.md": "d7b4c7943f3674bb152389f4bef1a234", + "algebra/set.md": "049c5ff36ce8fe99b2c8a8f452d0514f", "algebra/boolean.md": "56d2e0be2853d49b5dface7fa2d785a9", - "git/merge-conflicts.md": "cb7d4d373639f75f6647be60f3fe97f3", + "git/merge-conflicts.md": "af3603c7a8fde60a1982c0950d209b77", "_journal/2024-05-28.md": "0f6aeb5ec126560acdc2d8c5c6570337", "_journal/2024-05/2024-05-27.md": "e498d5154558ebcf7261302403ea8016", "_journal/2024-05-29.md": "aee3f3766659789d7dfb63dd247844cc", - "_journal/2024-05/2024-05-28.md": "28297d2a418f591ebc15c74fa459ddd9" + "_journal/2024-05/2024-05-28.md": "28297d2a418f591ebc15c74fa459ddd9", + "_journal/2024-05-30.md": "0467b8ded9cf1d9e3b419fa76f18f3c5", + "_journal/2024-05/2024-05-29.md": "ac77a3dfa0d0a538e7febd81886aba80", + "_journal/2024-05-31.md": "93b6f1e2d4a03406d8e738091874fbe4", + "_journal/2024-05/2024-05-30.md": "0b93c5b5e07130fac0e200754d68a450", + "_journal/2024-06-01.md": "46c00cc59a2ae126ad54e9114ee97646", + "_journal/2024-05/2024-05-31.md": "4421312bffa6f3c7e501a28be1e3bd5b", + "_journal/2024-06-02.md": "0059e0332794e0007545b92bc4c1ff9f", + "_journal/2024-06/2024-06-01.md": "6d39286db9d89975e441c57f6a92cfaf", + "_journal/2024-06-03.md": "560019592d88237bdb4b0ea609465ef6", + "_journal/2024-06/2024-06-02.md": "0059e0332794e0007545b92bc4c1ff9f", + "programming/lean.md": "2815eac192c7e231937e2369817a6dc1", + "logic/equality.md": "1867b676e0e7c9ec8f1addc40fefb966" }, "fields_dict": { "Basic": [ diff --git a/notes/_journal/2024-05-29.md b/notes/_journal/2024-05/2024-05-29.md similarity index 100% rename from notes/_journal/2024-05-29.md rename to notes/_journal/2024-05/2024-05-29.md diff --git a/notes/_journal/2024-05/2024-05-30.md b/notes/_journal/2024-05/2024-05-30.md new file mode 100644 index 0000000..35494d0 --- /dev/null +++ b/notes/_journal/2024-05/2024-05-30.md @@ -0,0 +1,11 @@ +--- +title: "2024-05-30" +--- + +- [x] Anki Flashcards +- [x] KoL +- [x] OGS +- [ ] Sheet Music (10 min.) +- [ ] Korean (Read 1 Story) + +* Notes on monotonicity and antimonotonicity properties of $\subseteq$. \ No newline at end of file diff --git a/notes/_journal/2024-05/2024-05-31.md b/notes/_journal/2024-05/2024-05-31.md new file mode 100644 index 0000000..8388ab9 --- /dev/null +++ b/notes/_journal/2024-05/2024-05-31.md @@ -0,0 +1,9 @@ +--- +title: "2024-05-31" +--- + +- [x] Anki Flashcards +- [x] KoL +- [x] OGS +- [ ] Sheet Music (10 min.) +- [ ] Korean (Read 1 Story) \ No newline at end of file diff --git a/notes/_journal/2024-06-03.md b/notes/_journal/2024-06-03.md new file mode 100644 index 0000000..64dd7b4 --- /dev/null +++ b/notes/_journal/2024-06-03.md @@ -0,0 +1,11 @@ +--- +title: "2024-06-03" +--- + +- [x] Anki Flashcards +- [x] KoL +- [x] OGS +- [ ] Sheet Music (10 min.) +- [ ] Korean (Read 1 Story) + +* Add notes on [[lambda-calculus#Syntactic Identity|syntactic identity]]. Relate this concept to Lean's syntactic equality. \ No newline at end of file diff --git a/notes/_journal/2024-06/2024-06-01.md b/notes/_journal/2024-06/2024-06-01.md new file mode 100644 index 0000000..773d37c --- /dev/null +++ b/notes/_journal/2024-06/2024-06-01.md @@ -0,0 +1,9 @@ +--- +title: "2024-06-01" +--- + +- [x] Anki Flashcards +- [x] KoL +- [x] OGS +- [ ] Sheet Music (10 min.) +- [ ] Korean (Read 1 Story) \ No newline at end of file diff --git a/notes/_journal/2024-06/2024-06-02.md b/notes/_journal/2024-06/2024-06-02.md new file mode 100644 index 0000000..259f681 --- /dev/null +++ b/notes/_journal/2024-06/2024-06-02.md @@ -0,0 +1,11 @@ +--- +title: "2024-06-02" +--- + +- [x] Anki Flashcards +- [x] KoL +- [x] OGS +- [ ] Sheet Music (10 min.) +- [ ] Korean (Read 1 Story) + +* Generalization of distributive laws and De Morgan's laws. \ No newline at end of file diff --git a/notes/_templates/daily.md b/notes/_templates/daily.md index 307c56e..a5e33d0 100644 --- a/notes/_templates/daily.md +++ b/notes/_templates/daily.md @@ -4,6 +4,6 @@ title: "{{date:YYYY-MM-DD}}" - [ ] Anki Flashcards - [ ] KoL +- [ ] OGS - [ ] Sheet Music (10 min.) -- [ ] Go (1 Life & Death Problem) - [ ] Korean (Read 1 Story) \ No newline at end of file diff --git a/notes/algebra/set.md b/notes/algebra/set.md index 0fc30e3..d93da8f 100644 --- a/notes/algebra/set.md +++ b/notes/algebra/set.md @@ -141,6 +141,118 @@ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Pre END%% +%%ANKI +Basic +What concept in set theory relates the algebra of sets to boolean algebra? +Back: Membership. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What two equalities relates $A \cup B$ with $a \lor b$? +Back: $a = (x \in A)$ and $b = (x \in B)$. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What two equalities relates $A \cap B$ with $a \land b$? +Back: $a = (x \in A)$ and $b = (x \in B)$. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +More generally, for any sets $A$ and $\mathscr{B}$, $$\begin{align*} A \cup \bigcap \mathscr{B} & = \bigcap\, \{A \cup X \mid X \in \mathscr{B}\}, \text{ for } \mathscr{B} \neq \varnothing \\ A \cap \bigcup \mathscr{B} & = \bigcup\, \{A \cap X \mid X \in \mathscr{B}\} \end{align*}$$ + +%%ANKI +Basic +What is the generalization of identity $A \cap (B \cup C) = (A \cap B) \cup (A \cap C)$? +Back: $A \cap \bigcup \mathscr{B} = \bigcup\, \{A \cap X \mid X \in \mathscr{B}\}$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What is the generalization of identity $A \cup (B \cap C) = (A \cup B) \cap (A \cup C)$? +Back: $A \cup \bigcap \mathscr{B} = \bigcap\, \{A \cup X \mid X \in \mathscr{B}\}$ for $\mathscr{B} \neq \varnothing$. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Cloze +Assuming $\mathscr{B} \neq \varnothing$, the distributive law states {$A \cup \bigcap \mathscr{B}$} $=$ {$\bigcap\, \{A \cup X \mid X \in \mathscr{B}\}$}. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Cloze +The distributive law states {$A \cap \bigcup \mathscr{B}$} $=$ {$\bigcup\, \{A \cap X \mid X \in \mathscr{B}\}$}. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +How is set $\{A \cup X \mid X \in \mathscr{B}\}$ pronounced? +Back: The set of all $A \cup X$ such that $X \in \mathscr{B}$. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What is the specialization of identity $A \cap \bigcup \mathscr{B} = \bigcup\, \{A \cap X \mid X \in \mathscr{B}\}$? +Back: $A \cap (B \cup C) = (A \cap B) \cup (A \cap C)$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What is the specialization of identity $A \cup \bigcap \mathscr{B} = \bigcap\, \{A \cup X \mid X \in \mathscr{B}\}$? +Back: $A \cup (B \cap C) = (A \cup B) \cap (A \cup C)$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Does $\bigcup\, \{A \cap X \mid X \in \mathscr{B}\}$ get smaller or larger as $\mathscr{B}$ gets larger? +Back: Larger. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Does $\bigcup\, \{A \cap X \mid X \in \mathscr{B}\}$ get smaller or larger as $\mathscr{B}$ gets smaller? +Back: Smaller. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Does $\bigcap\, \{A \cup X \mid X \in \mathscr{B}\}$ get smaller or larger as $\mathscr{B} \neq \varnothing$ gets larger? +Back: Smaller. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Does $\bigcap\, \{A \cup X \mid X \in \mathscr{B}\}$ get smaller or larger as $\mathscr{B} \neq \varnothing$ gets smaller? +Back: Larger. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + ### De Morgan's Laws For any sets $A$, $B$, and $C$, $$\begin{align*} C - (A \cup B) & = (C - A) \cap (C - B) \\ C - (A \cap B) & = (C - A) \cup (C - B) \end{align*}$$ @@ -188,6 +300,226 @@ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Pre END%% +More generally, for any sets $C$ and $\mathscr{A} \neq \varnothing$, $$\begin{align*} C - \bigcup \mathscr{A} & = \bigcap\, \{C - X \mid X \in \mathscr{A}\} \\ C - \bigcap \mathscr{A} & = \bigcup\, \{C - X \mid X \in \mathscr{A}\} \end{align*}$$ + +%%ANKI +Basic +What is the generalization of identity $C - (A \cup B) = (C - A) \cap (C - B)$? +Back: $C - \bigcup \mathscr{A} = \bigcap\, \{C - X \mid X \in \mathscr{A}\}$ for $\mathscr{A} \neq \varnothing$. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What is the generalization of identity $C - (A \cap B) = (C - A) \cup (C - B)$? +Back: $C - \bigcap \mathscr{A} = \bigcup\, \{C - X \mid X \in \mathscr{A}\}$ for $\mathscr{A} \neq \varnothing$. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Cloze +For $\mathscr{A} \neq \varnothing$, De Morgan's law states that {$C - \bigcap \mathscr{A}$} $=$ {$\bigcup\, \{C - X \mid X \in \mathscr{A}\}$}. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What is the specialization of identity $C - \bigcup \mathscr{A} = \bigcap\, \{C - X \mid X \in \mathscr{A}\}$? +Back: $C - (A \cup B) = (C - A) \cap (C - B)$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What is the specialization of identity $C - \bigcap \mathscr{A} = \bigcup\, \{C - X \mid X \in \mathscr{A}\}$? +Back: $C - (A \cap B) = (C - A) \cup (C - B)$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Which law of the algebra of sets is represented by e.g. $C - (A \cup B) = (C - A) \cap (C - B)$? +Back: De Morgan's Law. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Cloze +For $\mathscr{A} \neq \varnothing$, De Morgan's law states that {$C - \bigcup \mathscr{A}$} $=$ {$\bigcap\, \{C - X \mid X \in \mathscr{A}\}$}. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Why does identity $C - \bigcup \mathscr{A} = \bigcap\, \{C - X \mid X \in \mathscr{A}\}$ fail when $\mathscr{A} = \varnothing$? +Back: The RHS evaluates to class $\bigcap \varnothing$. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Why does identity $C - \bigcap \mathscr{A} = \bigcup\, \{C - X \mid X \in \mathscr{A}\}$ fail when $\mathscr{A} = \varnothing$? +Back: $\bigcap \mathscr{A}$ is undefined. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Does $\bigcap\, \{C - X \mid X \in \mathscr{A}\}$ get smaller or larger as $\mathscr{A} \neq \varnothing$ gets larger? +Back: Smaller. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Does $\bigcap\, \{C - X \mid X \in \mathscr{A}\}$ get smaller or larger as $\mathscr{A} \neq \varnothing$ gets smaller? +Back: Larger. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Does $\bigcup\, \{C - X \mid X \in \mathscr{A}\}$ get smaller or larger as $\mathscr{A} \neq \varnothing$ gets larger? +Back: Larger. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Does $\bigcup\, \{C - X \mid X \in \mathscr{A}\}$ get smaller or larger as $\mathscr{A} \neq \varnothing$ gets smaller? +Back: Smaller. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). +END%% + +### Monotonicity + +Let $A$, $B$, and $C$ be arbitrary sets. Then + +* $A \subseteq B \Rightarrow A \cup C \subseteq B \cup C$, +* $A \subseteq B \Rightarrow A \cap C \subseteq B \cap C$, +* $A \subseteq B \Rightarrow \bigcup A \subseteq \bigcup B$ + +%%ANKI +Basic +What kind of propositional logical statement are the monotonicity properties of $\subseteq$? +Back: An implication. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What is the shared antecedent of the monotonicity properties of $\subseteq$? +Back: $A \subseteq B$ for some sets $A$ and $B$. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Given sets $A$, $B$, and $C$, state the monotonicity property of $\subseteq$ related to the $\cup$ operator. +Back: $A \subseteq B \Rightarrow A \cup C \subseteq B \cup C$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Given sets $A$, $B$, and $C$, state the monotonicity property of $\subseteq$ related to the $\cap$ operator. +Back: $A \subseteq B \Rightarrow A \cap C \subseteq B \cap C$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Given sets $A$ and $B$, state the monotonicity property of $\subseteq$ related to the $\bigcup$ operator. +Back: $A \subseteq B \Rightarrow \bigcup A \subseteq \bigcup B$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Why are the monotonicity properties of $\subseteq$ named the way they are? +Back: The ordering of operands in the antecedent are preserved in the consequent. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +### Antimonotonicity + +Let $A$, $B$, and $C$ be arbitrary sets. Then + +* $A \subseteq B \Rightarrow C - B \subseteq C - A$, +* $\varnothing \neq A \subseteq B \Rightarrow \bigcap B \subseteq \bigcap A$ + +%%ANKI +Basic +What kind of propositional logical statement are the antimonotonicity properties of $\subseteq$? +Back: An implication. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What is the shared antecedent of the antimonotonicity properties of $\subseteq$? +Back: N/A. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Cloze +{1:Monotonicity} of $\subseteq$ is to {2:$\bigcup$} whereas {2:antimonotonicity} of $\subseteq$ is to {1:$\bigcap$}. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Why are the antimonotonicity properties of $\subseteq$ named the way they are? +Back: The ordering of operands in the antecedent are reversed in the consequent. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Given sets $A$ and $B$, state the antimonotonicity property of $\subseteq$ related to the $\bigcap$ operator. +Back: $\varnothing \neq A \subseteq B \Rightarrow \bigcap B \subseteq \bigcap A$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Given sets $A$, $B$, and $C$, state the antimonotonicity property of $\subseteq$ related to the $-$ operator. +Back: $A \subseteq B \Rightarrow C - B \subseteq C - A$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Why do we need the empty set check in $\varnothing \neq A \subseteq B \Rightarrow \bigcap B \subseteq \bigcap A$? +Back: $\bigcap A$ is not a set. +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/algorithms/order-growth.md b/notes/algorithms/order-growth.md index 4446bc2..8297313 100644 --- a/notes/algorithms/order-growth.md +++ b/notes/algorithms/order-growth.md @@ -13,8 +13,8 @@ The **running time** of an algorithm is usually considered as a function of its %%ANKI Basic -How is the running time of a program measured as a function? -Back: As a function of its input size. +What is the input of a function used to measure a program's running time? +Back: The size of the program's input. Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). END%% diff --git a/notes/c17/strings.md b/notes/c17/strings.md index b349fc4..b507c66 100644 --- a/notes/c17/strings.md +++ b/notes/c17/strings.md @@ -74,7 +74,7 @@ END%% %%ANKI Cloze -The {`width` and `precision`} fields are output related whereas the {`length`} field is input related. +The {1:`width`} and {1:`precision`} fields are output related whereas the {2:`length`} field is input related. 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 @@ -90,7 +90,7 @@ END%% %%ANKI Cloze -The {`-`} flag {left-aligns the output}. +The {`-`} flag {left-aligns} the output. 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/git/merge-conflicts.md b/notes/git/merge-conflicts.md index 9e78f59..e342c60 100644 --- a/notes/git/merge-conflicts.md +++ b/notes/git/merge-conflicts.md @@ -69,7 +69,7 @@ END%% %%ANKI Basic In a `git merge`, what changes are between `=======` and `<<<<<<<`? -Back: The changes present on the branch being merged into `HEAD`. +Back: N/A. Reference: Scott Chacon, *Pro Git*, Second edition, The Expert’s Voice in Software Development (New York, NY: Apress, 2014). END%% diff --git a/notes/hashing/index.md b/notes/hashing/index.md index b097cac..b7793fd 100644 --- a/notes/hashing/index.md +++ b/notes/hashing/index.md @@ -13,7 +13,7 @@ A **hash table** `T[0:m-1]` uses a **hash function** to map a universe of keys i %%ANKI Basic With respect to hashing, what does the "universe" of keys refer to? -Back: Every potential key that may be inserted into the underlying dictionary. +Back: Every potential key that may be provided to the hash function. Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). END%% diff --git a/notes/logic/equality.md b/notes/logic/equality.md new file mode 100644 index 0000000..05450e9 --- /dev/null +++ b/notes/logic/equality.md @@ -0,0 +1,15 @@ +--- +title: Equality +TARGET DECK: Obsidian::STEM +FILE TAGS: equality +tags: + - equality +--- + +## Overview + + + +## Bibliography + +* Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). \ No newline at end of file diff --git a/notes/programming/lambda-calculus.md b/notes/programming/lambda-calculus.md index 16c05e7..9b2fb6e 100644 --- a/notes/programming/lambda-calculus.md +++ b/notes/programming/lambda-calculus.md @@ -243,6 +243,53 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi END%% +### Syntactic Identity + +**Syntactic identity** of terms is denoted by "$\equiv$". + +%%ANKI +Basic +What does it mean for two terms to be syntactically identical? +Back: The terms are written out using the exact same sequence of characters. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +What form of Lean equality corresponds to $\lambda$-calculus's $\equiv$ operator? +Back: Syntactic equality. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). +Tags: lean + +END%% + +%%ANKI +Basic +How does Hindley et al. denote syntactic identity of $\lambda$-terms $M$ and $N$? +Back: $M \equiv N$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +What syntactic identities are assumed when $MN \equiv PQ$? +Back: $M \equiv P$ and $N \equiv Q$. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +What syntactic identities are assumed when $\lambda x. M \equiv \lambda y. P$? +Back: $x \equiv y$ and $M \equiv P$. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +### Length + The length of a $\lambda$-term (denoted $lgh$) is equal to the number of atoms in the term: * $lgh(a) = 1$ for all atoms $a$; @@ -320,6 +367,8 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi END%% +### Occurrence + For $\lambda$-terms $P$ and $Q$, the relation **$P$ occurs in $Q$** is defined by induction on $Q$ as: * $P$ occurs in $P$; @@ -437,6 +486,8 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi END%% +### Free and Bound Variables + An occurrence of a variable $x$ in a term $P$ is called * **bound** if it is in the scope of a $\lambda x$ in $P$; @@ -574,7 +625,7 @@ END%% %%ANKI Basic -Which specific occurrences are bpund and binding in $\lambda x. x(\lambda y. yz)$? +Which specific occurrences are bound and binding in $\lambda x. x(\lambda y. yz)$? Back: The first $x$ and the first $y$. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). @@ -596,7 +647,7 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi END%% -## Substitution +### Substitution For any $M$, $N$, and $x$, define $[N/x]M$ to be the result of substituting $N$ for every free occurrence of $x$ in $M$, and changing bound variables to avoid clashes. @@ -634,9 +685,9 @@ END%% %%ANKI Cloze -$[N/x]M$ is the result of substituting {$N$} for every free occurrence of {$x$} in {$M$}. +$[N/x]M$ is the result of substituting {1:$N$} for every free occurrence of {1:$x$} in {1:$M$}. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). - + END%% %%ANKI @@ -656,7 +707,7 @@ END%% %%ANKI Basic -What is the result of $[N/x]a$, for some atom $a \neq x$? +What is the result of $[N/x]a$, for some atom $a \not\equiv x$? Back: $a$ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). @@ -664,7 +715,7 @@ END%% %%ANKI Basic -What is the result of $[N/x]a$, for some atom $a = x$? +What is the result of $[N/x]a$, for some atom $a \equiv x$? Back: $N$ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). diff --git a/notes/programming/lean.md b/notes/programming/lean.md new file mode 100644 index 0000000..06383e5 --- /dev/null +++ b/notes/programming/lean.md @@ -0,0 +1,9 @@ +--- +title: Lean +TARGET DECK: Obsidian::STEM +FILE TAGS: lean +tags: + - lean +--- + +## Overview \ No newline at end of file diff --git a/notes/programming/pred-trans.md b/notes/programming/pred-trans.md index cd57519..a6a21e1 100644 --- a/notes/programming/pred-trans.md +++ b/notes/programming/pred-trans.md @@ -563,14 +563,14 @@ END%% %%ANKI Basic *Why* can't the $abort$ command be executed? -Back: Because it terminates in state $F$ which is impossible. +Back: By definition it executes in state $F$ which is impossible. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. END%% %%ANKI Basic -Which command does Gries introduce as the only whose predicate transformer is "constant"? +Which command does Gries introduce as the only "constant" predicate transformer? Back: $abort$ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. @@ -578,15 +578,15 @@ END%% %%ANKI Basic -*Why* is $abort$ considered the only "constant" predicate transformer? -Back: The Law of the Excluded Miracle ensures $wp(S, F) = F$ for any other commands $S$. +How do we prove that $abort$ is the only "constant" predicate transformer? +Back: For any command $S$, the Law of the Excluded Miracle proves $wp(S, F) = F$. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. END%% %%ANKI Basic -Consider $makeTrue$ defined as $wp(makeTrue, R) = T$ for all predicates $R$. What's wrong? +Suppose $makeTrue$ is defined as $wp(makeTrue, R) = T$ for all predicates $R$. What's wrong? Back: If $R = F$, $makeTrue$ violates the Law of the Excluded Miracle. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. diff --git a/notes/set/classes.md b/notes/set/classes.md index f724731..9984096 100644 --- a/notes/set/classes.md +++ b/notes/set/classes.md @@ -305,7 +305,7 @@ END%% %%ANKI Basic Let $A$ be a set. What does $\{x \in A \mid x \not\in x\}$ evaluate to? -Back: $A$. +Back: $A$ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). END%% diff --git a/notes/set/index.md b/notes/set/index.md index f9e3bdd..a149916 100644 --- a/notes/set/index.md +++ b/notes/set/index.md @@ -8,6 +8,30 @@ tags: ## Overview +%%ANKI +Basic +What are the two primitive notions of set theory? +Back: Sets and membership. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +How does Enderton describe a primitive notion? +Back: An undefined concept other concepts are defined with. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Axioms can be thought of as doing what to primitive notions? +Back: Divulging partial information about their meaning. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + %%ANKI Basic How does Knuth define a *dynamic* set? @@ -223,6 +247,14 @@ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Pre END%% +%%ANKI +Basic +What axiom is used to prove two sets are equal to one another? +Back: Extensionality. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + ## Empty Set Axiom There exists a set having no members: $$\exists B, \forall x, x \not\in B$$ @@ -747,7 +779,7 @@ END%% %%ANKI Basic *Why* does $\bigcap \varnothing$ present a problem? -Back: Every set $x$ is a member of every member of $\varnothing$ (vacuously). +Back: Every set is a member of every member of $\varnothing$ (vacuously). Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). END%% @@ -777,6 +809,30 @@ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Pre END%% +%%ANKI +Basic +The "subset axioms" are more accurately classified as what? +Back: An axiom schema. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What is an axiom schema? +Back: An infinite bundle of axioms. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Which of the set theory axioms are more accurately described as an axiom schema? +Back: The subset axioms. +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).