commit ec95456119d26bdc0240bfd25d2b0d0032950c79
parent 6b27e16f6670a5753ea79d8bf72c75069b6401c5
Author: Alex Balgavy <alex@balgavy.eu>
Date: Sat, 19 Mar 2022 00:10:16 +0100
Update advanced logic notes
Diffstat:
9 files changed, 235 insertions(+), 0 deletions(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md
@@ -19,6 +19,7 @@ title = 'Advanced Logic'
15. [Some midterm solutions](some-midterm-solutions/)
16. [Lecture 11](lecture-11/)
17. [Lecture 12](lecture-12/)
+18. [Exercise 5](exercise-5/)
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/exercise-5/index.md b/content/advanced-logic-notes/exercise-5/index.md
@@ -0,0 +1,45 @@
++++
+title = 'Exercise 5'
+template = 'page-math.html'
++++
+# Exercise 5
+## 2b
+Show validity of: [a\*] ↔ φ ∧ [α][α\*]φ
+- Take a PDL model M = ((W,R),V) and let x ∈ W
+- Implication left-to-right:
+ - assume x ⊨ [a\*]φ
+ - so for every y ∈ W such that $(x,y) \in R_{\alpha *}$, y ⊨ φ
+ - because M is a PDL model, $R_{\alpha \*} = (R_{\alpha})\* = R_{\alpha}^{0} \cup R_{\alpha}^{1} \cup R_{\alpha}^{2} \dots$
+ - So $R_{\alpha}^{0} = Id \subseteq R_{\alpha \*}$ so $(x,x) \in R_{\alpha \*}$ so x ⊨ φ.
+ - To prove x ⊨ [α][α\*]φ, take u ∈ W such that $(x,u) \in R_{\alpha}^{1}$.
+ - Aim to show u ⊨ [α\*]φ
+ - Take state v ∈ W such that $(u,v) \in R_{\alpha \*}$
+ - We have $(x,u) \in (R_{\alpha} ; R_{\alpha \*}) \subseteq R_{\alpha \*}$
+ - So $(x,v) \in R_{\alpha \*}$ so v ⊨ φ (because x ⊨ [α\*]φ)
+- Other way is similar.
+
+## 4
+### a
+
+
+$\begin{aligned}
+\delta &= \text{while $\lnot p$ do $b \cup ac$} \\\\
+\hat{R}_{\lnot p} &= \\{(2,2), (3,3), (4,4)\\} \\\\
+\hat{R}\_{ac} &= R\_{a}; R\_{c} = \\{(1,2), (2,3), (4,3)\\}; \\{(3,1)\\} \\\\
+ &= \\{(2,1), (4,1) \\} \\\\
+R\_{b \cup ac} &= R\_{b} \cup R\_{ac} = \\{(3,4), (3,2), (2,1) \\} \cup \\{(2,1), (4,1)\\} \\\\
+ &= \\{(3,4), (3,2), (2,1), (4,1)\\} \\\\
+R\_{\lnot p; b \cup ac} &= \\{ (2,2), (3,3), (4,4) \\}; \\{(3,4), (3,2), (2,1), (4,1) \\} \\\\
+ &= \\{(2,1), (3,4), (3,2), (4,1) \\} \\\\
+R\_{(\lnot p; b \cup ac)*}: R\_{\lnot p; b \cup ac}^{0} &= \\{(1,1), (2,2), (3,3), (4,4) \\} \\\\
+R\_{\lnot p; b \cup ac}^{1} &= \\{(2,1), (3,4), (3,2), (4,1)\\} \\\\
+R\_{\lnot p; b \cup ac}^{2} &= R\_{\lnot p; b \cup ac}^{1} \cup \\{(3,1)\\} \\\\
+R\_{p} &= \\{(1,1)\\} \\\\
+R\_{\delta} &= \\{(1,1), (2,1), (4,1), (3,1) \\}
+\end{aligned}$
+
+
+### b
+M ?⊨ [δ]p → p
+- No.
+- For example, 2 ⊨ [δ]p because $(2,1) \in R_{\delta}$ and 1 ⊨ p, but 2 ⊭ p.
diff --git a/content/advanced-logic-notes/some-midterm-solutions/bisimulation-contraction.dot b/content/advanced-logic-notes/some-midterm-solutions/bisimulation-contraction.dot
@@ -0,0 +1,7 @@
+digraph g {
+ac -> b
+b -> ac
+ac -> ac
+b [xlabel="[p]"]
+}
+
diff --git a/content/advanced-logic-notes/some-midterm-solutions/bisimulation-contraction.dot.svg b/content/advanced-logic-notes/some-midterm-solutions/bisimulation-contraction.dot.svg
@@ -0,0 +1,44 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
+ "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<!-- Generated by graphviz version 2.50.0 (20211204.2007)
+ -->
+<!-- Title: g Pages: 1 -->
+<svg width="96pt" height="116pt"
+ viewBox="0.00 0.00 96.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 92,-112 92,4 -4,4"/>
+<!-- ac -->
+<g id="node1" class="node">
+<title>ac</title>
+<ellipse fill="none" stroke="black" cx="43" cy="-90" rx="27" ry="18"/>
+<text text-anchor="middle" x="43" y="-86.3" font-family="Times,serif" font-size="14.00">ac</text>
+</g>
+<!-- ac->ac -->
+<g id="edge3" class="edge">
+<title>ac->ac</title>
+<path fill="none" stroke="black" d="M62.9,-102.43C75.69,-105.68 88,-101.53 88,-90 88,-81.62 81.5,-77.14 73.04,-76.56"/>
+<polygon fill="black" stroke="black" points="72.5,-73.1 62.9,-77.57 73.19,-80.07 72.5,-73.1"/>
+</g>
+<!-- b -->
+<g id="node2" class="node">
+<title>b</title>
+<ellipse fill="none" stroke="black" cx="43" cy="-18" rx="27" ry="18"/>
+<text text-anchor="middle" x="43" y="-14.3" font-family="Times,serif" font-size="14.00">b</text>
+<text text-anchor="middle" x="8" y="-39.8" font-family="Times,serif" font-size="14.00">[p]</text>
+</g>
+<!-- ac->b -->
+<g id="edge1" class="edge">
+<title>ac->b</title>
+<path fill="none" stroke="black" d="M37.16,-72.41C36.3,-64.51 36.05,-54.85 36.41,-45.94"/>
+<polygon fill="black" stroke="black" points="39.9,-46.18 37.12,-35.96 32.92,-45.68 39.9,-46.18"/>
+</g>
+<!-- b->ac -->
+<g id="edge2" class="edge">
+<title>b->ac</title>
+<path fill="none" stroke="black" d="M48.88,-35.96C49.71,-43.83 49.95,-53.37 49.58,-62.19"/>
+<polygon fill="black" stroke="black" points="46.07,-62.18 48.84,-72.41 53.06,-62.69 46.07,-62.18"/>
+</g>
+</g>
+</svg>
diff --git a/content/advanced-logic-notes/some-midterm-solutions/index.md b/content/advanced-logic-notes/some-midterm-solutions/index.md
@@ -39,3 +39,86 @@ rankdir=LR
"Has no blind successor": ¬ ◇ □ ⊥, □ ◇ T ("wherever I go, I can do a step"), □ ¬ □ ⊥
"Has at least one non blind successor": ◇ ◇ T
+
+## Bisimulation & contraction
+That question about two models, if asked say they are bisimilar, just give a bisimulation and say the pair consisting of the two states is in the bisimulation.
+
+The bisimulation contraction is then:
+
+
+
+<details>
+<summary>Graphviz code</summary>
+
+<!-- :Tangle(dot) bisimulation-contraction.dot -->
+```dot
+digraph g {
+ac -> b
+b -> ac
+ac -> ac
+b [xlabel="[p]"]
+}
+```
+
+</details>
+
+## Global diamond
+Asked to see if global diamond is definable in basic modal logic (BML), as given by: M,x ⊨ E φ iff there is y ∈ W such that y ⊨ φ.
+(Side remark: if we can define it, the operator is like an abbreviation, it doesn't change the expressive power).
+
+Steps:
+- Suppose E is definable in BML by ζ.
+- Suppose Ep is definable in BML by ζ(p).
+- Consider the models:
+
+ <table>
+ <thead><th>M</th><th>N</th></thead>
+ <tbody>
+ <tr>
+ <td>
+
+ <img alt="Model M" src="model-m.dot.svg"/>
+
+ <details>
+ <summary>Graphviz code</summary>
+
+ <!-- :Tangle(dot) model-m.dot -->
+ ```dot
+ digraph g {
+ a
+ b [label="b | [p]"]
+ }
+ ```
+
+ </details>
+ </td>
+
+ <td>
+
+ <img alt="Model N" src="model-n.dot.svg"/>
+
+ <details>
+ <summary>Graphviz code</summary>
+
+ <!-- :Tangle(dot) model-n.dot -->
+ ```dot
+ digraph g {
+ x
+ }
+ ```
+
+ </details>
+ </td>
+ </tr>
+ </tbody>
+ </table>
+
+- We have M,a ⊨ Ep because M,b ⊨ p, so M,a ⊨ ζ(p).
+- N,x ⊭ Ep so N,x ⊭ ζ(p).
+- We have M,a bisimilar with N,x because Z = {(a,x)} is a bisimulation and (a,x) ∈ Z.
+- Because bisimilar states are modally equivalent, they must make true the same formulas in BML. So a ⊨ ζ(p) iff x ⊨ ζ(p).
+- Contradiction: N,x ⊭ ζ(p)
+- So, the assumption that E is definable in BML does not hold.
+- Therefore, E is not definable in BML.
+
+
diff --git a/content/advanced-logic-notes/some-midterm-solutions/model-m.dot b/content/advanced-logic-notes/some-midterm-solutions/model-m.dot
@@ -0,0 +1,5 @@
+digraph g {
+a
+b [label="b | [p]", shape="Mrecord"]
+}
+
diff --git a/content/advanced-logic-notes/some-midterm-solutions/model-m.dot.svg b/content/advanced-logic-notes/some-midterm-solutions/model-m.dot.svg
@@ -0,0 +1,27 @@
+<?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="136pt" height="45pt"
+ viewBox="0.00 0.00 135.50 45.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 41)">
+<title>g</title>
+<polygon fill="white" stroke="transparent" points="-4,4 -4,-41 131.5,-41 131.5,4 -4,4"/>
+<!-- a -->
+<g id="node1" class="node">
+<title>a</title>
+<ellipse fill="none" stroke="black" cx="27" cy="-18.5" rx="27" ry="18"/>
+<text text-anchor="middle" x="27" y="-14.8" font-family="Times,serif" font-size="14.00">a</text>
+</g>
+<!-- b -->
+<g id="node2" class="node">
+<title>b</title>
+<path fill="none" stroke="black" d="M84.5,-0.5C84.5,-0.5 115.5,-0.5 115.5,-0.5 121.5,-0.5 127.5,-6.5 127.5,-12.5 127.5,-12.5 127.5,-24.5 127.5,-24.5 127.5,-30.5 121.5,-36.5 115.5,-36.5 115.5,-36.5 84.5,-36.5 84.5,-36.5 78.5,-36.5 72.5,-30.5 72.5,-24.5 72.5,-24.5 72.5,-12.5 72.5,-12.5 72.5,-6.5 78.5,-0.5 84.5,-0.5"/>
+<text text-anchor="middle" x="84" y="-14.8" font-family="Times,serif" font-size="14.00">b</text>
+<polyline fill="none" stroke="black" points="95.5,-0.5 95.5,-36.5 "/>
+<text text-anchor="middle" x="111.5" y="-14.8" font-family="Times,serif" font-size="14.00">[p]</text>
+</g>
+</g>
+</svg>
diff --git a/content/advanced-logic-notes/some-midterm-solutions/model-n.dot b/content/advanced-logic-notes/some-midterm-solutions/model-n.dot
@@ -0,0 +1,4 @@
+digraph g {
+x
+}
+
diff --git a/content/advanced-logic-notes/some-midterm-solutions/model-n.dot.svg b/content/advanced-logic-notes/some-midterm-solutions/model-n.dot.svg
@@ -0,0 +1,19 @@
+<?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="44pt"
+ viewBox="0.00 0.00 62.00 44.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
+<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 40)">
+<title>g</title>
+<polygon fill="white" stroke="transparent" points="-4,4 -4,-40 58,-40 58,4 -4,4"/>
+<!-- x -->
+<g id="node1" class="node">
+<title>x</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">x</text>
+</g>
+</g>
+</svg>
