commit 0a008b59bc549406fc89acbf8afad725cd52758a parent b4ca636c616458caa4b9bf49650bee9709de15e0 Author: Alex Balgavy <alex@balgavy.eu> Date: Tue, 1 Mar 2022 14:12:39 +0100 Update advanced logic lecture notes Diffstat:
12 files changed, 324 insertions(+), 1 deletion(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md @@ -7,7 +7,9 @@ title = 'Advanced Logic' 3. [Exercise 1](exercise-1/) 4. [Lecture 3](lecture-3/) 5. [Lecture 4](lecture-4/) -6. [Exercise 3](exercise-3/) +6. [Lecture 5](lecture-5/) +7. [Lecture 6](lecture-6/) +8. [Exercise 3](exercise-3/) 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/lecture-5/index.md b/content/advanced-logic-notes/lecture-5/index.md @@ -0,0 +1,126 @@ ++++ +title = 'Lecture 5' +template = 'page-math.html' ++++ +# Lecture 5 +If two states are bisimilar, then they are modally equivalent. +Prove by induction on definition of formulas. + +For finitely branching models, if two states modally equivalent, then they are bisimilar. +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. + +Asymmetry is not modally definable. +To deal with only frames, we can use surjective bounded morphisms. + +Function f : W → W' is bounded morphism from (W,R) to (W',R') if: +- for all w,v ∈ W: if Rwv then Rf(w)f(v) +- for all w ∈ W and for all v' ∈ W': if R'f(w)v' then there exists v ∈ W such that f(v) = v' and Rwv + +A bounded morphism f is surjective if for every w' ∈ W' there exists w ∈ W such that f(w) = w' + +If f: W → W' is surjective bounded morphism from (W,R) to (W',R'), then if (W,R) ⊨ φ then (W', R') ⊨ φ + +### Bisimulation games for two players +Spoiler S claims M,s an N,t to be different. +Duplicator D claims they are similar. + +Play consists of sequence of links, starting with link s ~ t. + +At current link m ~ n (with m in M and n in N): +- if m an n different in their atoms, then S wins +- if not, then S picks a successor x either of m or of n +- then D has to find a matching transition to y in the other model +- play continues with next link x ~ y (or y ~ x) + +If player cannot make a move, he loses. +D wins infinite games. + +Modal depth of formulas. +Modal formulas are 'nearsighted': +- md(p) = md(⊥) = md(T) = 0 +- md(¬φ) = md(φ) +- md(φ ∨ ψ) = md(φ ∧ ψ) = max{md(φ), md(ψ)} +- md(□ φ) = md(◇ φ) = md(φ) + 1 + +We need a formula of model depth k to distuinguish 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. +Formulas of modal depth less than k cannot distinguish between x and y. + +M,s and N,t satisfy the same formulas up to modal depth k iff duplicator has winning strategy in the k-round game starting in s ~ t. +If Spoiler can win in k rounds, then there is a distinguishing formula of modal depth k. + +### Transforming and constructing models +#### Tree unraveling +Basically taking the states with possible paths between them, and drawing a tree. + +Example: + +<table> +<tr> <th>Model</th> <th>Tree unraveling</th> </tr> + +<tr> +<td> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) model-diagram.dot --> +```dot +digraph g { +1 -> 2 +1 -> 1 +} +``` + +</details> +</td> +<td> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) tree-unraveling.dot --> +```dot +digraph g { +a [label="(1)"] +b [label="(1,2)"]; a -> b +c [label="(1,1)"]; a -> c +d [label="(1,1,2)"]; c -> d +e [label="(1,1,1)"]; c -> e +f [label="(1,1,1,2)"]; e -> f +g [label="..."]; e -> g +} +``` + +</details> + +</td> +</tr> +</table> + +If two trees have the same structure, they're bisimilar. + +#### Model contraction +Basically getting rid of 'unnecessary' states. + + + +### Validity and satisfiability +If φ is satisfiable, then it is satisfiable using a model with at most $2^{s(\phi)}$ elements with s(φ) the number of subformulas of φ. diff --git a/content/advanced-logic-notes/lecture-5/model-contraction.png b/content/advanced-logic-notes/lecture-5/model-contraction.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-5/model-diagram.dot b/content/advanced-logic-notes/lecture-5/model-diagram.dot @@ -0,0 +1,5 @@ +digraph g { +1 -> 2 +1 -> 1 +} + diff --git a/content/advanced-logic-notes/lecture-5/model-diagram.dot.svg b/content/advanced-logic-notes/lecture-5/model-diagram.dot.svg @@ -0,0 +1,37 @@ +<?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="80pt" height="116pt" + viewBox="0.00 0.00 80.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 76,-112 76,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">1</text> +</g> +<!-- 1->1 --> +<g id="edge2" class="edge"> +<title>1->1</title> +<path fill="none" stroke="black" d="M46.9,-102.43C59.69,-105.68 72,-101.53 72,-90 72,-81.62 65.5,-77.14 57.04,-76.56"/> +<polygon fill="black" stroke="black" points="56.5,-73.1 46.9,-77.57 57.19,-80.07 56.5,-73.1"/> +</g> +<!-- 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="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-5/tree-unraveling.dot b/content/advanced-logic-notes/lecture-5/tree-unraveling.dot @@ -0,0 +1,10 @@ +digraph g { +a [label="(1)"] +b [label="(1,2)"]; a -> b +c [label="(1,1)"]; a -> c +d [label="(1,1,2)"]; c -> d +e [label="(1,1,1)"]; c -> e +f [label="(1,1,1,2)"]; e -> f +g [label="..."]; e -> g +} + diff --git a/content/advanced-logic-notes/lecture-5/tree-unraveling.dot.svg b/content/advanced-logic-notes/lecture-5/tree-unraveling.dot.svg @@ -0,0 +1,91 @@ +<?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="223pt" height="260pt" + viewBox="0.00 0.00 222.95 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>g</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-256 218.95,-256 218.95,4 -4,4"/> +<!-- a --> +<g id="node1" class="node"> +<title>a</title> +<ellipse fill="none" stroke="black" cx="64.95" cy="-234" rx="27" ry="18"/> +<text text-anchor="middle" x="64.95" y="-230.3" 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="27.95" cy="-162" rx="27.9" ry="18"/> +<text text-anchor="middle" x="27.95" y="-158.3" font-family="Times,serif" font-size="14.00">(1,2)</text> +</g> +<!-- a->b --> +<g id="edge1" class="edge"> +<title>a->b</title> +<path fill="none" stroke="black" d="M56.37,-216.76C51.88,-208.28 46.3,-197.71 41.27,-188.2"/> +<polygon fill="black" stroke="black" points="44.25,-186.35 36.48,-179.15 38.06,-189.62 44.25,-186.35"/> +</g> +<!-- c --> +<g id="node3" class="node"> +<title>c</title> +<ellipse fill="none" stroke="black" cx="101.95" cy="-162" rx="27.9" ry="18"/> +<text text-anchor="middle" x="101.95" y="-158.3" font-family="Times,serif" font-size="14.00">(1,1)</text> +</g> +<!-- a->c --> +<g id="edge2" class="edge"> +<title>a->c</title> +<path fill="none" stroke="black" d="M73.53,-216.76C78.01,-208.28 83.6,-197.71 88.63,-188.2"/> +<polygon fill="black" stroke="black" points="91.83,-189.62 93.41,-179.15 85.65,-186.35 91.83,-189.62"/> +</g> +<!-- d --> +<g id="node4" class="node"> +<title>d</title> +<ellipse fill="none" stroke="black" cx="57.95" cy="-90" rx="34.39" ry="18"/> +<text text-anchor="middle" x="57.95" y="-86.3" font-family="Times,serif" font-size="14.00">(1,1,2)</text> +</g> +<!-- c->d --> +<g id="edge3" class="edge"> +<title>c->d</title> +<path fill="none" stroke="black" d="M91.96,-145.12C86.53,-136.47 79.68,-125.58 73.56,-115.83"/> +<polygon fill="black" stroke="black" points="76.48,-113.91 68.2,-107.31 70.56,-117.64 76.48,-113.91"/> +</g> +<!-- e --> +<g id="node5" class="node"> +<title>e</title> +<ellipse fill="none" stroke="black" cx="144.95" cy="-90" rx="34.39" ry="18"/> +<text text-anchor="middle" x="144.95" y="-86.3" font-family="Times,serif" font-size="14.00">(1,1,1)</text> +</g> +<!-- c->e --> +<g id="edge4" class="edge"> +<title>c->e</title> +<path fill="none" stroke="black" d="M111.7,-145.12C117.02,-136.47 123.71,-125.58 129.69,-115.83"/> +<polygon fill="black" stroke="black" points="132.68,-117.66 134.93,-107.31 126.71,-114 132.68,-117.66"/> +</g> +<!-- f --> +<g id="node6" class="node"> +<title>f</title> +<ellipse fill="none" stroke="black" cx="100.95" cy="-18" rx="41.69" ry="18"/> +<text text-anchor="middle" x="100.95" y="-14.3" font-family="Times,serif" font-size="14.00">(1,1,1,2)</text> +</g> +<!-- e->f --> +<g id="edge5" class="edge"> +<title>e->f</title> +<path fill="none" stroke="black" d="M134.74,-72.76C129.43,-64.32 122.82,-53.8 116.86,-44.31"/> +<polygon fill="black" stroke="black" points="119.69,-42.24 111.4,-35.63 113.76,-45.96 119.69,-42.24"/> +</g> +<!-- g --> +<g id="node7" class="node"> +<title>g</title> +<ellipse fill="none" stroke="black" cx="187.95" cy="-18" rx="27" ry="18"/> +<text text-anchor="middle" x="187.95" y="-14.3" font-family="Times,serif" font-size="14.00">...</text> +</g> +<!-- e->g --> +<g id="edge6" class="edge"> +<title>e->g</title> +<path fill="none" stroke="black" d="M154.92,-72.76C160.19,-64.19 166.76,-53.49 172.65,-43.9"/> +<polygon fill="black" stroke="black" points="175.78,-45.5 178.03,-35.15 169.81,-41.84 175.78,-45.5"/> +</g> +</g> +</svg> diff --git a/content/advanced-logic-notes/lecture-6/example-tableau.png b/content/advanced-logic-notes/lecture-6/example-tableau.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-6/index.md b/content/advanced-logic-notes/lecture-6/index.md @@ -0,0 +1,52 @@ ++++ +title = 'Lecture 6' ++++ +# Lecture 6 +## Sequents +φ₁...φn ⇒ ψ₁...ψm valid if in every model, in every world in that model, the conjunction of the φᵢ implies the disjunction of the ψᵢ. + +Empty conjunction is true, empty disjunction is false. + +Reducing modal sequents: + + + +φ valid iff the sequent (⇒ φ) valid. + +For modal logic: +- If we get a sequent of the form p₁...n, ◇φ₁..◇φm ⇒ q₁..qk, ◇ψ₁...◇ψl +- Such a sequent only valid iff either pᵢ = qj for some i and j, or φᵢ ⇒ ψ₁...ψl is valid for some i ∈ {1...m} + +Start with intended conclusion, try to build a proof while moving upwards. +Formula is valid iff it is derivable in sequent calculus. +Validity using sequents: +1. Rewrite formula + - (a → b) to (¬ a ∨ b) + - (¬ □ a) to (◇ ¬ a) + - (□ a) to (¬ ◇ ¬ a) + +2. Rewrite sequent, based on rules above +3. Maybe rewrite formula again +4. Decide on validity of sequent +5. Conclude on validity of formula + +## Tableaux +Tableau is finite tree of sequents. +If all solid branches close, yields validity of initial sequent. +If at least one branch does not close, yields a counterexample. + +The dot separates assumptions on the left from what's true on the right. +A branch closes if what's assumed also holds in the state. + + + +In modal logic: + + + +Example: + + + +It's not valid because in the two red states, the letters on the left of the dot are not on the right. +The countermodel comes from taking the numbers next to each step (the numbers are states), connecting them, and creating a valuation where the letters on the left side of the dot (the assumptions) are true. diff --git a/content/advanced-logic-notes/lecture-6/reducing-modal-sequents.png b/content/advanced-logic-notes/lecture-6/reducing-modal-sequents.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-6/tableau-modal-logic.png b/content/advanced-logic-notes/lecture-6/tableau-modal-logic.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-6/tableau-rules.png b/content/advanced-logic-notes/lecture-6/tableau-rules.png Binary files differ.
