lectures.alex.balgavy.eu

commit 1d66e79e369528044673cd6f8ca6467a0316a1eb
parent 13befac35ead3dada88cb30e1d38f24b7baa3446
Author: Alex Balgavy <alex@balgavy.eu>
Date:   Fri, 11 Mar 2022 20:12:24 +0100

Update advanced logic notes

Diffstat:
M
content/advanced-logic-notes/_index.md
 | 
1
+
A
content/advanced-logic-notes/exercise-4/diagram.dot
 | 
8
++++++++
A
content/advanced-logic-notes/exercise-4/diagram.dot.svg
 | 
44
++++++++++++++++++++++++++++++++++++++++++++
A
content/advanced-logic-notes/exercise-4/index.md
 | 
55
+++++++++++++++++++++++++++++++++++++++++++++++++++++++

4 files changed, 108 insertions(+), 0 deletions(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md
@@ -15,6 +15,7 @@ title = 'Advanced Logic'
 11. [Lecture 8](lecture-8/)
 12. [Lecture 9](lecture-9/)
 13. [Lecture 10](lecture-10/)
+14. [Exercise 4](exercise-4/)
 
 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-4/diagram.dot b/content/advanced-logic-notes/exercise-4/diagram.dot
@@ -0,0 +1,8 @@
+digraph g {
+rankdir=LR
+1 -> 1
+2 -> 2
+2 -> 1
+2 [xlabel="(¬ p)"]
+}
+
diff --git a/content/advanced-logic-notes/exercise-4/diagram.dot.svg b/content/advanced-logic-notes/exercise-4/diagram.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="180pt" height="77pt"
+ viewBox="0.00 0.00 180.00 77.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 73)">
+<title>g</title>
+<polygon fill="white" stroke="transparent" points="-4,4 -4,-73 176,-73 176,4 -4,4"/>
+<!-- 1 -->
+<g id="node1" class="node">
+<title>1</title>
+<ellipse fill="none" stroke="black" cx="145" cy="-33" rx="27" ry="18"/>
+<text text-anchor="middle" x="145" y="-29.3" font-family="Times,serif" font-size="14.00">1</text>
+</g>
+<!-- 1&#45;&gt;1 -->
+<g id="edge1" class="edge">
+<title>1&#45;&gt;1</title>
+<path fill="none" stroke="black" d="M129.77,-48.17C125.16,-58.66 130.23,-69 145,-69 154.92,-69 160.47,-64.33 161.64,-58.09"/>
+<polygon fill="black" stroke="black" points="165.1,-57.57 160.23,-48.17 158.17,-58.56 165.1,-57.57"/>
+</g>
+<!-- 2 -->
+<g id="node2" class="node">
+<title>2</title>
+<ellipse fill="none" stroke="black" cx="55" cy="-33" rx="27" ry="18"/>
+<text text-anchor="middle" x="55" y="-29.3" font-family="Times,serif" font-size="14.00">2</text>
+<text text-anchor="middle" x="14" y="-3.8" font-family="Times,serif" font-size="14.00">(¬ p)</text>
+</g>
+<!-- 2&#45;&gt;1 -->
+<g id="edge3" class="edge">
+<title>2&#45;&gt;1</title>
+<path fill="none" stroke="black" d="M82.4,-33C90.39,-33 99.31,-33 107.82,-33"/>
+<polygon fill="black" stroke="black" points="107.92,-36.5 117.92,-33 107.92,-29.5 107.92,-36.5"/>
+</g>
+<!-- 2&#45;&gt;2 -->
+<g id="edge2" class="edge">
+<title>2&#45;&gt;2</title>
+<path fill="none" stroke="black" d="M39.77,-48.17C35.16,-58.66 40.23,-69 55,-69 64.92,-69 70.47,-64.33 71.64,-58.09"/>
+<polygon fill="black" stroke="black" points="75.1,-57.57 70.23,-48.17 68.17,-58.56 75.1,-57.57"/>
+</g>
+</g>
+</svg>
diff --git a/content/advanced-logic-notes/exercise-4/index.md b/content/advanced-logic-notes/exercise-4/index.md
@@ -0,0 +1,55 @@
++++
+title = 'Exercise 4'
++++
+# Exercise 4
+"show that x not derivable": use soundness and completeness.
+show that there is frame in the right class.
+
+¬ □ ¬ □ p → p not derivable in S4 (I think reflexive + transitive)
+
+![Diagram](diagram.dot.svg)
+
+<details>
+<summary>Graphviz code</summary>
+
+<!-- :Tangle(dot) diagram.dot -->
+```dot
+digraph g {
+rankdir=LR
+1 -> 1
+2 -> 2
+2 -> 1
+2 [xlabel="(¬ p)"]
+}
+```
+
+</details>
+
+Derivation of ¬ □ ¬ □ p → p in S5:
+1. S5 has as axiom ¬ □ p → □ ¬ □ p
+2. ¬ □ ¬ □ p → □ p. prop contrapositive 1
+3. □ p → p. axiom A1.
+4. ¬ □ ¬ □ p → p. prop 2, 3.
+
+## Exercise sheet 5
+### 1a
+N = (ℕ, <). ◇ □ p → □ ◇ p?
+1. take arbitrary valuation for N, M=(N,V).
+2. Take M ∈ N.
+3. Assume n ⊨ ◇ □ p. Goal to show n ⊨ □ ◇ p.
+4. Take x arbitrary successor of n. Goal x ⊨ ◇ p.
+5. x + n > x and x + n ⊨ p.
+6. So x ⊨ ◇ p...and so the formula valid.
+
+### 4b
+Until is not modally definable in BML.
+* Until defined with M,t ⊨ φ U ψ ↔ ∃ v, t < v, v ⊨ ψ, ∀x t < x < v and x ⊨ φ.
+* temporal frame, so irreflexive and transitive
+
+Proof:
+- create two models M where a ⊨ p U q, M' where a' ⊭ p U q.
+- claim bisimilar by giving bisimulation, states a and a'.
+- because a and a' bisimilar, are modally equivalent.
+- suppose that until is definable in BML by a formula ζ(x, y)
+- then we have a ⊨ p U q, so a ⊨ ζ(p, q). Opposite for a'.
+- contradiction, a and a' modally equivalent but satisfy different formulas (i.e. a ⊨ ζ but a' ⊭ ζ).