diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index 5cbd355..3435297 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -68,11 +68,14 @@ "bash/index.md": "3b5296277f095acdf16655adcdf524af", "bash/shebang.md": "ad178efeb4a05190b80b5df108c175c7", "bash/robustness.md": "de97cd77aae047b5eea27440b43c9c42", - "journal/2024-02-01.md": "f4cc061bfc8e41ce15ae9a354c65ffe9", + "journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb", "journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970", "bash/quoting.md": "b1d8869a91001f8b22f0cdc54d806f61", "nix/callPackage.md": "5ef6bc5d1a549c55d43ebb4d48c64427", - "nix/index.md": "dd5ddd19e95d9bdbe020c68974d77a33" + "nix/index.md": "dd5ddd19e95d9bdbe020c68974d77a33", + "logic/propositional.md": "2e79b758dd161cc377f18cd1fa845285", + "logic/index.md": "d41d8cd98f00b204e9800998ecf8427e", + "journal/2024-02-03.md": "1359532c63e14251da04181fb0873d66" }, "fields_dict": { "Basic": [ 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