commit 5475f4bdc98f3d89c5eac9c449c5a4d39e022b71
parent 160b714ff6f80a919ed860806d788bb9dde31ec0
Author: Alex Balgavy <alex@balgavy.eu>
Date: Thu, 10 Feb 2022 13:40:52 +0100
Advanced logic update
Diffstat:
6 files changed, 336 insertions(+), 0 deletions(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md
@@ -3,3 +3,4 @@ title = 'Advanced Logic'
+++
# Advanced Logic
1. [Lecture 1](lecture-1)
+2. [Lecture 2](lecture-2)
diff --git a/content/advanced-logic-notes/lecture-1/index.md b/content/advanced-logic-notes/lecture-1/index.md
@@ -8,6 +8,8 @@ Basic model logic operators:
- □: necessary, known, provable
- ◇: possible, considered possible
+In a diagram, one of these symbols is exactly one transition step (use multiple for multiple steps).
+
- ◇ φ ⇔ ¬□ ¬φ
- □ φ ⇔ ¬◇ ¬φ
diff --git a/content/advanced-logic-notes/lecture-2/digraph.svg b/content/advanced-logic-notes/lecture-2/digraph.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: 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/example-characterizing.png b/content/advanced-logic-notes/lecture-2/example-characterizing.png
Binary files differ.
diff --git a/content/advanced-logic-notes/lecture-2/index.md b/content/advanced-logic-notes/lecture-2/index.md
@@ -0,0 +1,127 @@
++++
+title = 'Lecture 2'
++++
+# Lecture 2
+## Semantics: local truth
+Valuation notation:
+- V : Var → P(W) means Var → W → {0,1}
+- V(p,w) = 1 is the same as w ∈ V(p)
+
+A formula φ _characterizes_ a state x in model M if φ is true in x but not in other states of M.
+
+A formula φ _distinguishes_ state x from state y in a model M if φ is true in x but not in y.
+
+
+
+Above:
+- the formula 3 ⊨ □ ⊥ characterizes state 3
+- the formula 2 ⊨ ◇ □ ⊥ characterizes state 2
+
+## Game semantics
+We have:
+- model M = ((W,R), V), world w ∈ W, formula φ
+- two players:
+ - Verifier V claims that φ is true in w (sort of like ∀)
+ - Falsifier F claims that φ is false in w (sort of like ∃, try to find a _witness_)
+- position: pair (w, φ) with w ∈ W a world and φ a formula
+- move: from position (w, φ), determined by main operator of φ
+
+Assume that negation only applied to prop. variables.
+Transform formulas from ¬ □ p to ◇ ¬ p, ¬(p ∧ q) to ¬p ∨ ¬q.
+
+The position determines the move, e.g. in a position (t, ◇ φ), V chooses a successor _u_ of _t_, and play continues with (u, φ).
+For (t,p), if p is true in t then V wins, otherwise F wins.
+For (t, ¬p), if p is false in t then V wins, otherwise F wins.
+If a player should but cannot choose a successor, they lose.
+
+Who starts:
+- V: ∨, ◇
+- F: ∧, □
+
+A complete game tree for φ and (M,w) starts with (w,φ) and contains all possible moves.
+A strategy for player P is subset of steps for P, and it's a winning strategy if it ensures that P wins the game.
+φ is true in M in s ⇔ V has a winning strategy for M,s,φ.
+
+### Example
+Diagram:
+
+
+<details>
+<summary>PlantUML/Dot code</summary>
+```plantuml
+@startdot
+digraph example {
+1 -> 2
+1 -> 3
+2 -> 3
+3 -> 2
+3 -> 4
+4 -> 2
+4 -> 3
+}
+@enddot
+```
+</details>
+
+formula ◇ p ∨ □ ◇ p, in state 2.
+
+p is true in state 3.
+
+Complete game tree:
+
+
+
+<details>
+<summary>PlantUML/Dot code</summary>
+```plantuml
+@startdot
+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
+}
+@enddot
+```
+</details>
+
+## Truth and validity
+(((W,R),V),w) ⊨ φ means φ is valid in a point w.
+(W,R) ⊨ φ means φ is valid in a frame (W,R).
+⊨ φ means φ is valid/tautology.
+If a part is omitted, it's implicitly universally quantified.
+
+Satisfiability:
+- φ _satisfiable in model M_ if there's a world w ∈ M such that M,w ⊨ φ
+- φ _satisfiable_ if there's a model M and a world w ∈ M such that M,w ⊨ φ
+- φ and ψ _semantically equivalent_ if ∀ M,w: M,w ⊨ φ ⇔ M,w ⊨ ψ
+- φ valid iff ¬ φ not satisfiable
+
+### Example
+Show universal validity of □ (φ → ψ) → (□ φ → □ ψ)
+
+1. let F = (W,R) be frame, V valuation on F, let x ∈ W.
+2. Assume a1: F,V,x ⊨ □ (φ → ψ)
+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.
+7. Have y ⊨ φ → ψ and y ⊨ φ.
+8. From a2, have y ⊨ φ.
+9. From a1, have have y ⊨ ψ.
+10. Hence x ⊨ □ ψ, hence x ⊨ □ φ → □ ψ. Hence formula is valid.
diff --git a/content/advanced-logic-notes/lecture-2/tree.svg b/content/advanced-logic-notes/lecture-2/tree.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: 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>
