diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index 7ed6084..1594104 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -251,7 +251,7 @@ "combinatorics/inclusion-exclusion.md": "c27b49ee03cc5ee854d0e8bd12a1d505", "_journal/2024-02-21.md": "b9d944ecebe625da5dd72aeea6a916a2", "_journal/2024-02/2024-02-20.md": "af2ef10727726200c4defe2eafc7d841", - "algebra/radices.md": "56919586bfbbb96c53ac12924bdb04b1", + "algebra/radices.md": "81c887836b38a8584234a74d612aef12", "_journal/2024-02-22.md": "e01f1d4bd2f7ac2a667cdfd500885a2a", "_journal/2024-02/2024-02-21.md": "f423137ae550eb958378750d1f5e98c7", "_journal/2024-02-23.md": "219ce9ad15a8733edd476c97628b71fd", @@ -325,7 +325,7 @@ "_journal/2024-03/2024-03-17.md": "23f9672f5c93a6de52099b1b86834e8b", "set/directed-graph.md": "b4b8ad1be634a0a808af125fe8577a53", "set/index.md": "6670c57f29c84eef8dcfff7a8901befe", - "set/graphs.md": "1a0c09f643829dae6a101b96de31eb40", + "set/graphs.md": "f0cd201673f2a999321dda6c726e8734", "_journal/2024-03-19.md": "a0807691819725bf44c0262405e97cbb", "_journal/2024-03/2024-03-18.md": "63c3c843fc6cfc2cd289ac8b7b108391", "awk/variables.md": "e40a20545358228319f789243d8b9f77", @@ -485,7 +485,7 @@ "_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": "843b092a980133ba7bd61b1750a6df08", + "algebra/set.md": "fe0121964ae8c788a2afb6031b4086d9", "algebra/boolean.md": "ee41e624f4d3d3aca00020d9a9ae42c8", "git/merge-conflicts.md": "761ad6137ec51d3877f7d5b3615ca5cb", "_journal/2024-05-28.md": "0f6aeb5ec126560acdc2d8c5c6570337", @@ -510,14 +510,14 @@ "_journal/2024-06/2024-06-04.md": "52b28035b9c91c9b14cef1154c1a0fa1", "_journal/2024-06-06.md": "3f9109925dea304e7172df39922cc95a", "_journal/2024-06/2024-06-05.md": "b06a0fa567bd81e3b593f7e1838f9de1", - "set/relations.md": "07d593f334d656d1deb3d11055a21c37", + "set/relations.md": "29f9b8220cc147ae638e4832c0e82919", "_journal/2024-06-07.md": "795be41cc3c9c0f27361696d237604a2", "_journal/2024-06/2024-06-06.md": "db3407dcc86fa759b061246ec9fbd381", "_journal/2024-06-08.md": "b20d39dab30b4e12559a831ab8d2f9b8", "_journal/2024-06/2024-06-07.md": "c6bfc4c1e5913d23ea7828a23340e7d3", "lambda-calculus/alpha-conversion.md": "007828faf9b4ace5bd30b87a36a90dcf", "lambda-calculus/index.md": "64efe9e4f6036d3f5b4ec0dc8cd3e7b9", - "x86-64/instructions/condition-codes.md": "67d325298b9b605a59c4855d0c9f2043", + "x86-64/instructions/condition-codes.md": "1f59f0b81b2e15582b855d96d1d377da", "x86-64/instructions/logical.md": "818428b9ef84753920dc61e5c2de9199", "x86-64/instructions/arithmetic.md": "271218d855e7291f119f96e91f582738", "x86-64/instructions/access.md": "c19bc3392cf493fcc9becf46c818cc50", @@ -536,7 +536,7 @@ "_journal/2024-06/2024-06-12.md": "f82dfa74d0def8c3179d3d076f94558e", "_journal/2024-06-14.md": "5d12bc272238ac985a1d35d3d63ea307", "_journal/2024-06/2024-06-13.md": "e2722a00585d94794a089e8035e05728", - "set/functions.md": "5740a88e79df5fcd8096485954c0a26a", + "set/functions.md": "b739ef156a4420a141f76dbcecaff8cf", "_journal/2024-06-15.md": "92cb8dc5c98e10832fb70c0e3ab3cec4", "_journal/2024-06/2024-06-14.md": "5d12bc272238ac985a1d35d3d63ea307", "lambda-calculus/beta-reduction.md": "6c9a9f4983b0974e0184acaee7c27a22", @@ -620,18 +620,21 @@ "_journal/2024-07/2024-07-18.md": "237918b58424435959cbc949d01e7932", "_journal/2024-07-20.md": "d8685729effc374e4ece1e618c2fdad3", "_journal/2024-07/2024-07-19.md": "e9fe4569f88e1ba9393292bcf092edfc", - "_journal/2024-07-21.md": "dd5dd93f119f69571a78e027fab7da5d", + "_journal/2024-07-21.md": "62c2651999371dd9ab10d964dac3d0f8", "_journal/2024-07/2024-07-20.md": "d8685729effc374e4ece1e618c2fdad3", "logic/classical/index.md": "ee0a4b2bfcfa2cab0880db449cb62df1", "logic/classical/truth-tables.md": "b739e2824a4a5c26ac446e7c15ce02aa", "formal-system/proof-system/index.md": "1c95481cbb2e79ae27f6be1869599657", - "formal-system/proof-system/equiv-trans.md": "00f6d209a448ab25acaa3bff7fd5c6b6", + "formal-system/proof-system/equiv-trans.md": "4d5e9236944c3ea99f484bfcb14292d0", "formal-system/logical-system/index.md": "708bb1547e7343c236068c18da3f5dc0", "formal-system/logical-system/pred-logic.md": "2524ccc09561bc219dab3f32010a0161", "formal-system/logical-system/prop-logic.md": "b61ce051795d5a951c763b928ec5cea8", "formal-system/index.md": "3d31c99bffdcb05de9f2e32ac6319952", "programming/short-circuit.md": "c256ced42dc3b493aff5a356e5383b6e", - "formal-system/abstract-rewriting.md": "8424314a627851c5b94be6163f64ba30" + "formal-system/abstract-rewriting.md": "8424314a627851c5b94be6163f64ba30", + "_journal/2024-07-22.md": "dbbf1666c0ed939ce0ce339d41231b04", + "_journal/2024-07/2024-07-21.md": "62c2651999371dd9ab10d964dac3d0f8", + "formal-system/proof-system/natural-deduction.md": "c910adfd2b6d162936db02d2c7f4563e" }, "fields_dict": { "Basic": [ diff --git a/notes/_journal/2024-07-22.md b/notes/_journal/2024-07-22.md new file mode 100644 index 0000000..b33a593 --- /dev/null +++ b/notes/_journal/2024-07-22.md @@ -0,0 +1,11 @@ +--- +title: "2024-07-22" +--- + +- [x] Anki Flashcards +- [x] KoL +- [x] OGS +- [ ] Sheet Music (10 min.) +- [ ] Korean (Read 1 Story) + +* Beginning notes on [[natural-deduction|natural deduction]]. \ No newline at end of file diff --git a/notes/_journal/2024-07-21.md b/notes/_journal/2024-07/2024-07-21.md similarity index 71% rename from notes/_journal/2024-07-21.md rename to notes/_journal/2024-07/2024-07-21.md index 5001192..81e5ac0 100644 --- a/notes/_journal/2024-07-21.md +++ b/notes/_journal/2024-07/2024-07-21.md @@ -2,8 +2,8 @@ title: "2024-07-21" --- -- [ ] Anki Flashcards -- [ ] KoL +- [x] Anki Flashcards +- [x] KoL - [ ] OGS - [ ] Sheet Music (10 min.) - [ ] Korean (Read 1 Story) diff --git a/notes/algebra/radices.md b/notes/algebra/radices.md index 8c4652a..2888031 100644 --- a/notes/algebra/radices.md +++ b/notes/algebra/radices.md @@ -241,7 +241,7 @@ END%% %%ANKI Basic How is the *remainder* of e.g. `158 / 16` managed in decimal to hex conversion? -Back: As the next least significant bit of our conversion. +Back: Assuming big-endian, as the next most significant bit of our conversion. Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. Tags: binary::hex diff --git a/notes/algebra/set.md b/notes/algebra/set.md index ec6699b..bd18db5 100644 --- a/notes/algebra/set.md +++ b/notes/algebra/set.md @@ -231,36 +231,6 @@ END%% ## Laws -The algebra of sets obey laws reminiscent (but not exactly) of the algebra of real numbers. - -%%ANKI -Cloze -{$\cup$} is to algebra of sets whereas {$+$} is to algebra of real numbers. -Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). - -END%% - -%%ANKI -Cloze -{$\cap$} is to algebra of sets whereas {$\cdot$} is to algebra of real numbers. -Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). - -END%% - -%%ANKI -Cloze -{$-$} is to algebra of sets whereas {$-$} is to algebra of real numbers. -Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). - -END%% - -%%ANKI -Cloze -{$\subseteq$} is to algebra of sets whereas {$\leq$} is to algebra of real numbers. -Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). - -END%% - ### Commutative Laws For any sets $A$ and $B$, $$\begin{align*} A \cup B & = B \cup A \\ A \cap B & = B \cap A \end{align*}$$ diff --git a/notes/formal-system/proof-system/equiv-trans.md b/notes/formal-system/proof-system/equiv-trans.md index e2b8130..aa00236 100644 --- a/notes/formal-system/proof-system/equiv-trans.md +++ b/notes/formal-system/proof-system/equiv-trans.md @@ -10,7 +10,7 @@ tags: ## Overview -**Equivalence-transformation** is a [[formal-system/index|formal-system]] based on classical truth-functional [[pred-logic|predicate logic]] developed by David Gries. It is the foundation upon which [[pred-trans|predicate transformers]] are based. +**Equivalence-transformation** is a proof system used alongside classical truth-functional [[pred-logic|predicate logic]]. It is the foundation upon which [[pred-trans|predicate transformers]] are based. %%ANKI Basic @@ -140,6 +140,7 @@ END%% Basic What is the commutative law of e.g. $\land$? Back: $E1 \land E2 = E2 \land E1$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. END%% diff --git a/notes/formal-system/proof-system/natural-deduction.md b/notes/formal-system/proof-system/natural-deduction.md new file mode 100644 index 0000000..168fc99 --- /dev/null +++ b/notes/formal-system/proof-system/natural-deduction.md @@ -0,0 +1,179 @@ +--- +title: Natural Deduction +TARGET DECK: Obsidian::STEM +FILE TAGS: formal-system::natural-deduction +tags: + - logic + - natural-deduction + - programming +--- + +## Overview + +Natural deduction is a proof system typically used alongside classical truth-functional [[prop-logic|propositional]] and [[pred-logic|predicate]] logic. It is meant to mimic the patterns of reasoning that one might "naturally" make when forming arguments in plain English. + +%%ANKI +Basic +Why is natural deduction named the way it is? +Back: It is mean to mimic the patterns of reasoning one might "naturally" make when forming arguments in plain English. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +## Axioms + +Natural deduction is interesting in that it has no axioms. + +%%ANKI +Basic +How many axioms does natural deduction include? +Back: $0$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +## Inference Rules + +Scoped to just propositional logic, there are 10 inference rules corresponding to an "introduction" and "elimination" of each propositional logic operator. When extending to predicate logic, we also include an introduction and elimination rule for both the [[pred-logic#Existentials|existential]] and [[pred-logic#Universals|universal]] quantifers. + +%%ANKI +Basic +With respect to propositional logic, how many inference rules does natural deduction include? +Back: $10$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +With respect to predicate logic, how many inference rules does natural deduction include? +Back: $14$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How are natural deduction's inference rules categorized into two? +Back: As introduction and elimination rules. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +With respect to propositional logic, how are natural deduction's inference rules categorized into five? +Back: As an introduction and elimination rule per propositional logic operators. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +### Conjunction + +For propositions $E_1, \ldots, E_n$, $$\land{\text{-}}I{:} \quad \begin{array}{c} E_1, \ldots, E_n \\ \hline E_1 \land \cdots \land E_n \end{array}$$ +and $$\land{\text{-}}E{:} \quad \begin{array}{c} E_1 \land \cdots \land E_n \\ \hline E_i \end{array}$$ + +%%ANKI +Basic +In natural deduction, how is conjunction introduction denoted? +Back: As $\land{\text{-}}I$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +In natural deduction, how is conjunction elimination denoted? +Back: As $\land{\text{-}}E$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $\land{\text{-}}I$ expressed in schematic notation? +Back: $$\begin{array}{c} E_1, \ldots, E_n \\ \hline E_1 \land \cdots \land E_n \end{array}$$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $\land{\text{-}}E$ expressed in schematic notation? +Back: $$\begin{array}{c} E_1 \land \cdots \land E_n \\ \hline E_i \end{array}$$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Which natural deduction inference rule is used in the following? $$\begin{array}{c} P, Q, R \\ \hline P \land R \end{array}$$ +Back: $\land{\text{-}}I$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Which natural deduction inference rule is used in the following? $$\begin{array}{c} P \land Q \\ \hline P \end{array}$$ +Back: $\land{\text{-}}E$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +### Disjunction + +For propositions $E_1, \ldots, E_n$, $$\lor{\text{-}}I{:} \quad \begin{array}{c} E_i \\ \hline E_1 \lor \cdots \lor E_n \end{array}$$ +and $$\lor{\text{-}}E{:} \quad \begin{array}{c} E_1 \lor \cdots \lor E_n, E_1 \Rightarrow E, \ldots, E_n \Rightarrow E \\ \hline E \end{array}$$ + +%%ANKI +Basic +In natural deduction, how is disjunction introduction denoted? +Back: As $\lor{\text{-}}I$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +In natural deduction, how is disjunction elimination denoted?? +Back: As $\lor{\text{-}}E$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $\lor{\text{-}}I$ expressed in schematic notation? +Back: $$\lor{\text{-}}I{:} \quad \begin{array}{c} E_i \\ \hline E_1 \lor \cdots \lor E_n \end{array}$$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $\lor{\text{-}}E$ expressed in schematic notation? +Back: $$\lor{\text{-}}E{:} \quad \begin{array}{c} E_1 \lor \cdots \lor E_n, E_1 \Rightarrow E, \ldots, E_n \Rightarrow E \\ \hline E \end{array}$$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Which natural deduction inference rule is used in the following? $$\begin{array}{c} P, Q \\ \hline R \lor P \end{array}$$ +Back: $\lor{\text{-}}I$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Which natural deduction inference rule is used in the following? $$\begin{array}{c} P \lor Q, P \Rightarrow R, Q \Rightarrow R \\ \hline P \end{array}$$ +Back: $\lor{\text{-}}E$ +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. diff --git a/notes/set/functions.md b/notes/set/functions.md index 30bd417..490ecd6 100644 --- a/notes/set/functions.md +++ b/notes/set/functions.md @@ -1673,8 +1673,8 @@ END%% %%ANKI Basic -Let $F \colon A \rightarrow B$. What does $\mathop{\text{coim}}F$ refer to? -Back: The coimage of $F$. +Let $F \colon A \rightarrow B$. Term "$\mathop{\text{coim}}F$" is shorthand for what? +Back: The **coim**age of $F$. Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). END%% @@ -1682,14 +1682,14 @@ END%% %%ANKI Basic How is the coimage of function $F \colon A \rightarrow B$ defined? -Back: As $A / {\sim}$ where $x \sim y \Leftrightarrow F(x) = F(y)$. +Back: As $A / \mathop{\text{ker}}(F)$. Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). END%% %%ANKI Basic -Let $F \colon A \rightarrow B$. What specific name does a member of $\mathop{\text{coim}}F$ go by? +Let $F \colon A \rightarrow B$. What term refers to a member of $\mathop{\text{coim}}F$? Back: A fiber. Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). @@ -1714,7 +1714,7 @@ END%% %%ANKI Basic Let $F \colon A \rightarrow B$. How is $\mathop{\text{coim}}F$ denoted as a quotient set? -Back: As $A / {\sim}$ where $x \sim y \Leftrightarrow F(x) = F(y)$. +Back: As $A / \mathop{\text{ker}}(F)$ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). END%% @@ -1747,7 +1747,7 @@ END%% %%ANKI Basic -Consider factoring $F \colon A \rightarrow B$ by its kernel $\sim$. What name does $\sim$ go by? +Consider factoring $F \colon A \rightarrow B$ by its kernel $\sim$. What name does $A /{\sim}$ go by? ![[function-kernel.png]] Back: $\mathop{\text{coim}} F$ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). diff --git a/notes/set/graphs.md b/notes/set/graphs.md index ae8da4b..f34ae99 100644 --- a/notes/set/graphs.md +++ b/notes/set/graphs.md @@ -279,7 +279,7 @@ END%% %%ANKI Basic Under what conditions is a multigraph considered a graph? -Back: When the number of edges between any two vertices is $1$. +Back: When the number of edges from any vertex to any other vertex is at most $1$. 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%% diff --git a/notes/set/relations.md b/notes/set/relations.md index c297a96..a0f8e23 100644 --- a/notes/set/relations.md +++ b/notes/set/relations.md @@ -1123,7 +1123,7 @@ END%% %%ANKI Cloze -Let $R$ be an equivalence relation on $A$ and $x \in A$. Then {1:$x$ (modulo $R$)} is an {2:equivalence class} whereas {2:$A$ modulo $R$} is a {1:quotient set}. +Let $R$ be an equivalence relation on $A$ and $x \in A$. Then {1:$x$} (modulo {1:$R$}) is an {2:equivalence class} whereas {2:$A$} modulo {2:$R$} is a {1:quotient set}. Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). END%% diff --git a/notes/x86-64/instructions/condition-codes.md b/notes/x86-64/instructions/condition-codes.md index 9af8eed..19a5d7a 100644 --- a/notes/x86-64/instructions/condition-codes.md +++ b/notes/x86-64/instructions/condition-codes.md @@ -135,7 +135,7 @@ END%% %%ANKI Basic -What is `e` in the `setz` instruction short for? +What is `z` in the `setz` instruction short for? Back: **Z**ero. Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.