commit f5ca5df8b25870b6768905a5f77c4c1a8c598012 parent 6aea3a00fa9ab5db4634c2d2f8cbdec7f5b6e17d Author: Alex Balgavy <alex@balgavy.eu> Date: Sat, 26 Feb 2022 19:45:30 +0100 Exercise class 3 Diffstat:
15 files changed, 785 insertions(+), 7 deletions(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md @@ -2,12 +2,13 @@ title = 'Advanced Logic' +++ # Advanced Logic -1. [Lecture 1](lecture-1) -2. [Lecture 2](lecture-2) -3. [Exercise 1](exercise-1) -4. [Lecture 3](lecture-3) -5. [Lecture 4](lecture-4) +1. [Lecture 1](lecture-1/) +2. [Lecture 2](lecture-2/) +3. [Exercise 1](exercise-1/) +4. [Lecture 3](lecture-3/) +5. [Lecture 4](lecture-4/) +6. [Exercise 3](exercise-3/) -I drew the graphs on these pages with [Graphviz](https://graphviz.org/). +I drew the graphs on these pages with [Graphviz](https://graphviz.org/), I used [vim-literate-markdown](https://github.com/thezeroalpha/vim-literate-markdown)'s tangling functionality to quickly extract graph code to separate files. 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/index.md b/content/advanced-logic-notes/exercise-1/index.md @@ -77,7 +77,7 @@ M, a₁ ⊨ □ □ (p ∨ q) M, a₂ ⊨ ◇ q → ◇ ◇ q - R[a₂] = {a₅}. - Since a₅ ⊭ q, then a₂ ⊭ ◇ q. -- So formula holds because ◇ q doesn't hold. <!-- TODO: really? --> +- So formula holds because ◇ q doesn't hold. ### 1d Change V by making p true in all states. diff --git a/content/advanced-logic-notes/exercise-3/1-model-k.dot b/content/advanced-logic-notes/exercise-3/1-model-k.dot @@ -0,0 +1,8 @@ +digraph g { +rankdir=LR +1 -> 2 +2 -> 3 +3 -> 1 +1 -> 4 +} + diff --git a/content/advanced-logic-notes/exercise-3/1-model-k.dot.svg b/content/advanced-logic-notes/exercise-3/1-model-k.dot.svg @@ -0,0 +1,61 @@ +<?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="111pt" + viewBox="0.00 0.00 242.00 110.98" 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 106.98)"> +<title>g</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-106.98 238,-106.98 238,4 -4,4"/> +<!-- 1 --> +<g id="node1" class="node"> +<title>1</title> +<ellipse fill="none" stroke="black" cx="27" cy="-30.98" rx="27" ry="18"/> +<text text-anchor="middle" x="27" y="-27.28" 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="-84.98" rx="27" ry="18"/> +<text text-anchor="middle" x="117" y="-81.28" 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="M47.53,-42.96C59.38,-50.24 74.7,-59.64 87.84,-67.7"/> +<polygon fill="black" stroke="black" points="86.17,-70.78 96.52,-73.03 89.83,-64.82 86.17,-70.78"/> +</g> +<!-- 4 --> +<g id="node4" class="node"> +<title>4</title> +<ellipse fill="none" stroke="black" cx="117" cy="-30.98" rx="27" ry="18"/> +<text text-anchor="middle" x="117" y="-27.28" font-family="Times,serif" font-size="14.00">4</text> +</g> +<!-- 1->4 --> +<g id="edge4" class="edge"> +<title>1->4</title> +<path fill="none" stroke="black" d="M54.4,-30.98C62.39,-30.98 71.31,-30.98 79.82,-30.98"/> +<polygon fill="black" stroke="black" points="79.92,-34.48 89.92,-30.98 79.92,-27.48 79.92,-34.48"/> +</g> +<!-- 3 --> +<g id="node3" class="node"> +<title>3</title> +<ellipse fill="none" stroke="black" cx="207" cy="-34.98" rx="27" ry="18"/> +<text text-anchor="middle" x="207" y="-31.28" 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="M137.97,-73.63C149.48,-67.1 164.15,-58.76 176.92,-51.51"/> +<polygon fill="black" stroke="black" points="178.84,-54.44 185.81,-46.45 175.38,-48.35 178.84,-54.44"/> +</g> +<!-- 3->1 --> +<g id="edge3" class="edge"> +<title>3->1</title> +<path fill="none" stroke="black" d="M187.06,-22.62C175.22,-15.64 159.34,-7.6 144,-3.98 120.64,1.53 113.5,0.91 90,-3.98 78.94,-6.28 67.43,-10.67 57.38,-15.25"/> +<polygon fill="black" stroke="black" points="55.74,-12.15 48.24,-19.64 58.77,-18.46 55.74,-12.15"/> +</g> +</g> +</svg> diff --git a/content/advanced-logic-notes/exercise-3/1-model-m.dot b/content/advanced-logic-notes/exercise-3/1-model-m.dot @@ -0,0 +1,8 @@ +digraph g { +rankdir=LR +a -> b +a -> c +c -> a +c -> d +} + diff --git a/content/advanced-logic-notes/exercise-3/1-model-m.dot.svg b/content/advanced-logic-notes/exercise-3/1-model-m.dot.svg @@ -0,0 +1,61 @@ +<?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="98pt" + viewBox="0.00 0.00 242.00 98.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 94)"> +<title>g</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-94 238,-94 238,4 -4,4"/> +<!-- a --> +<g id="node1" class="node"> +<title>a</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">a</text> +</g> +<!-- b --> +<g id="node2" class="node"> +<title>b</title> +<ellipse fill="none" stroke="black" cx="117" cy="-72" rx="27" ry="18"/> +<text text-anchor="middle" x="117" y="-68.3" font-family="Times,serif" font-size="14.00">b</text> +</g> +<!-- a->b --> +<g id="edge1" class="edge"> +<title>a->b</title> +<path fill="none" stroke="black" d="M47.53,-29.98C59.38,-37.26 74.7,-46.66 87.84,-54.72"/> +<polygon fill="black" stroke="black" points="86.17,-57.8 96.52,-60.05 89.83,-51.84 86.17,-57.8"/> +</g> +<!-- c --> +<g id="node3" class="node"> +<title>c</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">c</text> +</g> +<!-- a->c --> +<g id="edge2" class="edge"> +<title>a->c</title> +<path fill="none" stroke="black" d="M52.51,-11.88C61.4,-11.27 71.62,-11.1 81.22,-11.38"/> +<polygon fill="black" stroke="black" points="81.16,-14.88 91.31,-11.86 81.49,-7.89 81.16,-14.88"/> +</g> +<!-- c->a --> +<g id="edge3" class="edge"> +<title>c->a</title> +<path fill="none" stroke="black" d="M91.31,-24.14C82.41,-24.74 72.18,-24.9 62.59,-24.61"/> +<polygon fill="black" stroke="black" points="62.67,-21.11 52.51,-24.12 62.33,-28.1 62.67,-21.11"/> +</g> +<!-- d --> +<g id="node4" class="node"> +<title>d</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">d</text> +</g> +<!-- c->d --> +<g id="edge4" class="edge"> +<title>c->d</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> +</g> +</svg> diff --git a/content/advanced-logic-notes/exercise-3/5-1-tableau.dot b/content/advanced-logic-notes/exercise-3/5-1-tableau.dot @@ -0,0 +1,6 @@ +graph g { +a [label="* ◇ ¬ p ∨ ◇ p", xlabel="1"] +a -- b +b [label="* ◇ ¬ p, ◇ p", xlabel="1"] +} + diff --git a/content/advanced-logic-notes/exercise-3/5-1-tableau.dot.svg b/content/advanced-logic-notes/exercise-3/5-1-tableau.dot.svg @@ -0,0 +1,32 @@ +<?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="135pt" height="131pt" + viewBox="0.00 0.00 134.59 131.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 127)"> +<title>g</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-127 130.59,-127 130.59,4 -4,4"/> +<!-- a --> +<g id="node1" class="node"> +<title>a</title> +<ellipse fill="none" stroke="black" cx="66.79" cy="-90" rx="59.59" ry="18"/> +<text text-anchor="middle" x="66.79" y="-86.3" font-family="Times,serif" font-size="14.00">* ◇ ¬ p ∨ ◇ p</text> +<text text-anchor="middle" x="3.5" y="-111.8" font-family="Times,serif" font-size="14.00">1</text> +</g> +<!-- b --> +<g id="node2" class="node"> +<title>b</title> +<ellipse fill="none" stroke="black" cx="66.79" cy="-18" rx="54.69" ry="18"/> +<text text-anchor="middle" x="66.79" y="-14.3" font-family="Times,serif" font-size="14.00">* ◇ ¬ p, ◇ p</text> +<text text-anchor="middle" x="8.7" y="-39.8" font-family="Times,serif" font-size="14.00">1</text> +</g> +<!-- a--b --> +<g id="edge1" class="edge"> +<title>a--b</title> +<path fill="none" stroke="black" d="M66.79,-71.7C66.79,-60.85 66.79,-46.92 66.79,-36.1"/> +</g> +</g> +</svg> diff --git a/content/advanced-logic-notes/exercise-3/5-2-tableau.dot b/content/advanced-logic-notes/exercise-3/5-2-tableau.dot @@ -0,0 +1,12 @@ +graph g { +a [label="* ◇ (p ∧ ¬ q), ◇ ¬ p, ¬ ◇ ¬ q", xlabel="1"] +b [label="◇ ¬ q * ◇ (p ∧ ¬ q), ◇ ¬ p", xlabel="1"]; a -- b +c [label="¬ q * p ∧ ¬ q, ¬ p", xlabel="2"]; b -- c [style="dashed"] +d [label="p * p ∧ ¬ q, q", xlabel="2"]; c -- d + +el [shape="record", label="{ p * p, q | closes. }", xlabel="2"]; d -- el + +er [label="p * ¬ q, q", xlabel="2"]; d -- er +f [shape="record", label="{ p, q * q | closes. }", xlabel="2"]; er -- f +} + diff --git a/content/advanced-logic-notes/exercise-3/5-2-tableau.dot.svg b/content/advanced-logic-notes/exercise-3/5-2-tableau.dot.svg @@ -0,0 +1,96 @@ +<?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="246pt" height="441pt" + viewBox="0.00 0.00 246.38 441.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 437)"> +<title>g</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-437 242.38,-437 242.38,4 -4,4"/> +<!-- a --> +<g id="node1" class="node"> +<title>a</title> +<ellipse fill="none" stroke="black" cx="122.69" cy="-400" rx="115.88" ry="18"/> +<text text-anchor="middle" x="122.69" y="-396.3" font-family="Times,serif" font-size="14.00">* ◇ (p ∧ ¬ q), ◇ ¬ p, ¬ ◇ ¬ q</text> +<text text-anchor="middle" x="3.5" y="-421.8" font-family="Times,serif" font-size="14.00">1</text> +</g> +<!-- b --> +<g id="node2" class="node"> +<title>b</title> +<ellipse fill="none" stroke="black" cx="122.69" cy="-328" rx="105.08" ry="18"/> +<text text-anchor="middle" x="122.69" y="-324.3" font-family="Times,serif" font-size="14.00">◇ ¬ q * ◇ (p ∧ ¬ q), ◇ ¬ p</text> +<text text-anchor="middle" x="13.9" y="-349.8" font-family="Times,serif" font-size="14.00">1</text> +</g> +<!-- a--b --> +<g id="edge1" class="edge"> +<title>a--b</title> +<path fill="none" stroke="black" d="M122.69,-381.7C122.69,-370.85 122.69,-356.92 122.69,-346.1"/> +</g> +<!-- c --> +<g id="node3" class="node"> +<title>c</title> +<ellipse fill="none" stroke="black" cx="122.69" cy="-256" rx="76.09" ry="18"/> +<text text-anchor="middle" x="122.69" y="-252.3" font-family="Times,serif" font-size="14.00">¬ q * p ∧ ¬ q, ¬ p</text> +<text text-anchor="middle" x="43.15" y="-277.8" font-family="Times,serif" font-size="14.00">2</text> +</g> +<!-- b--c --> +<g id="edge2" class="edge"> +<title>b--c</title> +<path fill="none" stroke="black" stroke-dasharray="5,2" d="M122.69,-309.7C122.69,-298.85 122.69,-284.92 122.69,-274.1"/> +</g> +<!-- d --> +<g id="node4" class="node"> +<title>d</title> +<ellipse fill="none" stroke="black" cx="122.69" cy="-184" rx="60.39" ry="18"/> +<text text-anchor="middle" x="122.69" y="-180.3" font-family="Times,serif" font-size="14.00">p * p ∧ ¬ q, q</text> +<text text-anchor="middle" x="58.75" y="-205.8" font-family="Times,serif" font-size="14.00">2</text> +</g> +<!-- c--d --> +<g id="edge3" class="edge"> +<title>c--d</title> +<path fill="none" stroke="black" d="M122.69,-237.7C122.69,-226.85 122.69,-212.92 122.69,-202.1"/> +</g> +<!-- el --> +<g id="node5" class="node"> +<title>el</title> +<polygon fill="none" stroke="black" points="46.19,-83.5 46.19,-129.5 105.19,-129.5 105.19,-83.5 46.19,-83.5"/> +<text text-anchor="middle" x="75.69" y="-114.3" font-family="Times,serif" font-size="14.00">p * p, q</text> +<polyline fill="none" stroke="black" points="46.19,-106.5 105.19,-106.5 "/> +<text text-anchor="middle" x="75.69" y="-91.3" font-family="Times,serif" font-size="14.00">closes.</text> +<text text-anchor="middle" x="42.69" y="-133.8" font-family="Times,serif" font-size="14.00">2</text> +</g> +<!-- d--el --> +<g id="edge4" class="edge"> +<title>d--el</title> +<path fill="none" stroke="black" d="M112.26,-166.24C105.55,-155.47 96.76,-141.35 89.48,-129.66"/> +</g> +<!-- er --> +<g id="node6" class="node"> +<title>er</title> +<ellipse fill="none" stroke="black" cx="169.69" cy="-106.5" rx="46.29" ry="18"/> +<text text-anchor="middle" x="169.69" y="-102.8" font-family="Times,serif" font-size="14.00">p * ¬ q, q</text> +<text text-anchor="middle" x="120.04" y="-128.3" font-family="Times,serif" font-size="14.00">2</text> +</g> +<!-- d--er --> +<g id="edge5" class="edge"> +<title>d--er</title> +<path fill="none" stroke="black" d="M133.12,-166.24C140.91,-153.73 151.51,-136.71 159.29,-124.21"/> +</g> +<!-- f --> +<g id="node7" class="node"> +<title>f</title> +<polygon fill="none" stroke="black" points="140.19,-0.5 140.19,-46.5 199.19,-46.5 199.19,-0.5 140.19,-0.5"/> +<text text-anchor="middle" x="169.69" y="-31.3" font-family="Times,serif" font-size="14.00">p, q * q</text> +<polyline fill="none" stroke="black" points="140.19,-23.5 199.19,-23.5 "/> +<text text-anchor="middle" x="169.69" y="-8.3" font-family="Times,serif" font-size="14.00">closes.</text> +<text text-anchor="middle" x="136.69" y="-50.8" font-family="Times,serif" font-size="14.00">2</text> +</g> +<!-- er--f --> +<g id="edge6" class="edge"> +<title>er--f</title> +<path fill="none" stroke="black" d="M169.69,-88.32C169.69,-76.15 169.69,-59.73 169.69,-46.59"/> +</g> +</g> +</svg> diff --git a/content/advanced-logic-notes/exercise-3/5-3-counter-model.dot b/content/advanced-logic-notes/exercise-3/5-3-counter-model.dot @@ -0,0 +1,6 @@ +digraph g { +rankdir=LR +1 -> 2; 2 [shape="Mrecord", label="{2 | p}"] +1 -> 3 +} + diff --git a/content/advanced-logic-notes/exercise-3/5-3-counter-model.dot.svg b/content/advanced-logic-notes/exercise-3/5-3-counter-model.dot.svg @@ -0,0 +1,45 @@ +<?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="152pt" height="100pt" + viewBox="0.00 0.00 152.00 99.50" 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 95.5)"> +<title>g</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-95.5 148,-95.5 148,4 -4,4"/> +<!-- 1 --> +<g id="node1" class="node"> +<title>1</title> +<ellipse fill="none" stroke="black" cx="27" cy="-45" rx="27" ry="18"/> +<text text-anchor="middle" x="27" y="-41.3" font-family="Times,serif" font-size="14.00">1</text> +</g> +<!-- 2 --> +<g id="node2" class="node"> +<title>2</title> +<path fill="none" stroke="black" d="M102,-55C102,-55 132,-55 132,-55 138,-55 144,-61 144,-67 144,-67 144,-79 144,-79 144,-85 138,-91 132,-91 132,-91 102,-91 102,-91 96,-91 90,-85 90,-79 90,-79 90,-67 90,-67 90,-61 96,-55 102,-55"/> +<text text-anchor="middle" x="103.5" y="-69.3" font-family="Times,serif" font-size="14.00">2</text> +<polyline fill="none" stroke="black" points="117,-55 117,-91 "/> +<text text-anchor="middle" x="130.5" y="-69.3" font-family="Times,serif" font-size="14.00">p</text> +</g> +<!-- 1->2 --> +<g id="edge1" class="edge"> +<title>1->2</title> +<path fill="none" stroke="black" d="M51.58,-52.5C60.35,-55.29 70.5,-58.52 80.12,-61.58"/> +<polygon fill="black" stroke="black" points="79.28,-64.99 89.87,-64.69 81.4,-58.32 79.28,-64.99"/> +</g> +<!-- 3 --> +<g id="node3" class="node"> +<title>3</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">3</text> +</g> +<!-- 1->3 --> +<g id="edge2" class="edge"> +<title>1->3</title> +<path fill="none" stroke="black" d="M52.05,-37.62C61.44,-34.74 72.36,-31.39 82.5,-28.28"/> +<polygon fill="black" stroke="black" points="83.75,-31.55 92.29,-25.28 81.7,-24.86 83.75,-31.55"/> +</g> +</g> +</svg> diff --git a/content/advanced-logic-notes/exercise-3/5-3-tableau.dot b/content/advanced-logic-notes/exercise-3/5-3-tableau.dot @@ -0,0 +1,20 @@ +graph g { +a [label="* (¬ ◇ ¬ p ∧ ◇ ¬ q), ¬ ◇ (p ∧ ¬ q)", xlabel="1"] +b [label="◇ (p ∧ ¬ q) * ¬ ◇ ¬ p ∧ ◇ ¬ q", xlabel="1"]; a -- b + +la [label="◇ (p ∧ ¬ q) * ¬ ◇ ¬ p", xlabel="1"]; a -- la +lb [label="◇ (p ∧ ¬ q), ◇ ¬ p *", xlabel="1"]; la -- lb + +lla [label="p ∧ ¬ q *", xlabel="2"]; lb -- lla [style="dashed"] +llb [label="p, ¬ q *", xlabel="2"]; lla -- llb +llc [label="{p * q | does not close}", xlabel="2", shape="record"]; llb -- llc + +lra [label="{¬ p * | does not close}", xlabel="3", shape="record"]; lb -- lra [style="dashed"] + +ra [label="◇ (p ∧ ¬ q) * ◇ ¬ q", xlabel="1"]; b -- ra +rb [label="p ∧ ¬ q * ¬ q", xlabel="4"]; ra -- rb [style="dashed"] +rc [label="p ∧ ¬ q, q *", xlabel="4"]; rb -- rc +rd [label="p, ¬ q, q *", xlabel="4"]; rc -- rd +re [label="{p, q * q | closes}", xlabel="4", shape="record"]; rd -- re +} + diff --git a/content/advanced-logic-notes/exercise-3/5-3-tableau.dot.svg b/content/advanced-logic-notes/exercise-3/5-3-tableau.dot.svg @@ -0,0 +1,170 @@ +<?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="462pt" height="524pt" + viewBox="0.00 0.00 462.29 524.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 520)"> +<title>g</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-520 458.29,-520 458.29,4 -4,4"/> +<!-- a --> +<g id="node1" class="node"> +<title>a</title> +<ellipse fill="none" stroke="black" cx="237.29" cy="-483" rx="134.58" ry="18"/> +<text text-anchor="middle" x="237.29" y="-479.3" font-family="Times,serif" font-size="14.00">* (¬ ◇ ¬ p ∧ ◇ ¬ q), ¬ ◇ (p ∧ ¬ q)</text> +<text text-anchor="middle" x="99.25" y="-504.8" font-family="Times,serif" font-size="14.00">1</text> +</g> +<!-- b --> +<g id="node2" class="node"> +<title>b</title> +<ellipse fill="none" stroke="black" cx="125.29" cy="-411" rx="118.08" ry="18"/> +<text text-anchor="middle" x="125.29" y="-407.3" font-family="Times,serif" font-size="14.00">◇ (p ∧ ¬ q) * ¬ ◇ ¬ p ∧ ◇ ¬ q</text> +<text text-anchor="middle" x="3.5" y="-432.8" font-family="Times,serif" font-size="14.00">1</text> +</g> +<!-- a--b --> +<g id="edge1" class="edge"> +<title>a--b</title> +<path fill="none" stroke="black" d="M210.46,-465.23C192.73,-454.15 169.58,-439.68 151.9,-428.63"/> +</g> +<!-- la --> +<g id="node3" class="node"> +<title>la</title> +<ellipse fill="none" stroke="black" cx="350.29" cy="-411" rx="88.28" ry="18"/> +<text text-anchor="middle" x="350.29" y="-407.3" font-family="Times,serif" font-size="14.00">◇ (p ∧ ¬ q) * ¬ ◇ ¬ p</text> +<text text-anchor="middle" x="258.4" y="-432.8" font-family="Times,serif" font-size="14.00">1</text> +</g> +<!-- a--la --> +<g id="edge2" class="edge"> +<title>a--la</title> +<path fill="none" stroke="black" d="M264.36,-465.23C282.38,-454.07 305.94,-439.47 323.83,-428.39"/> +</g> +<!-- ra --> +<g id="node9" class="node"> +<title>ra</title> +<ellipse fill="none" stroke="black" cx="125.29" cy="-339" rx="80.69" ry="18"/> +<text text-anchor="middle" x="125.29" y="-335.3" font-family="Times,serif" font-size="14.00">◇ (p ∧ ¬ q) * ◇ ¬ q</text> +<text text-anchor="middle" x="41.2" y="-360.8" font-family="Times,serif" font-size="14.00">1</text> +</g> +<!-- b--ra --> +<g id="edge8" class="edge"> +<title>b--ra</title> +<path fill="none" stroke="black" d="M125.29,-392.7C125.29,-381.85 125.29,-367.92 125.29,-357.1"/> +</g> +<!-- lb --> +<g id="node4" class="node"> +<title>lb</title> +<ellipse fill="none" stroke="black" cx="350.29" cy="-339" rx="83.39" ry="18"/> +<text text-anchor="middle" x="350.29" y="-335.3" font-family="Times,serif" font-size="14.00">◇ (p ∧ ¬ q), ◇ ¬ p *</text> +<text text-anchor="middle" x="263.6" y="-360.8" font-family="Times,serif" font-size="14.00">1</text> +</g> +<!-- la--lb --> +<g id="edge3" class="edge"> +<title>la--lb</title> +<path fill="none" stroke="black" d="M350.29,-392.7C350.29,-381.85 350.29,-367.92 350.29,-357.1"/> +</g> +<!-- lla --> +<g id="node5" class="node"> +<title>lla</title> +<ellipse fill="none" stroke="black" cx="298.29" cy="-261.5" rx="44.39" ry="18"/> +<text text-anchor="middle" x="298.29" y="-257.8" font-family="Times,serif" font-size="14.00">p ∧ ¬ q *</text> +<text text-anchor="middle" x="250.59" y="-283.3" font-family="Times,serif" font-size="14.00">2</text> +</g> +<!-- lb--lla --> +<g id="edge4" class="edge"> +<title>lb--lla</title> +<path fill="none" stroke="black" stroke-dasharray="5,2" d="M338.49,-320.87C329.86,-308.34 318.22,-291.44 309.69,-279.05"/> +</g> +<!-- lra --> +<g id="node8" class="node"> +<title>lra</title> +<polygon fill="none" stroke="black" points="360.29,-238.5 360.29,-284.5 454.29,-284.5 454.29,-238.5 360.29,-238.5"/> +<text text-anchor="middle" x="407.29" y="-269.3" font-family="Times,serif" font-size="14.00">¬ p *</text> +<polyline fill="none" stroke="black" points="360.29,-261.5 454.29,-261.5 "/> +<text text-anchor="middle" x="407.29" y="-246.3" font-family="Times,serif" font-size="14.00">does not close</text> +<text text-anchor="middle" x="356.79" y="-288.8" font-family="Times,serif" font-size="14.00">3</text> +</g> +<!-- lb--lra --> +<g id="edge7" class="edge"> +<title>lb--lra</title> +<path fill="none" stroke="black" stroke-dasharray="5,2" d="M363.22,-320.87C371.3,-310.17 381.79,-296.27 390.51,-284.73"/> +</g> +<!-- llb --> +<g id="node6" class="node"> +<title>llb</title> +<ellipse fill="none" stroke="black" cx="298.29" cy="-184" rx="38.99" ry="18"/> +<text text-anchor="middle" x="298.29" y="-180.3" font-family="Times,serif" font-size="14.00">p, ¬ q *</text> +<text text-anchor="middle" x="255.79" y="-205.8" font-family="Times,serif" font-size="14.00">2</text> +</g> +<!-- lla--llb --> +<g id="edge5" class="edge"> +<title>lla--llb</title> +<path fill="none" stroke="black" d="M298.29,-243.37C298.29,-231.01 298.29,-214.4 298.29,-202.06"/> +</g> +<!-- llc --> +<g id="node7" class="node"> +<title>llc</title> +<polygon fill="none" stroke="black" points="251.29,-83.5 251.29,-129.5 345.29,-129.5 345.29,-83.5 251.29,-83.5"/> +<text text-anchor="middle" x="298.29" y="-114.3" font-family="Times,serif" font-size="14.00">p * q</text> +<polyline fill="none" stroke="black" points="251.29,-106.5 345.29,-106.5 "/> +<text text-anchor="middle" x="298.29" y="-91.3" font-family="Times,serif" font-size="14.00">does not close</text> +<text text-anchor="middle" x="247.79" y="-133.8" font-family="Times,serif" font-size="14.00">2</text> +</g> +<!-- llb--llc --> +<g id="edge6" class="edge"> +<title>llb--llc</title> +<path fill="none" stroke="black" d="M298.29,-165.87C298.29,-155.17 298.29,-141.27 298.29,-129.73"/> +</g> +<!-- rb --> +<g id="node10" class="node"> +<title>rb</title> +<ellipse fill="none" stroke="black" cx="125.29" cy="-261.5" rx="59.29" ry="18"/> +<text text-anchor="middle" x="125.29" y="-257.8" font-family="Times,serif" font-size="14.00">p ∧ ¬ q * ¬ q</text> +<text text-anchor="middle" x="62.64" y="-283.3" font-family="Times,serif" font-size="14.00">4</text> +</g> +<!-- ra--rb --> +<g id="edge9" class="edge"> +<title>ra--rb</title> +<path fill="none" stroke="black" stroke-dasharray="5,2" d="M125.29,-320.87C125.29,-308.51 125.29,-291.9 125.29,-279.56"/> +</g> +<!-- rc --> +<g id="node11" class="node"> +<title>rc</title> +<ellipse fill="none" stroke="black" cx="125.29" cy="-184" rx="53.89" ry="18"/> +<text text-anchor="middle" x="125.29" y="-180.3" font-family="Times,serif" font-size="14.00">p ∧ ¬ q, q *</text> +<text text-anchor="middle" x="67.84" y="-205.8" font-family="Times,serif" font-size="14.00">4</text> +</g> +<!-- rb--rc --> +<g id="edge10" class="edge"> +<title>rb--rc</title> +<path fill="none" stroke="black" d="M125.29,-243.37C125.29,-231.01 125.29,-214.4 125.29,-202.06"/> +</g> +<!-- rd --> +<g id="node12" class="node"> +<title>rd</title> +<ellipse fill="none" stroke="black" cx="125.29" cy="-106.5" rx="48.19" ry="18"/> +<text text-anchor="middle" x="125.29" y="-102.8" font-family="Times,serif" font-size="14.00">p, ¬ q, q *</text> +<text text-anchor="middle" x="73.69" y="-128.3" font-family="Times,serif" font-size="14.00">4</text> +</g> +<!-- rc--rd --> +<g id="edge11" class="edge"> +<title>rc--rd</title> +<path fill="none" stroke="black" d="M125.29,-165.87C125.29,-153.51 125.29,-136.9 125.29,-124.56"/> +</g> +<!-- re --> +<g id="node13" class="node"> +<title>re</title> +<polygon fill="none" stroke="black" points="95.79,-0.5 95.79,-46.5 154.79,-46.5 154.79,-0.5 95.79,-0.5"/> +<text text-anchor="middle" x="125.29" y="-31.3" font-family="Times,serif" font-size="14.00">p, q * q</text> +<polyline fill="none" stroke="black" points="95.79,-23.5 154.79,-23.5 "/> +<text text-anchor="middle" x="125.29" y="-8.3" font-family="Times,serif" font-size="14.00">closes</text> +<text text-anchor="middle" x="92.29" y="-50.8" font-family="Times,serif" font-size="14.00">4</text> +</g> +<!-- rd--re --> +<g id="edge12" class="edge"> +<title>rd--re</title> +<path fill="none" stroke="black" d="M125.29,-88.32C125.29,-76.15 125.29,-59.73 125.29,-46.59"/> +</g> +</g> +</svg> diff --git a/content/advanced-logic-notes/exercise-3/index.md b/content/advanced-logic-notes/exercise-3/index.md @@ -0,0 +1,252 @@ ++++ +title = 'Exercise class 3' ++++ + +# Exercise class 3 +## Exercise 1 +The two models: + +<table> +<tr> +<th>M</th> +<th>K</th> +</tr> +<tr> +<td> +<img src="1-model-m.dot.svg" alt="Model M"> + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) 1-model-m.dot --> +```dot +digraph g { +a -> b +a -> c +c -> a +c -> d +} +``` + +</details> + +</td> +<td><img src="1-model-k.dot.svg" alt="Model K"> + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) 1-model-k.dot --> +```dot +digraph g { +1 -> 2 +2 -> 3 +3 -> 1 +1 -> 4 +} +``` + +</details> +</td> +</tr> +</table> + +### a) + +| Round | S | D | link | local harmony | +|-------|--------|--------------|-------|---------------| +| 0 | | | a ~ 1 | ok | +| 1 | a -> c | (1/2) 1 -> 2 | c ~ 2 | ok | +| 2 | c -> d | 2 -> 3 | d ~ 3 | ok | +| 3 | 3 -> 1 | stuck. | | | +| ... | ... | ... | ... | ... | +| 1 | a -> c | (2/2) 1 -> 4 | c ~ 4 | ok | +| 2 | c -> a | stuck. | | | + +So even in an optimal game, D gets stuck. + +Once we find a winning strategy for S no matter what D does, we can stop. + +### b) +◇ ◇ □ ⊥ + +In two steps, we reach a blind state. + +## Sequents and tableaux (exercise 5) +### □ p → ◇ p +Show validity of: □ p → ◇ p + +Pre-processing: + +``` +□ p → ◇ p ≡ ¬ □ p ∨ ◇ p + ≡ ◇ ¬ p ∨ ◇ p +``` + +<table> +<tr><th>Sequent</th><th>Tableau</th></tr> +<tr> +<td> + +``` +⇒ ◇ ¬ p ∨ ◇ p +⇒ ◇ ¬ p, ◇ p +``` + +Stuck. No diamond on left, so cannot take a step. + +◇ ¬ p ∨ ◇ p not valid, so □ p → ◇ p not valid. +</td> +<td> +<img src="5-1-tableau.dot.svg" alt="Tableau" /> + +Zero non-solid successors. Stuck, does not close, so non-validity. + +Counter-model F = ({1}, ∅), V(p) = ∅. + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) 5-1-tableau.dot --> +```dot +graph g { +a [label="* ◇ ¬ p ∨ ◇ p", xlabel="1"] +a -- b +b [label="* ◇ ¬ p, ◇ p", xlabel="1"] +} +``` + +</details> + +</td> +</tr> +</table> + +### □ (p → q) → (□ p → □ q) +Show validity of: □ (p → q) → (□ p → □ q) + +Pre-processing: + +``` +□ (p → q) → (□ p → □ q) ≡ ¬ ◇ ¬ (¬ p ∨ q) → (¬ ◇ ¬ p → ¬ ◇ ¬ q) + ≡ ◇ ¬ (¬ p ∨ q) ∨ (◇ ¬ p ∨ ¬ ◇ ¬ q) + ≡ ◇ (p ∧ ¬ q) ∨ ◇ ¬ p ∨ ¬ ◇ ¬ q +``` + +<table> +<tr> <th>Sequent</th> <th>Tableau</th> </tr> +<tr> +<td> + +``` +⇒ ◇ (p ∧ ¬ q), ◇ ¬ p, ¬ ◇ ¬ q +◇ ¬ q ⇒ ◇ (p ∧ ¬ q), ◇ ¬ p + +One case: +¬ q ⇒ p ∧ ¬ q, ¬ p +p, ¬ q ⇒ p ∧ ¬ q +p ⇒ p ∧ ¬ q, q + +Two goals, both must be valid: + A) p ⇒ p, q + Valid. + B) p ⇒ ¬ q, q + p, q ⇒ q + Valid. + +Sequent is valid, so initial formula is valid. +``` + +</td> +<td> +<img src="5-2-tableau.dot.svg" alt="Tableau" /> + +Closes, so initial formula is valid. + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) 5-2-tableau.dot --> +```dot +graph g { +a [label="* ◇ (p ∧ ¬ q), ◇ ¬ p, ¬ ◇ ¬ q", xlabel="1"] +b [label="◇ ¬ q * ◇ (p ∧ ¬ q), ◇ ¬ p", xlabel="1"]; a -- b +c [label="¬ q * p ∧ ¬ q, ¬ p", xlabel="2"]; b -- c [style="dashed"] +d [label="p * p ∧ ¬ q, q", xlabel="2"]; c -- d + +el [shape="record", label="{ p * p, q | closes. }", xlabel="2"]; d -- el + +er [label="p * ¬ q, q", xlabel="2"]; d -- er +f [shape="record", label="{ p, q * q | closes. }", xlabel="2"]; er -- f +} +``` + +</details> + +</td> +</tr> +</table> + +### (□ p → □ q) → □ (p → q) +Show validity of: (□ p → □ q) → □ (p → q) + +Pre-processing: + +``` +(□ p → □ q) → □ (p → q) ≡ (¬ ◇ ¬ p → ¬ ◇ ¬ q) → ¬ ◇ ¬ (¬ p ∨ q) + ≡ ¬ (◇ ¬ p ∨ ¬ ◇ ¬ q) ∨ ¬ ◇ (p ∧ ¬ q) + ≡ (¬ ◇ ¬ p ∧ ◇ ¬ q) ∨ ¬ ◇ (p ∧ ¬ q) +``` + +Tableau: + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) 5-3-tableau.dot --> +```dot +graph g { +a [label="* (¬ ◇ ¬ p ∧ ◇ ¬ q), ¬ ◇ (p ∧ ¬ q)", xlabel="1"] +b [label="◇ (p ∧ ¬ q) * ¬ ◇ ¬ p ∧ ◇ ¬ q", xlabel="1"]; a -- b + +la [label="◇ (p ∧ ¬ q) * ¬ ◇ ¬ p", xlabel="1"]; a -- la +lb [label="◇ (p ∧ ¬ q), ◇ ¬ p *", xlabel="1"]; la -- lb + +lla [label="p ∧ ¬ q *", xlabel="2"]; lb -- lla [style="dashed"] +llb [label="p, ¬ q *", xlabel="2"]; lla -- llb +llc [label="{p * q | does not close}", xlabel="2", shape="record"]; llb -- llc + +lra [label="{¬ p * | does not close}", xlabel="3", shape="record"]; lb -- lra [style="dashed"] + +ra [label="◇ (p ∧ ¬ q) * ◇ ¬ q", xlabel="1"]; b -- ra +rb [label="p ∧ ¬ q * ¬ q", xlabel="4"]; ra -- rb [style="dashed"] +rc [label="p ∧ ¬ q, q *", xlabel="4"]; rb -- rc +rd [label="p, ¬ q, q *", xlabel="4"]; rc -- rd +re [label="{p, q * q | closes}", xlabel="4", shape="record"]; rd -- re +} +``` + +</details> + +This yields a counter-model: + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) 5-3-counter-model.dot --> +```dot +digraph g { +rankdir=LR +1 -> 2; 2 [shape="Mrecord", label="{2 | p}"] +1 -> 3 +} +``` + +</details> + +1 ⊭ □ (p → q) because 2 ⊭ p → q. +But 1 ⊨ (□ p → □ q) because 1 ⊭ □ p.
