Reorganize types of logic and formal systems.
parent
8530fbf45b
commit
6ba651c41b
|
|
@ -164,7 +164,7 @@
|
|||
"journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb",
|
||||
"journal/2024-02-02.md": "a3b222daee8a50bce4cbac699efc7180",
|
||||
"journal/2024-02-03.md": "c6d411f0e2e964270399dd3a99f48382",
|
||||
"logic/index.md": "46cdc7a552900e99a7d2d0140971118c",
|
||||
"logic/index.md": "717099c8fefb416eed7dcf83a2284297",
|
||||
"logic/propositional.md": "1ac07079aff07a7c2cb09daacefbb960",
|
||||
"lua/index.md": "fd3d0b66765f0e9df233e8e02ce33e94",
|
||||
"nix/callPackage.md": "9aeeaa22878434d3c4498cb92cfe230b",
|
||||
|
|
@ -457,7 +457,7 @@
|
|||
"_journal/2024-05-16.md": "580c7ec61ec56be92fa8d6affcf0a5f6",
|
||||
"_journal/2024-05/2024-05-15.md": "4e6a7e6df32e93f0d8a56bc76613d908",
|
||||
"logic/pred-logic.md": "a709cb45e7554ffc578cba0eb1e86e57",
|
||||
"logic/prop-logic.md": "daa927c5eb31813fcf21bcb18ba0f1ec",
|
||||
"logic/prop-logic.md": "e169a413c5f5866d1ea0b7c61e4bedf6",
|
||||
"_journal/2024-05-17.md": "fb880d68077b655ede36d994554f3aba",
|
||||
"_journal/2024-05/2024-05-16.md": "9fdfadc3f9ea6a4418fd0e7066d6b10c",
|
||||
"_journal/2024-05-18.md": "c0b58b28f84b31cea91404f43b0ee40c",
|
||||
|
|
@ -517,7 +517,7 @@
|
|||
"_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": "5524d1c49bb184b336f814194622a0ee",
|
||||
"x86-64/instructions/condition-codes.md": "67d325298b9b605a59c4855d0c9f2043",
|
||||
"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": "b41c04a596a7e711801c32eff9333a3e",
|
||||
"set/functions.md": "5740a88e79df5fcd8096485954c0a26a",
|
||||
"_journal/2024-06-15.md": "92cb8dc5c98e10832fb70c0e3ab3cec4",
|
||||
"_journal/2024-06/2024-06-14.md": "5d12bc272238ac985a1d35d3d63ea307",
|
||||
"lambda-calculus/beta-reduction.md": "6c9a9f4983b0974e0184acaee7c27a22",
|
||||
|
|
@ -613,13 +613,24 @@
|
|||
"_journal/2024-07/2024-07-16.md": "149222eab7a7f58993b8e4dc8a3fb884",
|
||||
"_journal/2024-07-18.md": "a9d26ce938228973f07178a15128a681",
|
||||
"_journal/2024-07/2024-07-17.md": "0c816cd6110bdd14d3eac4e5b82510cf",
|
||||
"ontology/dialetheism.md": "fa71c557744e009a067c68f9650a09b1",
|
||||
"ontology/dialetheism.md": "56dd05b38519f90c5cab93637978b3b3",
|
||||
"abstract-rewriting-systems/index.md": "b7486b7635cb0d8bafc2a2f095af90fb",
|
||||
"abstract-rewriting-systems/normal-form.md": "2fff9a1d85bca0a2941a54b0084a0309",
|
||||
"_journal/2024-07-19.md": "ced9d4c4759468885d85efa0b87b7823",
|
||||
"_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/2024-07-19.md": "e9fe4569f88e1ba9393292bcf092edfc",
|
||||
"_journal/2024-07-21.md": "682ee0ada782dd281d8fd217227e985c",
|
||||
"_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/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"
|
||||
},
|
||||
"fields_dict": {
|
||||
"Basic": [
|
||||
|
|
|
|||
|
|
@ -0,0 +1,11 @@
|
|||
---
|
||||
title: "2024-07-21"
|
||||
---
|
||||
|
||||
- [ ] Anki Flashcards
|
||||
- [ ] KoL
|
||||
- [ ] OGS
|
||||
- [ ] Sheet Music (10 min.)
|
||||
- [ ] Korean (Read 1 Story)
|
||||
|
||||
* Begin classification of [[formal-system/index|formal systems]] under different types of logic.
|
||||
|
|
@ -0,0 +1,279 @@
|
|||
---
|
||||
title: Logic
|
||||
TARGET DECK: Obsidian::STEM
|
||||
FILE TAGS: formal-system
|
||||
tags:
|
||||
- formal-system
|
||||
- logic
|
||||
---
|
||||
|
||||
## Overview
|
||||
|
||||
A **formal system** is an abstract structure and formalization of an axiomatic system used for inferring theorems from axioms by a set of inference rules. It consists of two components: a **formal language** and a **deductive system**.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How are conclusions drawn in deductive reasoning?
|
||||
Back: From valid inferences on a set of premises.
|
||||
Reference: “Deductive Reasoning,” in _Wikipedia_, June 16, 2024, [https://en.wikipedia.org/w/index.php?title=Deductive_reasoning](https://en.wikipedia.org/w/index.php?title=Deductive_reasoning&oldid=1229329170).
|
||||
<!--ID: 1721561534082-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How are conclusions drawn in inductive reasoning?
|
||||
Back: By generalizing from some body of observations.
|
||||
Reference: “Inductive Reasoning,” in _Wikipedia_, May 6, 2024, [https://en.wikipedia.org/w/index.php?title=Inductive_reasoning](https://en.wikipedia.org/w/index.php?title=Inductive_reasoning&oldid=1222455892).
|
||||
<!--ID: 1721561534087-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Do formal systems employ inductive or deductive reasoning?
|
||||
Back: Deductive reasoning.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534091-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Is the study of logic concerned with deductive or inductive reasoning?
|
||||
Back: Deductive reasoning.
|
||||
Reference: “Deductive Reasoning,” in _Wikipedia_, June 16, 2024, [https://en.wikipedia.org/w/index.php?title=Deductive_reasoning](https://en.wikipedia.org/w/index.php?title=Deductive_reasoning&oldid=1229329170).
|
||||
<!--ID: 1721561534094-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of deductive or inductive reasoning can provide "genuinely new information"?
|
||||
Back: Inductive reasoning.
|
||||
Reference: “Deductive Reasoning,” in _Wikipedia_, June 16, 2024, [https://en.wikipedia.org/w/index.php?title=Deductive_reasoning](https://en.wikipedia.org/w/index.php?title=Deductive_reasoning&oldid=1229329170).
|
||||
<!--ID: 1721561534099-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What does it mean for inductive reasoning to provide "genuinely new information"?
|
||||
Back: Information not found in the premises can be produced.
|
||||
Reference: “Deductive Reasoning,” in _Wikipedia_, June 16, 2024, [https://en.wikipedia.org/w/index.php?title=Deductive_reasoning](https://en.wikipedia.org/w/index.php?title=Deductive_reasoning&oldid=1229329170).
|
||||
<!--ID: 1721561534103-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of deductive or inductive reasoning is considered more formal?
|
||||
Back: Deductive reasoning.
|
||||
Reference: “Deductive Reasoning,” in _Wikipedia_, June 16, 2024, [https://en.wikipedia.org/w/index.php?title=Deductive_reasoning](https://en.wikipedia.org/w/index.php?title=Deductive_reasoning&oldid=1229329170).
|
||||
<!--ID: 1721561534107-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What two parts make up a formal system?
|
||||
Back: A formal language and a deductive system.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534111-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of a formal system or a deductive system is defined in terms of the other?
|
||||
Back: The formal system.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534115-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What does a formal system specify that a deductive system does not?
|
||||
Back: A formal language.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534119-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What does a formal system specify that a formal language does not?
|
||||
Back: A deductive system.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534124-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
The term "formal system" can be seen as a portmanteau of what other terms?
|
||||
Back: A **formal** language and a deductive **system**.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534129-->
|
||||
END%%
|
||||
|
||||
A formal language comprises of an **alphabet** and a **formal grammar**. The grammer has associated rules describing how symbols of the alphabet are manipulated to create **well-formed formulas** (WFFs). The **syntax** of a language describes the set of possible expressions that are valid utterances. The **semantics** of a language describe what these valid utterances actually mean.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What two parts make up a formal language?
|
||||
Back: An alphabet and a formal grammer.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534134-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What is the purpose of a formal language's alphabet?
|
||||
Back: It defines the set of valid symbols used in the language.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534138-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What is the purpose of a formal language's grammar?
|
||||
Back: It defines how to construct well-formed formulas from the alphabet.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534142-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What is WFF an acronym for?
|
||||
Back: **W**-ell-**f**ormed **f**ormula.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534147-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Is the following a WFF of propositional logic?
|
||||
Back: $(a \Rightarrow b) \Leftrightarrow c$
|
||||
Back: Yes.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
Tags: formal-system::propositional
|
||||
<!--ID: 1721561534150-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Is the following a WFF of propositional logic?
|
||||
Back: $(a \Rightarrow b( \Leftrightarrow c$
|
||||
Back: No.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
Tags: formal-system::propositional
|
||||
<!--ID: 1721561574169-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Is the following a WFF of propositional logic?
|
||||
Back: $\forall x, x \in A \Rightarrow x = y$
|
||||
Back: No.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
Tags: logic::propositional logic::predicate
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
With respect to formal languages, what is syntax?
|
||||
Back: The set of possible expressions that are valid in the language.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534154-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
With respect to formal languages, what is semantics?
|
||||
Back: What valid expressions of the language mean.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534157-->
|
||||
END%%
|
||||
|
||||
A deductive system can be further subcategorized as either a [[formal-system/proof-system/index|proof system]] or a [[formal-system/logical-system/index|logical system]]. In both cases, the general principle is to define a (possibly empty) set of **axioms** alongside a set of **inference rules** that together can be used to infer **theorems**.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How are deductive systems further subcategorized?
|
||||
Back: As proof systems and logical systems.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534160-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Axioms belong to which of the two parts of a formal system?
|
||||
Back: The deductive system.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534163-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Inference rules belong to which of the two parts of a formal system?
|
||||
Back: The deductive system.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534167-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
An alphabet belong to which of the two parts of a formal system?
|
||||
Back: The formal language.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534170-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
A formal grammar belong to which of the two parts of a formal system?
|
||||
Back: The formal language.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534173-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
A deductive system derives {1:theorems} using {1:inference rules} starting with {1:axioms}.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534176-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
{1:Proof} systems are {2:syntactic} whereas {2:logical} systems are {1:syntactic and semantic}.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534180-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
A {metalanguage} refers to the {language used to talk about a formal system}.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534185-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
An {object language} refers to the {formal language found in a formal system}.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534189-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
In a discussion of propositional logic, what is the metalanguage?
|
||||
Back: English (or whatever natural language is being used).
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534194-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
In a discussion of propositional logic, what is the object language?
|
||||
Back: The formal language of propositional logic.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534200-->
|
||||
END%%
|
||||
|
||||
## Bibliography
|
||||
|
||||
* “Deductive Reasoning,” in _Wikipedia_, June 16, 2024, [https://en.wikipedia.org/w/index.php?title=Deductive_reasoning](https://en.wikipedia.org/w/index.php?title=Deductive_reasoning&oldid=1229329170).
|
||||
* “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
* “Inductive Reasoning,” in _Wikipedia_, May 6, 2024, [https://en.wikipedia.org/w/index.php?title=Inductive_reasoning](https://en.wikipedia.org/w/index.php?title=Inductive_reasoning&oldid=1222455892).
|
||||
|
|
@ -0,0 +1,47 @@
|
|||
---
|
||||
title: Logical Systems
|
||||
TARGET DECK: Obsidian::STEM
|
||||
FILE TAGS: formal-system
|
||||
tags:
|
||||
- formal-system
|
||||
- logic
|
||||
---
|
||||
|
||||
## Overview
|
||||
|
||||
A deductive system found in certain formal systems. Logical systems are syntactic and semantic. The syntax of WFFs found in these systems are interpretable and often defined recursively (e.g. propositional and predicate logic).
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
*Why* do we say formal systems using logical systems are semantic?
|
||||
Back: An interpretation is usually attached to the WFFs of the language.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534248-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
Logical systems are {syntactic} and {semantic}.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534254-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What kind of deductive system is propositional logic usually categorized as?
|
||||
Back: A logical system.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534261-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What kind of deductive system is predicate logic usually categorized as?
|
||||
Back: A logical system.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534266-->
|
||||
END%%
|
||||
|
||||
## Bibliography
|
||||
|
||||
* “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
---
|
||||
title: Predicate Logic
|
||||
TARGET DECK: Obsidian::STEM
|
||||
FILE TAGS: logic::predicate
|
||||
FILE TAGS: formal-system::predicate
|
||||
tags:
|
||||
- logic
|
||||
- predicate
|
||||
|
|
@ -9,7 +9,7 @@ tags:
|
|||
|
||||
## 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]].
|
||||
**Predicate logic** is a logical system 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
|
||||
|
|
@ -70,7 +70,9 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
|
|||
<!--ID: 1707674796766-->
|
||||
END%%
|
||||
|
||||
* **Existential quantification** ($\exists$) asserts the existence of at least one member in a set satisfying a property.
|
||||
### Existentials
|
||||
|
||||
**Existential quantification** ($\exists$) asserts the existence of at least one member in a set satisfying a property.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
|
|
@ -112,7 +114,9 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
|
|||
<!--ID: 1707494819970-->
|
||||
END%%
|
||||
|
||||
* **Universal quantification** ($\forall$) asserts that every member of a set satisfies a property.
|
||||
### Universals
|
||||
|
||||
**Universal quantification** ($\forall$) asserts that every member of a set satisfies a property.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
|
|
@ -167,7 +171,9 @@ Back: $\neg \forall x : S, \neg P(x)$
|
|||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
END%%
|
||||
|
||||
* **Counting quantification** ($\exists^{=k}$ or $\exists^{\geq k}$) asserts that (at least) $k$ (say) members of a set satisfy a property.
|
||||
### Counting
|
||||
|
||||
**Counting quantification** ($\exists^{=k}$ or $\exists^{\geq k}$) asserts that (at least) $k$ (say) members of a set satisfy a property.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
|
|
@ -245,7 +251,7 @@ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Pre
|
|||
<!--ID: 1720386023296-->
|
||||
END%%
|
||||
|
||||
### Identifiers
|
||||
## Identifiers
|
||||
|
||||
Identifiers are said to be **bound** if they are parameters to a quantifier. Identifiers that are not bound are said to be **free**. A first-order logic formula is said to be in **prenex normal form** (PNF) if written in two parts: the first consisting of quantifiers and bound variables (the **prefix**), and the second consisting of no quantifiers (the **matrix**).
|
||||
|
||||
|
|
@ -305,42 +311,6 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
|
|||
<!--ID: 1720665224639-->
|
||||
END%%
|
||||
|
||||
## As 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.
|
||||
<!--ID: 1715898219881-->
|
||||
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.
|
||||
<!--ID: 1715898219890-->
|
||||
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.
|
||||
<!--ID: 1715898219895-->
|
||||
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.
|
||||
<!--ID: 1715898219903-->
|
||||
END%%
|
||||
|
||||
## Bibliography
|
||||
|
||||
* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
|
|
@ -0,0 +1,322 @@
|
|||
---
|
||||
title: Propositional Logic
|
||||
TARGET DECK: Obsidian::STEM
|
||||
FILE TAGS: formal-system::propositional
|
||||
tags:
|
||||
- logic
|
||||
- propositional
|
||||
---
|
||||
|
||||
## Overview
|
||||
|
||||
**Propositional logic** is a logical system derived from negation ($\neg$), conjunction ($\land$), disjunction ($\lor$), implication ($\Rightarrow$), and biconditionals ($\Leftrightarrow$). A **proposition** is a sentence that can be assigned a truth 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.
|
||||
<!--ID: 1715897257085-->
|
||||
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.
|
||||
<!--ID: 1706994861291-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What is a proposition?
|
||||
Back: A declarative sentence that can be assigned 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).
|
||||
<!--ID: 1708199272076-->
|
||||
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).
|
||||
<!--ID: 1708199272083-->
|
||||
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).
|
||||
<!--ID: 1708199272087-->
|
||||
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).
|
||||
<!--ID: 1708199272091-->
|
||||
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).
|
||||
<!--ID: 1708199272095-->
|
||||
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).
|
||||
<!--ID: 1708199272099-->
|
||||
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.
|
||||
<!--ID: 1707422675517-->
|
||||
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
|
||||
<!--ID: 1706994861298-->
|
||||
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
|
||||
<!--ID: 1706994861300-->
|
||||
END%%
|
||||
|
||||
## Implication
|
||||
|
||||
Implication is denoted as $\Rightarrow$. In classical logic, it has truth table $$\begin{array}{c|c|c} p & q & p \Rightarrow q \\ \hline T & T & T \\ T & F & F \\ F & T & T \\ F & F & T \end{array}$$
|
||||
|
||||
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.
|
||||
<!--ID: 1706994861308-->
|
||||
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.
|
||||
<!--ID: 1706994861310-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ if $Q$" in propositional logic?
|
||||
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).
|
||||
<!--ID: 1708199272127-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ if $Q$" using "necessary"?
|
||||
Back: $P$ is necessary for $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).
|
||||
<!--ID: 1717853966420-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ if $Q$" using "sufficient"?
|
||||
Back: $Q$ is sufficient for $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).
|
||||
<!--ID: 1717853966425-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ only if $Q$" in propositional logic?
|
||||
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).
|
||||
<!--ID: 1708199272134-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ only if $Q$" using "necessary"?
|
||||
Back: $Q$ is necessary for $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).
|
||||
<!--ID: 1717853966429-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ only if $Q$" using "sufficient"?
|
||||
Back: $P$ is sufficient for $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).
|
||||
<!--ID: 1717853966432-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ is necessary for $Q$" in propositional logic?
|
||||
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).
|
||||
<!--ID: 1708199272140-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ is necessary for $Q$" using "if"?
|
||||
Back: $P$ if $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).
|
||||
<!--ID: 1717853966435-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ is necessary for $Q$" using "only if"?
|
||||
Back: $Q$ only if $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).
|
||||
<!--ID: 1717853966438-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ is sufficient for $Q$" in propositional logic?
|
||||
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).
|
||||
<!--ID: 1708199272145-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ is sufficient for $Q$" using "if"?
|
||||
Back: $Q$ if $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).
|
||||
<!--ID: 1717853966441-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ is sufficient for $Q$" using "only if"?
|
||||
Back: $P$ only if $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).
|
||||
<!--ID: 1717853966444-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ if $Q$" using "only if"?
|
||||
Back: $Q$ only if $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).
|
||||
<!--ID: 1717853966449-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ is sufficient for $Q$" using "necessary"?
|
||||
Back: $Q$ is necessary for $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).
|
||||
<!--ID: 1717853966454-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ only if $Q$" using "if"?
|
||||
Back: $Q$ if $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).
|
||||
<!--ID: 1717853966458-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ is necessary for $Q$" using "sufficient"?
|
||||
Back: $Q$ is sufficient for $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).
|
||||
<!--ID: 1717853966462-->
|
||||
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).
|
||||
<!--ID: 1708199272163-->
|
||||
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).
|
||||
<!--ID: 1708199272168-->
|
||||
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).
|
||||
<!--ID: 1708199272173-->
|
||||
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).
|
||||
<!--ID: 1708199272178-->
|
||||
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).
|
||||
<!--ID: 1708199272184-->
|
||||
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).
|
||||
<!--ID: 1708199272189-->
|
||||
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.
|
||||
<!--ID: 1715969047070-->
|
||||
END%%
|
||||
|
||||
## Bibliography
|
||||
|
||||
* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
* “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
|
||||
* * 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).
|
||||
* “Principle of Explosion,” in _Wikipedia_, July 3, 2024, [https://en.wikipedia.org/w/index.php?title=Principle_of_explosion](https://en.wikipedia.org/w/index.php?title=Principle_of_explosion&oldid=1232334233).
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
---
|
||||
title: Equivalence Transformation
|
||||
TARGET DECK: Obsidian::STEM
|
||||
FILE TAGS: programming::equiv-trans
|
||||
FILE TAGS: formal-system::equiv-trans
|
||||
tags:
|
||||
- equiv-trans
|
||||
- logic
|
||||
|
|
@ -10,9 +10,7 @@ tags:
|
|||
|
||||
## Overview
|
||||
|
||||
**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.
|
||||
**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.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
|
|
@ -46,9 +44,7 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
|
|||
<!--ID: 1707251673342-->
|
||||
END%%
|
||||
|
||||
## Equivalence Schemas
|
||||
|
||||
A proposition is said to be a **tautology** if it evaluates to $T$ in every state it is well-defined in. We say propositions $E1$ and $E2$ are **equivalent** if $E1 = E2$ is a tautology. In this case, we say $E1 = E2$ is an **equivalence**.
|
||||
A [[prop-logic|proposition]] is said to be a **tautology** if it evaluates to $T$ in every state it is well-defined in. We say propositions $E1$ and $E2$ are **equivalent** if $E1 = E2$ is a tautology. In this case, we say $E1 = E2$ is an **equivalence**.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
|
|
@ -114,7 +110,299 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
|
|||
<!--ID: 1707316178709-->
|
||||
END%%
|
||||
|
||||
## Equivalence Rules
|
||||
## Axioms
|
||||
|
||||
### Commutativity
|
||||
|
||||
For propositions $E1$ and $E2$:
|
||||
|
||||
* $(E1 \land E2) = (E2 \land E1)$
|
||||
* $(E1 \lor E2) = (E2 \lor E1)$
|
||||
* $(E1 = E2) = (E2 = E1)$
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of the basic logical operators do the commutative laws apply to?
|
||||
Back: $\land$, $\lor$, and $=$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673350-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What do the commutative laws allow us to do?
|
||||
Back: Reorder operands.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673351-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What is the commutative law of e.g. $\land$?
|
||||
Back: $E1 \land E2 = E2 \land E1$
|
||||
<!--ID: 1707251673353-->
|
||||
END%%
|
||||
|
||||
### Associativity
|
||||
|
||||
For propositions $E1$, $E2$, and $E3$:
|
||||
|
||||
* $E1 \land (E2 \land E3) = (E1 \land E2) \land E3$
|
||||
* $E1 \lor (E2 \lor E3) = (E1 \lor E2) \lor E3$
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of the basic logical operators do the associative laws apply to?
|
||||
Back: $\land$ and $\lor$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673354-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What do the associative laws allow us to do?
|
||||
Back: Remove parentheses.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673355-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What is the associative law of e.g. $\land$?
|
||||
Back: $E1 \land (E2 \land E3) = (E1 \land E2) \land E3$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673357-->
|
||||
END%%
|
||||
|
||||
### Distributivity
|
||||
|
||||
For propositions $E1$, $E2$, and $E3$:
|
||||
|
||||
* $E1 \lor (E2 \land E3) = (E1 \lor E2) \land (E1 \lor E3)$
|
||||
* $E1 \land (E2 \lor E3) = (E1 \land E2) \lor (E1 \land E3)$
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of the basic logical operators do the distributive laws apply to?
|
||||
Back: $\land$ and $\lor$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673358-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What do the distributive laws allow us to do?
|
||||
Back: "Factor" propositions.
|
||||
Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673360-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What is the distributive law of e.g. $\land$ over $\lor$?
|
||||
Back: $E1 \land (E2 \lor E3) = (E1 \land E2) \lor (E1 \land E3)$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673361-->
|
||||
END%%
|
||||
|
||||
### De Morgan's
|
||||
|
||||
For propositions $E1$ and $E2$:
|
||||
|
||||
* $\neg (E1 \land E2) = \neg E1 \lor \neg E2$
|
||||
* $\neg (E1 \lor E2) = \neg E1 \land \neg E2$
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of the basic logical operators do De Morgan's laws involve?
|
||||
Back: $\neg$, $\land$, and $\lor$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673363-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is De Morgan's law (distributing $\land$) expressed as an equivalence?
|
||||
Back: $\neg (E1 \land E2) = \neg E1 \lor \neg E2$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673364-->
|
||||
END%%
|
||||
|
||||
### Law of Negation
|
||||
|
||||
For any proposition $E1$, it follows that $\neg (\neg E1) = E1$.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the law of negation expressed as an equivalence?
|
||||
Back: $\neg (\neg E1) = E1$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673365-->
|
||||
END%%
|
||||
|
||||
### Law of Excluded Middle
|
||||
|
||||
For any proposition $E1$, it follows that $E1 \lor \neg E1 = T$.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of the basic logical operators does the law of excluded middle involve?
|
||||
Back: $\lor$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673367-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the law of excluded middle expressed as an equivalence?
|
||||
Back: $E1 \lor \neg E1 = T$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673368-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
"This sentence is false" questions which classical principle?
|
||||
Back: The law of excluded middle.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251779153-->
|
||||
END%%
|
||||
|
||||
### Law of Contradiction
|
||||
|
||||
For any proposition $E1$, it follows that $E1 \land \neg E1 = F$.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of the basic logical operators does the law of contradiction involve?
|
||||
Back: $\land$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673370-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the law of contradiction expressed as an equivalence?
|
||||
Back: $E1 \land \neg E1 = F$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673371-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
The law of {1:excluded middle} is to {2:$\lor$} whereas the law of {2:contradiction} is to {1:$\land$}.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673373-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What does the principle of explosion state?
|
||||
Back: That any statement can be proven from a contradiction.
|
||||
Reference: “Principle of Explosion,” in _Wikipedia_, July 3, 2024, [https://en.wikipedia.org/w/index.php?title=Principle_of_explosion](https://en.wikipedia.org/w/index.php?title=Principle_of_explosion&oldid=1232334233).
|
||||
<!--ID: 1721354092779-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the principle of explosion stated in first-order logic?
|
||||
Back: $\forall P, F \Rightarrow P$
|
||||
Reference: “Principle of Explosion,” in _Wikipedia_, July 3, 2024, [https://en.wikipedia.org/w/index.php?title=Principle_of_explosion](https://en.wikipedia.org/w/index.php?title=Principle_of_explosion&oldid=1232334233).
|
||||
<!--ID: 1721354092783-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What does the law of contradiction say?
|
||||
Back: For any proposition $P$, it holds that $\neg (P \land \neg P)$.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1721354092786-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How does the principle of explosion relate to the law of contradiction?
|
||||
Back: If a contradiction could be proven, then anything can be proven.
|
||||
Reference: “Principle of Explosion,” in _Wikipedia_, July 3, 2024, [https://en.wikipedia.org/w/index.php?title=Principle_of_explosion](https://en.wikipedia.org/w/index.php?title=Principle_of_explosion&oldid=1232334233).
|
||||
<!--ID: 1721354092789-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Suppose $P$ and $\neg P$. Show schematically how to use the principle of explosion to prove $Q$.
|
||||
Back: $$\begin{align*} P \\ \neg P \\ P \lor Q \\ \hline Q \end{align*}$$Reference: “Principle of Explosion,” in _Wikipedia_, July 3, 2024, [https://en.wikipedia.org/w/index.php?title=Principle_of_explosion](https://en.wikipedia.org/w/index.php?title=Principle_of_explosion&oldid=1232334233).
|
||||
<!--ID: 1721354092792-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
The law of {contradiction} and law of {excluded middle} create a dichotomy in "logical space".
|
||||
Reference: “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
|
||||
<!--ID: 1721354092795-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which property of partitions is analagous to the law of contradiction on "logical space"?
|
||||
Back: Disjointedness.
|
||||
Reference: “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
|
||||
<!--ID: 1721354092798-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which property of partitions is analagous to the law of excluded middle on "logical space"?
|
||||
Back: Exhaustiveness.
|
||||
Reference: “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
|
||||
<!--ID: 1721354092801-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
The law of {1:contradiction} is to "{2:mutually exclusive}" whereas the law of {2:excluded middle} is "{1:jointly exhaustive}".
|
||||
Reference: “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
|
||||
<!--ID: 1721354092805-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which logical law proves equivalence of the law of contradiction and excluded middle?
|
||||
Back: De Morgan's law.
|
||||
Reference: “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
|
||||
<!--ID: 1721355020261-->
|
||||
END%%
|
||||
|
||||
### Law of Implication
|
||||
|
||||
For any propositions $E1$ and $E2$, it follows that $E1 \Rightarrow E2 = \neg E1 \lor E2$.
|
||||
|
||||
### Law of Equality
|
||||
|
||||
For any propositions $E1$ and $E2$, it follows that $(E1 = E2) = (E1 \Rightarrow E2) \land (E2 \Rightarrow E1)$.
|
||||
|
||||
### Law of Or-Simplification
|
||||
|
||||
For any propositions $E1$ and $E2$, it follows that:
|
||||
|
||||
* $E1 \lor E1 = E1$
|
||||
* $E1 \lor T = T$
|
||||
* $E1 \lor F = E1$
|
||||
* $E1 \lor (E1 \land E2) = E1$
|
||||
|
||||
### Law of And-Simplification
|
||||
|
||||
For any propositions $E1$ and $E2$, it follows that:
|
||||
|
||||
* $E1 \land E1 = E1$
|
||||
* $E1 \land T = E1$
|
||||
* $E1 \land F = F$
|
||||
* $E1 \land (E1 \lor E2) = E1$
|
||||
|
||||
### Law of Identity
|
||||
|
||||
For any proposition $E1$, $E1 = E1$.
|
||||
|
||||
## Inference Rules
|
||||
|
||||
* Rule of Substitution
|
||||
* Let $P(r)$ be a predicate and $E1 = E2$ be an equivalence. Then $P(E1) = P(E2)$ is an equivalence.
|
||||
|
|
@ -1081,6 +1369,208 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
|
|||
<!--ID: 1707939006297-->
|
||||
END%%
|
||||
|
||||
## States
|
||||
|
||||
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.
|
||||
<!--ID: 1706994861314-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Is $(b \land c)$ well-defined in $\{\langle b, T \rangle, \langle c, F \rangle\}$?
|
||||
Back: Yes.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1706994861318-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Is $(b \lor d)$ well-defined in $\{\langle b, T \rangle, \langle c, F \rangle\}$?
|
||||
Back: No.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1706994861320-->
|
||||
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.
|
||||
<!--ID: 1706994861316-->
|
||||
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.
|
||||
<!--ID: 1706994861337-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What set of states does proposition $a \land b$ represent?
|
||||
Back: $\{\{\langle a, T \rangle, \langle b, T \rangle\}\}$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1706994861339-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What set of states does proposition $a \lor b$ represent?
|
||||
Back: $\{\{\langle a, T \rangle, \langle b, T \rangle\}, \{\langle a, T \rangle, \langle b, F \rangle\}, \{\langle a, F \rangle, \langle b, T \rangle\}\}$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1715895996324-->
|
||||
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.
|
||||
<!--ID: 1706994861341-->
|
||||
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.
|
||||
<!--ID: 1706994861348-->
|
||||
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.
|
||||
<!--ID: 1706994861350-->
|
||||
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.
|
||||
<!--ID: 1706994861352-->
|
||||
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.
|
||||
<!--ID: 1706994861354-->
|
||||
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.
|
||||
<!--ID: 1706994861335-->
|
||||
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.
|
||||
<!--ID: 1706994861343-->
|
||||
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.
|
||||
<!--ID: 1715631869202-->
|
||||
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.
|
||||
<!--ID: 1706994861346-->
|
||||
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.
|
||||
<!--ID: 1715631869207-->
|
||||
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.
|
||||
<!--ID: 1706994861356-->
|
||||
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.
|
||||
<!--ID: 1715969047071-->
|
||||
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.
|
||||
<!--ID: 1715969047073-->
|
||||
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.
|
||||
<!--ID: 1715969047074-->
|
||||
END%%
|
||||
|
||||
%%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.
|
||||
<!--ID: 1715898219881-->
|
||||
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.
|
||||
<!--ID: 1715898219890-->
|
||||
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.
|
||||
<!--ID: 1715898219895-->
|
||||
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.
|
||||
<!--ID: 1715898219903-->
|
||||
END%%
|
||||
|
||||
## Bibliography
|
||||
|
||||
* Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
|
||||
|
|
@ -0,0 +1,71 @@
|
|||
---
|
||||
title: Proof Systems
|
||||
TARGET DECK: Obsidian::STEM
|
||||
FILE TAGS: formal-system
|
||||
tags:
|
||||
- formal-system
|
||||
- logic
|
||||
---
|
||||
|
||||
## Overview
|
||||
|
||||
A deductive system found in certain formal systems. Proof systems are syntactic in nature. Proofs are sequences of WFFs, each of which are entailed from previous ones in the sequence. A theorem is then the last WFF in any valid sequence of WFFs.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
*Why* do we say formal systems using proof systems are purely syntactic?
|
||||
Back: No meaning is attached to the WFFs of the formal language.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534205-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
Proof systems are {syntactic}, not {semantic}.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534211-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is it purely syntactic proof systems can produce theorems?
|
||||
Back: Inference rules define how to produce theorems from sequences of WFFs.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534217-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What kind of deductive system is natural deduction usually categorized as?
|
||||
Back: A proof system.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534223-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
In a proof system, a proof is used to produce what?
|
||||
Back: A theorem.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534230-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
In a proof system, a proof is a sequence of what?
|
||||
Back: Well-formed formulas.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534235-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
In a proof system, how are WFFs produced from one another?
|
||||
Back: Via inference rules.
|
||||
Reference: “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
<!--ID: 1721561534241-->
|
||||
END%%
|
||||
|
||||
## Bibliography
|
||||
|
||||
* “Formal System,” in _Wikipedia_, May 10, 2024, [https://en.wikipedia.org/w/index.php?title=Formal_system](https://en.wikipedia.org/w/index.php?title=Formal_system&oldid=1223254138).
|
||||
|
|
@ -0,0 +1,8 @@
|
|||
---
|
||||
title: Classical Logic
|
||||
TARGET DECK: Obsidian::STEM
|
||||
FILE TAGS: logic::classical
|
||||
tags:
|
||||
- classical
|
||||
- logic
|
||||
---
|
||||
|
|
@ -1,14 +1,14 @@
|
|||
---
|
||||
title: Truth Tables
|
||||
TARGET DECK: Obsidian::STEM
|
||||
FILE TAGS: logic
|
||||
FILE TAGS: logic::classical
|
||||
tags:
|
||||
- logic
|
||||
---
|
||||
|
||||
## Overview
|
||||
|
||||
Every proposition can be written in **disjunctive normal form** (DNF) and **conjunctive normal form** (CNF). This is evident with the use of truth tables. To write a proposition in DNF, write its corresponding truth table and $\lor$ each row that evaluates to $T$. To write the same proposition in CNF, apply $\lor$ to each row that evaluates to $F$ and negate it.
|
||||
In classical logic, every [[prop-logic|proposition]] can be written in **disjunctive normal form** (DNF) and **conjunctive normal form** (CNF). This is evident with the use of truth tables. To write a proposition in DNF, write its corresponding truth table and $\lor$ each row that evaluates to $T$. To write the same proposition in CNF, apply $\lor$ to each row that evaluates to $F$ and negate it.
|
||||
|
||||
$$\neg (a \Rightarrow b) \Leftrightarrow c$$
|
||||
|
||||
|
|
@ -1,5 +1,7 @@
|
|||
---
|
||||
title: Logic
|
||||
TARGET DECK: Obsidian::STEM
|
||||
FILE TAGS: logic
|
||||
tags:
|
||||
- logic
|
||||
---
|
||||
|
|
|
|||
|
|
@ -1,758 +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$). 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.
|
||||
<!--ID: 1715897257085-->
|
||||
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.
|
||||
<!--ID: 1706994861291-->
|
||||
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).
|
||||
<!--ID: 1708199272076-->
|
||||
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).
|
||||
<!--ID: 1708199272083-->
|
||||
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).
|
||||
<!--ID: 1708199272087-->
|
||||
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).
|
||||
<!--ID: 1708199272091-->
|
||||
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).
|
||||
<!--ID: 1708199272095-->
|
||||
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).
|
||||
<!--ID: 1708199272099-->
|
||||
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.
|
||||
<!--ID: 1707422675517-->
|
||||
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
|
||||
<!--ID: 1706994861298-->
|
||||
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
|
||||
<!--ID: 1706994861300-->
|
||||
END%%
|
||||
|
||||
## Implication
|
||||
|
||||
Implication is denoted as $\Rightarrow$. It has truth table $$\begin{array}{c|c|c} p & q & p \Rightarrow q \\ \hline T & T & T \\ T & F & F \\ F & T & T \\ F & F & T \end{array}$$
|
||||
|
||||
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.
|
||||
<!--ID: 1706994861308-->
|
||||
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.
|
||||
<!--ID: 1706994861310-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ if $Q$" in propositional logic?
|
||||
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).
|
||||
<!--ID: 1708199272127-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ if $Q$" using "necessary"?
|
||||
Back: $P$ is necessary for $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).
|
||||
<!--ID: 1717853966420-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ if $Q$" using "sufficient"?
|
||||
Back: $Q$ is sufficient for $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).
|
||||
<!--ID: 1717853966425-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ only if $Q$" in propositional logic?
|
||||
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).
|
||||
<!--ID: 1708199272134-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ only if $Q$" using "necessary"?
|
||||
Back: $Q$ is necessary for $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).
|
||||
<!--ID: 1717853966429-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ only if $Q$" using "sufficient"?
|
||||
Back: $P$ is sufficient for $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).
|
||||
<!--ID: 1717853966432-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ is necessary for $Q$" in propositional logic?
|
||||
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).
|
||||
<!--ID: 1708199272140-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ is necessary for $Q$" using "if"?
|
||||
Back: $P$ if $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).
|
||||
<!--ID: 1717853966435-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ is necessary for $Q$" using "only if"?
|
||||
Back: $Q$ only if $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).
|
||||
<!--ID: 1717853966438-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ is sufficient for $Q$" in propositional logic?
|
||||
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).
|
||||
<!--ID: 1708199272145-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ is sufficient for $Q$" using "if"?
|
||||
Back: $Q$ if $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).
|
||||
<!--ID: 1717853966441-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ is sufficient for $Q$" using "only if"?
|
||||
Back: $P$ only if $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).
|
||||
<!--ID: 1717853966444-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ if $Q$" using "only if"?
|
||||
Back: $Q$ only if $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).
|
||||
<!--ID: 1717853966449-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ is sufficient for $Q$" using "necessary"?
|
||||
Back: $Q$ is necessary for $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).
|
||||
<!--ID: 1717853966454-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ only if $Q$" using "if"?
|
||||
Back: $Q$ if $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).
|
||||
<!--ID: 1717853966458-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How do you write "$P$ is necessary for $Q$" using "sufficient"?
|
||||
Back: $Q$ is sufficient for $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).
|
||||
<!--ID: 1717853966462-->
|
||||
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).
|
||||
<!--ID: 1708199272163-->
|
||||
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).
|
||||
<!--ID: 1708199272168-->
|
||||
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).
|
||||
<!--ID: 1708199272173-->
|
||||
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).
|
||||
<!--ID: 1708199272178-->
|
||||
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).
|
||||
<!--ID: 1708199272184-->
|
||||
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).
|
||||
<!--ID: 1708199272189-->
|
||||
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.
|
||||
<!--ID: 1715969047070-->
|
||||
END%%
|
||||
|
||||
## Laws
|
||||
|
||||
### Commutativity
|
||||
|
||||
For propositions $E1$ and $E2$:
|
||||
|
||||
* $(E1 \land E2) = (E2 \land E1)$
|
||||
* $(E1 \lor E2) = (E2 \lor E1)$
|
||||
* $(E1 = E2) = (E2 = E1)$
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of the basic logical operators do the commutative laws apply to?
|
||||
Back: $\land$, $\lor$, and $=$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673350-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What do the commutative laws allow us to do?
|
||||
Back: Reorder operands.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673351-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What is the commutative law of e.g. $\land$?
|
||||
Back: $E1 \land E2 = E2 \land E1$
|
||||
<!--ID: 1707251673353-->
|
||||
END%%
|
||||
|
||||
### Associativity
|
||||
|
||||
For propositions $E1$, $E2$, and $E3$:
|
||||
|
||||
* $E1 \land (E2 \land E3) = (E1 \land E2) \land E3$
|
||||
* $E1 \lor (E2 \lor E3) = (E1 \lor E2) \lor E3$
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of the basic logical operators do the associative laws apply to?
|
||||
Back: $\land$ and $\lor$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673354-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What do the associative laws allow us to do?
|
||||
Back: Remove parentheses.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673355-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What is the associative law of e.g. $\land$?
|
||||
Back: $E1 \land (E2 \land E3) = (E1 \land E2) \land E3$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673357-->
|
||||
END%%
|
||||
|
||||
### Distributivity
|
||||
|
||||
For propositions $E1$, $E2$, and $E3$:
|
||||
|
||||
* $E1 \lor (E2 \land E3) = (E1 \lor E2) \land (E1 \lor E3)$
|
||||
* $E1 \land (E2 \lor E3) = (E1 \land E2) \lor (E1 \land E3)$
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of the basic logical operators do the distributive laws apply to?
|
||||
Back: $\land$ and $\lor$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673358-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What do the distributive laws allow us to do?
|
||||
Back: "Factor" propositions.
|
||||
Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673360-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What is the distributive law of e.g. $\land$ over $\lor$?
|
||||
Back: $E1 \land (E2 \lor E3) = (E1 \land E2) \lor (E1 \land E3)$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673361-->
|
||||
END%%
|
||||
|
||||
### De Morgan's
|
||||
|
||||
For propositions $E1$ and $E2$:
|
||||
|
||||
* $\neg (E1 \land E2) = \neg E1 \lor \neg E2$
|
||||
* $\neg (E1 \lor E2) = \neg E1 \land \neg E2$
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of the basic logical operators do De Morgan's laws involve?
|
||||
Back: $\neg$, $\land$, and $\lor$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673363-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is De Morgan's law (distributing $\land$) expressed as an equivalence?
|
||||
Back: $\neg (E1 \land E2) = \neg E1 \lor \neg E2$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
Tags: programming::equiv-trans
|
||||
<!--ID: 1707251673364-->
|
||||
END%%
|
||||
|
||||
### Law of Negation
|
||||
|
||||
For any proposition $E1$, it follows that $\neg (\neg E1) = E1$.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the law of negation expressed as an equivalence?
|
||||
Back: $\neg (\neg E1) = E1$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
Tags: programming::equiv-trans
|
||||
<!--ID: 1707251673365-->
|
||||
END%%
|
||||
|
||||
### Law of Excluded Middle
|
||||
|
||||
For any proposition $E1$, it follows that $E1 \lor \neg E1 = T$.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of the basic logical operators does the law of excluded middle involve?
|
||||
Back: $\lor$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673367-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the law of excluded middle expressed as an equivalence?
|
||||
Back: $E1 \lor \neg E1 = T$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
Tags: programming::equiv-trans
|
||||
<!--ID: 1707251673368-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which equivalence schema is "refuted" by sentence, "This sentence is false."
|
||||
Back: The law of excluded middle
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251779153-->
|
||||
END%%
|
||||
|
||||
### Law of Contradiction
|
||||
|
||||
For any proposition $E1$, it follows that $E1 \land \neg E1 = F$.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of the basic logical operators does the law of contradiction involve?
|
||||
Back: $\land$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673370-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the law of contradiction expressed as an equivalence?
|
||||
Back: $E1 \land \neg E1 = F$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
Tags: programming::equiv-trans
|
||||
<!--ID: 1707251673371-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
The law of {1:excluded middle} is to {2:$\lor$} whereas the law of {2:contradiction} is to {1:$\land$}.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707251673373-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What does the principle of explosion state?
|
||||
Back: That any statement can be proven from a contradiction.
|
||||
Reference: “Principle of Explosion,” in _Wikipedia_, July 3, 2024, [https://en.wikipedia.org/w/index.php?title=Principle_of_explosion](https://en.wikipedia.org/w/index.php?title=Principle_of_explosion&oldid=1232334233).
|
||||
<!--ID: 1721354092779-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the principle of explosion stated in first-order logic?
|
||||
Back: $\forall P, F \Rightarrow P$
|
||||
Reference: “Principle of Explosion,” in _Wikipedia_, July 3, 2024, [https://en.wikipedia.org/w/index.php?title=Principle_of_explosion](https://en.wikipedia.org/w/index.php?title=Principle_of_explosion&oldid=1232334233).
|
||||
<!--ID: 1721354092783-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What does the law of contradiction say?
|
||||
Back: For any proposition $P$, it holds that $\neg (P \land \neg P)$.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1721354092786-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How does the principle of explosion relate to the law of contradiction?
|
||||
Back: If a contradiction could be proven, then anything can be proven.
|
||||
Reference: “Principle of Explosion,” in _Wikipedia_, July 3, 2024, [https://en.wikipedia.org/w/index.php?title=Principle_of_explosion](https://en.wikipedia.org/w/index.php?title=Principle_of_explosion&oldid=1232334233).
|
||||
<!--ID: 1721354092789-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Suppose $P$ and $\neg P$. Show schematically how to use the principle of explosion to prove $Q$.
|
||||
Back: $$\begin{align*} P \\ \neg P \\ P \lor Q \\ \hline Q \end{align*}$$Reference: “Principle of Explosion,” in _Wikipedia_, July 3, 2024, [https://en.wikipedia.org/w/index.php?title=Principle_of_explosion](https://en.wikipedia.org/w/index.php?title=Principle_of_explosion&oldid=1232334233).
|
||||
<!--ID: 1721354092792-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
The law of {contradiction} and law of {excluded middle} create a dichotomy in "logical space".
|
||||
Reference: “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
|
||||
<!--ID: 1721354092795-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which property of partitions is analagous to the law of contradiction on "logical space"?
|
||||
Back: Disjointedness.
|
||||
Reference: “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
|
||||
<!--ID: 1721354092798-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which property of partitions is analagous to the law of excluded middle on "logical space"?
|
||||
Back: Exhaustiveness.
|
||||
Reference: “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
|
||||
<!--ID: 1721354092801-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
The law of {1:contradiction} is to "{2:mutually exclusive}" whereas the law of {2:excluded middle} is "{1:jointly exhaustive}".
|
||||
Reference: “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
|
||||
<!--ID: 1721354092805-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which logical law proves equivalence of the law of contradiction and excluded middle?
|
||||
Back: De Morgan's law.
|
||||
Reference: “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
|
||||
<!--ID: 1721355020261-->
|
||||
END%%
|
||||
|
||||
## As 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.
|
||||
<!--ID: 1706994861314-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Is $(b \land c)$ well-defined in $\{\langle b, T \rangle, \langle c, F \rangle\}$?
|
||||
Back: Yes.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1706994861318-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Is $(b \lor d)$ well-defined in $\{\langle b, T \rangle, \langle c, F \rangle\}$?
|
||||
Back: No.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1706994861320-->
|
||||
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.
|
||||
<!--ID: 1706994861316-->
|
||||
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.
|
||||
<!--ID: 1706994861337-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What set of states does proposition $a \land b$ represent?
|
||||
Back: $\{\{\langle a, T \rangle, \langle b, T \rangle\}\}$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1706994861339-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What set of states does proposition $a \lor b$ represent?
|
||||
Back: $\{\{\langle a, T \rangle, \langle b, T \rangle\}, \{\langle a, T \rangle, \langle b, F \rangle\}, \{\langle a, F \rangle, \langle b, T \rangle\}\}$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1715895996324-->
|
||||
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.
|
||||
<!--ID: 1706994861341-->
|
||||
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.
|
||||
<!--ID: 1706994861348-->
|
||||
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.
|
||||
<!--ID: 1706994861350-->
|
||||
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.
|
||||
<!--ID: 1706994861352-->
|
||||
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.
|
||||
<!--ID: 1706994861354-->
|
||||
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.
|
||||
<!--ID: 1706994861335-->
|
||||
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.
|
||||
<!--ID: 1706994861343-->
|
||||
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.
|
||||
<!--ID: 1715631869202-->
|
||||
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.
|
||||
<!--ID: 1706994861346-->
|
||||
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.
|
||||
<!--ID: 1715631869207-->
|
||||
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.
|
||||
<!--ID: 1706994861356-->
|
||||
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.
|
||||
<!--ID: 1715969047071-->
|
||||
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.
|
||||
<!--ID: 1715969047073-->
|
||||
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.
|
||||
<!--ID: 1715969047074-->
|
||||
END%%
|
||||
|
||||
## Bibliography
|
||||
|
||||
* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
* “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
|
||||
* * 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).
|
||||
* “Principle of Explosion,” in _Wikipedia_, July 3, 2024, [https://en.wikipedia.org/w/index.php?title=Principle_of_explosion](https://en.wikipedia.org/w/index.php?title=Principle_of_explosion&oldid=1232334233).
|
||||
|
|
@ -9,11 +9,11 @@ tags:
|
|||
|
||||
## Overview
|
||||
|
||||
A **dialetheia** is a sentence $A$ such that both it and its negation ($\neg A$) are true. **Dialetheism** is the view that there are dialetheias. In other words, dialetheism admits the existence of true contradictions.
|
||||
A **dialetheia** is a proposition $A$ such that both it and its negation ($\neg A$) are true. **Dialetheism** is the view that there are dialetheias. In other words, dialetheism admits the existence of true contradictions.
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
A {dialetheia} is a {sentence such that both it and its negation are true}.
|
||||
A {dialetheia} is a {proposition such that both it and its negation are true}.
|
||||
Reference: Graham Priest, Francesco Berto, and Zach Weber, “Dialetheism,” in _The Stanford Encyclopedia of Philosophy_, ed. Edward N. Zalta and Uri Nodelman, Summer 2024 (Metaphysics Research Lab, Stanford University, 2024), [https://plato.stanford.edu/archives/sum2024/entries/dialetheism/](https://plato.stanford.edu/archives/sum2024/entries/dialetheism/).
|
||||
<!--ID: 1721354092768-->
|
||||
END%%
|
||||
|
|
|
|||
|
|
@ -1,9 +1,10 @@
|
|||
---
|
||||
title: Short-Circuit
|
||||
TARGET DECK: Obsidian::STEM
|
||||
FILE TAGS: logic
|
||||
FILE TAGS: programming::short-circuit
|
||||
tags:
|
||||
- logic
|
||||
- programming
|
||||
---
|
||||
|
||||
## Overview
|
||||
|
|
@ -211,7 +211,7 @@ Basic
|
|||
Suppose `Function.Injective f` for $f \colon A \rightarrow B$. What predicate logical formula describes $f$?
|
||||
Back: $\forall a_1, a_2 \in A, (f(a_1) = f(a_2) \Rightarrow a_1 = a_2$)
|
||||
Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
|
||||
Tags: lean logic::predicate
|
||||
Tags: lean formal-system::predicate
|
||||
<!--ID: 1718464498603-->
|
||||
END%%
|
||||
|
||||
|
|
@ -470,7 +470,7 @@ Basic
|
|||
Suppose `Function.Surjective f` for $f \colon A \rightarrow B$. What predicate logical formula describes $f$?
|
||||
Back: $\forall b \in B, \exists a \in A, f(a) = b$
|
||||
Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
|
||||
Tags: lean logic::predicate
|
||||
Tags: lean formal-system::predicate
|
||||
<!--ID: 1718464498615-->
|
||||
END%%
|
||||
|
||||
|
|
|
|||
|
|
@ -236,7 +236,7 @@ END%%
|
|||
|
||||
%%ANKI
|
||||
Basic
|
||||
In terms of condition codes, what value does `setz` put in its specified destination?
|
||||
In terms of condition codes, what value does `sets` put in its specified destination?
|
||||
Back: `SF`
|
||||
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
<!--ID: 1721387052533-->
|
||||
|
|
|
|||
Loading…
Reference in New Issue