commit 76a15ac585e2db32e57cfe25f8e5166706d809a4 parent 2f6af9155ce906fe3b599177be9152acc9a55b70 Author: Alex Balgavy <alex@balgavy.eu> Date: Wed, 11 Nov 2020 20:06:59 +0100 Logic & sets notes Diffstat:
56 files changed, 598 insertions(+), 137 deletions(-)
diff --git a/content/_index.md b/content/_index.md @@ -37,7 +37,7 @@ title = "Alex's university course notes" * [Computational thinking](https://thezeroalpha.github.io/compthink-notes) * [Systems architecture](https://thezeroalpha.github.io/sysarch-notes) * [Physical Computing](https://thezeroalpha.github.io/physcomp-notes) -* [Logic & sets](https://thezeroalpha.github.io/logicsets-notes) +* [Logic & sets](logicsets-notes/) * [Web tech](https://thezeroalpha.github.io/webtech-notes) * [Computer Networks](compnet-notes/) * [History of Science](history-science-notes/) diff --git a/content/logicsets-notes/Adequate systems of connectives.html b/content/logicsets-notes/Adequate systems of connectives.html @@ -1,3 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -<html><head><link rel="stylesheet" type="text/css" href="sitewide.css"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)"/><meta name="keywords" content="logic"/><meta name="altitude" content="-0.2514409720897675"/><meta name="author" content="Alex Balgavy"/><meta name="created" content="2018-02-20 14:47:19 +0000"/><meta name="latitude" content="52.33331960345897"/><meta name="longitude" content="4.865656661188186"/><meta name="source" content="desktop.mac"/><meta name="updated" content="2018-02-20 15:15:30 +0000"/><title>Adequate systems of connectives</title></head><body><div>a system C of connectives is adequate if every truth table can be expressed as formula with connectives C</div><div><br/></div><div>example:</div><div>express (p ∧ ¬ q) ∨ (¬ p ∧ q) in the system {¬, ∧}</div><div><ul><li>use: ϕ ∨ Ψ <span style="font-size: 14px;">≡ ¬ (¬ ϕ ∧ ¬ Ψ)</span></li><li>rewrite like hell</li><li>result: ¬ (¬ p ∨ ¬¬ q) ∨ ¬ (¬ ¬ p ∨ ¬ q)</li></ul><div><br/></div><div>Sheffer stroke is an adequate system — {|}</div></div><div>ϕ | Ψ means "not both ϕ and Ψ” (ϕ NAND Ψ)</div><div>ϕ | Ψ ≡ ¬ (ϕ ∧ Ψ)</div><div><br/></div><div>adequate systems are: {|}, {¬, ∧}, {¬, ∨}, {¬, ∧, ∨}, etc.</div></body></html>- \ No newline at end of file diff --git a/content/logicsets-notes/Adequate systems of connectives.md b/content/logicsets-notes/Adequate systems of connectives.md @@ -0,0 +1,18 @@ ++++ +title = 'Adequate systems of connectives' ++++ +# Adequate systems of connectives +a system C of connectives is adequate if every truth table can be expressed as formula with connectives C + +example: +express (p ∧ ¬ q) ∨ (¬ p ∧ q) in the system {¬, ∧} + +- use: ϕ ∨ Ψ ≡ ¬ (¬ ϕ ∧ ¬ Ψ) +- rewrite like hell +- result: ¬ (¬ p ∨ ¬¬ q) ∨ ¬ (¬ ¬ p ∨ ¬ q) + +Sheffer stroke is an adequate system — {|} +- ϕ | Ψ means "not both ϕ and Ψ” (ϕ NAND Ψ) +- ϕ | Ψ ≡ ¬ (ϕ ∧ Ψ) + +adequate systems are: {|}, {¬, ∧}, {¬, ∨}, {¬, ∧, ∨}, etc. diff --git a/content/logicsets-notes/Binary Decision Trees.html b/content/logicsets-notes/Binary Decision Trees.html @@ -1,3 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -<html><head><link rel="stylesheet" type="text/css" href="sitewide.css"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)"/><meta name="keywords" content="logic"/><meta name="altitude" content="-0.7498652935028076"/><meta name="author" content="Alex Balgavy"/><meta name="created" content="2018-03-06 14:33:04 +0000"/><meta name="latitude" content="52.33306697436191"/><meta name="longitude" content="4.865391302397034"/><meta name="source" content="desktop.mac"/><meta name="updated" content="2018-03-27 15:56:25 +0000"/><title>Binary Decision Trees</title></head><body><div><b>Binary Decision Trees</b></div><div>used to represent a boolean function</div><div>dashed line to left is 0, solid line to right is 1</div><div>a formula is satisfiable if there is at least 1 leaf with a 1</div><div><br/></div><div><div><img src="Binary%20Decision%20Trees.resources/screenshot.png" height="166" width="443"/><br/></div></div><div><br/></div><div><br/></div><div><span style="font-weight: bold;">Ordered Binary Decision Diagram (OBDD)</span></div><div>collapsing and removing nodes in a binary decision tree</div><div><br/></div><div>rules:</div><div><ol><li>leaves with 0 and 1 are collapsed</li><li>repeat:</li><ul><li>if 0 and 1 edge of non-leaf n lead to same node m:</li><ul><li>eliminate n</li><li>redirect its incoming edges to m</li></ul><li>if non-leaves associated with same bool variable have 0 edge to same node and 1 edge to same node, then collapse</li></ul></ol><div><br/></div></div><div>non-isomorphic reduced OBDDs are never semantically equivalent</div><div>sensitive to order change (which nodes are above which)</div><div><br/></div><div>logical operations:</div><div><ul><li>negation — swap 0 and 1 in leaf nodes</li><li>disjunction:</li><ul><li>leaves: O2 if O1 is 0, otherwise O1</li><li>non-leaves: draw new nodes with disjunctions of previous Os</li></ul></ul></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;"><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;"><div><img src="Binary%20Decision%20Trees.resources/screenshot_1.png" height="199" width="656"/><br/></div></blockquote></blockquote><div><ul><li>conjunction:</li><ul><li>leaves: O2 if O1 is 1, otherwise O1</li><li>non-leaves: same as disjunction</li></ul></ul></div><div><br/></div></body></html>- \ No newline at end of file diff --git a/content/logicsets-notes/Binary Decision Trees.resources/screenshot.png b/content/logicsets-notes/Binary Decision Trees/87789b5b531287daa9334829aa833355.png Binary files differ. diff --git a/content/logicsets-notes/Binary Decision Trees.resources/screenshot_1.png b/content/logicsets-notes/Binary Decision Trees/e75abc67fcda676fa88b094faefe3d3d.png Binary files differ. diff --git a/content/logicsets-notes/Binary Decision Trees/index.md b/content/logicsets-notes/Binary Decision Trees/index.md @@ -0,0 +1,40 @@ ++++ +title = 'Binary Decision Trees' ++++ +# Binary Decision Trees +used to represent a boolean function + +dashed line to left is 0, solid line to right is 1 + +a formula is satisfiable if there is at least 1 leaf with a 1 + + + +## Ordered Binary Decision Diagram (OBDD) +collapsing and removing nodes in a binary decision tree + +rules: +1. leaves with 0 and 1 are collapsed +2. repeat: + + - if 0 and 1 edge of non-leaf n lead to same node m: + - eliminate n + - redirect its incoming edges to m + - if non-leaves associated with same bool variable have 0 edge to same node and 1 edge to same node, then collapse + +non-isomorphic reduced OBDDs are never semantically equivalent + +sensitive to order change (which nodes are above which) + +logical operations: + +- negation — swap 0 and 1 in leaf nodes +- disjunction: + - leaves: O2 if O1 is 0, otherwise O1 + - non-leaves: draw new nodes with disjunctions of previous Os + + + +- conjunction: + - leaves: O2 if O1 is 1, otherwise O1 + - non-leaves: same as disjunction diff --git a/content/logicsets-notes/Cardinality.html b/content/logicsets-notes/Cardinality.html @@ -1,3 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -<html><head><link rel="stylesheet" type="text/css" href="sitewide.css"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)"/><meta name="keywords" content="sets"/><meta name="altitude" content="-1.531793236732483"/><meta name="author" content="Alex Balgavy"/><meta name="created" content="2018-03-08 16:20:26 +0000"/><meta name="latitude" content="52.33418990626854"/><meta name="longitude" content="4.867487486548002"/><meta name="source" content="desktop.mac"/><meta name="updated" content="2018-03-08 16:28:07 +0000"/><title>Cardinality</title></head><body><div><b>Cardinality (notion of size)</b></div><div>|A| cardinality of A (size)</div><div><ul><li>|A| ≤ |B| ⟷ there exists a total injection f: A ➝ B</li><li>|A| = |B| ⟷ there exists a bijection f: A ➝ B</li><li>|A| = #A = m ⟷ there exists a bijection f: {1,…,m} ➝ A</li></ul><div><br/></div></div><div><b>Cantor-Schroeder-Bernstein theorem (partial ordering of sets)</b></div><div>if there exist total injective functions f: A ➝ B, g: B ➝ A</div><div>then there exists a bijection h: A ➝ B</div><div><br/></div><div>so sets can be partially ordered by cardinality.</div><div><br/></div><div><b>Countable/Uncountable</b></div><div>set A is:</div><div><ul><li>countably infinite — there exists a bijection f: Nat ➝ A</li><li>countable — A is finite or countably infinite</li><li>uncountable — A is not countable</li></ul></div><div><br/></div><div>if a set is countable, it can be enumerated</div><div><br/></div><div><br/></div></body></html>- \ No newline at end of file diff --git a/content/logicsets-notes/Cardinality.md b/content/logicsets-notes/Cardinality.md @@ -0,0 +1,25 @@ ++++ +title = 'Cardinality' ++++ +# Cardinality (notion of size) +|A| cardinality of A (size) + +- |A| ≤ |B| ⟷ there exists a total injection f: A ➝ B +- |A| = |B| ⟷ there exists a bijection f: A ➝ B +- |A| = #A = m ⟷ there exists a bijection f: {1,…,m} ➝ A + +## Cantor-Schroeder-Bernstein theorem (partial ordering of sets) +if there exist total injective functions f: A ➝ B, g: B ➝ A + +then there exists a bijection h: A ➝ B + +so sets can be partially ordered by cardinality. + +## Countable/Uncountable +set A is: + +- countably infinite — there exists a bijection f: Nat ➝ A +- countable — A is finite or countably infinite +- uncountable — A is not countable + +if a set is countable, it can be enumerated diff --git a/content/logicsets-notes/Equivalence classes.html b/content/logicsets-notes/Equivalence classes.html @@ -1,3 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -<html><head><link rel="stylesheet" type="text/css" href="sitewide.css"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)"/><meta name="keywords" content="sets"/><meta name="altitude" content="-0.3668020665645599"/><meta name="author" content="Alex Balgavy"/><meta name="created" content="2018-02-27 14:56:56 +0000"/><meta name="latitude" content="52.33328100117655"/><meta name="longitude" content="4.86550032171256"/><meta name="source" content="desktop.mac"/><meta name="updated" content="2018-02-27 15:38:50 +0000"/><title>Equivalence classes</title></head><body style="zoom: 1;"><div>a <span style="font-style: italic;">binary </span>relation R is an equivalence relation if for all elements x, y, z in its domain, R satisfies:</div><div><ul><li>reflexivity: x R x</li><li>symmetry: x R y ➝ y R x</li><li>transitivity: x R y ∧ y R z ➝ x R z</li></ul><div><br/></div></div><div><span style="font-weight: bold;">Equivalence classes</span></div><div>an equivalence class consists of all elements x,y for which x R y</div><div>within an equivalence class, all formulas are semantically equivalent</div><div>each equivalence class contains infinitely many formulas</div><div>one class contains all tautologies, another all contradictions (all semantically equivalent)</div><div>for two vars p,q there are as many ≡-equivalence classes as truth tables for p,q — i.e. 16</div><div><br/></div><div><span style="text-decoration: underline;">how many equivalence classes?</span></div><div>for one variable p, there are two valuations (T or F)</div><div>each valuation has two possible outcomes (T or F)</div><div>therefore, 2<span style="vertical-align: super;">2</span> = 4 equivalence classes</div><div><br/></div><div>for two variables p,q there are four valuations (T or F for each var)</div><div>each valuation has two possible outcomes (T or F)</div><div>therefore, 2<span style="vertical-align: super;">4</span> = 16 equivalence classes</div><div>etc. for n variables, there are 2<span style="vertical-align: super;">n</span> valuations and 2<span style="vertical-align: super;">2^n</span> equivalence classes.</div></body></html>- \ No newline at end of file diff --git a/content/logicsets-notes/Equivalence classes.md b/content/logicsets-notes/Equivalence classes.md @@ -0,0 +1,32 @@ ++++ +title = 'Equivalence classes' +template = 'page-math.html' ++++ +# Equivalence classes +a *binary* relation R is an equivalence relation if for all elements x, y, z in its domain, R satisfies: + +- reflexivity: x R x +- symmetry: x R y ➝ y R x +- transitivity: x R y ∧ y R z ➝ x R z + +an equivalence class consists of all elements x,y for which x R y + +within an equivalence class, all formulas are semantically equivalent + +each equivalence class contains infinitely many formulas + +one class contains all tautologies, another all contradictions (all semantically equivalent) + +for two vars p,q there are as many ≡-equivalence classes as truth tables for p,q — i.e. 16 + +## How many equivalence classes? + +for one variable p, there are two valuations (T or F) +- each valuation has two possible outcomes (T or F) +- therefore, 22 = 4 equivalence classes + +for two variables p,q there are four valuations (T or F for each var) +- each valuation has two possible outcomes (T or F) +- therefore, 24 = 16 equivalence classes + +etc. for n variables, there are $2^n$ valuations and $2^{2^n}$ equivalence classes. diff --git a/content/logicsets-notes/Equivalence relations & classes.html b/content/logicsets-notes/Equivalence relations & classes.html @@ -1,3 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -<html><head><link rel="stylesheet" type="text/css" href="sitewide.css"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)"/><meta name="keywords" content="sets"/><meta name="altitude" content="-1.320224285125732"/><meta name="author" content="Alex Balgavy"/><meta name="created" content="2018-03-08 15:42:52 +0000"/><meta name="latitude" content="52.33416412555773"/><meta name="longitude" content="4.867464486884508"/><meta name="source" content="desktop.mac"/><meta name="updated" content="2018-03-08 16:00:56 +0000"/><title>Equivalence relations & classes</title></head><body><div><b>Equivalence relation in V</b></div><div>relation R of type V × V that satisfies:</div><div><ul><li>reflexivity: x R x</li><li>transitivity: x R y ∧ y R z ➝ x R z</li><li>symmetry: x R y ➝ y R x</li></ul><div><br/></div></div><div><b>Equivalence classes</b></div><div>an equivalence relation ≡ in a set V partitions the set into equivalence classes</div><div><br/></div><div>equivalence class of p:</div><div>[p] = { x ∈ V: p ≡ x },<span> p ∈ V</span></div><div><span><br/></span></div><div><span>all elements of equivalence class relate to each other</span></div><div><span>elements of different equivalence classes are unrelated</span></div><div><span><br/></span></div><div><span>equivalence classes lead to a partition:</span></div><div><span>{ [p] : p ∈ V }</span></div><div><span><br/></span></div><div><span><b>Complete system of representatives</b></span></div><div>for ≡ in V is a set S ⊆ V that contains <i>exactly one </i>element from each equivalence class</div><div>in other words:</div><div><ol><li>every v ∈ V is equivalent to some s ∈ S</li><li>two different elements of S are not equivalent</li></ol><div><br/></div></div><div><br/></div><div><br/></div></body></html>- \ No newline at end of file diff --git a/content/logicsets-notes/Equivalence relations & classes.md b/content/logicsets-notes/Equivalence relations & classes.md @@ -0,0 +1,32 @@ ++++ +title = 'Equivalence relations & classes' ++++ +# Equivalence relations & classes +## Equivalence relation in V +relation R of type V × V that satisfies: + +- reflexivity: x R x +- transitivity: x R y ∧ y R z ➝ x R z +- symmetry: x R y ➝ y R x + +## Equivalence classes + +an equivalence relation ≡ in a set V partitions the set into equivalence classes + +equivalence class of p: +[p] = { x ∈ V: p ≡ x }, p ∈ V + +all elements of equivalence class relate to each other + +elements of different equivalence classes are unrelated + +equivalence classes lead to a partition: +{ [p] : p ∈ V } + +## Complete system of representatives + +for ≡ in V is a set S ⊆ V that contains *exactly one *element from each equivalence class + +in other words: +1. every v ∈ V is equivalent to some s ∈ S +2. two different elements of S are not equivalent diff --git a/content/logicsets-notes/Functional completeness.html b/content/logicsets-notes/Functional completeness.html @@ -1,3 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -<html><head><link rel="stylesheet" type="text/css" href="sitewide.css"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)"/><meta name="keywords" content="logic"/><meta name="altitude" content="-0.05603253096342087"/><meta name="author" content="Alex Balgavy"/><meta name="created" content="2018-02-20 14:35:25 +0000"/><meta name="latitude" content="52.33317063856025"/><meta name="longitude" content="4.865527388414661"/><meta name="source" content="desktop.mac"/><meta name="updated" content="2018-02-20 16:17:14 +0000"/><title>Functional completeness</title></head><body><div>functionally complete — every truth table can be represented by a propositional formula (and vice versa)</div><div><br/></div><div><img src="Functional%20completeness.resources/screenshot.png" height="474" width="702"/><br/></div><div><br/></div><div><span style="font-weight: bold;">Disjunctive normal form (DNF)</span></div><div>this results in a disjunctive normal form (DNF, terms combined with disjunctions)</div><div>a DNF is a clause (disjunction of literals)</div><div><br/></div><div>a DNF is of the form:</div><div><br/></div><div>Ψ<span style="vertical-align: sub;">1</span> ∨ Ψ<span style="vertical-align: sub;">2</span> ∨ … ∨ Ψ<span style="vertical-align: sub;">n</span></div><div><br/></div><div>where Ψ<span style="vertical-align: sub;">i</span> is conjunctions of literals (p, ¬p, etc.)</div><div>a single letter is also a DNF</div><div><br/></div><div><span style="font-weight: bold;">Conjunctive normal form (CNF)</span></div><div>a conjunctive normal form (CNF) is conjunction Ψ<span style="vertical-align: sub; font-size: smaller; font-size: smaller;">1</span> ∧ Ψ<span style="vertical-align: sub; font-size: smaller; font-size: 11.666666030883789px;">2</span><span style="font-size: 11.666666030883789px;"> </span><span style="font-size: 14px;">∧ … ∧ Ψ</span><span style="font-size: smaller; vertical-align: sub; font-size: smaller;">n </span><span style="font-size: 14px;">where Ψ</span><span style="font-size: smaller; vertical-align: sub; font-size: smaller;">i</span><span style="font-size: 14px;"> are disjunctions of literals</span></div><div><span style="font-size: 14px;">disjunctions of literals are clauses (DNF), a CNF is a conjunction of clauses</span></div><div><span style="font-size: 14px;"><br/></span></div><div><img src="Functional%20completeness.resources/screenshot_1.png" height="390" width="601"/></div><div><br/></div><div>Transform any ϕ to CNF using algorithm in three easy steps</div><div><ol><li>IMPL-FREE: eliminate implications</li></ol></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;"><div><div>ϕ ➝ Ψ ≡ ¬ ϕ ∨ Ψ </div></div></blockquote><div><ol start="2"><li>NNF: bring occurrences of ¬ inside, until directly in front of variable (removing double nots)</li></ol></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;"><div><div>¬ (ϕ ∧ Ψ) ≡ ¬ ϕ ∨ ¬ Ψ</div></div><div>¬ (ϕ ∨ Ψ) ≡ ¬ ϕ ∧ ¬ Ψ</div><div>¬ ¬ ϕ ≡ ϕ</div></blockquote><div><div><ol start="3"><li>DISTR: use distributivity law to rearrange conj/disj</li></ol></div></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;"><div><div><div>ϕ ∨ (Ψ ∧ Χ) ≡ (ϕ ∨ Ψ) ∧ (ϕ ∨ Χ)</div></div></div><div>(ϕ ∧ Ψ) ∨ Χ ≡ (ϕ ∨ Χ) ∧ (Ψ ∨ Χ)</div></blockquote><div><ol/></div><ol/><div><br/></div><div>Is a CNF Ψ<sub>1</sub> ∧ Ψ<sub>2</sub> ∧ … ∧ Ψ<sub>n</sub> a tautology?</div><div>Yes, only if in each of clauses Ψ<sub>i</sub> it contains literals p and ¬p for some variable p.</div><div><br/></div><div><b>Satisfiability problem</b></div><div>given a propositional formula ϕ, find a valuation that applied to ϕ yields T.</div><div>NP-complete — no efficient solution has been found</div><div><br/></div><div>DPLL (Davis-Putnam-Logemann-Loveland) procedure:</div><div>checks satisfiability of formula ϕ in CNF.</div><div>T — constant true</div><div>_|_ — constant false</div><div><br/></div><div>applies reduction rules:</div><div><img src="Functional%20completeness.resources/screenshot_2.png" height="161" width="600"/></div><div><br/></div><div>To check satisfiability of CNF ϕ:</div><div><ol><li>Eliminate “unit” clauses</li><ul><li>for clause p of ϕ, replace p in ϕ by T</li><li>for clause ¬ p of ϕ, replace p in ϕ by _|_</li></ul><li>Eliminate “pure” propositional variables</li><ul><li>if p only occurs positively in ϕ, replace all p in ϕ by T</li><li>if p only occurs negatively in ϕ, replace all p in ϕ by _|_</li></ul><li>If ϕ is T, it is satisfiable</li><li>If ϕ is _|_, it is unsatisfiable</li><li>Choose a p in ϕ:</li><ul><li>replace all p in ϕ by T, apply DPLL</li><li>if outcome is “unsatisfiable, replace all p in ϕ by _|_ and apply DPLL again<br/></li></ul></ol></div><div><br/></div></body></html>- \ No newline at end of file diff --git a/content/logicsets-notes/Functional completeness.resources/screenshot_2.png b/content/logicsets-notes/Functional completeness/12e10e38c653f0dd99a23ada6e4f05a1.png Binary files differ. diff --git a/content/logicsets-notes/Functional completeness.resources/screenshot_1.png b/content/logicsets-notes/Functional completeness/3bd83020b473511df602bc0a1820a413.png Binary files differ. diff --git a/content/logicsets-notes/Functional completeness.resources/screenshot.png b/content/logicsets-notes/Functional completeness/8297585d069e3ecfc5a670e14fd18623.png Binary files differ. diff --git a/content/logicsets-notes/Functional completeness/index.md b/content/logicsets-notes/Functional completeness/index.md @@ -0,0 +1,79 @@ ++++ +title = 'Functional completeness' ++++ +# Functional completeness +functionally complete — every truth table can be represented by a propositional formula (and vice versa) + + + +## Disjunctive normal form (DNF) + +this results in a disjunctive normal form (DNF, terms combined with disjunctions) + +a DNF is a clause (disjunction of literals) + +a DNF is of the form: + +Ψ1 ∨ Ψ2 ∨ … ∨ Ψn + +where Ψi is conjunctions of literals (p, ¬p, etc.) + +a single letter is also a DNF + +## Conjunctive normal form (CNF) + +a conjunctive normal form (CNF) is conjunction Ψ1 ∧ Ψ2 ∧ … ∧ Ψn where Ψi are disjunctions of literals + +disjunctions of literals are clauses (DNF), a CNF is a conjunction of clauses + + + +Transform any ϕ to CNF using algorithm in three easy steps +1. IMPL-FREE: eliminate implications +> ϕ ➝ Ψ ≡ ¬ ϕ ∨ Ψ + +1. NNF: bring occurrences of ¬ inside, until directly in front of variable (removing double nots) + +> ¬ (ϕ ∧ Ψ) ≡ ¬ ϕ ∨ ¬ Ψ +> ¬ (ϕ ∨ Ψ) ≡ ¬ ϕ ∧ ¬ Ψ +> ¬ ¬ ϕ ≡ ϕ +1. DISTR: use distributivity law to rearrange conj/disj +> ϕ ∨ (Ψ ∧ Χ) ≡ (ϕ ∨ Ψ) ∧ (ϕ ∨ Χ) +> (ϕ ∧ Ψ) ∨ Χ ≡ (ϕ ∨ Χ) ∧ (Ψ ∨ Χ) + +Is a CNF Ψ1 ∧ Ψ2 ∧ … ∧ Ψn a tautology? + +Yes, only if in each of clauses Ψi it contains literals p and ¬p for some variable p. + +## Satisfiability problem +given a propositional formula ϕ, find a valuation that applied to ϕ yields ⊤. + +NP-complete — no efficient solution has been found + +DPLL (Davis-Putnam-Logemann-Loveland) procedure: +checks satisfiability of formula ϕ in CNF. + +⊤ — constant true + +⊥ — constant false + +applies reduction rules: + + +To check satisfiability of CNF ϕ: +1. Eliminate “unit” clauses + + - for clause p of ϕ, replace p in ϕ by ⊤ + - for clause ¬ p of ϕ, replace p in ϕ by ⊥ + +2. Eliminate “pure” propositional variables + + - if p only occurs positively in ϕ, replace all p in ϕ by ⊤ + - if p only occurs negatively in ϕ, replace all p in ϕ by ⊥ + +3. If ϕ is ⊤, it is satisfiable +4. If ϕ is ⊥, it is unsatisfiable +5. Choose a p in ϕ: + + - replace all p in ϕ by ⊤, apply DPLL + - if outcome is “unsatisfiable, replace all p in ϕ by ⊥ and apply DPLL again diff --git a/content/logicsets-notes/Functions.html b/content/logicsets-notes/Functions.html @@ -1,3 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -<html><head><link rel="stylesheet" type="text/css" href="sitewide.css"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)"/><meta name="keywords" content="sets"/><meta name="altitude" content="-1.53328013420105"/><meta name="author" content="Alex Balgavy"/><meta name="created" content="2018-03-08 16:02:16 +0000"/><meta name="latitude" content="52.3341924041814"/><meta name="longitude" content="4.867576600778637"/><meta name="source" content="desktop.mac"/><meta name="updated" content="2018-03-08 16:31:17 +0000"/><title>Functions</title></head><body><div><span style="font-weight: bold;">Functions</span></div><div>Function f: A ➝ B — binary relation f of type A × B such that every x ∈ A relates to at most one y ∈ B</div><div><ul><li><br/></li><li>domain: all possible input values</li><li>domain of definition: all input values that actually produce defined output</li><li>codomain: what could be the output of a function (like “integers” with f(x)=2x)</li><li>range/image: what actually is the output of a function (like “even numbers” with f(x)=2x)</li></ul><div><br/></div></div><div>injective: if each element x of domain maps to at most one element y of codomain (“one-to-one”)</div><div>surjective: if each element x of domain maps to at least one element y of codomain; the range is the codomain (“onto”)</div><div>total: if the function is defined for all possible input values (domain)</div><div>bijective: if the function is total, injective, and surjective</div><div><br/></div><div><span style="font-weight: bold;">Composition:</span></div><div>(g o f) of f: A ➝ B and g: B ➝ C</div><div><ul><li>D<span style="vertical-align: sub;">gof</span> ⊆ D<span style="vertical-align: sub;">f</span></li><li>R<span style="vertical-align: sub;">gof</span> ⊆ R<span style="vertical-align: sub;">g</span></li></ul><div><br/></div><div><font style="font-size: 14px;"><span style="font-size: 14px; font-weight: bold;">Inverse:</span></font></div></div><div><span style="font-size: 14px;">a function has an inverse only if it’s injective (one-to-one)</span></div><div><br/></div><div><br/></div></body></html>- \ No newline at end of file diff --git a/content/logicsets-notes/Functions.md b/content/logicsets-notes/Functions.md @@ -0,0 +1,29 @@ ++++ +title = 'Functions' +template = 'page-math.html' ++++ +# Functions +Function f: A ➝ B — binary relation f of type A × B such that every x ∈ A relates to at most one y ∈ B + +- domain: all possible input values +- domain of definition: all input values that actually produce defined output +- codomain: what could be the output of a function (like “integers” with f(x)=2x) +- range/image: what actually is the output of a function (like “even numbers” with f(x)=2x) + +injective: if each element x of domain maps to at most one element y of codomain (“one-to-one”) + +surjective: if each element x of domain maps to at least one element y of codomain; the range is the codomain (“onto”) + +total: if the function is defined for all possible input values (domain) + +bijective: if the function is total, injective, and surjective + + +## Composition: +(g o f) of f: A ➝ B and g: B ➝ C + +- $D_{g \circ f} \subseteq D_f$ +- $R_{g \circ f} \subseteq R_g$ + +## Inverse: +a function has an inverse only if it’s injective (one-to-one) diff --git a/content/logicsets-notes/Logic circuits.html b/content/logicsets-notes/Logic circuits.html @@ -1,3 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -<html><head><link rel="stylesheet" type="text/css" href="sitewide.css"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)"/><meta name="keywords" content="logic"/><meta name="altitude" content="-1.502202033996582"/><meta name="author" content="Alex Balgavy"/><meta name="created" content="2018-02-27 15:38:54 +0000"/><meta name="latitude" content="52.33380247189034"/><meta name="longitude" content="4.867544767489887"/><meta name="source" content="desktop.mac"/><meta name="updated" content="2018-02-27 16:01:06 +0000"/><title>Logic circuits</title></head><body><div>Adding in binary arithmetic:</div><div><table style="border-collapse: collapse; min-width: 100%;"><colgroup><col style="width: 223px;"/><col style="width: 404px;"/></colgroup><tbody><tr><td style="border: 1px solid rgb(219, 219, 219); width: 223px; padding: 8px;"><div>Two bits</div><div><img src="Logic%20circuits.resources/screenshot_1.png" height="155" width="235"/><br/></div><div><br/></div><div><img src="Logic%20circuits.resources/screenshot_3.png" height="96" width="179"/><br/></div></td><td style="border: 1px solid rgb(219, 219, 219); width: 404px; padding: 8px;"><div>Two pairs of bits</div><div><img src="Logic%20circuits.resources/screenshot_2.png" height="144" width="280"/><br/></div><div><img src="Logic%20circuits.resources/screenshot_4.png" height="278" width="446"/><br/></div></td></tr></tbody></table><div><br/></div></div><div>Half adder:<br/></div><div><br/></div><div><img src="Logic%20circuits.resources/screenshot.png" height="514" width="703"/><br/></div><div><br/></div><div>Full adder:</div><div><br/></div><div><img src="Logic%20circuits.resources/screenshot_5.png" height="410" width="803"/><br/></div><div><br/></div><div><br/></div><div><br/></div><div><br/></div><div><br/></div><div><br/></div><div><br/></div><div><br/></div></body></html>- \ No newline at end of file diff --git a/content/logicsets-notes/Logic circuits.resources/screenshot_1.png b/content/logicsets-notes/Logic circuits/2d9914a5e9fdb98f9ecfeedf73e8cf21.png Binary files differ. diff --git a/content/logicsets-notes/Logic circuits.resources/screenshot_4.png b/content/logicsets-notes/Logic circuits/8a116670ff579f06b7a0f39bed1aecab.png Binary files differ. diff --git a/content/logicsets-notes/Logic circuits.resources/screenshot_3.png b/content/logicsets-notes/Logic circuits/a69c21cea86d85910a54c75ec7ce325c.png Binary files differ. diff --git a/content/logicsets-notes/Logic circuits.resources/screenshot_2.png b/content/logicsets-notes/Logic circuits/ac03beaec629c5878f8d0f88cf80b9c8.png Binary files differ. diff --git a/content/logicsets-notes/Logic circuits.resources/screenshot_5.png b/content/logicsets-notes/Logic circuits/bc7bf4d10778d096738ae7e5983990dd.png Binary files differ. diff --git a/content/logicsets-notes/Logic circuits.resources/screenshot.png b/content/logicsets-notes/Logic circuits/ee37d8f767487f8a4b820b686ded9d23.png Binary files differ. diff --git a/content/logicsets-notes/Logic circuits/index.md b/content/logicsets-notes/Logic circuits/index.md @@ -0,0 +1,23 @@ ++++ +title = 'Logic circuits' ++++ +# Logic circuits +Adding in binary arithmetic: + +<table> +<tr> +<th>Two bits</th> +<th>Two pairs of bits</th> +</tr> +<tr> +<td><img src="2d9914a5e9fdb98f9ecfeedf73e8cf21.png"/><br><img src="a69c21cea86d85910a54c75ec7ce325c.png"/></td><td><img src="ac03beaec629c5878f8d0f88cf80b9c8.png"/><br><img src="8a116670ff579f06b7a0f39bed1aecab.png"/></td> +</tr> +</table> + +Half adder: + + + +Full adder: + + diff --git a/content/logicsets-notes/Partial orders.html b/content/logicsets-notes/Partial orders.html @@ -1,3 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -<html><head><link rel="stylesheet" type="text/css" href="sitewide.css"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)"/><meta name="keywords" content="sets"/><meta name="altitude" content="-2.172817707061768"/><meta name="author" content="Alex Balgavy"/><meta name="created" content="2018-02-22 14:42:21 +0000"/><meta name="latitude" content="52.33466509195276"/><meta name="longitude" content="4.86638665785288"/><meta name="source" content="desktop.mac"/><meta name="updated" content="2018-02-26 20:46:09 +0000"/><title>Partial orders</title></head><body><div>partial order on V: relation R of type V × V. satisfies reflexivity, anti-symmetry, transitivity</div><div>example: relation ≤ is partial order on N</div><div><ul><li>∀n: n ≤ n (reflexivity)</li><li>∀m, n: m≤n ∧ n≤m ➝ m = n (anti-symmetry)</li><li>∀k, m, n: k≤m ∧ m≤n ➝ k≤n (transitivity)</li></ul><div><br/></div></div><div>example: the relation ⊆ is partial order on P(V)</div><div><ul><li>∀A: A ⊆ A (reflexivity)</li><li>∀A,B: A ⊆ B ∧ A ➝ A = B (anti-symmetry)</li><li>∀A,B,C: A ⊆ B ∧ B ⊆ C ➝ A ⊆ C (transitivity)</li></ul><div><br/></div><div><span style="font-weight: bold;">linear ordering relations</span></div><div>partial order R on set V, then:</div><div><ul><li>x, y ∈ V are <span style="text-decoration: underline;">comparable</span> if x R y or y R x</li><li>R is <span style="text-decoration: underline;">linear/total order</span> if all x,y ∈ V are comparable</li></ul><div><br/></div></div><div>e.g. relation ≤ on N: for all n,m in N — n ≤ m or m ≤ n — <span style="text-decoration: underline;">total</span></div><div>e.g. relation ⊆ on P({1,2}): {1} is not a subset of {2}, {2} is not a subset of {1} — <span style="text-decoration: underline;">not total</span></div><div><br/></div><div><span style="font-weight: bold;">strict partial ordering relations</span></div></div><div>if partial order R on set V, then <span style="text-decoration: underline;">strict partial order</span> S corresponding to R is defined by</div><div>x S y ⟷ x R y and x ≠ y</div><div><br/></div><div>a strict partial order is irreflexive, anti-symmetric, transitive</div><div><br/></div><div><span style="font-weight: bold;">Hasse diagrams</span></div><div>apparently a partial ordering relation is complicated as fuck:</div><div><br/></div><div><img src="Partial%20orders.resources/screenshot.png" height="370" width="617"/><br/></div><div><br/></div><div>so get rid of some arrows and make a Hasse diagram — omit reflexivity and transitivity</div><div>the arrows create chains that split and merge, elements in the same chain are comparable</div><div><br/></div><div><img src="Partial%20orders.resources/screenshot_1.png" height="330" width="434"/><br/></div><div><br/></div><div>Algorithm:</div><div><ol><li>For all x ∈ V — G<span style="vertical-align: sub;">x</span> := {y : y ≠ x and x R y}</li><li>For all x ∈ V — H<span style="vertical-align: sub;">x</span> := G<span style="vertical-align: sub;">x </span>\ {z : z ∈ G<span style="vertical-align: sub;">y</span> for a y ∈ G<span style="vertical-align: sub;">x</span>}</li><li>For all x ∈ V — draw and arrow from x to every y ∈ H<span style="vertical-align: sub;">x</span></li></ol></div><div><br/></div><div><span style="font-size: 14px;">example:</span></div><div><img src="Partial%20orders.resources/screenshot_2.png" height="214" width="475"/><br/></div><div><br/></div><div><span style="font-weight: bold;">Cartesian order on A × B</span></div><div><a<span style="vertical-align: sub;">1</span>, b<span style="vertical-align: sub;">1</span>> ≤ <<span style="font-size: 14px;">a</span><span style="font-size: 14px; vertical-align: sub;">2</span><span style="font-size: 14px;">, b</span><span style="font-size: 14px; vertical-align: sub;">2</span><span style="font-size: 14px;">> ⟷ a1 ≤</span><span style="font-size: 14px; vertical-align: sub;">A</span><span style="font-size: 14px;"> a</span><span style="font-size: 14px; vertical-align: sub;">2</span><span style="font-size: 14px;"> and b</span><span style="font-size: 14px; vertical-align: sub;">1</span><span style="font-size: 14px;"> ≤</span><span style="font-size: 14px; vertical-align: sub;">B</span><span style="font-size: 14px;"> b</span><span style="font-size: 14px; vertical-align: sub;">2</span></div><div>ordered by points, if both are smaller</div><div>cartesian order on A × B is a partial order</div><div><br/></div><div><img src="Partial%20orders.resources/screenshot_3.png" height="241" width="569"/><br/></div><div><br/></div><div><span style="font-weight: bold;">Lexicographic order on A × B</span></div><div><a<span style="font-size: 11.666666030883789px;">1, </span>b<span style="font-size: 14px;">1</span><span style="font-size: 14px;">></span><span style="font-size: 14px;"> ≤ <a2, b2> ⟷ (a1 <A a2) ∨ (a1 = a2 ∧ b1 ≤B b2)</span></div><div>like in a dictionary</div><div>lexicographic order on A× B is a partial order, total if ≤A on A and ≤B on B are total</div><div><br/></div><div><img src="Partial%20orders.resources/screenshot_4.png" height="248" width="610"/><br/></div><div><br/></div><div><span style="font-weight: bold;">Minimal and maximal elements</span></div><div>(V, ≤) is a partially ordered set, A ⊆ V, m ∈ A</div><div><br/></div><div>m is:</div><div><ul><li>largest element of A — if ∀a ∈ A : a ≤ m</li><li>smallest element of A — if ∀a ∈ A : m ≤ a</li><li>maximal element of A — if ∀a ∈ A : (M ≤ a ➝ m = a) — no outgoing arrows on Hasse diagram</li><li>minimal element of A — if ∀a ∈ A : (a ≤ m ➝ a = m) — no incoming arrows on Hasse diagram</li></ul><div><br/></div></div><div>Every maximum of A is a maximal element of A.</div><div>If A has a maximum, it is the only maximal element.</div><div><br/></div><div><br/></div><div><br/></div></body></html>- \ No newline at end of file diff --git a/content/logicsets-notes/Partial orders.resources/screenshot.png b/content/logicsets-notes/Partial orders/2eda764900f11b3ddad4f1040903a76e.png Binary files differ. diff --git a/content/logicsets-notes/Partial orders.resources/screenshot_4.png b/content/logicsets-notes/Partial orders/3303376e4e02317b96c25be114c24644.png Binary files differ. diff --git a/content/logicsets-notes/Partial orders.resources/screenshot_2.png b/content/logicsets-notes/Partial orders/5e55945abe6bf157aa776b75860a0963.png Binary files differ. diff --git a/content/logicsets-notes/Partial orders.resources/screenshot_1.png b/content/logicsets-notes/Partial orders/c05050e0c42af9ad30fd4c47bd1ee899.png Binary files differ. diff --git a/content/logicsets-notes/Partial orders.resources/screenshot_3.png b/content/logicsets-notes/Partial orders/dcc75437f5e4e97d00b4697b6bdc2468.png Binary files differ. diff --git a/content/logicsets-notes/Partial orders/index.md b/content/logicsets-notes/Partial orders/index.md @@ -0,0 +1,85 @@ ++++ +title = 'Partial orders' ++++ +# Partial orders +partial order on V: relation R of type V × V. satisfies reflexivity, anti-symmetry, transitivity + +example: relation ≤ is partial order on N + +- ∀n: n ≤ n (reflexivity) +- ∀m, n: m≤n ∧ n≤m ➝ m = n (anti-symmetry) +- ∀k, m, n: k≤m ∧ m≤n ➝ k≤n (transitivity) + +example: the relation ⊆ is partial order on P(V) + +- ∀A: A ⊆ A (reflexivity) +- ∀A,B: A ⊆ B ∧ A ➝ A = B (anti-symmetry) +- ∀A,B,C: A ⊆ B ∧ B ⊆ C ➝ A ⊆ C (transitivity) + +## linear ordering relations +partial order R on set V, then: + +- x, y ∈ V are _comparable_ if x R y or y R x +- R is _linear/total order_ if all x,y ∈ V are comparable + +e.g. relation ≤ on N: for all n,m in N — n ≤ m or m ≤ n — _total_ + +e.g. relation ⊆ on P({1,2}): {1} is not a subset of {2}, {2} is not a subset of {1} — _not total_ + +## strict partial ordering relations + +if partial order R on set V, then strict partial order S corresponding to R is defined by + +x S y ⟷ x R y and x ≠ y + +a strict partial order is irreflexive, anti-symmetric, transitive + +## Hasse diagrams +apparently a partial ordering relation is complicated as fuck: + + + +so get rid of some arrows and make a Hasse diagram — omit reflexivity and transitivity + +the arrows create chains that split and merge, elements in the same chain are comparable + + + +Algorithm: +1. For all x ∈ V — Gx := {y : y ≠ x and x R y} +2. For all x ∈ V — Hx := Gx \ {z : z ∈ Gy for a y ∈ Gx} +3. For all x ∈ V — draw and arrow from x to every y ∈ Hx + +example: + + +## Cartesian order on A × B +\<a1, b1\> ≤ \<a2, b2\> ⟷ a1 ≤A a2 and b1 ≤B b2 + +ordered by points, if both are smaller + +cartesian order on A × B is a partial order + + + +## Lexicographic order on A × B +\<a1, b1\> ≤ \<a2, b2\> ⟷ (a1 \<A a2) ∨ (a1 = a2 ∧ b1 ≤B b2) + +like in a dictionary + +lexicographic order on A× B is a partial order, total if ≤A on A and ≤B on B are total + + + +## Minimal and maximal elements +(V, ≤) is a partially ordered set, A ⊆ V, m ∈ A + +m is: + +- largest element of A — if ∀a ∈ A : a ≤ m +- smallest element of A — if ∀a ∈ A : m ≤ a +- maximal element of A — if ∀a ∈ A : (M ≤ a ➝ m = a) — no outgoing arrows on Hasse diagram +- minimal element of A — if ∀a ∈ A : (a ≤ m ➝ a = m) — no incoming arrows on Hasse diagram + +Every maximum of A is a maximal element of A. +If A has a maximum, it is the only maximal element. diff --git a/content/logicsets-notes/Predicate Logic.html b/content/logicsets-notes/Predicate Logic.html @@ -1,3 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -<html><head><link rel="stylesheet" type="text/css" href="sitewide.css"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)"/><meta name="keywords" content="logic"/><meta name="altitude" content="-1.601898908615112"/><meta name="author" content="Alex Balgavy"/><meta name="created" content="2018-03-13 15:34:56 +0000"/><meta name="latitude" content="52.33283313851265"/><meta name="longitude" content="4.866307919883771"/><meta name="source" content="desktop.mac"/><meta name="updated" content="2018-03-13 16:02:49 +0000"/><title>Predicate Logic</title></head><body><div><b>Atomic formulas</b></div><div>role of propositional vars p,q,r is taken over by atomic formulas with objects and predicates</div><div><br/></div><div>C(j)</div><div><ul><li>C is a unary predicate symbol</li><li>can mean e.g. Jane (j) is clever (C)</li></ul><div><br/></div></div><div>K(a,b)</div><div><ul><li>K is a binary predicate symbol</li><li>can mean e.g. A knows B</li><li>A and B are objects a and b</li></ul><div><br/></div></div><div><b>Quantifiers</b></div><div>∃x C(x) — somebody is clever</div><div>∀x C(x) — everybody is clever</div><div><br/></div><div>same priority level as for ¬</div><div><br/></div><div><b>Models</b></div><div>if L(r,j) means Robert loves Jane, it holds in M1 but not M2</div><div><br/></div><div><img src="Predicate%20Logic.resources/screenshot.png" height="264" width="725"/></div><div><br/></div><div>meaning/truth value of a formula from predicate logic depends on underlying model M, consisting of:</div><div><ul><li>set A of elements</li><li>interpretation of constants (r, j)</li><li>interpretation of predicate symbols (L, C, K)</li></ul></div><div><br/></div><div>∀x ϕ is true in M if true for <i>every</i> element in A</div><div>∃x ϕ is true in M if true for <i>some</i> element in A</div><div>for each e ∈ A, ϕ [x := e] is true in M</div><div><br/></div><div><b>Semantic entailment</b></div><div>for formula ϕ, M ⊨ ϕ means that ϕ is true in M</div><div>tautology — true in all models</div><div>contradiction — false in all models</div><div>contingent — true in some model, false in another</div><div>satisfiable — true in some model</div><div><br/></div><div><b>Semantic equivalence</b></div><div>if for all models M, <span> </span>M ⊨ ϕ ⟷ M ⊨ Ψ</div><div>then ϕ ≡ Ψ</div><div><br/></div><div>also, given that “nobody is perfect”, this holds:</div><div>¬∃x P(x) ≡ ∀x ¬P(x)</div><div><br/></div><div><b>Alpha conversion</b></div><div>you can rename bound variables like in lambda calc</div><div>∀x C(x) ≡ ∀y C(y)</div></body></html>- \ No newline at end of file diff --git a/content/logicsets-notes/Predicate Logic.resources/screenshot.png b/content/logicsets-notes/Predicate Logic/9732066421db3041336264c0e73649a3.png Binary files differ. diff --git a/content/logicsets-notes/Predicate Logic/index.md b/content/logicsets-notes/Predicate Logic/index.md @@ -0,0 +1,61 @@ ++++ +title = 'Predicate Logic' ++++ +# Predicate Logic +## Atomic formulas + +role of propositional vars p,q,r is taken over by atomic formulas with objects and predicates + +C(j) + +- C is a unary predicate symbol +- can mean e.g. Jane (j) is clever (C) + +K(a,b) + +- K is a binary predicate symbol +- can mean e.g. A knows B +- A and B are objects a and b + +## Quantifiers +∃x C(x) — somebody is clever + +∀x C(x) — everybody is clever + +same priority level as for ¬ + +## Models +if L(r,j) means Robert loves Jane, it holds in M1 but not M2 + + + +meaning/truth value of a formula from predicate logic depends on underlying model M, consisting of: + +- set A of elements +- interpretation of constants (r, j) +- interpretation of predicate symbols (L, C, K) + +∀x ϕ is true in M if true for *every* element in A + +∃x ϕ is true in M if true for *some* element in A + +for each e ∈ A, ϕ [x := e] is true in M + +## Semantic entailment +for formula ϕ, M ⊨ ϕ means that ϕ is true in M + +- tautology — true in all models +- contradiction — false in all models +- contingent — true in some model, false in another +- satisfiable — true in some model + +## Semantic equivalence +1. if for all models M, M ⊨ ϕ ⟷ M ⊨ Ψ +2. then ϕ ≡ Ψ + +also, given that “nobody is perfect”, this holds: +> ¬∃x P(x) ≡ ∀x ¬P(x) + +## Alpha conversion +you can rename bound variables like in lambda calc +> ∀x C(x) ≡ ∀y C(y) diff --git a/content/logicsets-notes/Propositional logic.html b/content/logicsets-notes/Propositional logic.html @@ -1,3 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -<html><head><link rel="stylesheet" type="text/css" href="sitewide.css"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)"/><meta name="keywords" content="logic"/><meta name="created" content="2018-02-06 14:46:07 +0000"/><meta name="updated" content="2018-03-27 15:54:45 +0000"/><title>Propositional logic</title></head><body><div><div>Declarative sentence — true or false</div></div><div>Argument abstraction — If p and not g, then r. Not r. p. Therefore q.</div><div>Argument formalisation: [ ( (p ∧ ¬ q) ➝ r ) ∧ (¬ r ∧ p) ) ] ➝ q</div><div>Symbols: ∧ (and), ∨ (or), ⨁ (xor), ¬ (not), ➝ (implication)</div><div><br/></div><div>Constructing formulae</div><div><ul><li>every propositional variable is a formula</li><li>so is its negation</li><li>so are constructors wit operators</li></ul></div><div><br/></div><div>Symbol priority: negation, then conjunction/disjunction, then implication</div><div><br/></div><div>Types of proposition:</div><div><ul><li>Tautology (p ∨ ¬ p) is always true</li><li>Contradiction (p ∧ ¬ p) is always false</li><li>Contingency is neither a tautology nor a contradiction</li></ul></div><div><br/></div><div>Rules of propositional logic</div><div><ul><li>Implication ϕ ➝ Ψ is </li><ul><li>false if ϕ true and Ψ false</li><li>true otherwise</li></ul><li>Bi-implication ϕ ⟷ Ψ (“ϕ if and only if Ψ”) is </li><ul><li>true if ϕ and Ψ have same truth value</li><li>false otherwise</li></ul></ul></div><div><ul><li>conjunction/disjunction (with conjunction as example)</li><ul><li>p ∧ q ⟷ q ∧ p</li><li>p ∧ (q ∧ r) ⟷ (p ∧ q) ∧ r</li><li>p ∧ (q ∨ r) ⟷ (p ∧ q) ∨ (p ∧ r)</li><li>p ∧ p ⟷ p</li><li>p ∧ (p ∨ q) ⟷ p</li></ul><li>negation</li><ul><li>p ∧ ¬ p ⟷ F</li><li>p ∨ ¬ p ⟷ T</li><li>¬ ¬ p ⟷ p</li></ul><li>demorgan</li><ul><li>¬ p ∧ ¬ q ⟷ ¬ (p ∨ q)</li><li>¬ (p ∧ q) ⟷ ¬ p ∨ ¬ q</li></ul><li>identity</li><ul><li>disjunction</li><ul><li>p ∨ T ⟷ T</li><li>p ∨ F ⟷ p</li></ul><li>conjunction</li><ul><li>p ∧ T ⟷ p</li><li>p ∧ F ⟷ F</li></ul></ul><li>implication</li><ul><li>p ➝ q == ¬ p ∨ q</li></ul></ul></div><div><br/></div></body></html>- \ No newline at end of file diff --git a/content/logicsets-notes/Propositional logic.md b/content/logicsets-notes/Propositional logic.md @@ -0,0 +1,54 @@ ++++ +title = 'Propositional logic' ++++ + +# Propositional logic +- Declarative sentence: true or false +- Argument abstraction: If p and not g, then r. Not r. p. Therefore q. +- Argument formalisation: [ ( (p ∧ ¬ q) ➝ r ) ∧ (¬ r ∧ p) ) ] ➝ q +- Symbols: ∧ (and), ∨ (or), ⨁ (xor), ¬ (not), ➝ (implication) + +Constructing formulae + +- every propositional variable is a formula +- so is its negation +- so are constructors wit operators + +Symbol priority: negation, then conjunction/disjunction, then implication + +Types of proposition: + +- Tautology (p ∨ ¬ p) is always true +- Contradiction (p ∧ ¬ p) is always false +- Contingency is neither a tautology nor a contradiction + +Rules of propositional logic + +- Implication ϕ ➝ Ψ is + - false if ϕ true and Ψ false + - true otherwise +- Bi-implication ϕ ⟷ Ψ (“ϕ if and only if Ψ”) is + - true if ϕ and Ψ have same truth value + - false otherwise +- conjunction/disjunction (with conjunction as example) + - p ∧ q ⟷ q ∧ p + - p ∧ (q ∧ r) ⟷ (p ∧ q) ∧ r + - p ∧ (q ∨ r) ⟷ (p ∧ q) ∨ (p ∧ r) + - p ∧ p ⟷ p + - p ∧ (p ∨ q) ⟷ p +- negation + - p ∧ ¬ p ⟷ F + - p ∨ ¬ p ⟷ T + - ¬ ¬ p ⟷ p +- demorgan + - ¬ p ∧ ¬ q ⟷ ¬ (p ∨ q) + - ¬ (p ∧ q) ⟷ ¬ p ∨ ¬ q +- identity + - disjunction + - p ∨ T ⟷ T + - p ∨ F ⟷ p + - conjunction + - p ∧ T ⟷ p + - p ∧ F ⟷ F +- implication + - p ➝ q == ¬ p ∨ q diff --git a/content/logicsets-notes/Relations.html b/content/logicsets-notes/Relations.html @@ -1,3 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -<html><head><link rel="stylesheet" type="text/css" href="sitewide.css"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)"/><meta name="keywords" content="sets"/><meta name="altitude" content="-1.882289528846741"/><meta name="author" content="Alex Balgavy"/><meta name="created" content="2018-02-15 14:42:35 +0000"/><meta name="latitude" content="52.33467867860909"/><meta name="longitude" content="4.866408472356967"/><meta name="source" content="desktop.mac"/><meta name="updated" content="2018-02-15 16:13:50 +0000"/><title>Relations</title></head><body><div><b>Cartesian product of sets</b></div><div><br/></div><div>A × B := {<a,b> : a ∈ A ∩ b ∈ B}</div><div>A × A := A<sup>2</sup></div><div><sup><br/></sup></div><div>#(A×B) = #A ⋅ #B</div><div><br/></div><div><b>Binary relation:</b> relation of type A × B or A × A</div><div><b>Relation in set A:</b> relation of type A × A</div><div><br/></div><div><b>Infix notation:</b></div><div>x R y — <x, y> ∈ R</div><div><br/></div><div><br/></div><div><b>Visualisation</b></div><div>directed graphs & matrix:</div><div><br/></div><div><br/></div><div><img src="Relations.resources/screenshot_2.png" height="301" width="619"/></div><div><br/></div><div>Venn diagrams & matrix:</div><div><br/></div><div><img src="Relations.resources/screenshot_1.png" height="301" width="627"/></div><div><br/></div><div><b>Inverse of binary relation</b></div><div>Inverse of R: R<sup>-1</sup> := {<x,y> : <y,x> ∈ R}</div><div>R ⊆ A × B => R<sup>-1</sup> ⊆ B × A</div><div><br/></div><div>For Venn diagrams, you reverse the arrows.</div><div><br/></div><div><b>Composite relations</b></div><div>R ∘ S := {<x,z> : x S y ∩ y R z for some y}</div><div><br/></div><div><img src="Relations.resources/screenshot_3.png" height="209" width="644"/></div><div><br/></div><div>Composition is associative.</div><div>Inverse: (R ∘ S)<sup style="font-size: 11.666666030883789px;">-1</sup><span style="font-size: 11.666666030883789px;"> </span><font style="font-size: 14px;">= S<sup>-1</sup> ∘ R<sup>-1</sup></font></div><div><font style="font-size: 14px;"><sup><br/></sup></font></div><div><font style="font-size: 14px;"><b>Properties of relations</b></font></div><div><img src="Relations.resources/screenshot.png" height="372" width="635"/></div><div><img src="Relations.resources/screenshot_4.png" height="372" width="635"/></div><div><br/></div></body></html>- \ No newline at end of file diff --git a/content/logicsets-notes/Relations.resources/screenshot_3.png b/content/logicsets-notes/Relations/22dc5693b6ce96c68d71fc69d2f9d0d8.png Binary files differ. diff --git a/content/logicsets-notes/Relations.resources/screenshot.png b/content/logicsets-notes/Relations/565aefaad582e4e41d23e0d0c072b464.png Binary files differ. diff --git a/content/logicsets-notes/Relations.resources/screenshot_4.png b/content/logicsets-notes/Relations/5dfd0a52a1c98207ba2d5b7cfdb10f97.png Binary files differ. diff --git a/content/logicsets-notes/Relations.resources/screenshot_1.png b/content/logicsets-notes/Relations/6e00283393a5ecb2b30c10ee0adc206a.png Binary files differ. diff --git a/content/logicsets-notes/Relations.resources/screenshot_2.png b/content/logicsets-notes/Relations/976a431a1cc75280f0fd2bca62a722da.png Binary files differ. diff --git a/content/logicsets-notes/Relations/index.md b/content/logicsets-notes/Relations/index.md @@ -0,0 +1,47 @@ ++++ +title = 'Relations' ++++ +# Relations +## Cartesian product of sets + +A × B := {<a,b> : a ∈ A ∩ b ∈ B} + +A × A := A2 + +#(A×B) = #A ⋅ #B + +**Binary relation:** relation of type A × B or A × A + +**Relation in set A:** relation of type A × A + +## Infix notation: +x R y — <x, y> ∈ R + +## Visualisation +directed graphs & matrix: + + + +Venn diagrams & matrix: + + + +## Inverse of binary relation +Inverse of R: R-1 := {<x,y> : <y,x> ∈ R} + +R ⊆ A × B => R-1 ⊆ B × A + +For Venn diagrams, you reverse the arrows. + +## Composite relations +R ∘ S := {<x,z> : x S y ∩ y R z for some y} + + + +Composition is associative. + +Inverse: (R ∘ S)-1 = S-1 ∘ R-1 + +## Properties of relations + + diff --git a/content/logicsets-notes/Semantic entailment.html b/content/logicsets-notes/Semantic entailment.html @@ -1,3 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -<html><head><link rel="stylesheet" type="text/css" href="sitewide.css"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)"/><meta name="keywords" content="logic"/><meta name="created" content="2018-02-13 14:40:36 +0000"/><meta name="updated" content="2018-03-27 15:53:19 +0000"/><title>Semantic entailment</title></head><body><div>ϕ₁, …, ϕ<span style="vertical-align: sub;">n </span>⊨<span style="vertical-align: sub;" />Ψ</div><div><br/></div><div>A formula Ψ is semantically entailed by premises (ϕ₁, …, ϕ<span style="vertical-align: sub;">n</span>) if every valuation that makes premises true makes Ψ true.</div><div><br/></div><div>counterexample makes premises true but not conclusion</div><div><br/></div><div>if ϕ ⊨ Ψ and Ψ ⊨ ϕ, ϕ ≡ Ψ </div><div><img src="Semantic%20entailment.resources/screenshot.png" height="203" width="825"/><br/></div><div><img src="Semantic%20entailment.resources/screenshot_1.png" height="236" width="824"/><br/></div><div><br/></div></body></html>- \ No newline at end of file diff --git a/content/logicsets-notes/Semantic entailment.resources/screenshot.png b/content/logicsets-notes/Semantic entailment/11bb7fc4feb2fffc9faa39267a68a701.png Binary files differ. diff --git a/content/logicsets-notes/Semantic entailment.resources/screenshot_1.png b/content/logicsets-notes/Semantic entailment/b0e73f3474b3ae38b7ea5452e14d53e3.png Binary files differ. diff --git a/content/logicsets-notes/Semantic entailment/index.md b/content/logicsets-notes/Semantic entailment/index.md @@ -0,0 +1,14 @@ ++++ +title = 'Semantic entailment' ++++ +# Semantic entailment +ϕ₁, …, ϕn ⊨ Ψ + +A formula Ψ is semantically entailed by premises (ϕ₁, …, ϕn) if every valuation that makes premises true makes Ψ true. + +counterexample makes premises true but not conclusion + +if ϕ ⊨ Ψ and Ψ ⊨ ϕ, ϕ ≡ Ψ + + + diff --git a/content/logicsets-notes/Universal & Existential quantification.html b/content/logicsets-notes/Universal & Existential quantification.html @@ -1,3 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -<html><head><link rel="stylesheet" type="text/css" href="sitewide.css"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)"/><meta name="keywords" content="logic"/><meta name="altitude" content="-1.32824182510376"/><meta name="author" content="Alex Balgavy"/><meta name="created" content="2018-03-06 15:59:00 +0000"/><meta name="latitude" content="52.33302833890655"/><meta name="longitude" content="4.86553639720129"/><meta name="source" content="desktop.mac"/><meta name="updated" content="2018-03-06 16:15:09 +0000"/><title>Universal & Existential quantification</title></head><body><div><span style="font-weight: bold;">Universal</span></div><div>∀x ϕ — for all values of x, ϕ is true</div><div>∀x x — contradiction</div><div><br/></div><div>in propositional logic:</div><div>∀x ϕ ≡ ϕ<span style="vertical-align: sub;">1</span> ∧ ϕ<span style="vertical-align: sub;">0</span></div><div><br/></div><div><span style="font-weight: bold;">Existential</span></div><div>∃x ϕ — there exists a value of x where ϕ is true</div><div>∃x x — tautology</div><div><br/></div><div>in propositional logic:</div><div>∃x ϕ ≡ ϕ<sub>1</sub> ∨ ϕ<sub>0</sub></div><div><sub><br/></sub></div><div>Build OBDDs using the propositional logic versions. Compute the variables and then take conjunction (∀) or disjunction (∃).</div><div><br/></div><div><br/></div></body></html>- \ No newline at end of file diff --git a/content/logicsets-notes/Universal & Existential quantification.md b/content/logicsets-notes/Universal & Existential quantification.md @@ -0,0 +1,23 @@ ++++ +title = 'Universal & Existential quantification' ++++ +# Universal & Existential quantification +## Universal +∀x ϕ — for all values of x, ϕ is true + +∀x x — contradiction + +in propositional logic: + +∀x ϕ ≡ ϕ1 ∧ ϕ0 + +## Existential +∃x ϕ — there exists a value of x where ϕ is true + +∃x x — tautology + +in propositional logic: + +∃x ϕ ≡ ϕ1 ∨ ϕ0 + +Build OBDDs using the propositional logic versions. Compute the variables and then take conjunction (∀) or disjunction (∃). diff --git a/content/logicsets-notes/_index.md b/content/logicsets-notes/_index.md @@ -0,0 +1,35 @@ ++++ +title = 'Logic & Sets' ++++ +# Logic & Sets +Logic: + +1. [Propositional logic](propositional-logic) + +2. [Semantic entailment](semantic-entailment) + +3. [Adequate systems of connectives](adequate-systems-of-connectives) + +4. [Functional completeness](functional-completeness) — CNF, DNF, Satisfiability & DPLL + +5. [Logic circuits](logic-circuits) + +6. [Binary Decision Trees](binary-decision-trees), OBDD + +7. [Universal & Existential quantification](universal-existential-quantification) + +8. [Predicate Logic](predicate-logic) + +Sets + +1. [Relations](relations) + +2. [Partial orders](partial-orders) + +3. [Equivalence classes](equivalence-classes) + +4. [Equivalence relations & classes](equivalence-relations-classes) + +5. [Cardinality](cardinality) + +6. [Functions](functions) diff --git a/content/logicsets-notes/index.html b/content/logicsets-notes/index.html @@ -1,49 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -<html> - -<head><link rel="stylesheet" type="text/css" href="sitewide.css"> - <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> - <meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)" /> - <meta name="altitude" content="-1.627367734909058" /> - <meta name="author" content="Alex Balgavy" /> - <meta name="created" content="2018-03-12 14:37:30 +0000" /> - <meta name="latitude" content="52.33370100163172" /> - <meta name="longitude" content="4.867379630557172" /> - <meta name="source" content="desktop.mac" /> - <meta name="updated" content="2018-03-27 15:56:31 +0000" /> - <title>Logic & Sets</title> -</head> - -<body> - <nav> -<a href="http://thezeroalpha.github.io">Homepage</a> -</nav> - - <h1>Logic & Sets</h1> - <h3>Alex Balgavy, 2018</h3> - <div>Logic:</div> - <ol> - <li><a href="Propositional%20logic.html">Propositional logic</a></li> - <li><a href="Semantic%20entailment.html">Semantic entailment</a></li> - <li><a href="Adequate%20systems%20of%20connectives.html">Adequate systems of connectives</a></li> - <li><a href="Functional%20completeness.html">Functional completeness</a> — CNF, DNF, Satisfiability & DPLL</li> - <li><a href="Logic%20circuits.html">Logic circuits</a></li> - <li><a href="Binary%20Decision%20Trees.html">Binary Decision Trees</a>, OBDD</li> - <li><a href="Universal%20&%20Existential%20quantification.html">Universal & Existential quantification</a></li> - <li><a href="Predicate%20Logic.html">Predicate Logic</a></li> - </ol> - <div><br/></div> - <div>Sets</div> - <ol> - <li><a href="Relations.html">Relations</a></li> - <li><a href="Partial%20orders.html">Partial orders</a></li> - <li><a href="Equivalence%20classes.html">Equivalence classes</a></li> - <li><a href="Equivalence%20relations%20&%20classes.html">Equivalence relations &amp; classes</a></li> - <li><a href="Cardinality.html">Cardinality</a></li> - <li><a href="Functions.html">Functions</a></li> - </ol> - <div><br/></div> -</body> - -</html> diff --git a/content/logicsets-notes/sitewide.css b/content/logicsets-notes/sitewide.css @@ -1,30 +0,0 @@ -@charset 'UTF-8'; -@font-face{font-family:'FontAwesome';src:url('font/fontawesome-webfont.eot?v=4.0.1');src:url('font/fontawesome-webfont.eot?#iefix&v=4.0.1') format('embedded-opentype'),url('font/fontawesome-webfont.woff?v=4.0.1') format('woff'),url('font/fontawesome-webfont.ttf?v=4.0.1') format('truetype'),url('font/fontawesome-webfont.svg?v=4.0.1#fontawesomeregular') format('svg');font-weight:normal;font-style:normal} - -body { - margin: 0px; - padding: 1em; - background: #f3f2ed; - font-family: 'Lato', sans-serif; - font-size: 12pt; - font-weight: 300; - color: #8A8A8A; - padding-left: 50px; -} -h1, h2, h3 { - margin: 0px; - padding: 0px; - font-weight: 300; - text-align: center; -} -h3 { - font-style: italic; -} -a { - color: #D1551F; - } - - strong { - font-weight: 700; - color: #2A2A2A; - }- \ No newline at end of file
