From c293adba2863a1e525fc4cd31118e77a58838ebd Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sat, 3 Feb 2024 14:15:12 -0700 Subject: [PATCH] Add cards on propositional logic. --- .../plugins/obsidian-to-anki-plugin/data.json | 5 +- notes/logic/index.md | 0 notes/logic/propositional.md | 305 ++++++++++++++++++ 3 files changed, 309 insertions(+), 1 deletion(-) create mode 100644 notes/logic/index.md create 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 de477aa..44136fd 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -78,6 +78,9 @@ "algorithms/sorting/index.md": "cd189e1a2cf32b5656b16aaf9f488874", "algorithms/sorting/insertion-sort.md": "c78c9983f87cdc4198f82803d418967f", "algorithms/index.md": "1583c07edea4736db27c38fe2b6c4c31" + "logic/propositional.md": "2e79b758dd161cc377f18cd1fa845285", + "logic/index.md": "d41d8cd98f00b204e9800998ecf8427e", + "journal/2024-02-03.md": "1359532c63e14251da04181fb0873d66" }, "fields_dict": { "Basic": [ @@ -124,4 +127,4 @@ "Reference" ] } -} \ No newline at end of file +} diff --git a/notes/logic/index.md b/notes/logic/index.md new file mode 100644 index 0000000..e69de29 diff --git a/notes/logic/propositional.md b/notes/logic/propositional.md new file mode 100644 index 0000000..31dbf8c --- /dev/null +++ b/notes/logic/propositional.md @@ -0,0 +1,305 @@ +--- +title: Propositional Logic +TARGET DECK: Obsidian::STEM +FILE TAGS: logic::0-order +tags: + - logic + - 0-order +--- + +## Overview + +%%ANKI +Basic +Who is the author of "The Science of Programming"? +Back: David Gries +Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What are the constant propositions? +Back: $T$ and $F$ +Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What are the five 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 +Cloze +Gries replaces logical operator {$\Leftrightarrow$} in favor of {$=$}. +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%% + +%%ANKI +Basic +What Lean theorem justifies Gries choice of $=$ over $\Leftrightarrow$? +Back: `propext` +Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +Tags: lean + +END%% + +%%ANKI +Basic +What name is given to $\land$ operands? +Back: Conjuncts +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 $\lor$ operands? +Back: Disjuncts +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 $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 +What does the evaluation model of propositional logic refer to? +Back: An interpretation of propositional logic that associates values to identifiers. +Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Evaluation model. 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 is necessary to determine if a proposition is well-defined? +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 +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 +Evaluation model. What does it mean for a proposition to be a tautology? +Back: A proposition is true in every state it is well-defined in. +Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What C operator corresponds to $\neg$? +Back: `!` +Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +Tags: c + +END%% + +%%ANKI +Basic +What C operator corresponds to $\land$? +Back: There isn't one. +Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +Tags: c + +END%% + +%%ANKI +Basic +What C operator corresponds to $\lor$? +Back: There isn't one. +Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +Tags: c + +END%% + +%%ANKI +Basic +What C operator corresponds to $\Rightarrow$? +Back: There isn't one. +Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +Tags: c + +END%% + +%%ANKI +Basic +What C operator corresponds to $\Leftrightarrow$? +Back: `=` +Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +Tags: c + +END%% + +%%ANKI +Basic +Evaluation model. 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 +Evaluation model. 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 +Evaluation model. 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 +Evaluation model. What is sloppy about phrase "the states in $b \lor \neg c$"? +Back: $b \lor \neg c$ is not a set. +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 +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 +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 +Evaluation model. 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 +How is $\Rightarrow$ written in terms of other logical operators? +Back: $p \Rightarrow q$ is equivalent to $\neg p \lor q$. +Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $\Leftrightarrow$ written in terms of other logical operators? +Back: $p \Leftrightarrow q$ is equivalent to $(p \Rightarrow q) \land (q \Rightarrow p)$. +Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +## References + +* Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. +* Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. \ No newline at end of file