commit 9ee9ee677ad1a21810c947573692b501ff2ab897
parent 787a5d8badcbe9cdc2dd14f4e3c7876c78e6d7da
Author: Alex Balgavy <alex@balgavy.eu>
Date: Tue, 15 Mar 2022 20:48:23 +0100
Update advanced logic notes
Diffstat:
8 files changed, 126 insertions(+), 1 deletion(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md
@@ -16,6 +16,8 @@ title = 'Advanced Logic'
12. [Lecture 9](lecture-9/)
13. [Lecture 10](lecture-10/)
14. [Exercise 4](exercise-4/)
+15. [Some midterm solutions](some-midterm-solutions/)
+15. [Lecture 11](lecture-11/)
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-11/formula-examples.png b/content/advanced-logic-notes/lecture-11/formula-examples.png
Binary files differ.
diff --git a/content/advanced-logic-notes/lecture-11/index.md b/content/advanced-logic-notes/lecture-11/index.md
@@ -0,0 +1,29 @@
++++
+title = 'Lecture 11'
++++
+# Lecture 11
+In propositional dynamic logic (PDL), aim to prove: φ → [while σ do α] ψ
+- i.e. starting with φ true, for any terminating execution of the program, we have ψ true.
+
+Definitions:
+- state of program execution: state/world
+- program: regular program which slightly generalizes a while program
+- statement {pre}program{post}: formula pre → [program] post
+
+For every program α we have modality \<α\>:
+- \<α\>: it's possible to execute α from current state, and successfully halt in state satisfying φ (like existential quantification)
+- [α]φ: for all executions of α, if α successfully halts, then it halts in a state satisfying φ (like universal quantification)
+
+Program definitions:
+- a: program from set A of atomic programs (letters, like in prop. logic)
+- α; β: sequential composition
+- α ∪ β: non-deterministic choice
+- α\*: iteration, 0 or more times.
+- φ?: test, depends on the grammar for formulas
+ - if φ then continue without changing state, if not then block without halting
+
+Examples of formulas:
+
+
+
+We obtain semantics of PDL as instance of multi-modal logic.
diff --git a/content/advanced-logic-notes/lecture-8/index.md b/content/advanced-logic-notes/lecture-8/index.md
@@ -31,7 +31,7 @@ Need to memorize soundness and completeness results
- T: K with □ p → p
- S4 sound and complete for all _reflexive-transitive_ frames
- S4: T with □ p → □ □ p
-- S5 sound and complete for for frames with R an equivalence relation
+- S5 sound and complete for all frames with R an equivalence relation
- S5: S4 with ¬ □ p → □ ¬ □ p
## Example of derivation
diff --git a/content/advanced-logic-notes/some-midterm-solutions/counter-model.dot b/content/advanced-logic-notes/some-midterm-solutions/counter-model.dot
@@ -0,0 +1,7 @@
+digraph g {
+rankdir=LR
+1 -> 2
+1 -> 3
+3 [xlabel="p"]
+}
+
diff --git a/content/advanced-logic-notes/some-midterm-solutions/counter-model.dot.svg b/content/advanced-logic-notes/some-midterm-solutions/counter-model.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="152pt" height="113pt"
+ viewBox="0.00 0.00 152.00 113.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 109)">
+<title>g</title>
+<polygon fill="white" stroke="transparent" points="-4,4 -4,-109 148,-109 148,4 -4,4"/>
+<!-- 1 -->
+<g id="node1" class="node">
+<title>1</title>
+<ellipse fill="none" stroke="black" cx="27" cy="-60" rx="27" ry="18"/>
+<text text-anchor="middle" x="27" y="-56.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="117" cy="-87" rx="27" ry="18"/>
+<text text-anchor="middle" x="117" y="-83.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="M52.05,-67.38C61.44,-70.26 72.36,-73.61 82.5,-76.72"/>
+<polygon fill="black" stroke="black" points="81.7,-80.14 92.29,-79.72 83.75,-73.45 81.7,-80.14"/>
+</g>
+<!-- 3 -->
+<g id="node3" class="node">
+<title>3</title>
+<ellipse fill="none" stroke="black" cx="117" cy="-33" rx="27" ry="18"/>
+<text text-anchor="middle" x="117" y="-29.3" font-family="Times,serif" font-size="14.00">3</text>
+<text text-anchor="middle" x="86.5" y="-3.8" font-family="Times,serif" font-size="14.00">p</text>
+</g>
+<!-- 1->3 -->
+<g id="edge2" class="edge">
+<title>1->3</title>
+<path fill="none" stroke="black" d="M52.05,-52.62C61.44,-49.74 72.36,-46.39 82.5,-43.28"/>
+<polygon fill="black" stroke="black" points="83.75,-46.55 92.29,-40.28 81.7,-39.86 83.75,-46.55"/>
+</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
@@ -0,0 +1,41 @@
++++
+title = 'Some midterm solutions'
++++
+# Some midterm solutions
+## Universal validity
+Is this formula universally valid: ◇ (p → q) → (◇ p → ◇ q)
+- Take arbitrary frame F = (W,R) and arbitrary valuation V for F.
+- Take arbitrary state x ∈ W
+- ? F,V,x ⊨ φ
+- Assume x ⊨ ◇ (p → q). That is: there is a state y ∈ W such that Rxy and y ⊨ p → q
+- Want to show x ⊨ ◇ p → ◇ q
+- Assume x ⊨ ◇ p. That is: there is a state z ∈ W such that Rxz and z ⊨ p.
+- Note: y and z are not necessarily the same! (but they might be)
+- Counter-model:
+
+ 
+
+ - 3 ⊨ p so 1 ⊨ ◇ p
+ - 2 ⊨ ¬ p so 2 ⊨ p → q so 1 ⊨ ◇ (p → q)
+ - 2 ⊭ q, 3 ⊭ q so 1 ⊭ ◇ q
+- By counter-model, the formula is not universally valid
+
+<details>
+<summary>Graphviz code</summary>
+
+<!-- :Tangle(dot) counter-model.dot -->
+```dot
+digraph g {
+rankdir=LR
+1 -> 2
+1 -> 3
+3 [xlabel="p"]
+}
+```
+
+</details>
+
+## Formula for a statement
+"Has no blind successor": ¬ ◇ □ ⊥, □ ◇ T ("wherever I go, I can do a step"), □ ¬ □ ⊥
+
+"Has at least one non blind successor": ◇ ◇ T
diff --git a/templates/index.html b/templates/index.html
@@ -23,4 +23,6 @@
{% block content %}
{{ section.content | safe }}
+
+<!-- Q29uZ3JhdHMsIHlvdSBmb3VuZCBzb21ldGhpbmcgZXh0cmEuCgpIZXJlIGFyZSBhIGZldyAnbGlmZWhhY2tzJyBmcm9tIG15IDMgeWVhcnMgYXQgdGhlIFZVOgotIEdldCB0aGUgU1BBUiBhcHA6CiAgICAtIHRoZXkgaGF2ZSByZWFsbHkgZ29vZCBkaXNjb3VudHMgZHVyaW5nIHRoZSBkYXkKICAgIC0gWW91IGdldCBhIGZyZWUgY29mZmVlIGV2ZXJ5IHNvIG9mdGVuLgogICAgLSBZb3UgY2FuIGJ1eSAnemVybyB3YXN0ZSBiYWdzJywgd2hpY2ggY29zdCAzIGV1ciBhbmQgY29udGFpbiBzdHVmZiB0aGF0IHdvdWxkIGV4cGlyZSBzb29uLiBJZiB5b3UgcHV0IGl0IGluIHRoZSBmcmlkZ2UsIGl0IGNhbiBsYXN0IHR3byBkYXlzLiBBbmQgdXN1YWxseSB0aGUgc3R1ZmYgaW4gdGhlIGJhZ3Mgd291bGQgY29zdCB5b3UgMTAtMTUgZXVyLgotIERvIHdlbGwgaW4geW91ciBjbGFzc2VzIGR1cmluZyB0aGUgeWVhciwgYW5kIHRoZW4gYmVjb21lIGEgVEEuCiAgICAtIFlvdXIgd29ya2luZyBob3VycyBhcmUgdGhlIHNhbWUgc2Nob29sIGhvdXJzLCBhbmQgYXQgdGhlIHNhbWUgbG9jYXRpb24gKHRoaXMgc291bmRzIG9idmlvdXMgYnV0IGlzIHN1Y2ggYSBodWdlIGFkdmFudGFnZSkKICAgIC0gVGhlIHBheSBpcyBxdWl0ZSBnb29kIGZvciBhIHNpZGUgam9iCiAgICAtIFlvdSBnZXQgYW4gZW1wbG95ZWUgY2FyZCwgd2hpY2ggZ2l2ZXMgeW91OgogICAgICAgIC0gZnJlZSBjb2ZmZWUvdGVlL2hvdCBjaG9jb2xhdGUKICAgICAgICAtIGZyZWUgcHJpbnRpbmcgKGdvb2QgZm9yIHNjaG9vbCBzdHVmZiwgb3IgcG9zdGVycykKICAgICAgICAtIGFjY2VzcyB0aHJvdWdoIF9hbnlfIG9mIHRoZSBXJk4gZW50cmFuY2VzLCBpbmNsdWRpbmcgdGhlIG9uZXMgbmV4dCB0byB0aGUgU1BBUiAobWlnaHQgdmFyeSBkZXBlbmRpbmcgb24gdGhlIGZhY3VsdHkgeW91IHdvcmsgZm9yKQogICAgLSBUcnkgdG8gZ2V0IDU2IHdvcmtpbmcgaG91cnMgcGVyIG1vbnRoLiBUaGlzIGlzIDE0IGhvdXJzIHBlciB3ZWVrICh+MyBwZXIgZGF5KSwgd2hpY2ggaXMgdmVyeSBkb2FibGUgbmV4dCB0byBzY2hvb2wgd29yay4gV2h5PyBZb3UgZ2V0IGZyZWUgdHJhbnNwb3J0IGR1cmluZyB0aGUgd2VlayBvciB3ZWVrZW5kLCBhbmQgdGhhdCBpbmNsdWRlcyB0cmFpbnMuIFNvIGlmIHlvdSBoYXZlIGEgZGF5IG9mZiwgeW91IGNhbiB1c2UgdGhhdCB0byB0cmF2ZWwuCi0gVGhlcmUncyBhIHZlcnkgbmljZSBzdHVkeSByb29tIG9uIHRoZSB0aGlyZCBmbG9vciwgcm9vbSBudW1iZXIgX18uIEl0IGhhcyB3aW5kb3dzIHRoYXQgeW91IGNhbiBvcGVuLCBwbGVudHkgb2YgZWxlY3RyaWNpdHkgb3V0bGV0cywgYW5kIG5vdCBtYW55IHBlb3BsZSBrbm93IGFib3V0IGl0LiBJZiB5b3UncmUgcmVhZGluZyB0aGlzLCBwbGVhc2Uga2VlcCBpdCBhIHNlY3JldC4K -->
{% endblock content %}
