commit b1e3d5acba8ac40e3145254008f05f1379c0bce4 parent ece195497fd28d59ef96658a3e0aee8f280640a0 Author: Alex Balgavy <alex@balgavy.eu> Date: Thu, 3 Mar 2022 18:16:25 +0100 Update advanced logic notes Diffstat:
23 files changed, 802 insertions(+), 264 deletions(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md @@ -11,6 +11,7 @@ title = 'Advanced Logic' 7. [Lecture 6](lecture-6/) 8. [Exercise 3](exercise-3/) 9. [Lecture 7](lecture-7/) +10. [Homework 1](homework-1/) 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). diff --git a/content/advanced-logic-notes/homework-1/game-tree.dot b/content/advanced-logic-notes/homework-1/game-tree.dot @@ -0,0 +1,15 @@ +graph t { +t [label="M,v ⊨? ◇ (q ∧ ◇ p)", xlabel="V's turn"] +tl [label="M,y ⊨? q ∧ ◇ p", xlabel="F's turn"]; t -- tl +tll [label="{ M,y ⊨ q | Verifier wins }", shape="Mrecord"]; tl -- tll +tlr [label="M, y ⊨? ◇ p", xlabel="V's turn"]; tl -- tlr +tlrn [label="{ M, z ⊨ p | Verifier wins. }", shape="Mrecord"]; tlr -- tlrn + +tr [label="M, v ⊨? q ∧ ◇ p", xlabel="F's turn"]; t -- tr +trl [label="{ M, v ⊭ q | Falsifier wins }", shape="Mrecord", xlabel="V's turn"]; tr -- trl +trr [label="M, v ⊨? ◇ p", xlabel="V's turn"]; tr -- trr +trrl [label="{ M, v ⊭ p | Falsifier wins. }", shape="Mrecord"]; trr -- trrl +trrr [label="{M, y ⊭ p | Falsifier wins.}", shape="Mrecord"]; trr -- trrr +} + + diff --git a/content/advanced-logic-notes/homework-1/game-tree.dot.svg b/content/advanced-logic-notes/homework-1/game-tree.dot.svg @@ -0,0 +1,134 @@ +<?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: t Pages: 1 --> +<svg width="524pt" height="297pt" + viewBox="0.00 0.00 524.00 297.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 293)"> +<title>t</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-293 520,-293 520,4 -4,4"/> +<!-- t --> +<g id="node1" class="node"> +<title>t</title> +<ellipse fill="none" stroke="black" cx="226" cy="-256" rx="81.49" ry="18"/> +<text text-anchor="middle" x="226" y="-252.3" font-family="Times,serif" font-size="14.00">M,v ⊨? ◇ (q ∧ ◇ p)</text> +<text text-anchor="middle" x="123.26" y="-277.8" font-family="Times,serif" font-size="14.00">V's turn</text> +</g> +<!-- tl --> +<g id="node2" class="node"> +<title>tl</title> +<ellipse fill="none" stroke="black" cx="149" cy="-184" rx="67.69" ry="18"/> +<text text-anchor="middle" x="149" y="-180.3" font-family="Times,serif" font-size="14.00">M,y ⊨? q ∧ ◇ p</text> +<text text-anchor="middle" x="60.91" y="-205.8" font-family="Times,serif" font-size="14.00">F's turn</text> +</g> +<!-- t--tl --> +<g id="edge1" class="edge"> +<title>t--tl</title> +<path fill="none" stroke="black" d="M207.75,-238.41C195.48,-227.25 179.36,-212.6 167.12,-201.47"/> +</g> +<!-- tr --> +<g id="node6" class="node"> +<title>tr</title> +<ellipse fill="none" stroke="black" cx="304" cy="-184" rx="69.59" ry="18"/> +<text text-anchor="middle" x="304" y="-180.3" font-family="Times,serif" font-size="14.00">M, v ⊨? q ∧ ◇ p</text> +<text text-anchor="middle" x="213.96" y="-205.8" font-family="Times,serif" font-size="14.00">F's turn</text> +</g> +<!-- t--tr --> +<g id="edge5" class="edge"> +<title>t--tr</title> +<path fill="none" stroke="black" d="M244.48,-238.41C256.92,-227.25 273.24,-212.6 285.65,-201.47"/> +</g> +<!-- tll --> +<g id="node3" class="node"> +<title>tll</title> +<path fill="none" stroke="black" d="M12,-83.5C12,-83.5 74,-83.5 74,-83.5 80,-83.5 86,-89.5 86,-95.5 86,-95.5 86,-117.5 86,-117.5 86,-123.5 80,-129.5 74,-129.5 74,-129.5 12,-129.5 12,-129.5 6,-129.5 0,-123.5 0,-117.5 0,-117.5 0,-95.5 0,-95.5 0,-89.5 6,-83.5 12,-83.5"/> +<text text-anchor="middle" x="43" y="-114.3" font-family="Times,serif" font-size="14.00">M,y ⊨ q</text> +<polyline fill="none" stroke="black" points="0,-106.5 86,-106.5 "/> +<text text-anchor="middle" x="43" y="-91.3" font-family="Times,serif" font-size="14.00">Verifier wins</text> +</g> +<!-- tl--tll --> +<g id="edge2" class="edge"> +<title>tl--tll</title> +<path fill="none" stroke="black" d="M126.52,-166.99C111.21,-156.08 90.73,-141.5 73.89,-129.5"/> +</g> +<!-- tlr --> +<g id="node4" class="node"> +<title>tlr</title> +<ellipse fill="none" stroke="black" cx="159" cy="-106.5" rx="55.49" ry="18"/> +<text text-anchor="middle" x="159" y="-102.8" font-family="Times,serif" font-size="14.00">M, y ⊨? ◇ p</text> +<text text-anchor="middle" x="125.25" y="-128.3" font-family="Times,serif" font-size="14.00">V's turn</text> +</g> +<!-- tl--tlr --> +<g id="edge3" class="edge"> +<title>tl--tlr</title> +<path fill="none" stroke="black" d="M151.27,-165.87C152.91,-153.51 155.11,-136.9 156.74,-124.56"/> +</g> +<!-- tlrn --> +<g id="node5" class="node"> +<title>tlrn</title> +<path fill="none" stroke="black" d="M126,-0.5C126,-0.5 192,-0.5 192,-0.5 198,-0.5 204,-6.5 204,-12.5 204,-12.5 204,-34.5 204,-34.5 204,-40.5 198,-46.5 192,-46.5 192,-46.5 126,-46.5 126,-46.5 120,-46.5 114,-40.5 114,-34.5 114,-34.5 114,-12.5 114,-12.5 114,-6.5 120,-0.5 126,-0.5"/> +<text text-anchor="middle" x="159" y="-31.3" font-family="Times,serif" font-size="14.00">M, z ⊨ p</text> +<polyline fill="none" stroke="black" points="114,-23.5 204,-23.5 "/> +<text text-anchor="middle" x="159" y="-8.3" font-family="Times,serif" font-size="14.00">Verifier wins.</text> +</g> +<!-- tlr--tlrn --> +<g id="edge4" class="edge"> +<title>tlr--tlrn</title> +<path fill="none" stroke="black" d="M159,-88.32C159,-76.15 159,-59.73 159,-46.59"/> +</g> +<!-- trl --> +<g id="node7" class="node"> +<title>trl</title> +<path fill="none" stroke="black" d="M262,-83.5C262,-83.5 328,-83.5 328,-83.5 334,-83.5 340,-89.5 340,-95.5 340,-95.5 340,-117.5 340,-117.5 340,-123.5 334,-129.5 328,-129.5 328,-129.5 262,-129.5 262,-129.5 256,-129.5 250,-123.5 250,-117.5 250,-117.5 250,-95.5 250,-95.5 250,-89.5 256,-83.5 262,-83.5"/> +<text text-anchor="middle" x="295" y="-114.3" font-family="Times,serif" font-size="14.00">M, v ⊭ q</text> +<polyline fill="none" stroke="black" points="250,-106.5 340,-106.5 "/> +<text text-anchor="middle" x="295" y="-91.3" font-family="Times,serif" font-size="14.00">Falsifier wins</text> +<text text-anchor="middle" x="228.5" y="-133.8" font-family="Times,serif" font-size="14.00">V's turn</text> +</g> +<!-- tr--trl --> +<g id="edge6" class="edge"> +<title>tr--trl</title> +<path fill="none" stroke="black" d="M301.96,-165.87C300.68,-155.17 299.03,-141.27 297.65,-129.73"/> +</g> +<!-- trr --> +<g id="node8" class="node"> +<title>trr</title> +<ellipse fill="none" stroke="black" cx="413" cy="-106.5" rx="55.49" ry="18"/> +<text text-anchor="middle" x="413" y="-102.8" font-family="Times,serif" font-size="14.00">M, v ⊨? ◇ p</text> +<text text-anchor="middle" x="379.25" y="-128.3" font-family="Times,serif" font-size="14.00">V's turn</text> +</g> +<!-- tr--trr --> +<g id="edge7" class="edge"> +<title>tr--trr</title> +<path fill="none" stroke="black" d="M327.12,-166.99C345.86,-154 372.13,-135.81 390.66,-122.97"/> +</g> +<!-- trrl --> +<g id="node9" class="node"> +<title>trrl</title> +<path fill="none" stroke="black" d="M322,-0.5C322,-0.5 392,-0.5 392,-0.5 398,-0.5 404,-6.5 404,-12.5 404,-12.5 404,-34.5 404,-34.5 404,-40.5 398,-46.5 392,-46.5 392,-46.5 322,-46.5 322,-46.5 316,-46.5 310,-40.5 310,-34.5 310,-34.5 310,-12.5 310,-12.5 310,-6.5 316,-0.5 322,-0.5"/> +<text text-anchor="middle" x="357" y="-31.3" font-family="Times,serif" font-size="14.00">M, v ⊭ p</text> +<polyline fill="none" stroke="black" points="310,-23.5 404,-23.5 "/> +<text text-anchor="middle" x="357" y="-8.3" font-family="Times,serif" font-size="14.00">Falsifier wins.</text> +</g> +<!-- trr--trrl --> +<g id="edge8" class="edge"> +<title>trr--trrl</title> +<path fill="none" stroke="black" d="M401.4,-88.72C393,-76.58 381.57,-60.05 372.41,-46.8"/> +</g> +<!-- trrr --> +<g id="node10" class="node"> +<title>trrr</title> +<path fill="none" stroke="black" d="M434,-0.5C434,-0.5 504,-0.5 504,-0.5 510,-0.5 516,-6.5 516,-12.5 516,-12.5 516,-34.5 516,-34.5 516,-40.5 510,-46.5 504,-46.5 504,-46.5 434,-46.5 434,-46.5 428,-46.5 422,-40.5 422,-34.5 422,-34.5 422,-12.5 422,-12.5 422,-6.5 428,-0.5 434,-0.5"/> +<text text-anchor="middle" x="469" y="-31.3" font-family="Times,serif" font-size="14.00">M, y ⊭ p</text> +<polyline fill="none" stroke="black" points="422,-23.5 516,-23.5 "/> +<text text-anchor="middle" x="469" y="-8.3" font-family="Times,serif" font-size="14.00">Falsifier wins.</text> +</g> +<!-- trr--trrr --> +<g id="edge9" class="edge"> +<title>trr--trrr</title> +<path fill="none" stroke="black" d="M424.6,-88.72C433,-76.58 444.43,-60.05 453.59,-46.8"/> +</g> +</g> +</svg> diff --git a/content/advanced-logic-notes/homework-1/index.md b/content/advanced-logic-notes/homework-1/index.md @@ -0,0 +1,163 @@ ++++ +title = 'Homework 1' ++++ +# Homework 1 +## 1 +### a +- We aim to show M,v ⊨ ◇ (q ∧ ◇ p). +- For the formula to hold, (q ∧ ◇ p) must hold in at least one successor of v. +- v has two R-successors: v and y. +- q ∧ ◇ p does not hold in v, because v ⊭ q. +- However, y ⊨ q ∧ ◇ p: y ⊨ q, and Ryz and z ⊨ p, thus y ⊨ ◇ p. +- Therefore, M,v ⊨ ◇ (q ∧ ◇ p). + +### b + + +If Verifier chooses the left branch (M, y ⊨ q ∧ ◇ p), he always wins. + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) game-tree.dot --> +```dot +graph t { +t [label="M,v ⊨? ◇ (q ∧ ◇ p)", xlabel="V's turn"] +tl [label="M,y ⊨? q ∧ ◇ p", xlabel="F's turn"]; t -- tl +tll [label="{ M,y ⊨ q | Verifier wins }", shape="Mrecord"]; tl -- tll +tlr [label="M, y ⊨? ◇ p", xlabel="V's turn"]; tl -- tlr +tlrn [label="{ M, z ⊨ p | Verifier wins. }", shape="Mrecord"]; tlr -- tlrn + +tr [label="M, v ⊨? q ∧ ◇ p", xlabel="F's turn"]; t -- tr +trl [label="{ M, v ⊭ q | Falsifier wins }", shape="Mrecord", xlabel="V's turn"]; tr -- trl +trr [label="M, v ⊨? ◇ p", xlabel="V's turn"]; tr -- trr +trrl [label="{ M, v ⊭ p | Falsifier wins. }", shape="Mrecord"]; trr -- trrl +trrr [label="{M, y ⊭ p | Falsifier wins.}", shape="Mrecord"]; trr -- trrr +} + +``` + +</details> + +## 2 +### a +- Goal is to show ⊨ (◇ p → □ q) → (□ p → □ q). +- Take an arbitrary frame F = (W,R), V a valuation on F, and x ∈ W. Let M = (F, V). +- Assume M, x ⊨ (◇ p → □ q), where M = (F, V). +- Aim to show M, x ⊨ □ p → □ q. +- Assume M, x ⊨ □ p, aim to show M, x ⊨ □ q. +- If x has no successors, ◇ p does not hold, hence M, x ⊨ □ q ex falso (also by assumption). +- If x has successors, and p is valid in at least one of them, x ⊨ ◇ p, hence M, x ⊨ □ q by assumption. +- If x has successors, an p is not valid in any of them, x ⊨ □ q because ◇ p is not valid in x. +- Because the model and state are arbitrary, the formula is universally valid. + +### b +- Goal is to show ⊨ ¬ ◇ □ p → ◇ ◇ ¬ p. +- Consider the frame F = ({x}, ∅) and valuation V(p) = ∅. +- In state x, ◇ □ p is not valid, because x has no successors, hence x ⊨ ¬ ◇ □ p. +- However, since x has no successors, x ⊭ ◇ ◇ ¬ p. +- Therefore, the implication doesn't hold, and the formula is not universally valid. + +## 3 +We aim to show that F ⊨ p → □ ◇ p iff F is symmetric: ∀ x, y ∈ W (Rxy → Ryx). + +* Assume that in a frame F = (W,R), F ⊨ p → □ ◇ p. + - Assume towards a contradiction that F is not symmetric. + - Then there must be states x, y ∈ W such that Rxy but not Ryx. + - Take a model M = (F, V), with valuation V(p) = {x}. + - Then, M, x ⊨ p. + - x has successor y, but y does not have x as a successor, therefore M, y ⊭ p → □ ◇ p, so F ⊭ □ ◇ p. + - This contradicts the assumption. + +* Assume that a frame F = (W, R) is symmetric. + - We aim to show that F ⊨ p → □ ◇ p. + - Take an arbitrary model M = (F, V) and an arbitrary state x ∈ M. + - Assume that M, x ⊨ p and aim to show M, x ⊨ □ ◇ p. + - If x has no successors, then x ⊨ □ ◇ p. + - If there is y ∈ W such that Rxy, then we must also have Ryx by the assumption that F is symmetric. + - Because x ⊨ p and y ⊨ p, x ⊨ □ ◇ p and y ⊨ □ ◇ p. + - Because the state x and the model M are arbitrary, F ⊨ □ ◇ p. + +* We have therefore shown that the formula p → □ ◇ p characterizes the frame property "symmetry". + +## 4 +### a + +<table> +<tr> <th>Model A</th> <th>Model B</th> <th>Model C</th> </tr> +<tr> + +<td> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) model-a.dot --> +```dot +digraph g { +a -> b +b -> a +a -> c +b -> d +} +``` + +</details> +</td> + +<td> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) model-b.dot --> +```dot +digraph g { +1 -> 2 +2 -> 1 +1 -> 3 +1 -> 4 +} +``` + +</details> + +</td> + +<td> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) model-c.dot --> +```dot +digraph g { +1 [label="#"] +1 -> b +} +``` + +</details> + +</td> +</tr> +</table> + +### b +- A, a ⊨ ◇ ◇ □ ⊥, but B, 1 ⊭ ◇ ◇ □ ⊥. +- A, d ⊨ □ ⊥, so A, b ⊨ ◇ □ ⊥, so A, a ⊨ ◇ ◇ □ ⊥. +- B, 4 ⊨ □ ⊥, so B, 1 ⊨ ◇ □ ⊥ but only B, 2 ⊨ ◇ ◇ □ ⊥, not state 1. + +### c +Because the states a ∈ A and 1 ∈ B are not modally equivalent as shown in exercise 4b above. + +### d +Take the set Z = {(a, #), (b, #), (c, b), (d, b)}. +We claim that Z is a bisimulation, and (a, #) ∈ Z, therefore they are bisimilar. +No proof is necessary here. diff --git a/content/advanced-logic-notes/homework-1/model-a.dot b/content/advanced-logic-notes/homework-1/model-a.dot @@ -0,0 +1,7 @@ +digraph g { +a -> b +b -> a +a -> c +b -> d +} + diff --git a/content/advanced-logic-notes/homework-1/model-a.dot.svg b/content/advanced-logic-notes/homework-1/model-a.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="134pt" height="188pt" + viewBox="0.00 0.00 134.00 188.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 184)"> +<title>g</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-184 130,-184 130,4 -4,4"/> +<!-- a --> +<g id="node1" class="node"> +<title>a</title> +<ellipse fill="none" stroke="black" cx="27" cy="-162" rx="27" ry="18"/> +<text text-anchor="middle" x="27" y="-158.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="27" cy="-90" rx="27" ry="18"/> +<text text-anchor="middle" x="27" y="-86.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="M21.16,-144.41C20.3,-136.51 20.05,-126.85 20.41,-117.94"/> +<polygon fill="black" stroke="black" points="23.9,-118.18 21.12,-107.96 16.92,-117.68 23.9,-118.18"/> +</g> +<!-- c --> +<g id="node3" class="node"> +<title>c</title> +<ellipse fill="none" stroke="black" cx="99" cy="-90" rx="27" ry="18"/> +<text text-anchor="middle" x="99" y="-86.3" font-family="Times,serif" font-size="14.00">c</text> +</g> +<!-- a->c --> +<g id="edge3" class="edge"> +<title>a->c</title> +<path fill="none" stroke="black" d="M41.57,-146.83C51.75,-136.94 65.52,-123.55 77.03,-112.36"/> +<polygon fill="black" stroke="black" points="79.47,-114.87 84.2,-105.38 74.59,-109.85 79.47,-114.87"/> +</g> +<!-- b->a --> +<g id="edge2" class="edge"> +<title>b->a</title> +<path fill="none" stroke="black" d="M32.88,-107.96C33.71,-115.83 33.95,-125.37 33.58,-134.19"/> +<polygon fill="black" stroke="black" points="30.07,-134.18 32.84,-144.41 37.06,-134.69 30.07,-134.18"/> +</g> +<!-- d --> +<g id="node4" class="node"> +<title>d</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">d</text> +</g> +<!-- b->d --> +<g id="edge4" class="edge"> +<title>b->d</title> +<path fill="none" stroke="black" d="M27,-71.7C27,-63.98 27,-54.71 27,-46.11"/> +<polygon fill="black" stroke="black" points="30.5,-46.1 27,-36.1 23.5,-46.1 30.5,-46.1"/> +</g> +</g> +</svg> diff --git a/content/advanced-logic-notes/homework-1/model-b.dot b/content/advanced-logic-notes/homework-1/model-b.dot @@ -0,0 +1,7 @@ +digraph g { +1 -> 2 +2 -> 1 +1 -> 3 +1 -> 4 +} + diff --git a/content/advanced-logic-notes/homework-1/model-b.dot.svg b/content/advanced-logic-notes/homework-1/model-b.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="206pt" height="116pt" + viewBox="0.00 0.00 206.00 116.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 112)"> +<title>g</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-112 202,-112 202,4 -4,4"/> +<!-- 1 --> +<g id="node1" class="node"> +<title>1</title> +<ellipse fill="none" stroke="black" cx="63" cy="-90" rx="27" ry="18"/> +<text text-anchor="middle" x="63" y="-86.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="27" cy="-18" rx="27" ry="18"/> +<text text-anchor="middle" x="27" 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="M49.73,-74.15C44.38,-65.79 38.57,-55.09 33.99,-45.34"/> +<polygon fill="black" stroke="black" points="37.12,-43.77 29.88,-36.04 30.71,-46.6 37.12,-43.77"/> +</g> +<!-- 3 --> +<g id="node3" class="node"> +<title>3</title> +<ellipse fill="none" stroke="black" cx="99" cy="-18" rx="27" ry="18"/> +<text text-anchor="middle" x="99" y="-14.3" font-family="Times,serif" font-size="14.00">3</text> +</g> +<!-- 1->3 --> +<g id="edge3" class="edge"> +<title>1->3</title> +<path fill="none" stroke="black" d="M71.35,-72.76C75.71,-64.28 81.15,-53.71 86.04,-44.2"/> +<polygon fill="black" stroke="black" points="89.23,-45.64 90.7,-35.15 83.01,-42.44 89.23,-45.64"/> +</g> +<!-- 4 --> +<g id="node4" class="node"> +<title>4</title> +<ellipse fill="none" stroke="black" cx="171" cy="-18" rx="27" ry="18"/> +<text text-anchor="middle" x="171" y="-14.3" 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="M81.81,-76.81C99,-65.67 124.62,-49.06 143.99,-36.5"/> +<polygon fill="black" stroke="black" points="145.92,-39.43 152.4,-31.05 142.11,-33.56 145.92,-39.43"/> +</g> +<!-- 2->1 --> +<g id="edge2" class="edge"> +<title>2->1</title> +<path fill="none" stroke="black" d="M40.3,-33.89C45.66,-42.28 51.48,-53 56.06,-62.75"/> +<polygon fill="black" stroke="black" points="52.93,-64.32 60.16,-72.05 59.33,-61.49 52.93,-64.32"/> +</g> +</g> +</svg> diff --git a/content/advanced-logic-notes/homework-1/model-c.dot b/content/advanced-logic-notes/homework-1/model-c.dot @@ -0,0 +1,5 @@ +digraph g { +1 [label="#"] +1 -> b +} + diff --git a/content/advanced-logic-notes/homework-1/model-c.dot.svg b/content/advanced-logic-notes/homework-1/model-c.dot.svg @@ -0,0 +1,31 @@ +<?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="62pt" height="116pt" + viewBox="0.00 0.00 62.00 116.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 112)"> +<title>g</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-112 58,-112 58,4 -4,4"/> +<!-- 1 --> +<g id="node1" class="node"> +<title>1</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">#</text> +</g> +<!-- b --> +<g id="node2" class="node"> +<title>b</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">b</text> +</g> +<!-- 1->b --> +<g id="edge1" class="edge"> +<title>1->b</title> +<path fill="none" stroke="black" d="M27,-71.7C27,-63.98 27,-54.71 27,-46.11"/> +<polygon fill="black" stroke="black" points="30.5,-46.1 27,-36.1 23.5,-46.1 30.5,-46.1"/> +</g> +</g> +</svg> diff --git a/content/advanced-logic-notes/lecture-1/index.md b/content/advanced-logic-notes/lecture-1/index.md @@ -23,6 +23,7 @@ a valuation v : Var → {0,1} maps propositional variables to truth values. the semantics of a formula under a valuation is defined with ⟦p⟧ᵥ = v(p), with p ∈ Var if ⟦φ⟧ᵥ = 1, we write v ⊨ φ (read "v models φ") +- that is, if φ is true in the model v - then, φ has a model, so φ is satisfiable If every model of all φᵢ is a model of ψ, we write φ₁,...,φn ⊨ ψ @@ -45,20 +46,23 @@ Veridicality: □ φ → φ Truth s relative to current situation/world/environment: - formulas evaluated in given structure -- necessity: truth in all accessible worlds -- possibility: truth in some accessible world (at least one) +- necessity (□): truth in all accessible worlds. if there are no accessible worlds, it's true. +- possibility (◇): truth in some accessible world (at least one). if there are no accessible worlds, it's false. ## Frames A situation is set by a frame F = (W,R) - W ≠ ∅ set of possible worlds/states - R ⊆ W × W an accessibility/transition relation +A frame is just the states and transitions between them, without a valuation (i.e. without saying what's true in each state). + A frame could be (ℕ, <), or ({1,2,3,4}, {(1,2), (2,4), (1,3), (3,4), (2,2)}) ## Models model: pair M = (F, V) - a frame F = (W,R) - a valuation V : Var → W → {0,1}, or V : Var → P(W) + - the valuation says which letters/formulas are true in which states pointed model: pair (M,w) of model M and w a world in M diff --git a/content/advanced-logic-notes/lecture-2/index.md b/content/advanced-logic-notes/lecture-2/index.md @@ -18,6 +18,8 @@ Above: - the formula 2 ⊨ ◇ □ ⊥ characterizes state 2 ## Game semantics +This is an approach to determine if a formula φ holds in a pointed model M, w. + We have: - model M = ((W,R), V), world w ∈ W, formula φ - two players: @@ -45,11 +47,12 @@ A strategy for player P is subset of steps for P, and it's a winning strategy if ### Example Diagram: - + <details> -<summary>Dot code</summary> +<summary>Graphviz code</summary> +<!-- :Tangle(dot) states.dot --> ```dot digraph states { 1 -> 2 @@ -62,8 +65,6 @@ digraph states { } ``` -Generated with PlantUML, surround it with `@startdot` and `@enddot`. - </details> Given: @@ -72,11 +73,12 @@ Given: Complete game tree: - + <details> -<summary>Dot code</summary> +<summary>Graphviz code</summary> +<!-- :Tangle(dot) tree.dot --> ```dot digraph gametree { top [label="[V] ◇ p ∨ □ ◇ p, 2"] @@ -101,8 +103,6 @@ digraph gametree { } ``` -Generated with PlantUML, surround it with `@startdot` and `@enddot`. - </details> ## Truth and validity @@ -125,7 +125,7 @@ Show universal validity of □ (φ → ψ) → (□ φ → □ ψ) 3. Assume a2: F,V,x ⊨ □ φ 4. Aim to show F,V,x ⊨ □ ψ. 5. □ is universal quantification, so take an arbitrary successor y ∈ W. -6. If Rxy, aim to show y ⊨ ψ. If not, we are one. +6. If Rxy, aim to show y ⊨ ψ. If not, □ ψ holds. 7. Have y ⊨ φ → ψ and y ⊨ φ. 8. From a2, have y ⊨ φ. 9. From a1, have have y ⊨ ψ. diff --git a/content/advanced-logic-notes/lecture-2/states.dot b/content/advanced-logic-notes/lecture-2/states.dot @@ -0,0 +1,10 @@ +digraph states { +1 -> 2 +1 -> 3 +2 -> 3 +3 -> 2 +3 -> 4 +4 -> 2 +4 -> 3 +} + diff --git a/content/advanced-logic-notes/lecture-2/states.dot.svg b/content/advanced-logic-notes/lecture-2/states.dot.svg @@ -0,0 +1,79 @@ +<?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: states Pages: 1 --> +<svg width="90pt" height="260pt" + viewBox="0.00 0.00 90.00 260.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 256)"> +<title>states</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-256 86,-256 86,4 -4,4"/> +<!-- 1 --> +<g id="node1" class="node"> +<title>1</title> +<ellipse fill="none" stroke="black" cx="27" cy="-234" rx="27" ry="18"/> +<text text-anchor="middle" x="27" y="-230.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="55" cy="-162" rx="27" ry="18"/> +<text text-anchor="middle" x="55" y="-158.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="M33.64,-216.41C36.91,-208.22 40.94,-198.14 44.62,-188.95"/> +<polygon fill="black" stroke="black" points="47.95,-190.05 48.41,-179.47 41.45,-187.45 47.95,-190.05"/> +</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="edge2" class="edge"> +<title>1->3</title> +<path fill="none" stroke="black" d="M23.75,-215.89C21.95,-205.54 19.91,-192.06 19,-180 17.8,-164.04 17.8,-159.96 19,-144 19.64,-135.52 20.84,-126.34 22.12,-118.04"/> +<polygon fill="black" stroke="black" points="25.58,-118.55 23.75,-108.11 18.68,-117.41 25.58,-118.55"/> +</g> +<!-- 2->3 --> +<g id="edge3" class="edge"> +<title>2->3</title> +<path fill="none" stroke="black" d="M43.07,-145.46C38.89,-137.42 34.58,-127.36 31.24,-118.09"/> +<polygon fill="black" stroke="black" points="34.52,-116.85 28.05,-108.46 27.87,-119.05 34.52,-116.85"/> +</g> +<!-- 3->2 --> +<g id="edge4" class="edge"> +<title>3->2</title> +<path fill="none" stroke="black" d="M39,-106.67C43.18,-114.74 47.49,-124.81 50.82,-134.08"/> +<polygon fill="black" stroke="black" points="47.54,-135.3 53.99,-143.7 54.18,-133.1 47.54,-135.3"/> +</g> +<!-- 4 --> +<g id="node4" class="node"> +<title>4</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">4</text> +</g> +<!-- 3->4 --> +<g id="edge5" class="edge"> +<title>3->4</title> +<path fill="none" stroke="black" d="M21.16,-72.41C20.3,-64.51 20.05,-54.85 20.41,-45.94"/> +<polygon fill="black" stroke="black" points="23.9,-46.18 21.12,-35.96 16.92,-45.68 23.9,-46.18"/> +</g> +<!-- 4->2 --> +<g id="edge6" class="edge"> +<title>4->2</title> +<path fill="none" stroke="black" d="M40.75,-33.93C48.96,-43.9 58.62,-57.75 63,-72 69.25,-92.33 66.51,-116.41 62.62,-134.39"/> +<polygon fill="black" stroke="black" points="59.2,-133.66 60.25,-144.2 66,-135.3 59.2,-133.66"/> +</g> +<!-- 4->3 --> +<g id="edge7" class="edge"> +<title>4->3</title> +<path fill="none" stroke="black" d="M32.88,-35.96C33.71,-43.83 33.95,-53.37 33.58,-62.19"/> +<polygon fill="black" stroke="black" points="30.07,-62.18 32.84,-72.41 37.06,-62.69 30.07,-62.18"/> +</g> +</g> +</svg> diff --git a/content/advanced-logic-notes/lecture-2/states.svg b/content/advanced-logic-notes/lecture-2/states.svg @@ -1,79 +0,0 @@ -<?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: example Pages: 1 --> -<svg width="90pt" height="260pt" - viewBox="0.00 0.00 90.00 260.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 256)"> -<title>example</title> -<polygon fill="white" stroke="transparent" points="-4,4 -4,-256 86,-256 86,4 -4,4"/> -<!-- 1 --> -<g id="node1" class="node"> -<title>1</title> -<ellipse fill="none" stroke="black" cx="27" cy="-234" rx="27" ry="18"/> -<text text-anchor="middle" x="27" y="-230.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="55" cy="-162" rx="27" ry="18"/> -<text text-anchor="middle" x="55" y="-158.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="M33.64,-216.41C36.91,-208.22 40.94,-198.14 44.62,-188.95"/> -<polygon fill="black" stroke="black" points="47.95,-190.05 48.41,-179.47 41.45,-187.45 47.95,-190.05"/> -</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="edge2" class="edge"> -<title>1->3</title> -<path fill="none" stroke="black" d="M23.75,-215.89C21.95,-205.54 19.91,-192.06 19,-180 17.8,-164.04 17.8,-159.96 19,-144 19.64,-135.52 20.84,-126.34 22.12,-118.04"/> -<polygon fill="black" stroke="black" points="25.58,-118.55 23.75,-108.11 18.68,-117.41 25.58,-118.55"/> -</g> -<!-- 2->3 --> -<g id="edge3" class="edge"> -<title>2->3</title> -<path fill="none" stroke="black" d="M43.07,-145.46C38.89,-137.42 34.58,-127.36 31.24,-118.09"/> -<polygon fill="black" stroke="black" points="34.52,-116.85 28.05,-108.46 27.87,-119.05 34.52,-116.85"/> -</g> -<!-- 3->2 --> -<g id="edge4" class="edge"> -<title>3->2</title> -<path fill="none" stroke="black" d="M39,-106.67C43.18,-114.74 47.49,-124.81 50.82,-134.08"/> -<polygon fill="black" stroke="black" points="47.54,-135.3 53.99,-143.7 54.18,-133.1 47.54,-135.3"/> -</g> -<!-- 4 --> -<g id="node4" class="node"> -<title>4</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">4</text> -</g> -<!-- 3->4 --> -<g id="edge5" class="edge"> -<title>3->4</title> -<path fill="none" stroke="black" d="M21.16,-72.41C20.3,-64.51 20.05,-54.85 20.41,-45.94"/> -<polygon fill="black" stroke="black" points="23.9,-46.18 21.12,-35.96 16.92,-45.68 23.9,-46.18"/> -</g> -<!-- 4->2 --> -<g id="edge6" class="edge"> -<title>4->2</title> -<path fill="none" stroke="black" d="M40.75,-33.93C48.96,-43.9 58.62,-57.75 63,-72 69.25,-92.33 66.51,-116.41 62.62,-134.39"/> -<polygon fill="black" stroke="black" points="59.2,-133.66 60.25,-144.2 66,-135.3 59.2,-133.66"/> -</g> -<!-- 4->3 --> -<g id="edge7" class="edge"> -<title>4->3</title> -<path fill="none" stroke="black" d="M32.88,-35.96C33.71,-43.83 33.95,-53.37 33.58,-62.19"/> -<polygon fill="black" stroke="black" points="30.07,-62.18 32.84,-72.41 37.06,-62.69 30.07,-62.18"/> -</g> -</g> -</svg> diff --git a/content/advanced-logic-notes/lecture-2/tree.dot b/content/advanced-logic-notes/lecture-2/tree.dot @@ -0,0 +1,22 @@ +digraph gametree { + top [label="[V] ◇ p ∨ □ ◇ p, 2"] + l11 [label="[V] ◇ p, 2"] + l12 [label="[F] □ ◇ p, 2"] + top -> l11 + top -> l12 + l21 [label="p 3"] + l22 [label="[V] ◇ p, 3"] + l11 -> l21 + l12 -> l22 + l31 [label="Verifier wins"] + l32 [label="p, 2"] + l33 [label="p, 4"] + l21 -> l31 + l22 -> l32 + l22 -> l33 + l41 [label="Falsifier wins."] + l42 [label="Falsifier wins."] + l32 -> l41 + l33 -> l42 +} + diff --git a/content/advanced-logic-notes/lecture-2/tree.dot.svg b/content/advanced-logic-notes/lecture-2/tree.dot.svg @@ -0,0 +1,127 @@ +<?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: gametree Pages: 1 --> +<svg width="358pt" height="332pt" + viewBox="0.00 0.00 357.99 332.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 328)"> +<title>gametree</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-328 353.99,-328 353.99,4 -4,4"/> +<!-- top --> +<g id="node1" class="node"> +<title>top</title> +<ellipse fill="none" stroke="black" cx="114.9" cy="-306" rx="77.19" ry="18"/> +<text text-anchor="middle" x="114.9" y="-302.3" font-family="Times,serif" font-size="14.00">[V] ◇ p ∨ □ ◇ p, 2</text> +</g> +<!-- l11 --> +<g id="node2" class="node"> +<title>l11</title> +<ellipse fill="none" stroke="black" cx="55.9" cy="-234" rx="46.59" ry="18"/> +<text text-anchor="middle" x="55.9" y="-230.3" font-family="Times,serif" font-size="14.00">[V] ◇ p, 2</text> +</g> +<!-- top->l11 --> +<g id="edge1" class="edge"> +<title>top->l11</title> +<path fill="none" stroke="black" d="M100.61,-288.05C93.26,-279.33 84.17,-268.54 76.11,-258.98"/> +<polygon fill="black" stroke="black" points="78.76,-256.7 69.64,-251.31 73.41,-261.21 78.76,-256.7"/> +</g> +<!-- l12 --> +<g id="node3" class="node"> +<title>l12</title> +<ellipse fill="none" stroke="black" cx="173.9" cy="-234" rx="53.09" ry="18"/> +<text text-anchor="middle" x="173.9" y="-230.3" font-family="Times,serif" font-size="14.00">[F] □ ◇ p, 2</text> +</g> +<!-- top->l12 --> +<g id="edge2" class="edge"> +<title>top->l12</title> +<path fill="none" stroke="black" d="M129.18,-288.05C136.35,-279.54 145.18,-269.07 153.09,-259.68"/> +<polygon fill="black" stroke="black" points="155.98,-261.69 159.74,-251.79 150.62,-257.18 155.98,-261.69"/> +</g> +<!-- l21 --> +<g id="node4" class="node"> +<title>l21</title> +<ellipse fill="none" stroke="black" cx="55.9" cy="-162" rx="27" ry="18"/> +<text text-anchor="middle" x="55.9" y="-158.3" font-family="Times,serif" font-size="14.00">p 3</text> +</g> +<!-- l11->l21 --> +<g id="edge3" class="edge"> +<title>l11->l21</title> +<path fill="none" stroke="black" d="M55.9,-215.7C55.9,-207.98 55.9,-198.71 55.9,-190.11"/> +<polygon fill="black" stroke="black" points="59.4,-190.1 55.9,-180.1 52.4,-190.1 59.4,-190.1"/> +</g> +<!-- l22 --> +<g id="node5" class="node"> +<title>l22</title> +<ellipse fill="none" stroke="black" cx="173.9" cy="-162" rx="46.59" ry="18"/> +<text text-anchor="middle" x="173.9" y="-158.3" font-family="Times,serif" font-size="14.00">[V] ◇ p, 3</text> +</g> +<!-- l12->l22 --> +<g id="edge4" class="edge"> +<title>l12->l22</title> +<path fill="none" stroke="black" d="M173.9,-215.7C173.9,-207.98 173.9,-198.71 173.9,-190.11"/> +<polygon fill="black" stroke="black" points="177.4,-190.1 173.9,-180.1 170.4,-190.1 177.4,-190.1"/> +</g> +<!-- l31 --> +<g id="node6" class="node"> +<title>l31</title> +<ellipse fill="none" stroke="black" cx="55.9" cy="-90" rx="55.79" ry="18"/> +<text text-anchor="middle" x="55.9" y="-86.3" font-family="Times,serif" font-size="14.00">Verifier wins</text> +</g> +<!-- l21->l31 --> +<g id="edge5" class="edge"> +<title>l21->l31</title> +<path fill="none" stroke="black" d="M55.9,-143.7C55.9,-135.98 55.9,-126.71 55.9,-118.11"/> +<polygon fill="black" stroke="black" points="59.4,-118.1 55.9,-108.1 52.4,-118.1 59.4,-118.1"/> +</g> +<!-- l32 --> +<g id="node7" class="node"> +<title>l32</title> +<ellipse fill="none" stroke="black" cx="165.9" cy="-90" rx="27" ry="18"/> +<text text-anchor="middle" x="165.9" y="-86.3" font-family="Times,serif" font-size="14.00">p, 2</text> +</g> +<!-- l22->l32 --> +<g id="edge6" class="edge"> +<title>l22->l32</title> +<path fill="none" stroke="black" d="M171.92,-143.7C171.04,-135.98 169.98,-126.71 168.99,-118.11"/> +<polygon fill="black" stroke="black" points="172.46,-117.64 167.85,-108.1 165.51,-118.44 172.46,-117.64"/> +</g> +<!-- l33 --> +<g id="node8" class="node"> +<title>l33</title> +<ellipse fill="none" stroke="black" cx="271.9" cy="-90" rx="27" ry="18"/> +<text text-anchor="middle" x="271.9" y="-86.3" font-family="Times,serif" font-size="14.00">p, 4</text> +</g> +<!-- l22->l33 --> +<g id="edge7" class="edge"> +<title>l22->l33</title> +<path fill="none" stroke="black" d="M195.16,-145.81C209.98,-135.23 229.85,-121.04 245.65,-109.75"/> +<polygon fill="black" stroke="black" points="247.85,-112.47 253.96,-103.81 243.78,-106.78 247.85,-112.47"/> +</g> +<!-- l41 --> +<g id="node9" class="node"> +<title>l41</title> +<ellipse fill="none" stroke="black" cx="148.9" cy="-18" rx="61.19" ry="18"/> +<text text-anchor="middle" x="148.9" y="-14.3" font-family="Times,serif" font-size="14.00">Falsifier wins.</text> +</g> +<!-- l32->l41 --> +<g id="edge8" class="edge"> +<title>l32->l41</title> +<path fill="none" stroke="black" d="M161.78,-72.05C159.89,-64.26 157.59,-54.82 155.47,-46.08"/> +<polygon fill="black" stroke="black" points="158.85,-45.17 153.09,-36.28 152.05,-46.82 158.85,-45.17"/> +</g> +<!-- l42 --> +<g id="node10" class="node"> +<title>l42</title> +<ellipse fill="none" stroke="black" cx="288.9" cy="-18" rx="61.19" ry="18"/> +<text text-anchor="middle" x="288.9" y="-14.3" font-family="Times,serif" font-size="14.00">Falsifier wins.</text> +</g> +<!-- l33->l42 --> +<g id="edge9" class="edge"> +<title>l33->l42</title> +<path fill="none" stroke="black" d="M276.01,-72.05C277.9,-64.26 280.2,-54.82 282.32,-46.08"/> +<polygon fill="black" stroke="black" points="285.74,-46.82 284.7,-36.28 278.94,-45.17 285.74,-46.82"/> +</g> +</g> +</svg> diff --git a/content/advanced-logic-notes/lecture-2/tree.svg b/content/advanced-logic-notes/lecture-2/tree.svg @@ -1,127 +0,0 @@ -<?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: x Pages: 1 --> -<svg width="358pt" height="332pt" - viewBox="0.00 0.00 357.99 332.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 328)"> -<title>x</title> -<polygon fill="white" stroke="transparent" points="-4,4 -4,-328 353.99,-328 353.99,4 -4,4"/> -<!-- top --> -<g id="node1" class="node"> -<title>top</title> -<ellipse fill="none" stroke="black" cx="114.9" cy="-306" rx="77.19" ry="18"/> -<text text-anchor="middle" x="114.9" y="-302.3" font-family="Times,serif" font-size="14.00">[V] ◇ p ∨ □ ◇ p, 2</text> -</g> -<!-- l11 --> -<g id="node2" class="node"> -<title>l11</title> -<ellipse fill="none" stroke="black" cx="55.9" cy="-234" rx="46.59" ry="18"/> -<text text-anchor="middle" x="55.9" y="-230.3" font-family="Times,serif" font-size="14.00">[V] ◇ p, 2</text> -</g> -<!-- top->l11 --> -<g id="edge1" class="edge"> -<title>top->l11</title> -<path fill="none" stroke="black" d="M100.61,-288.05C93.26,-279.33 84.17,-268.54 76.11,-258.98"/> -<polygon fill="black" stroke="black" points="78.76,-256.7 69.64,-251.31 73.41,-261.21 78.76,-256.7"/> -</g> -<!-- l12 --> -<g id="node3" class="node"> -<title>l12</title> -<ellipse fill="none" stroke="black" cx="173.9" cy="-234" rx="53.09" ry="18"/> -<text text-anchor="middle" x="173.9" y="-230.3" font-family="Times,serif" font-size="14.00">[F] □ ◇ p, 2</text> -</g> -<!-- top->l12 --> -<g id="edge2" class="edge"> -<title>top->l12</title> -<path fill="none" stroke="black" d="M129.18,-288.05C136.35,-279.54 145.18,-269.07 153.09,-259.68"/> -<polygon fill="black" stroke="black" points="155.98,-261.69 159.74,-251.79 150.62,-257.18 155.98,-261.69"/> -</g> -<!-- l21 --> -<g id="node4" class="node"> -<title>l21</title> -<ellipse fill="none" stroke="black" cx="55.9" cy="-162" rx="27" ry="18"/> -<text text-anchor="middle" x="55.9" y="-158.3" font-family="Times,serif" font-size="14.00">p 3</text> -</g> -<!-- l11->l21 --> -<g id="edge3" class="edge"> -<title>l11->l21</title> -<path fill="none" stroke="black" d="M55.9,-215.7C55.9,-207.98 55.9,-198.71 55.9,-190.11"/> -<polygon fill="black" stroke="black" points="59.4,-190.1 55.9,-180.1 52.4,-190.1 59.4,-190.1"/> -</g> -<!-- l22 --> -<g id="node5" class="node"> -<title>l22</title> -<ellipse fill="none" stroke="black" cx="173.9" cy="-162" rx="46.59" ry="18"/> -<text text-anchor="middle" x="173.9" y="-158.3" font-family="Times,serif" font-size="14.00">[V] ◇ p, 3</text> -</g> -<!-- l12->l22 --> -<g id="edge4" class="edge"> -<title>l12->l22</title> -<path fill="none" stroke="black" d="M173.9,-215.7C173.9,-207.98 173.9,-198.71 173.9,-190.11"/> -<polygon fill="black" stroke="black" points="177.4,-190.1 173.9,-180.1 170.4,-190.1 177.4,-190.1"/> -</g> -<!-- l31 --> -<g id="node6" class="node"> -<title>l31</title> -<ellipse fill="none" stroke="black" cx="55.9" cy="-90" rx="55.79" ry="18"/> -<text text-anchor="middle" x="55.9" y="-86.3" font-family="Times,serif" font-size="14.00">Verifier wins</text> -</g> -<!-- l21->l31 --> -<g id="edge5" class="edge"> -<title>l21->l31</title> -<path fill="none" stroke="black" d="M55.9,-143.7C55.9,-135.98 55.9,-126.71 55.9,-118.11"/> -<polygon fill="black" stroke="black" points="59.4,-118.1 55.9,-108.1 52.4,-118.1 59.4,-118.1"/> -</g> -<!-- l32 --> -<g id="node7" class="node"> -<title>l32</title> -<ellipse fill="none" stroke="black" cx="165.9" cy="-90" rx="27" ry="18"/> -<text text-anchor="middle" x="165.9" y="-86.3" font-family="Times,serif" font-size="14.00">p, 2</text> -</g> -<!-- l22->l32 --> -<g id="edge6" class="edge"> -<title>l22->l32</title> -<path fill="none" stroke="black" d="M171.92,-143.7C171.04,-135.98 169.98,-126.71 168.99,-118.11"/> -<polygon fill="black" stroke="black" points="172.46,-117.64 167.85,-108.1 165.51,-118.44 172.46,-117.64"/> -</g> -<!-- l33 --> -<g id="node8" class="node"> -<title>l33</title> -<ellipse fill="none" stroke="black" cx="271.9" cy="-90" rx="27" ry="18"/> -<text text-anchor="middle" x="271.9" y="-86.3" font-family="Times,serif" font-size="14.00">p, 4</text> -</g> -<!-- l22->l33 --> -<g id="edge7" class="edge"> -<title>l22->l33</title> -<path fill="none" stroke="black" d="M195.16,-145.81C209.98,-135.23 229.85,-121.04 245.65,-109.75"/> -<polygon fill="black" stroke="black" points="247.85,-112.47 253.96,-103.81 243.78,-106.78 247.85,-112.47"/> -</g> -<!-- l41 --> -<g id="node9" class="node"> -<title>l41</title> -<ellipse fill="none" stroke="black" cx="148.9" cy="-18" rx="61.19" ry="18"/> -<text text-anchor="middle" x="148.9" y="-14.3" font-family="Times,serif" font-size="14.00">Falsifier wins.</text> -</g> -<!-- l32->l41 --> -<g id="edge8" class="edge"> -<title>l32->l41</title> -<path fill="none" stroke="black" d="M161.78,-72.05C159.89,-64.26 157.59,-54.82 155.47,-46.08"/> -<polygon fill="black" stroke="black" points="158.85,-45.17 153.09,-36.28 152.05,-46.82 158.85,-45.17"/> -</g> -<!-- l42 --> -<g id="node10" class="node"> -<title>l42</title> -<ellipse fill="none" stroke="black" cx="288.9" cy="-18" rx="61.19" ry="18"/> -<text text-anchor="middle" x="288.9" y="-14.3" font-family="Times,serif" font-size="14.00">Falsifier wins.</text> -</g> -<!-- l33->l42 --> -<g id="edge9" class="edge"> -<title>l33->l42</title> -<path fill="none" stroke="black" d="M276.01,-72.05C277.9,-64.26 280.2,-54.82 282.32,-46.08"/> -<polygon fill="black" stroke="black" points="285.74,-46.82 284.7,-36.28 278.94,-45.17 285.74,-46.82"/> -</g> -</g> -</svg> diff --git a/content/advanced-logic-notes/lecture-3.md b/content/advanced-logic-notes/lecture-3.md @@ -44,6 +44,7 @@ This holds in the opposite. So the formula □ p → p characterizes the frame property 'reflexivity'. In general, formula φ characterizes the frame property P means: F has property P iff F ⊨ φ. +If you need to prove that a formula characterizes a property, you need to prove this bi-implication in _both_ directions. ## Modal equivalence Two states M, w and M', w' are modally equivalent if they satisfy the same formulas. diff --git a/content/advanced-logic-notes/lecture-4.md b/content/advanced-logic-notes/lecture-4.md @@ -1,38 +0,0 @@ -+++ -title = 'Lecture 4' -template = 'page-math.html' -+++ - -# Lecture 4 -## Bisimulations -A non-empty relation Z ⊆ W × W' is bisimulation ($Z : M \underline{\leftrightarrow} M'$) if for all pairs (w, w') ∈ Z we have: -- w ∈ V(p) iff w' ∈ V'(p) -- if Rwv then for some v' ∈ W' we have R'w'v' and vZv' -- if R'w'v' then for some v ∈ W we have Rwv and vZv' - -Two models are bisimilar ($M \underline{\leftrightarrow} M'$) if there exists a bisimulation Z ∈ W × W'. - -Two pointed models are bisimilar if there exists a bisimulation such that (w,w') ∈ Z - -Two states are modally equivalent if they satisfy exactly the same formulas. -So if M,w and M',w' are bisimilar, then they are modally equivalent. - -## Transforming and constructing models -Disjoint union of models: combine models by union of states, relations, and valuations. -A state in one of the models is modally equivalent with the state in the union. - -Generated submodel: starting from state w, only take its future. - -Tree unravelling: unravelling of world s in (W,R,V) is: -- $W' : (s_{1} \dots s_{n})$ with $s_{1} = s$ and $Rs_{i} s_{i+1}$ -- $R'$ relates ($s_{1} \dots s_{n}$) to ($s_{1} \dots s_{n+1}$) if $Rs_{n} s_{n+1}$ -- $V'(p) = \{ (s_{1} \dots s_{n} | s_{n} \in V(p) \}$ -- a state in (W',R',V') is bisimilar to $s_{n}$ in (W,R,V) -- if φ is satisfiable in M,w it is satisfiable in tree unravelling of s in M - -Bisimulation contraction -- W' consists of equivalence classes |s| = { t such that $s \underline{\leftrightarrow} t$ } -- R' relates |s| to |t| if Ruv for some u ∈ |s| and some v ∈ |t| -- V'(p) = { |s| | s ∈ V(p) } - -If two states are modally equivalent, then they are bisimilar. diff --git a/content/advanced-logic-notes/lecture-4/bisimulation-example.png b/content/advanced-logic-notes/lecture-4/bisimulation-example.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-4/index.md b/content/advanced-logic-notes/lecture-4/index.md @@ -0,0 +1,53 @@ ++++ +title = 'Lecture 4' +template = 'page-math.html' ++++ + +# Lecture 4 +## Bisimulations +A non-empty relation Z ⊆ W × W' is bisimulation ($Z : M \underline{\leftrightarrow} M'$) if for all pairs (w, w') ∈ Z we have: +- w ∈ V(p) iff w' ∈ V'(p) +- if Rwv then for some v' ∈ W' we have R'w'v' and vZv' +- if R'w'v' then for some v ∈ W we have Rwv and vZv' + +Two models are bisimilar ($M \underline{\leftrightarrow} M'$) if there exists a bisimulation Z ∈ W × W'. + +Basically, models are bisimilar if they are, in essence, the same (there may be extra states or relations in one of the models but those states/relations do not add any new information compared to the other model). A bisimulation then is the set of states that are bisimilar between two models. + +Two pointed models are bisimilar if there exists a bisimulation such that (w,w') ∈ Z + +Two states are modally equivalent if they satisfy exactly the same formulas. +So if M,w and M',w' are bisimilar, then they are modally equivalent. + +If two states are modally equivalent, then they are bisimilar. + +### Example +It's a bit hard to describe this in words, but intuitive if you see it. +Here's an example: + + + +You see that from the top state, you can get to a terminal state in one or two steps, in both models. +Therefore, the top states of both models are _bisimilar_. +Since all of the states in the models are bisimilar, _the two models are bisimilar_. +The dotted lines connect the pairs that make up the _bisimulation_. + +## Transforming and constructing models +Disjoint union of models: combine models by union of states, relations, and valuations. +A state in one of the models is modally equivalent with the state in the union. + +Generated submodel: starting from state w, only take its future. + +Tree unravelling: unravelling of world s in (W,R,V) is: +- $W' : (s_{1} \dots s_{n})$ with $s_{1} = s$ and $Rs_{i} s_{i+1}$ +- $R'$ relates ($s_{1} \dots s_{n}$) to ($s_{1} \dots s_{n+1}$) if $Rs_{n} s_{n+1}$ +- $V'(p) = \{ (s_{1} \dots s_{n} | s_{n} \in V(p) \}$ +- a state in (W',R',V') is bisimilar to $s_{n}$ in (W,R,V) +- if φ is satisfiable in M,w it is satisfiable in tree unravelling of s in M + +Bisimulation contraction +- W' consists of equivalence classes |s| = { t such that $s \underline{\leftrightarrow} t$ } +- R' relates |s| to |t| if Ruv for some u ∈ |s| and some v ∈ |t| +- V'(p) = { |s| | s ∈ V(p) } + +More on this, with examples, in [lecture 5](../lecture-5/#transforming-and-constructing-models). diff --git a/content/advanced-logic-notes/lecture-5/index.md b/content/advanced-logic-notes/lecture-5/index.md @@ -11,14 +11,15 @@ Prove by taking modal equivalence as bisimulation. Let Z := {(x, x') | for all φ: x ⊨ φ iff x' ⊨ φ}. Z is a bisimulation. -Local harmony is satisfied. -zig: suppose (x, x') ∈ Z and x → y. -Because x ⊨ ◇ T also x' ⊨ ◇ T. -So x' has finitely many successor y'₁...y'n with n ≥ 1. -Suppose for all i: y is not modally equivalent to y'ᵢ. -There are φ₁...φn such that y ⊨ φᵢ and y'ᵢ notmodel φᵢ. -x ⊨ ◇(φ₁ ∧ ... ∧ φn) so also x' ⊨ ◇ (φ₁ ∧ ... ∧ φn) -Contradiction. +- Local harmony is satisfied. +- zig: suppose (x, x') ∈ Z and x → y. + Because x ⊨ ◇ T also x' ⊨ ◇ T. + So x' has finitely many successors y'₁...y'n with n ≥ 1. + Suppose for all i: y is not modally equivalent to y'ᵢ. + There are φ₁...φn such that y ⊨ φᵢ and y'ᵢ ⊭ φᵢ. + x ⊨ ◇(φ₁ ∧ ... ∧ φn) so also x' ⊨ ◇ (φ₁ ∧ ... ∧ φn). + Contradiction. + Asymmetry is not modally definable. To deal with only frames, we can use surjective bounded morphisms. @@ -53,7 +54,7 @@ Modal formulas are 'nearsighted': - md(φ ∨ ψ) = md(φ ∧ ψ) = max{md(φ), md(ψ)} - md(□ φ) = md(◇ φ) = md(φ) + 1 -We need a formula of model depth k to distuinguish states x and y. +We need a formula of model depth k to distinguish states x and y. Spoiler can win bisimulation game in k rounds. Every winning strategy for Spoiler corresponds to a distinguishing formula. Games of less than k rounds can be won by Duplicator.
