commit ece195497fd28d59ef96658a3e0aee8f280640a0
parent 0a008b59bc549406fc89acbf8afad725cd52758a
Author: Alex Balgavy <alex@balgavy.eu>
Date: Tue, 1 Mar 2022 17:21:17 +0100
Advanced logic lecture 7
Diffstat:
4 files changed, 54 insertions(+), 0 deletions(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md
@@ -10,6 +10,7 @@ title = 'Advanced Logic'
6. [Lecture 5](lecture-5/)
7. [Lecture 6](lecture-6/)
8. [Exercise 3](exercise-3/)
+9. [Lecture 7](lecture-7/)
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-7/index.md b/content/advanced-logic-notes/lecture-7/index.md
@@ -0,0 +1,53 @@
++++
+title = 'Lecture 7'
++++
+# Lecture 7
+## Standard translation
+Aim to map formulas of basic modal logic to first-order predicate logic such that:
+- φ in BML is *valid* iff its translation in first-order predicate logic is *valid*
+- φ in BML is *satisfiable* iff its translation in first-order predicate logic is *satisfiable*
+
+Translation:
+- translate "p is true in world x" as "predicate P holds for x"
+- translate "accessibility relation R" as "binary predicate R"
+- translation is relative to some state
+- notation: Px instead of P(x), Rxy instead of R(x,y)
+
+Rules for standard translation:
+
+
+
+Examples of translation:
+
+
+
+first-order predicate logic is decidable _if it uses at most 2 variables_.
+therefore, adapt standard translation to only use 2 variables.
+
+In a formula, check the situation with bound variables, and rename where possible.
+When you are in state _a_ and start a quantification, use the variable _b_, and vice versa.
+
+## Finite model property
+If φ is satisfiable, then φ is satisfiable on a finite model.
+
+Effective finite model property: if φ is satisfiable, then φ is satisfiable in a model of size ≤ f(φ)
+
+Via selection:
+- suppose there is a model that makes φ true
+- unravel the model at x to a tree model
+- φ has finite modal depth n, so restrict tree model to height n
+- rewrite φ to a conjunction of first-order propositional logic formulas and diamonds
+- take for every diamond formula a successor
+
+Via filtration:
+- suppose there is a model that makes φ true
+- consider set S of all subformulas of φ
+- define equivalence relation on S: u ~ v iff u and v are modally equivalent
+ - i.e., if they agree on letters/formulas
+- define W' to consist of equivalence classes [u] of states from W
+- define V' using u ∈ V(p) iff [u] ∈ V'(p) for every p in S
+- define a R' using R'[u][v] if Ruv, and requiring:
+ - if R'[u][v] and ◇ ψ ∈ S and [v] ⊨ ψ, then [u] ⊨ ◇ φ
+ - then (W', R'), V' is finite and (W', R'), V', [x] ⊨ φ
+
+
diff --git a/content/advanced-logic-notes/lecture-7/standard-translation-examples.png b/content/advanced-logic-notes/lecture-7/standard-translation-examples.png
Binary files differ.
diff --git a/content/advanced-logic-notes/lecture-7/standard-translation-rules.png b/content/advanced-logic-notes/lecture-7/standard-translation-rules.png
Binary files differ.
