commit 7842b4c4c006088f2f73196b308104f4e9c2c007
parent 02fa111555aa61d9781330ad100046114aa634b3
Author: Alex Balgavy <alex@balgavy.eu>
Date: Tue, 15 Feb 2022 18:11:08 +0100
Advanced logic lecture 3
Diffstat:
2 files changed, 50 insertions(+), 0 deletions(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md
@@ -5,6 +5,7 @@ title = 'Advanced Logic'
1. [Lecture 1](lecture-1)
2. [Lecture 2](lecture-2)
3. [Exercise 1](exercise-1)
+4. [Lecture 3](lecture-3)
I drew the graphs on these pages with [Graphviz](https://graphviz.org/).
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-3.md b/content/advanced-logic-notes/lecture-3.md
@@ -0,0 +1,49 @@
++++
+title = 'Lecture 3'
+template = 'page-math.html'
++++
+# Lecture 3
+## Preservation of truth and validity
+### Substitution
+Substitution for propositional variables
+- σ : Var → Form
+- T and ⊥ not substituted
+
+If (W,R), V ⊨ φ then not necessarily $(W,R) V \models \phi^{\sigma}$
+
+But validity in a frame is preserved under substitution: if F ⊨ φ, then $F \models \phi^{\sigma}$ for any substitution σ.
+
+Validity is closed under substitution: if F ⊨ φ, then $F \models \phi^{\sigma}$ for any substitution σ.
+
+### Alternative semantics
+The interpretation $[\![ \phi ]\!] _{M}$ of a formula φ in model M = (W,R,V) is set of worlds in which φ is true.
+
+M, w ⊨ φ iff $w \in [\![\phi]\!]_{M}$
+
+M ⊨ φ iff $[\![\phi]\!]_{M} = W$
+
+### Preservation of truth and validity
+Local truth preserved by modus ponens: if M, w ⊨ φ → ψ and M, w ⊨ φ then M, w ⊨ ψ
+
+Global truth preserved by modus ponens and necessitation: if M ⊨ φ then M ⊨ □ φ
+
+Frame validity preserved by modus ponens, necessitation, and substitution: if F ⊨ φ then $F \models \phi^{\sigma}$.
+
+## Modal tautologies
+⊨ □ (p → q) → □ p → □ q
+
+If ⊨ φ → ψ and ⊨ φ then ⊨ ψ
+
+If ⊨ φ then ⊨ □ φ
+
+If ⊨ φ then $\models \phi^{\sigma}$
+
+## Characterizations of frame properties
+If F reflexive then F ⊨ □ p → p.
+This holds in the opposite.
+So the formula □ p → p characterizes the frame property 'reflexivity'.
+
+In general, formula φ characterizes the frame property P means: F has property P iff F ⊨ φ.
+
+## Modal equivalence
+Two states M, w and M', w' are modally equivalent if they satisfy the same formulas.