Beta-equality and dialetheism.
parent
af53475ee2
commit
9acf6ca60e
|
|
@ -183,7 +183,7 @@
|
|||
"_journal/2024-02-02.md": "a3b222daee8a50bce4cbac699efc7180",
|
||||
"_journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb",
|
||||
"_journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970",
|
||||
"logic/equiv-trans.md": "64b6110fdfb3d2c254de6d2dc6d7f312",
|
||||
"logic/equiv-trans.md": "f910dc13cb20db291b1d1241e8046bee",
|
||||
"_journal/2024-02-07.md": "8d81cd56a3b33883a7706d32e77b5889",
|
||||
"algorithms/loop-invariants.md": "cbefc346842c21a6cce5c5edce451eb2",
|
||||
"algorithms/loop-invariant.md": "3b390e720f3b2a98e611b49a0bb1f5a9",
|
||||
|
|
@ -325,7 +325,7 @@
|
|||
"_journal/2024-03/2024-03-17.md": "23f9672f5c93a6de52099b1b86834e8b",
|
||||
"set/directed-graph.md": "b4b8ad1be634a0a808af125fe8577a53",
|
||||
"set/index.md": "ea5e92b9792a8e093bac259f85f1f829",
|
||||
"set/graphs.md": "55298be7241906cb6b61673cf0a2e709",
|
||||
"set/graphs.md": "1a0c09f643829dae6a101b96de31eb40",
|
||||
"_journal/2024-03-19.md": "a0807691819725bf44c0262405e97cbb",
|
||||
"_journal/2024-03/2024-03-18.md": "63c3c843fc6cfc2cd289ac8b7b108391",
|
||||
"awk/variables.md": "e40a20545358228319f789243d8b9f77",
|
||||
|
|
@ -456,8 +456,8 @@
|
|||
"_journal/2024-05/2024-05-14.md": "f6ece1d6c178d57875786f87345343c5",
|
||||
"_journal/2024-05-16.md": "580c7ec61ec56be92fa8d6affcf0a5f6",
|
||||
"_journal/2024-05/2024-05-15.md": "4e6a7e6df32e93f0d8a56bc76613d908",
|
||||
"logic/pred-logic.md": "c23c3da8756ac0ef17b9710a67440d84",
|
||||
"logic/prop-logic.md": "5f20f5c27c7b59c59fc125ba78e37bd8",
|
||||
"logic/pred-logic.md": "a709cb45e7554ffc578cba0eb1e86e57",
|
||||
"logic/prop-logic.md": "daa927c5eb31813fcf21bcb18ba0f1ec",
|
||||
"_journal/2024-05-17.md": "fb880d68077b655ede36d994554f3aba",
|
||||
"_journal/2024-05/2024-05-16.md": "9fdfadc3f9ea6a4418fd0e7066d6b10c",
|
||||
"_journal/2024-05-18.md": "c0b58b28f84b31cea91404f43b0ee40c",
|
||||
|
|
@ -485,7 +485,7 @@
|
|||
"_journal/2024-05/2024-05-25.md": "3e8a0061fa58a6e5c48d12800d1ab869",
|
||||
"_journal/2024-05-27.md": "b36636d10eab34380f17f288868df3ae",
|
||||
"_journal/2024-05/2024-05-26.md": "abe84b5beae74baa25501c818e64fc95",
|
||||
"algebra/set.md": "ecf6aef8bc64fc14a73178adcdd3594e",
|
||||
"algebra/set.md": "843b092a980133ba7bd61b1750a6df08",
|
||||
"algebra/boolean.md": "ee41e624f4d3d3aca00020d9a9ae42c8",
|
||||
"git/merge-conflicts.md": "761ad6137ec51d3877f7d5b3615ca5cb",
|
||||
"_journal/2024-05-28.md": "0f6aeb5ec126560acdc2d8c5c6570337",
|
||||
|
|
@ -515,7 +515,7 @@
|
|||
"_journal/2024-06/2024-06-06.md": "db3407dcc86fa759b061246ec9fbd381",
|
||||
"_journal/2024-06-08.md": "b20d39dab30b4e12559a831ab8d2f9b8",
|
||||
"_journal/2024-06/2024-06-07.md": "c6bfc4c1e5913d23ea7828a23340e7d3",
|
||||
"lambda-calculus/alpha-conversion.md": "c9b7d60602e13e8a60d8784a859d4655",
|
||||
"lambda-calculus/alpha-conversion.md": "007828faf9b4ace5bd30b87a36a90dcf",
|
||||
"lambda-calculus/index.md": "64efe9e4f6036d3f5b4ec0dc8cd3e7b9",
|
||||
"x86-64/instructions/condition-codes.md": "efb0a3244139e91461c1b327d897206f",
|
||||
"x86-64/instructions/logical.md": "818428b9ef84753920dc61e5c2de9199",
|
||||
|
|
@ -539,7 +539,7 @@
|
|||
"set/functions.md": "b41c04a596a7e711801c32eff9333a3e",
|
||||
"_journal/2024-06-15.md": "92cb8dc5c98e10832fb70c0e3ab3cec4",
|
||||
"_journal/2024-06/2024-06-14.md": "5d12bc272238ac985a1d35d3d63ea307",
|
||||
"lambda-calculus/beta-reduction.md": "e40e64be380bbe7852cfe6a310e400bf",
|
||||
"lambda-calculus/beta-reduction.md": "6c9a9f4983b0974e0184acaee7c27a22",
|
||||
"_journal/2024-06-16.md": "ded6ab660ecc7c3dce3afd2e88e5a725",
|
||||
"_journal/2024-06/2024-06-15.md": "c3a55549da9dfc2770bfcf403bf5b30b",
|
||||
"_journal/2024-06-17.md": "63df6757bb3384e45093bf2b9456ffac",
|
||||
|
|
@ -610,7 +610,10 @@
|
|||
"_journal/2024-07/2024-07-15.md": "462fb4294cbbe8855071c638351df147",
|
||||
"ontology/nominalism.md": "46245c644238157e15c7cb6def27d90a",
|
||||
"_journal/2024-07-17.md": "e0371a91e99f131e7258cc82c2a04cc8",
|
||||
"_journal/2024-07/2024-07-16.md": "149222eab7a7f58993b8e4dc8a3fb884"
|
||||
"_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": "4d14b681d6913bd775450c52c2417767"
|
||||
},
|
||||
"fields_dict": {
|
||||
"Basic": [
|
||||
|
|
|
|||
|
|
@ -0,0 +1,12 @@
|
|||
---
|
||||
title: "2024-07-18"
|
||||
---
|
||||
|
||||
- [x] Anki Flashcards
|
||||
- [x] KoL
|
||||
- [x] OGS
|
||||
- [ ] Sheet Music (10 min.)
|
||||
- [ ] Korean (Read 1 Story)
|
||||
|
||||
* Notes on [[beta-reduction#β-equality|β-equality]].
|
||||
* Brief notes on [[dialetheism]].
|
||||
|
|
@ -142,7 +142,7 @@ END%%
|
|||
|
||||
%%ANKI
|
||||
Basic
|
||||
Let $I$ be an index set and $H$ a function $I \subseteq \mathop{\text{dom}}H$. How is $\bigtimes_{i \in I} H(i)$ defined?
|
||||
Let $I$ be an index set and $H$ a function such that $I \subseteq \mathop{\text{dom}}H$. How is $\bigtimes_{i \in I} H(i)$ defined?
|
||||
Back: $\bigtimes_{i \in I} H(i) = \{ f \mid f \text{ is a function with domain } I \text { and } \forall i \in I, f(i) \in H(i) \}$
|
||||
Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
|
||||
<!--ID: 1720964209677-->
|
||||
|
|
@ -825,8 +825,8 @@ Let $A$, $B$, and $C$ be arbitrary sets. Then
|
|||
|
||||
%%ANKI
|
||||
Basic
|
||||
What kind of propositional logical statement are the antimonotonicity properties of $\subseteq$?
|
||||
Back: An implication.
|
||||
What kind of propositional logical statements are the antimonotonicity properties of $\subseteq$?
|
||||
Back: Implications.
|
||||
Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
|
||||
<!--ID: 1717073536988-->
|
||||
END%%
|
||||
|
|
|
|||
|
|
@ -59,6 +59,14 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi
|
|||
<!--ID: 1718475424871-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Is $\alpha$-conversion a symmetric relation?
|
||||
Back: Yes.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567259-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
$\alpha$-conversion is most related to what kind of $\lambda$-term?
|
||||
|
|
|
|||
|
|
@ -497,6 +497,126 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi
|
|||
<!--ID: 1720665224645-->
|
||||
END%%
|
||||
|
||||
## β-equality
|
||||
|
||||
We say $P$ is **$\beta$-equal** or **$\beta$-convertible** to $Q$ ($P =_\beta Q$) iff $Q$ can be obtained from $P$ by a finite series of $\beta$-contractions, reversed $\beta$-contractions, and changes of bound variables. That is, $P =_\beta Q$ iff there exist $P_0, \ldots, P_n$ ($n \geq 0$) such that $P_0 \equiv P$, $P_n \equiv Q$, and $$\forall i \leq n - 1, (P_i \,\triangleright_{1\beta}\, P_{i+1}) \lor (P_{i+1} \,\triangleright_{1\beta}\, P_i) \lor (P_i \equiv_\alpha P_{i+1}).$$
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
$\triangleright_\beta$ denotes what relation?
|
||||
Back: $\beta$-reduction.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567121-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
$\triangleright_{1\beta}$ denotes what relation?
|
||||
Back: $\beta$-contraction.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567128-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
$=_{\beta}$ denotes what relation?
|
||||
Back: $\beta$-equality.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567134-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
{$\beta$-equality} is also known as {$\beta$-convertibility}.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567144-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Is $\beta$-reduction a symmetric relation?
|
||||
Back: No.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567151-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Is $\beta$-equality a symmetric relation?
|
||||
Back: Yes.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567156-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
{$\beta$-equality} is the symmetric generalization of {$\beta$-reduction}.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567163-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What does it mean for $P$ to be $\beta$-equal to $Q$?
|
||||
Back: $Q$ can be obtained from $P$ by a finite series of $\beta$-contractions, reversed $\beta$-contractions, and $\alpha$-conversions.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567175-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is "$P$ is $\beta$-equal to $Q$" denoted?
|
||||
Back: $P =_\beta Q$
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567182-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
$P =_\beta Q$ iff $\exists P_0, \ldots, P_n$ s.t. $P_0 \equiv P$, $P_n \equiv Q$, and $\forall i \leq n - 1$, {$P_i \,\triangleright_{1\beta}\, P_{i+1}$} or {$P_{i+1} \,\triangleright_{1\beta}\, P_i$} or {$P_i \equiv_\alpha P_{i+1}$}.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567189-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
$\beta$-reduction constitute what two operations?
|
||||
Back: $\beta$-contractions and $\alpha$-conversions.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567196-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
$\beta$-equality constitute what three operations?
|
||||
Back: $\beta$-contractions, reversed $\beta$-contractions, and $\alpha$-conversions.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567202-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
{$M =_\beta M' \land N =_\beta N'$} $\Rightarrow [N/x]M =_\beta [N'/x]M'$
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567212-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How would Hindley et al. describe the following implication? $$M =_\beta M' \land N =_\beta N' \Rightarrow [N/x]M =_\beta [N'/x]M'$$
|
||||
Back: As "substitution is well-defined with respect to $\beta$-equality."
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567219-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
If $P =_\beta Q$, how do $P$ and $Q$'s $\beta$-normal forms relate to one another?
|
||||
Back: Either $P$ and $Q$ have the same $\beta$-normal form or neither $P$ nor $Q$ have a $\beta$-normal form.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567227-->
|
||||
END%%
|
||||
|
||||
## Church-Rosser Theorem
|
||||
|
||||
If $P \,\triangleright_\beta\, M$ and $P \,\triangleright_\beta\, N$, then there exists a term $T$ such that $M \,\triangleright_\beta\, T$ and $N \,\triangleright_\beta\, T$. As an immediate corollary, if $P$ has a $\beta$-normal form then it it is unique modulo $\equiv_\alpha$.
|
||||
|
|
@ -567,7 +687,7 @@ END%%
|
|||
|
||||
%%ANKI
|
||||
Basic
|
||||
What does the Church-Rosser theorem for $\triangleright_\beta$ state in terms of confluence?
|
||||
What does the Church-Rosser theorem state in terms of confluence?
|
||||
Back: $\beta$-reduction is confluent.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1719577152613-->
|
||||
|
|
@ -577,7 +697,7 @@ END%%
|
|||
Basic
|
||||
The following diagram is a representation of what theorem?
|
||||
![[church-rosser.png]]
|
||||
Back: The Church-Rosser theorem for $\triangleright_\beta$.
|
||||
Back: The Church-Rosser theorem.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1719577152616-->
|
||||
END%%
|
||||
|
|
@ -600,13 +720,31 @@ END%%
|
|||
|
||||
%%ANKI
|
||||
Basic
|
||||
In the following Church-Rosser diagram, what do the arrows represent?
|
||||
In the following diagram of the Church-Rosser theorem, what do the arrows represent?
|
||||
![[church-rosser.png]]
|
||||
Back: $\beta$-reductions.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1719577152627-->
|
||||
END%%
|
||||
|
||||
Likewise, if $P =_\beta Q$, then there exists a term $T$ such that $P \,\triangleright_\beta\, T$ and $Q \,\triangleright_\beta\, T$.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What does the Church-Rosser theorem state in terms of $=_\beta$?
|
||||
Back: If $P =_\beta Q$ then there exists a term $T$ such that $P \,\triangleright_\beta\, T$ and $Q \,\triangleright_\beta\, T$.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567238-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What theorem encourages giving $\beta$-equality its name?
|
||||
Back: The Church-Rosser theorem.
|
||||
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
<!--ID: 1721305567250-->
|
||||
END%%
|
||||
|
||||
## Bibliography
|
||||
|
||||
* Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
|
|
@ -1,15 +0,0 @@
|
|||
---
|
||||
title: Equality
|
||||
TARGET DECK: Obsidian::STEM
|
||||
FILE TAGS: equality
|
||||
tags:
|
||||
- equality
|
||||
---
|
||||
|
||||
## Overview
|
||||
|
||||
|
||||
|
||||
## Bibliography
|
||||
|
||||
* Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
||||
|
|
@ -90,176 +90,6 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
|
|||
<!--ID: 1707251673348-->
|
||||
END%%
|
||||
|
||||
* Commutative Laws
|
||||
* $(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%%
|
||||
|
||||
* Associative Laws
|
||||
* $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%%
|
||||
|
||||
* Distributive Laws
|
||||
* $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 Laws
|
||||
* $\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 apply to?
|
||||
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
|
||||
What is De Morgan's Law of e.g. $\land$?
|
||||
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
|
||||
* $\neg (\neg E1) = E1$
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What does the Law of Negation say?
|
||||
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 the Excluded Middle
|
||||
* $E1 \lor \neg E1 = T$
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of the basic logical operators does the Law of the Excluded Middle apply to?
|
||||
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
|
||||
What does the Law of the Excluded Middle say?
|
||||
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
|
||||
Which equivalence schema is "refuted" by sentence, "This sentence is false."
|
||||
Back: Law of the 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
|
||||
* $E1 \land \neg E1 = F$
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which of the basic logical operators does the Law of Contradiction apply to?
|
||||
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
|
||||
What does the Law of Contradiction say?
|
||||
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:the 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%%
|
||||
|
||||
Gries lists other "Laws" but they don't seem as important to note here.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is $\Rightarrow$ written in terms of other logical operators?
|
||||
|
|
|
|||
|
|
@ -50,7 +50,262 @@ Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n
|
|||
<!--ID: 1708199272121-->
|
||||
END%%
|
||||
|
||||
## Sets
|
||||
## Quantification
|
||||
|
||||
A **quantifier** refers to an operator that specifies how many members of a set satisfy some formula. The most common quantifiers are $\exists$ and $\forall$, though others (such as the counting quantifier) are also used.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What are the most common first-order logic quantifiers?
|
||||
Back: $\exists$ and $\forall$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796763-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What term refers to operators like $\exists$ and $\forall$?
|
||||
Back: Quantifiers.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796766-->
|
||||
END%%
|
||||
|
||||
* **Existential quantification** ($\exists$) asserts the existence of at least one member in a set satisfying a property.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What symbol denotes existential quantification?
|
||||
Back: $\exists$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819964-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How many members in the domain of discourse must satisfy a property in existential quantification?
|
||||
Back: At least one.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819967-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
$\exists x : S, P(x)$ is shorthand for what?
|
||||
Back: $\exists x, x \in S \land P(x)$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819968-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What term refers to $S$ in $\exists x : S, P(x)$?
|
||||
Back: The domain of discourse.
|
||||
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: 1708199272194-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What is the identity element of $\lor$?
|
||||
Back: $F$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819970-->
|
||||
END%%
|
||||
|
||||
* **Universal quantification** ($\forall$) asserts that every member of a set satisfies a property.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What symbol denotes universal quantification?
|
||||
Back: $\forall$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819971-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How many members in the domain of discourse must satisfy a property in universal quantification?
|
||||
Back: All of them.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819973-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
$\forall x : S, P(x)$ is shorthand for what?
|
||||
Back: $\forall x, x \in S \Rightarrow P(x)$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819976-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What is the identity element of $\land$?
|
||||
Back: $T$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819978-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
{1:$\exists$} is to {2:$\lor$} as {2:$\forall$} is to {1:$\land$}.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819979-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is $\forall x : S, P(x)$ equivalently written in terms of existential quantification?
|
||||
Back: $\neg \exists x : S, \neg P(x)$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819981-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
How is $\exists x : S, P(x)$ equivalently written in terms of universal quantification?
|
||||
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.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What symbol denotes counting quantification (of *exactly* $k$ members)?
|
||||
Back: $\exists^{=k}$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819983-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What symbol denotes counting quantification (of *at least* $k$ members)?
|
||||
Back: $\exists^{\geq k}$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819985-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is $\exists x : S, P(x)$ written in terms of counting quantification?
|
||||
Back: $\exists^{\geq 1}\, x : S, P(x)$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494832056-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is $\forall x : S, P(x)$ written in terms of counting quantification?
|
||||
Back: Assuming $S$ has $k$ members, $\exists^{= k}\, x : S, P(x)$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494832058-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
Propositional logical operator: $\forall x, \forall y, P(x, y)$ {$\Leftrightarrow$} $\forall y, \forall x, P(x, y)$.
|
||||
Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
|
||||
<!--ID: 1718327739967-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
Propositional logical operator: $\forall x, \exists y, P(x, y)$ {$\Leftarrow$} {$\exists y, \forall x, P(x, y)$}.
|
||||
Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
|
||||
<!--ID: 1718327739972-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
Propositional logical operator: $\exists x, \forall y, P(x, y)$ {$\Rightarrow$} $\forall y, \exists x, P(x, y)$.
|
||||
Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
|
||||
<!--ID: 1718327739978-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
Propositional logical operator: $\exists x, \exists y, P(x, y)$ {$\Leftrightarrow$} $\exists y, \exists x, P(x, y)$.
|
||||
Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
|
||||
<!--ID: 1718327812365-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
When does $\exists x, \forall y, P(x, y) \Rightarrow \forall y, \exists x, P(x, y)$ hold true?
|
||||
Back: Always.
|
||||
Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
|
||||
<!--ID: 1720386023292-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
When does $\forall x, \exists y, P(x, y) \Rightarrow \exists y, \forall x, P(x, y)$ hold true?
|
||||
Back: When there exists a $y$ that $P(x, y)$ holds for over all quantified $x$.
|
||||
Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
|
||||
<!--ID: 1720386023296-->
|
||||
END%%
|
||||
|
||||
### 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**).
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Prenex normal form consists of what two parts?
|
||||
Back: The prefix and the matrix.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796773-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the prefix of a formula in PNF formatted?
|
||||
Back: As only quantifiers and bound variables.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796775-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the matrix of a formula in PNF formatted?
|
||||
Back: Without quantifiers.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796776-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which identifiers in the following are bound? $\exists x, P(x) \land P(y)$
|
||||
Back: Just $x$.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796777-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which identifiers in the following are free? $\exists x, P(x) \land P(y)$
|
||||
Back: Just $y$.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796779-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the following rewritten in PNF? $(\exists x, P(x)) \land (\exists y, Q(y))$
|
||||
Back: $\exists x \;y, P(x) \land Q(y)$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707675399517-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the following rewritten in PNF? $(\exists x, P(x)) \land (\forall y, Q(y))$
|
||||
Back: N/A.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--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.
|
||||
|
||||
|
|
|
|||
|
|
@ -104,14 +104,7 @@ END%%
|
|||
|
||||
## Implication
|
||||
|
||||
Implication is denoted as $\Rightarrow$. It has truth table
|
||||
|
||||
$p$ | $q$ | $p \Rightarrow q$
|
||||
--- | --- | -----------------
|
||||
$T$ | $T$ | $T$
|
||||
$T$ | $F$ | $F$
|
||||
$F$ | $T$ | $T$
|
||||
$F$ | $F$ | $T$
|
||||
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:
|
||||
|
|
@ -321,7 +314,273 @@ Reference: Reference: Gries, David. *The Science of Programming*. Texts and Mon
|
|||
<!--ID: 1715969047070-->
|
||||
END%%
|
||||
|
||||
## Sets
|
||||
## 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.
|
||||
|
||||
|
|
@ -494,4 +753,6 @@ END%%
|
|||
## Bibliography
|
||||
|
||||
* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
* 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).
|
||||
* “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,268 +0,0 @@
|
|||
---
|
||||
title: Quantification
|
||||
TARGET DECK: Obsidian::STEM
|
||||
FILE TAGS: logic::quantification
|
||||
tags:
|
||||
- logic
|
||||
- quantification
|
||||
---
|
||||
|
||||
## Overview
|
||||
|
||||
A **quantifier** refers to an operator that specifies how many members of a set satisfy some formula. The most common quantifiers are $\exists$ and $\forall$, though others (such as the counting quantifier) are also used.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What are the most common first-order logic quantifiers?
|
||||
Back: $\exists$ and $\forall$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796763-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What term refers to operators like $\exists$ and $\forall$?
|
||||
Back: Quantifiers.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796766-->
|
||||
END%%
|
||||
|
||||
* **Existential quantification** ($\exists$) asserts the existence of at least one member in a set satisfying a property.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What symbol denotes existential quantification?
|
||||
Back: $\exists$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819964-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How many members in the domain of discourse must satisfy a property in existential quantification?
|
||||
Back: At least one.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819967-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
$\exists x : S, P(x)$ is shorthand for what?
|
||||
Back: $\exists x, x \in S \land P(x)$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819968-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What term refers to $S$ in $\exists x : S, P(x)$?
|
||||
Back: The domain of discourse.
|
||||
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: 1708199272194-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What is the identity element of $\lor$?
|
||||
Back: $F$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819970-->
|
||||
END%%
|
||||
|
||||
* **Universal quantification** ($\forall$) asserts that every member of a set satisfies a property.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What symbol denotes universal quantification?
|
||||
Back: $\forall$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819971-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How many members in the domain of discourse must satisfy a property in universal quantification?
|
||||
Back: All of them.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819973-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
$\forall x : S, P(x)$ is shorthand for what?
|
||||
Back: $\forall x, x \in S \Rightarrow P(x)$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819976-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What is the identity element of $\land$?
|
||||
Back: $T$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819978-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
{1:$\exists$} is to {2:$\lor$} as {2:$\forall$} is to {1:$\land$}.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819979-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is $\forall x : S, P(x)$ equivalently written in terms of existential quantification?
|
||||
Back: $\neg \exists x : S, \neg P(x)$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819981-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
How is $\exists x : S, P(x)$ equivalently written in terms of universal quantification?
|
||||
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.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What symbol denotes counting quantification (of *exactly* $k$ members)?
|
||||
Back: $\exists^{=k}$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819983-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What symbol denotes counting quantification (of *at least* $k$ members)?
|
||||
Back: $\exists^{\geq k}$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819985-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is $\exists x : S, P(x)$ written in terms of counting quantification?
|
||||
Back: $\exists^{\geq 1}\, x : S, P(x)$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494832056-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is $\forall x : S, P(x)$ written in terms of counting quantification?
|
||||
Back: Assuming $S$ has $k$ members, $\exists^{= k}\, x : S, P(x)$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494832058-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
Propositional logical operator: $\forall x, \forall y, P(x, y)$ {$\Leftrightarrow$} $\forall y, \forall x, P(x, y)$.
|
||||
Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
|
||||
<!--ID: 1718327739967-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
Propositional logical operator: $\forall x, \exists y, P(x, y)$ {$\Leftarrow$} {$\exists y, \forall x, P(x, y)$}.
|
||||
Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
|
||||
<!--ID: 1718327739972-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
Propositional logical operator: $\exists x, \forall y, P(x, y)$ {$\Rightarrow$} $\forall y, \exists x, P(x, y)$.
|
||||
Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
|
||||
<!--ID: 1718327739978-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
Propositional logical operator: $\exists x, \exists y, P(x, y)$ {$\Leftrightarrow$} $\exists y, \exists x, P(x, y)$.
|
||||
Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
|
||||
<!--ID: 1718327812365-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
When does $\exists x, \forall y, P(x, y) \Rightarrow \forall y, \exists x, P(x, y)$ hold true?
|
||||
Back: Always.
|
||||
Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
|
||||
<!--ID: 1720386023292-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
When does $\forall x, \exists y, P(x, y) \Rightarrow \exists y, \forall x, P(x, y)$ hold true?
|
||||
Back: When there exists a $y$ that $P(x, y)$ holds for over all quantified $x$.
|
||||
Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
|
||||
<!--ID: 1720386023296-->
|
||||
END%%
|
||||
|
||||
## 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**).
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Prenex normal form consists of what two parts?
|
||||
Back: The prefix and the matrix.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796773-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the prefix of a formula in PNF formatted?
|
||||
Back: As only quantifiers and bound variables.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796775-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the matrix of a formula in PNF formatted?
|
||||
Back: Without quantifiers.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796776-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which identifiers in the following are bound? $\exists x, P(x) \land P(y)$
|
||||
Back: Just $x$.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796777-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which identifiers in the following are free? $\exists x, P(x) \land P(y)$
|
||||
Back: Just $y$.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796779-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the following rewritten in PNF? $(\exists x, P(x)) \land (\exists y, Q(y))$
|
||||
Back: $\exists x \;y, P(x) \land Q(y)$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707675399517-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the following rewritten in PNF? $(\exists x, P(x)) \land (\forall y, Q(y))$
|
||||
Back: N/A.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1720665224639-->
|
||||
END%%
|
||||
|
||||
## Bibliography
|
||||
|
||||
* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
* 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).
|
||||
|
|
@ -0,0 +1,31 @@
|
|||
---
|
||||
title: Dialetheism
|
||||
TARGET DECK: Obsidian::H&SS
|
||||
FILE TAGS: ontology::dialetheism
|
||||
tags:
|
||||
- dialetheism
|
||||
- ontology
|
||||
---
|
||||
|
||||
## 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.
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
A {dialetheia} is a {sentence 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%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
{Dialetheism} is the view that {dialetheia} exist.
|
||||
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: 1721354092775-->
|
||||
END%%
|
||||
|
||||
## Bibliography
|
||||
|
||||
* 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/).
|
||||
* Nikk Effingham, _An Introduction to Ontology_ (Cambridge: Polity Press, 2013).
|
||||
|
|
@ -563,7 +563,7 @@ END%%
|
|||
|
||||
%%ANKI
|
||||
Cloze
|
||||
Given a directed graph, incident {1:to} is to {1:in}-degrees whereas incident {1:from} is to {1:out}-degrees.
|
||||
Given a directed graph, incident {1:to} is to {2:in}-degrees whereas incident {2:from} is to {1:out}-degrees.
|
||||
Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022).
|
||||
<!--ID: 1710796091058-->
|
||||
END%%
|
||||
|
|
|
|||
Loading…
Reference in New Issue