commit 02fa111555aa61d9781330ad100046114aa634b3
parent 4e6d289ddd682159630c342e404487d0c9f668db
Author: Alex Balgavy <alex@balgavy.eu>
Date: Fri, 11 Feb 2022 16:27:02 +0100
Update advanced logic notes
Diffstat:
7 files changed, 551 insertions(+), 0 deletions(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md
@@ -4,3 +4,8 @@ title = 'Advanced Logic'
# Advanced Logic
1. [Lecture 1](lecture-1)
2. [Lecture 2](lecture-2)
+3. [Exercise 1](exercise-1)
+
+I drew the graphs on these pages with [Graphviz](https://graphviz.org/).
+You can install Graphviz and run e.g. `dot < graph.dot -Tsvg > graph.svg` (also accepts input files as parameters).
+Or you can install [PlantUML](https://plantuml.com/), surround the code with `@startdot...@enddot`, and run `plantuml -p -Tsvg < graph.puml > graph.svg`.
diff --git a/content/advanced-logic-notes/exercise-1/fifth.svg b/content/advanced-logic-notes/exercise-1/fifth.svg
@@ -0,0 +1,150 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
+ "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<!-- Generated by graphviz version 2.50.0 (20211204.2007)
+ -->
+<!-- Title: g Pages: 1 -->
+<svg width="402pt" height="347pt"
+ viewBox="0.00 0.00 402.29 347.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
+<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 343)">
+<title>g</title>
+<polygon fill="white" stroke="transparent" points="-4,4 -4,-343 398.29,-343 398.29,4 -4,4"/>
+<!-- root -->
+<g id="node1" class="node">
+<title>root</title>
+<ellipse fill="none" stroke="black" cx="265.49" cy="-306" rx="67.69" ry="18"/>
+<text text-anchor="middle" x="265.49" y="-302.3" font-family="Times,serif" font-size="14.00">M, 1 ⊨ ◇ □ ◇ p</text>
+<text text-anchor="middle" x="175.9" y="-327.8" font-family="Times,serif" font-size="14.00">Turn: V</text>
+</g>
+<!-- l11 -->
+<g id="node2" class="node">
+<title>l11</title>
+<ellipse fill="none" stroke="black" cx="196.49" cy="-234" rx="59.59" ry="18"/>
+<text text-anchor="middle" x="196.49" y="-230.3" font-family="Times,serif" font-size="14.00">M, 4 ⊨ □ ◇ p</text>
+<text text-anchor="middle" x="115.7" y="-255.8" font-family="Times,serif" font-size="14.00">Turn: F</text>
+</g>
+<!-- root->l11 -->
+<g id="edge1" class="edge">
+<title>root->l11</title>
+<path fill="none" stroke="black" d="M249.14,-288.41C240.38,-279.52 229.43,-268.41 219.79,-258.63"/>
+<polygon fill="black" stroke="black" points="222.24,-256.13 212.73,-251.47 217.26,-261.05 222.24,-256.13"/>
+</g>
+<!-- r11 -->
+<g id="node3" class="node">
+<title>r11</title>
+<ellipse fill="none" stroke="black" cx="334.49" cy="-234" rx="59.59" ry="18"/>
+<text text-anchor="middle" x="334.49" y="-230.3" font-family="Times,serif" font-size="14.00">M, 3 ⊨ □ ◇ p</text>
+<text text-anchor="middle" x="253.7" y="-255.8" font-family="Times,serif" font-size="14.00">Turn: F</text>
+</g>
+<!-- root->r11 -->
+<g id="edge2" class="edge">
+<title>root->r11</title>
+<path fill="none" stroke="black" d="M281.85,-288.41C290.61,-279.52 301.56,-268.41 311.2,-258.63"/>
+<polygon fill="black" stroke="black" points="313.73,-261.05 318.26,-251.47 308.75,-256.13 313.73,-261.05"/>
+</g>
+<!-- r21 -->
+<g id="node4" class="node">
+<title>r21</title>
+<ellipse fill="none" stroke="black" cx="196.49" cy="-162" rx="51.99" ry="18"/>
+<text text-anchor="middle" x="196.49" y="-158.3" font-family="Times,serif" font-size="14.00">M, 3 ⊨ ◇ p</text>
+<text text-anchor="middle" x="122.5" y="-183.8" font-family="Times,serif" font-size="14.00">Turn: V</text>
+</g>
+<!-- l11->r21 -->
+<g id="edge11" class="edge">
+<title>l11->r21</title>
+<path fill="none" stroke="black" d="M196.49,-215.7C196.49,-207.98 196.49,-198.71 196.49,-190.11"/>
+<polygon fill="black" stroke="black" points="199.99,-190.1 196.49,-180.1 192.99,-190.1 199.99,-190.1"/>
+</g>
+<!-- r11->r21 -->
+<g id="edge3" class="edge">
+<title>r11->r21</title>
+<path fill="none" stroke="black" d="M305.23,-218.15C284.37,-207.57 256.16,-193.26 233.7,-181.87"/>
+<polygon fill="black" stroke="black" points="235.28,-178.75 224.78,-177.35 232.11,-184.99 235.28,-178.75"/>
+</g>
+<!-- r22 -->
+<g id="node9" class="node">
+<title>r22</title>
+<ellipse fill="none" stroke="black" cx="334.49" cy="-162" rx="51.99" ry="18"/>
+<text text-anchor="middle" x="334.49" y="-158.3" font-family="Times,serif" font-size="14.00">M, 2 ⊨ ◇ p</text>
+<text text-anchor="middle" x="260.5" y="-183.8" font-family="Times,serif" font-size="14.00">Turn: V</text>
+</g>
+<!-- r11->r22 -->
+<g id="edge8" class="edge">
+<title>r11->r22</title>
+<path fill="none" stroke="black" d="M334.49,-215.7C334.49,-207.98 334.49,-198.71 334.49,-190.11"/>
+<polygon fill="black" stroke="black" points="337.99,-190.1 334.49,-180.1 330.99,-190.1 337.99,-190.1"/>
+</g>
+<!-- r31 -->
+<g id="node5" class="node">
+<title>r31</title>
+<ellipse fill="none" stroke="black" cx="72.49" cy="-90" rx="46.29" ry="18"/>
+<text text-anchor="middle" x="72.49" y="-86.3" font-family="Times,serif" font-size="14.00">M, 2 ⊨ p.</text>
+</g>
+<!-- r21->r31 -->
+<g id="edge4" class="edge">
+<title>r21->r31</title>
+<path fill="none" stroke="black" d="M170.5,-146.33C151.9,-135.83 126.69,-121.59 106.49,-110.19"/>
+<polygon fill="black" stroke="black" points="108.04,-107.04 97.61,-105.18 104.6,-113.14 108.04,-107.04"/>
+</g>
+<!-- r32 -->
+<g id="node7" class="node">
+<title>r32</title>
+<ellipse fill="none" stroke="black" cx="196.49" cy="-90" rx="46.29" ry="18"/>
+<text text-anchor="middle" x="196.49" y="-86.3" font-family="Times,serif" font-size="14.00">M, 3 ⊨ p.</text>
+</g>
+<!-- r21->r32 -->
+<g id="edge6" class="edge">
+<title>r21->r32</title>
+<path fill="none" stroke="black" d="M196.49,-143.7C196.49,-135.98 196.49,-126.71 196.49,-118.11"/>
+<polygon fill="black" stroke="black" points="199.99,-118.1 196.49,-108.1 192.99,-118.1 199.99,-118.1"/>
+</g>
+<!-- r41 -->
+<g id="node6" class="node">
+<title>r41</title>
+<ellipse fill="none" stroke="black" cx="58.49" cy="-18" rx="58.49" ry="18"/>
+<text text-anchor="middle" x="58.49" y="-14.3" font-family="Times,serif" font-size="14.00">Verifier wins.</text>
+</g>
+<!-- r31->r41 -->
+<g id="edge5" class="edge">
+<title>r31->r41</title>
+<path fill="none" stroke="black" d="M69.03,-71.7C67.49,-63.98 65.64,-54.71 63.92,-46.11"/>
+<polygon fill="black" stroke="black" points="67.31,-45.22 61.92,-36.1 60.44,-46.6 67.31,-45.22"/>
+</g>
+<!-- r42 -->
+<g id="node8" class="node">
+<title>r42</title>
+<ellipse fill="none" stroke="black" cx="196.49" cy="-18" rx="61.19" ry="18"/>
+<text text-anchor="middle" x="196.49" y="-14.3" font-family="Times,serif" font-size="14.00">Falsifier wins.</text>
+</g>
+<!-- r32->r42 -->
+<g id="edge7" class="edge">
+<title>r32->r42</title>
+<path fill="none" stroke="black" d="M196.49,-71.7C196.49,-63.98 196.49,-54.71 196.49,-46.11"/>
+<polygon fill="black" stroke="black" points="199.99,-46.1 196.49,-36.1 192.99,-46.1 199.99,-46.1"/>
+</g>
+<!-- r33 -->
+<g id="node10" class="node">
+<title>r33</title>
+<ellipse fill="none" stroke="black" cx="334.49" cy="-90" rx="46.29" ry="18"/>
+<text text-anchor="middle" x="334.49" y="-86.3" font-family="Times,serif" font-size="14.00">M, 1 ⊨ p.</text>
+</g>
+<!-- r22->r33 -->
+<g id="edge9" class="edge">
+<title>r22->r33</title>
+<path fill="none" stroke="black" d="M334.49,-143.7C334.49,-135.98 334.49,-126.71 334.49,-118.11"/>
+<polygon fill="black" stroke="black" points="337.99,-118.1 334.49,-108.1 330.99,-118.1 337.99,-118.1"/>
+</g>
+<!-- r43 -->
+<g id="node11" class="node">
+<title>r43</title>
+<ellipse fill="none" stroke="black" cx="334.49" cy="-18" rx="58.49" ry="18"/>
+<text text-anchor="middle" x="334.49" y="-14.3" font-family="Times,serif" font-size="14.00">Verifier wins.</text>
+</g>
+<!-- r33->r43 -->
+<g id="edge10" class="edge">
+<title>r33->r43</title>
+<path fill="none" stroke="black" d="M334.49,-71.7C334.49,-63.98 334.49,-54.71 334.49,-46.11"/>
+<polygon fill="black" stroke="black" points="337.99,-46.1 334.49,-36.1 330.99,-46.1 337.99,-46.1"/>
+</g>
+</g>
+</svg>
diff --git a/content/advanced-logic-notes/exercise-1/first.svg b/content/advanced-logic-notes/exercise-1/first.svg
@@ -0,0 +1,44 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
+ "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<!-- Generated by graphviz version 2.50.0 (20211204.2007)
+ -->
+<!-- Title: g Pages: 1 -->
+<svg width="242pt" height="59pt"
+ viewBox="0.00 0.00 242.00 59.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
+<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 55)">
+<title>g</title>
+<polygon fill="white" stroke="transparent" points="-4,4 -4,-55 238,-55 238,4 -4,4"/>
+<!-- 2 -->
+<g id="node1" class="node">
+<title>2</title>
+<ellipse fill="none" stroke="black" cx="117" cy="-33" rx="27" ry="18"/>
+<text text-anchor="middle" x="117" y="-29.3" font-family="Times,serif" font-size="14.00">2</text>
+<text text-anchor="middle" x="86.5" y="-3.8" font-family="Times,serif" font-size="14.00">p</text>
+</g>
+<!-- 3 -->
+<g id="node3" class="node">
+<title>3</title>
+<ellipse fill="none" stroke="black" cx="207" cy="-33" rx="27" ry="18"/>
+<text text-anchor="middle" x="207" y="-29.3" font-family="Times,serif" font-size="14.00">3</text>
+</g>
+<!-- 2->3 -->
+<g id="edge2" class="edge">
+<title>2->3</title>
+<path fill="none" stroke="black" d="M144.4,-33C152.39,-33 161.31,-33 169.82,-33"/>
+<polygon fill="black" stroke="black" points="169.92,-36.5 179.92,-33 169.92,-29.5 169.92,-36.5"/>
+</g>
+<!-- 1 -->
+<g id="node2" class="node">
+<title>1</title>
+<ellipse fill="none" stroke="black" cx="27" cy="-33" rx="27" ry="18"/>
+<text text-anchor="middle" x="27" y="-29.3" font-family="Times,serif" font-size="14.00">1</text>
+</g>
+<!-- 1->2 -->
+<g id="edge1" class="edge">
+<title>1->2</title>
+<path fill="none" stroke="black" d="M54.4,-33C62.39,-33 71.31,-33 79.82,-33"/>
+<polygon fill="black" stroke="black" points="79.92,-36.5 89.92,-33 79.92,-29.5 79.92,-36.5"/>
+</g>
+</g>
+</svg>
diff --git a/content/advanced-logic-notes/exercise-1/fourth.svg b/content/advanced-logic-notes/exercise-1/fourth.svg
@@ -0,0 +1,75 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
+ "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<!-- Generated by graphviz version 2.50.0 (20211204.2007)
+ -->
+<!-- Title: g Pages: 1 -->
+<svg width="98pt" height="275pt"
+ viewBox="0.00 0.00 98.00 275.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
+<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 271)">
+<title>g</title>
+<polygon fill="white" stroke="transparent" points="-4,4 -4,-271 94,-271 94,4 -4,4"/>
+<!-- 1 -->
+<g id="node1" class="node">
+<title>1</title>
+<ellipse fill="none" stroke="black" cx="45" cy="-234" rx="27" ry="18"/>
+<text text-anchor="middle" x="45" y="-230.3" font-family="Times,serif" font-size="14.00">1</text>
+<text text-anchor="middle" x="14.5" y="-255.8" font-family="Times,serif" font-size="14.00">p</text>
+</g>
+<!-- 3 -->
+<g id="node3" class="node">
+<title>3</title>
+<ellipse fill="none" stroke="black" cx="27" cy="-90" rx="27" ry="18"/>
+<text text-anchor="middle" x="27" y="-86.3" font-family="Times,serif" font-size="14.00">3</text>
+</g>
+<!-- 1->3 -->
+<g id="edge1" class="edge">
+<title>1->3</title>
+<path fill="none" stroke="black" d="M31.25,-218.07C23.04,-208.1 13.38,-194.25 9,-180 2.58,-159.12 8.38,-134.77 15.06,-116.82"/>
+<polygon fill="black" stroke="black" points="18.4,-117.9 18.9,-107.32 11.91,-115.28 18.4,-117.9"/>
+</g>
+<!-- 4 -->
+<g id="node4" class="node">
+<title>4</title>
+<ellipse fill="none" stroke="black" cx="45" cy="-162" rx="27" ry="18"/>
+<text text-anchor="middle" x="45" y="-158.3" font-family="Times,serif" font-size="14.00">4</text>
+</g>
+<!-- 1->4 -->
+<g id="edge2" class="edge">
+<title>1->4</title>
+<path fill="none" stroke="black" d="M45,-215.7C45,-207.98 45,-198.71 45,-190.11"/>
+<polygon fill="black" stroke="black" points="48.5,-190.1 45,-180.1 41.5,-190.1 48.5,-190.1"/>
+</g>
+<!-- 2 -->
+<g id="node2" class="node">
+<title>2</title>
+<ellipse fill="none" stroke="black" cx="63" cy="-18" rx="27" ry="18"/>
+<text text-anchor="middle" x="63" y="-14.3" font-family="Times,serif" font-size="14.00">2</text>
+<text text-anchor="middle" x="32.5" y="-39.8" font-family="Times,serif" font-size="14.00">p</text>
+</g>
+<!-- 2->1 -->
+<g id="edge3" class="edge">
+<title>2->1</title>
+<path fill="none" stroke="black" d="M70.29,-35.82C74.33,-46.06 78.94,-59.54 81,-72 88.82,-119.36 95.11,-134.12 81,-180 77.71,-190.69 71.46,-201.15 65.07,-209.92"/>
+<polygon fill="black" stroke="black" points="62.12,-208.02 58.75,-218.07 67.65,-212.31 62.12,-208.02"/>
+</g>
+<!-- 3->2 -->
+<g id="edge4" class="edge">
+<title>3->2</title>
+<path fill="none" stroke="black" d="M35.35,-72.76C39.71,-64.28 45.15,-53.71 50.04,-44.2"/>
+<polygon fill="black" stroke="black" points="53.23,-45.64 54.7,-35.15 47.01,-42.44 53.23,-45.64"/>
+</g>
+<!-- 3->3 -->
+<g id="edge5" class="edge">
+<title>3->3</title>
+<path fill="none" stroke="black" d="M46.9,-102.43C59.69,-105.68 72,-101.53 72,-90 72,-81.62 65.5,-77.14 57.04,-76.56"/>
+<polygon fill="black" stroke="black" points="56.5,-73.1 46.9,-77.57 57.19,-80.07 56.5,-73.1"/>
+</g>
+<!-- 4->3 -->
+<g id="edge6" class="edge">
+<title>4->3</title>
+<path fill="none" stroke="black" d="M40.64,-144.05C38.61,-136.14 36.14,-126.54 33.86,-117.69"/>
+<polygon fill="black" stroke="black" points="37.2,-116.6 31.32,-107.79 30.42,-118.35 37.2,-116.6"/>
+</g>
+</g>
+</svg>
diff --git a/content/advanced-logic-notes/exercise-1/index.md b/content/advanced-logic-notes/exercise-1/index.md
@@ -0,0 +1,178 @@
++++
+title = 'Exercise class 1'
++++
+# Exercise class 1
+## Universal validity examples
+- □ φ → ◇ φ
+
+ Not universally valid, see model with one point & no relations.
+ Has □ p but not ◇ p.
+
+- ◇ φ → □ φ
+
+ Not universally valid.
+
+ Counterexample:
+ - W = {1,2}. R = {(1,1), (1,2)}. V(p) = {1}.
+ - Show ◇ p → □ p.
+ - (W,R),V,1 ⊨ ◇ p because R11 and 1 ⊨ p.
+ - But 1 ⊭ □ p because R12 and 2 ⊭ p.
+ - So not universally valid.
+
+- □ p → □ □ p
+
+ No.
+ Counterexample when left side of implication holds but right does not:
+
+ 
+
+ <details>
+ <summary>Dot code</summary>
+
+ ```dot
+ digraph g {
+ rankdir="LR"
+ 2 [label="2", xlabel="p"]
+ 1 -> 2
+ 2 -> 3
+ }
+ ```
+
+ </details>
+
+- ¬ □ p → □ ¬ □ p
+
+ No.
+ Counterexample:
+
+ 
+
+ <details>
+ <summary>Dot code</summary>
+
+ ```dot
+ digraph g {
+ rankdir="LR"
+ 3 [label="3", xlabel="p"]
+ 1 -> 2
+ 2 -> 3
+ }
+ ```
+
+ </details>
+
+## 1
+### 1a
+W = {a₁...a₇}. R = {(a₁, a₂), (a₁, a₃), ...}. V(p) = {a₁, a₂...}, V(q) = {a₂, a₃...}.
+
+Valuation can also be written as V(a₁) = {p}, etc.
+
+### 1b
+#### 1b i
+M, a₁ ⊨ □ □ (p ∨ q)
+- R[a₁] = {a₂, a₃, a₄} (the successors of a₁).
+- Holds by looking at the picture.
+
+#### 1b ii
+M, a₂ ⊨ ◇ q → ◇ ◇ q
+- R[a₂] = {a₅}.
+- Since a₅ ⊭ q, then a₂ ⊭ ◇ q.
+- So formula holds because ◇ q doesn't hold. <!-- TODO: really? -->
+
+### 1d
+Change V by making p true in all states.
+
+## 3
+### 3a
+⊨ □ (p → q) → (◇ p → ◇ q)
+- Take an arbitrary pointed model (W,R),V,x.
+- Assume x ⊨ □ (p → q), aim to show x ⊨ ◇ p → ◇ q.
+- Assume x ⊨ ◇ p, aim to show x ⊨ ◇ q.
+- x ⊨ ◇ p so x has a successor: there is y ∈ W such that y ⊨ p and Rxy.
+- Because Rxy, we have x ⊨ ◇ q.
+- So x ⊨ ◇ p → ◇ q.
+- So x ⊨ □ (p → q) → (◇ p → ◇ q).
+- Because x is arbitrary, the formula is universally valid.
+
+Remember: □ φ is true if no successor, ◇ φ is false if no successor.
+
+### 3b
+⊨ □ (p ∧ q) → (◇ p ∧ ◇ q)
+- Not valid with a singleton state and no relations. Premise is true, but not the right-hand side.
+
+### 3c
+□ (□ p → p) → □ p
+
+No.
+Counterexample:
+
+
+
+<details>
+<summary>Dot code</summary>
+
+```dot
+digraph g {
+ rankdir="LR"
+ 1 -> 2
+ 2 -> 3
+ 3 -> 4
+}
+```
+
+</details>
+
+## 4
+First, draw a picture:
+
+
+
+<details>
+<summary>Dot code</summary>
+
+```dot
+digraph g {
+ 1 [label="1", xlabel="p"]
+ 2 [label="2", xlabel="p"]
+ 1 -> 3
+ 1 -> 4
+ 2 -> 1
+ 3 -> 2
+ 3 -> 3
+ 4 -> 3
+}
+```
+
+</details>
+
+Then, create a tree:
+
+
+
+<details>
+<summary>Dot code</summary>
+
+```dot
+digraph g {
+ root [label="M, 1 ⊨ ◇ □ ◇ p", xlabel="Turn: V"]
+ l11 [label="M, 4 ⊨ □ ◇ p", xlabel="Turn: F"]; root -> l11
+ r11 [label="M, 3 ⊨ □ ◇ p", xlabel="Turn: F"]; root -> r11
+
+ // right branch
+ r21 [label="M, 3 ⊨ ◇ p", xlabel="Turn: V"]; r11 -> r21
+ r31 [label="M, 2 ⊨ p."]; r21 -> r31; r31 -> r41; r41 [label="Verifier wins."]
+ r32 [label="M, 3 ⊨ p."]; r21 -> r32; r32 -> r42; r42 [label="Falsifier wins."]
+
+ r22 [label="M, 2 ⊨ ◇ p", xlabel="Turn: V"]; r11 -> r22
+ r33 [label="M, 1 ⊨ p."]; r22 -> r33; r33 -> r43; r43 [label="Verifier wins."]
+
+ // left branch
+ l11 -> r21
+}
+```
+
+</details>
+
+We cannot influence falsifier here since we play as verifier (trying to show that it hols).
+But no matter what falsifier does, verifier has a winning strategy.
+
diff --git a/content/advanced-logic-notes/exercise-1/second.svg b/content/advanced-logic-notes/exercise-1/second.svg
@@ -0,0 +1,44 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
+ "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<!-- Generated by graphviz version 2.50.0 (20211204.2007)
+ -->
+<!-- Title: g Pages: 1 -->
+<svg width="242pt" height="59pt"
+ viewBox="0.00 0.00 242.00 59.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
+<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 55)">
+<title>g</title>
+<polygon fill="white" stroke="transparent" points="-4,4 -4,-55 238,-55 238,4 -4,4"/>
+<!-- 3 -->
+<g id="node1" class="node">
+<title>3</title>
+<ellipse fill="none" stroke="black" cx="207" cy="-33" rx="27" ry="18"/>
+<text text-anchor="middle" x="207" y="-29.3" font-family="Times,serif" font-size="14.00">3</text>
+<text text-anchor="middle" x="176.5" y="-3.8" font-family="Times,serif" font-size="14.00">p</text>
+</g>
+<!-- 1 -->
+<g id="node2" class="node">
+<title>1</title>
+<ellipse fill="none" stroke="black" cx="27" cy="-33" rx="27" ry="18"/>
+<text text-anchor="middle" x="27" y="-29.3" font-family="Times,serif" font-size="14.00">1</text>
+</g>
+<!-- 2 -->
+<g id="node3" class="node">
+<title>2</title>
+<ellipse fill="none" stroke="black" cx="117" cy="-33" rx="27" ry="18"/>
+<text text-anchor="middle" x="117" y="-29.3" font-family="Times,serif" font-size="14.00">2</text>
+</g>
+<!-- 1->2 -->
+<g id="edge1" class="edge">
+<title>1->2</title>
+<path fill="none" stroke="black" d="M54.4,-33C62.39,-33 71.31,-33 79.82,-33"/>
+<polygon fill="black" stroke="black" points="79.92,-36.5 89.92,-33 79.92,-29.5 79.92,-36.5"/>
+</g>
+<!-- 2->3 -->
+<g id="edge2" class="edge">
+<title>2->3</title>
+<path fill="none" stroke="black" d="M144.4,-33C152.39,-33 161.31,-33 169.82,-33"/>
+<polygon fill="black" stroke="black" points="169.92,-36.5 179.92,-33 169.92,-29.5 169.92,-36.5"/>
+</g>
+</g>
+</svg>
diff --git a/content/advanced-logic-notes/exercise-1/third.svg b/content/advanced-logic-notes/exercise-1/third.svg
@@ -0,0 +1,55 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
+ "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<!-- Generated by graphviz version 2.50.0 (20211204.2007)
+ -->
+<!-- Title: g Pages: 1 -->
+<svg width="332pt" height="44pt"
+ viewBox="0.00 0.00 332.00 44.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
+<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 40)">
+<title>g</title>
+<polygon fill="white" stroke="transparent" points="-4,4 -4,-40 328,-40 328,4 -4,4"/>
+<!-- 1 -->
+<g id="node1" class="node">
+<title>1</title>
+<ellipse fill="none" stroke="black" cx="27" cy="-18" rx="27" ry="18"/>
+<text text-anchor="middle" x="27" y="-14.3" font-family="Times,serif" font-size="14.00">1</text>
+</g>
+<!-- 2 -->
+<g id="node2" class="node">
+<title>2</title>
+<ellipse fill="none" stroke="black" cx="117" cy="-18" rx="27" ry="18"/>
+<text text-anchor="middle" x="117" y="-14.3" font-family="Times,serif" font-size="14.00">2</text>
+</g>
+<!-- 1->2 -->
+<g id="edge1" class="edge">
+<title>1->2</title>
+<path fill="none" stroke="black" d="M54.4,-18C62.39,-18 71.31,-18 79.82,-18"/>
+<polygon fill="black" stroke="black" points="79.92,-21.5 89.92,-18 79.92,-14.5 79.92,-21.5"/>
+</g>
+<!-- 3 -->
+<g id="node3" class="node">
+<title>3</title>
+<ellipse fill="none" stroke="black" cx="207" cy="-18" rx="27" ry="18"/>
+<text text-anchor="middle" x="207" y="-14.3" font-family="Times,serif" font-size="14.00">3</text>
+</g>
+<!-- 2->3 -->
+<g id="edge2" class="edge">
+<title>2->3</title>
+<path fill="none" stroke="black" d="M144.4,-18C152.39,-18 161.31,-18 169.82,-18"/>
+<polygon fill="black" stroke="black" points="169.92,-21.5 179.92,-18 169.92,-14.5 169.92,-21.5"/>
+</g>
+<!-- 4 -->
+<g id="node4" class="node">
+<title>4</title>
+<ellipse fill="none" stroke="black" cx="297" cy="-18" rx="27" ry="18"/>
+<text text-anchor="middle" x="297" y="-14.3" font-family="Times,serif" font-size="14.00">4</text>
+</g>
+<!-- 3->4 -->
+<g id="edge3" class="edge">
+<title>3->4</title>
+<path fill="none" stroke="black" d="M234.4,-18C242.39,-18 251.31,-18 259.82,-18"/>
+<polygon fill="black" stroke="black" points="259.92,-21.5 269.92,-18 259.92,-14.5 259.92,-21.5"/>
+</g>
+</g>
+</svg>
