commit 64f1d6e8b559cc9961cfa05b27d9b08d9271e559 parent ec95456119d26bdc0240bfd25d2b0d0032950c79 Author: Alex Balgavy <alex@balgavy.eu> Date: Thu, 24 Mar 2022 13:14:31 +0100 Reorganise advanced logic notes by topic Diffstat:
64 files changed, 1161 insertions(+), 1149 deletions(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md @@ -2,24 +2,27 @@ title = 'Advanced Logic' +++ # Advanced Logic -1. [Lecture 1](lecture-1/) -2. [Lecture 2](lecture-2/) -3. [Exercise 1](exercise-1/) -4. [Lecture 3](lecture-3/) -5. [Lecture 4](lecture-4/) -6. [Lecture 5](lecture-5/) -7. [Lecture 6](lecture-6/) -8. [Exercise 3](exercise-3/) -9. [Lecture 7](lecture-7/) -10. [Homework 1](homework-1/) -11. [Lecture 8](lecture-8/) -12. [Lecture 9](lecture-9/) -13. [Lecture 10](lecture-10/) -14. [Exercise 4](exercise-4/) -15. [Some midterm solutions](some-midterm-solutions/) -16. [Lecture 11](lecture-11/) -17. [Lecture 12](lecture-12/) -18. [Exercise 5](exercise-5/) +- [Intro to Modal Logic (operators, frames, models, tautologies)](intro-to-modal-logic-operators-frames-models-tautologies/) +- [Semantics: truth and validity, game semantics for formula validity](semantics-truth-and-validity-game-semantics-for-formula-validity/) +- [Bisimulations](bisimulations/) +- [Model transformations (tree unravelling, bisimulation contraction)](model-transformations-tree-unravelling-bisimulation-contraction/) +- [Formula validity using sequents and tableaux](formula-validity-using-sequents-and-tableaux/) +- [Standard translation: mapping basic modal logic to first-order predicate logic](standard-translation-mapping-basic-modal-logic-to-first-order-predicate-logic/) +- [Proof systems and derivation](proof-systems-and-derivation/) +- [Temporal logic](temporal-logic/) +- [Multi-modal logic](multi-modal-logic/) +- [Program correctness](program-correctness/) +- [Propositional dynamic logic (PDL)](propositional-dynamic-logic-pdl/) +- [Epistemic logic](epistemic-logic/) + +Worked exercises: + +- [Exercise 1](exercise-1/) +- [Exercise 3](exercise-3/) +- [Exercise 4](exercise-4/) +- [Exercise 5](exercise-5/) +- [Homework 1](homework-1/) +- [Some midterm solutions](some-midterm-solutions/) 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-4/bisimulation-example.png b/content/advanced-logic-notes/bisimulations/bisimulation-example.png Binary files differ. diff --git a/content/advanced-logic-notes/bisimulations/index.md b/content/advanced-logic-notes/bisimulations/index.md @@ -0,0 +1,179 @@ ++++ +title = 'Bisimulations' +template = 'page-math.html' ++++ + +# Lecture 4 +## Bisimulations +A non-empty relation Z ⊆ W × W' is bisimulation ($Z : M \underline{\leftrightarrow} M'$) if for all pairs (w, w') ∈ Z we have: +- w ∈ V(p) iff w' ∈ V'(p) +- if Rwv then for some v' ∈ W' we have R'w'v' and vZv' +- if R'w'v' then for some v ∈ W we have Rwv and vZv' + +Two models are bisimilar ($M \underline{\leftrightarrow} M'$) if there exists a bisimulation Z ∈ W × W'. + +Basically, models are bisimilar if they are, in essence, the same (there may be extra states or relations in one of the models but those states/relations do not add any new information compared to the other model). A bisimulation then is the set of states that are bisimilar between two models. + +Two pointed models are bisimilar if there exists a bisimulation such that (w,w') ∈ Z + +Two states are modally equivalent if they satisfy exactly the same formulas. +So if M,w and M',w' are bisimilar, then they are modally equivalent. + +If two states are modally equivalent, then they are bisimilar. + +### Example +It's a bit hard to describe this in words, but intuitive if you see it. +Here's an example: + + + +You see that from the top state, you can get to a terminal state in one or two steps, in both models. +Therefore, the top states of both models are _bisimilar_. +Since all of the states in the models are bisimilar, _the two models are bisimilar_. +The dotted lines connect the pairs that make up the _bisimulation_. + +### Example: finding bisimulations + +Take two example models: + +<table> +<thead> +<th>A</th> <th>B</th> +</thead> + +<tbody> +<tr> + +<td> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) model-a.dot --> +```dot +digraph g { +1 -> 2 +2 -> 3 +3 -> 4 +3 -> 5 +1 [xlabel="p"] +2 [xlabel="q"] +3 [xlabel="q"] +4 [xlabel="q"] +5 [xlabel="q"] +} +``` + +</details> +</td> + +<td> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) model-b.dot --> +```dot +digraph g { +a -> b +a -> c +c -> d +b -> d +d -> e +a [xlabel="p"] +b [xlabel="q"] +c [xlabel="q"] +d [xlabel="q"] +e [xlabel="q"] +} +``` + +</details> +</td> + +</tr> +</table> + +The claim is that states (A,1) and (B,a) are bisimilar. +How do you prove or refute the claim? + +Well, we need to find a bisimulation with the pair (1, a). +1. Start with pair (1, a) +2. In A, move from 1 to 2. Have to mimic the move in B, can do so by moving from a to b or from a to c. + Yields the pairs (2, b) and (2, c). +3. In A, move from 2 to 3. Have to mimic the move in B, can move from both b and c to d. + Yields the pair (3, d). +4. In A, two options: + - move from 3 to 4. Have to mimic the move in B, can move from d to e. + Yields the pair (4, e). + - move from 3 to 5. Have to mimic the move in B, can move from d to e. + Yields the pair (5, e). + +Since for any move in the first model, we can mimic it in the second model, we have a bisimulation. +The bisimulation contains exactly the pairs we just listed. +So there is a bisimulation Z = {(1, a), (2, b), (2, c), (3, d), (4, e), (5, e)}. +Since (1, a) ∈ Z, we can say that states (A, 1) and (B, a) are bisimilar. + +If two states are bisimilar, then they are modally equivalent. +Prove by induction on definition of formulas. + +For finitely branching models, if two states modally equivalent, then they are bisimilar. +Prove by taking modal equivalence as bisimulation. + +Let Z := {(x, x') | for all φ: x ⊨ φ iff x' ⊨ φ}. +Z is a bisimulation. +- Local harmony is satisfied. +- zig: suppose (x, x') ∈ Z and x → y. + Because x ⊨ ◇ T also x' ⊨ ◇ T. + So x' has finitely many successors y'₁...y'n with n ≥ 1. + Suppose for all i: y is not modally equivalent to y'ᵢ. + There are φ₁...φn such that y ⊨ φᵢ and y'ᵢ ⊭ φᵢ. + x ⊨ ◇(φ₁ ∧ ... ∧ φn) so also x' ⊨ ◇ (φ₁ ∧ ... ∧ φn). + Contradiction. + + +Asymmetry is not modally definable. +To deal with only frames, we can use surjective bounded morphisms. + +Function f : W → W' is bounded morphism from (W,R) to (W',R') if: +- for all w,v ∈ W: if Rwv then Rf(w)f(v) +- for all w ∈ W and for all v' ∈ W': if R'f(w)v' then there exists v ∈ W such that f(v) = v' and Rwv + +A bounded morphism f is surjective if for every w' ∈ W' there exists w ∈ W such that f(w) = w' + +If f: W → W' is surjective bounded morphism from (W,R) to (W',R'), then if (W,R) ⊨ φ then (W', R') ⊨ φ + +### Bisimulation games for two players +Spoiler S claims M,s an N,t to be different. +Duplicator D claims they are similar. + +Play consists of sequence of links, starting with link s ~ t. + +At current link m ~ n (with m in M and n in N): +- if m an n different in their atoms, then S wins +- if not, then S picks a successor x either of m or of n +- then D has to find a matching transition to y in the other model +- play continues with next link x ~ y (or y ~ x) + +If player cannot make a move, he loses. +D wins infinite games. + +Modal depth of formulas. +Modal formulas are 'nearsighted': +- md(p) = md(⊥) = md(T) = 0 +- md(¬φ) = md(φ) +- md(φ ∨ ψ) = md(φ ∧ ψ) = max{md(φ), md(ψ)} +- md(□ φ) = md(◇ φ) = md(φ) + 1 + +We need a formula of model depth k to distinguish states x and y. +Spoiler can win bisimulation game in k rounds. +Every winning strategy for Spoiler corresponds to a distinguishing formula. +Games of less than k rounds can be won by Duplicator. +Formulas of modal depth less than k cannot distinguish between x and y. + +M,s and N,t satisfy the same formulas up to modal depth k iff duplicator has winning strategy in the k-round game starting in s ~ t. +If Spoiler can win in k rounds, then there is a distinguishing formula of modal depth k. diff --git a/content/advanced-logic-notes/lecture-4/model-a.dot b/content/advanced-logic-notes/bisimulations/model-a.dot diff --git a/content/advanced-logic-notes/lecture-4/model-a.dot.svg b/content/advanced-logic-notes/bisimulations/model-a.dot.svg diff --git a/content/advanced-logic-notes/lecture-4/model-b.dot b/content/advanced-logic-notes/bisimulations/model-b.dot diff --git a/content/advanced-logic-notes/lecture-4/model-b.dot.svg b/content/advanced-logic-notes/bisimulations/model-b.dot.svg diff --git a/content/advanced-logic-notes/epistemic-logic.md b/content/advanced-logic-notes/epistemic-logic.md @@ -0,0 +1,13 @@ ++++ +title = 'Epistemic logic' ++++ +# Lecture 13 +Epistemic logic: +- □ φ: 'we know that φ is true' (also written Kφ) +- ◇ φ: 'we consider φ possible' +- [i] φ: 'agent i knows that φ is true' (also written Kᵢφ) +- 〈i〉φ: 'agent i considers φ possible' + +In an epistemic frame, the relation statemtn sRᵢt means: given his information in situation s, agent i considers t possible + + diff --git a/content/advanced-logic-notes/lecture-6/example-tableau.png b/content/advanced-logic-notes/formula-validity-using-sequents-and-tableaux/example-tableau.png Binary files differ. diff --git a/content/advanced-logic-notes/formula-validity-using-sequents-and-tableaux/index.md b/content/advanced-logic-notes/formula-validity-using-sequents-and-tableaux/index.md @@ -0,0 +1,52 @@ ++++ +title = 'Formula validity using sequents and tableaux' ++++ +# Lecture 6 +## Sequents +φ₁...φn ⇒ ψ₁...ψm valid if in every model, in every world in that model, the conjunction of the φᵢ implies the disjunction of the ψᵢ. + +Empty conjunction is true, empty disjunction is false. + +Reducing modal sequents: + + + +φ valid iff the sequent (⇒ φ) valid. + +For modal logic: +- If we get a sequent of the form p₁...n, ◇φ₁..◇φm ⇒ q₁..qk, ◇ψ₁...◇ψl +- Such a sequent only valid iff either pᵢ = qj for some i and j, or φᵢ ⇒ ψ₁...ψl is valid for some i ∈ {1...m} + +Start with intended conclusion, try to build a proof while moving upwards. +Formula is valid iff it is derivable in sequent calculus. +Validity using sequents: +1. Rewrite formula + - (a → b) to (¬ a ∨ b) + - (¬ □ a) to (◇ ¬ a) + - (□ a) to (¬ ◇ ¬ a) + +2. Rewrite sequent, based on rules above +3. Maybe rewrite formula again +4. Decide on validity of sequent +5. Conclude on validity of formula + +## Tableaux +Tableau is finite tree of sequents. +If all solid branches close, yields validity of initial sequent. +If at least one branch does not close, yields a counterexample. + +The dot separates assumptions on the left from what's true on the right. +A branch closes if what's assumed also holds in the state. + + + +In modal logic: + + + +Example: + + + +It's not valid because in the two red states, the letters on the left of the dot are not on the right. +The countermodel comes from taking the numbers next to each step (the numbers are states), connecting them, and creating a valuation where the letters on the left side of the dot (the assumptions) are true. diff --git a/content/advanced-logic-notes/lecture-6/reducing-modal-sequents.png b/content/advanced-logic-notes/formula-validity-using-sequents-and-tableaux/reducing-modal-sequents.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-6/tableau-modal-logic.png b/content/advanced-logic-notes/formula-validity-using-sequents-and-tableaux/tableau-modal-logic.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-6/tableau-rules.png b/content/advanced-logic-notes/formula-validity-using-sequents-and-tableaux/tableau-rules.png Binary files differ. diff --git a/content/advanced-logic-notes/intro-to-modal-logic-operators-frames-models-tautologies/index.md b/content/advanced-logic-notes/intro-to-modal-logic-operators-frames-models-tautologies/index.md @@ -0,0 +1,76 @@ ++++ +title = 'Intro to Modal Logic (operators, frames, models, tautologies)' ++++ + +# Intro + +Basic model logic operators: +- □: necessary, known, provable +- ◇: possible, considered possible + +In a diagram, one of these symbols is exactly one transition step (use multiple for multiple steps). + +- ◇ φ ⇔ ¬□ ¬φ +- □ φ ⇔ ¬◇ ¬φ + +# First-order propositional logic +Includes variables, T, ⊥, not, and, or, implication. +Proofs are given by structural induction. +Precedence is ¬, then ∧∨, then →. + +a valuation v : Var → {0,1} maps propositional variables to truth values. + +the semantics of a formula under a valuation is defined with ⟦p⟧ᵥ = v(p), with p ∈ Var + +if ⟦φ⟧ᵥ = 1, we write v ⊨ φ (read "v models φ") +- that is, if φ is true in the model v +- then, φ has a model, so φ is satisfiable + +If every model of all φᵢ is a model of ψ, we write φ₁,...,φn ⊨ ψ +- then ψ is a semantic consequence of φ₁,...,φn + +If v ⊨ φ for all valuations of v, then ⊨ φ (φ is a tautology) + +Soundness: ⊢ implies ⊨ -- what we can derive is true. proved by induction on length of proof + +Completeness: ⊨ implies ⊢ -- we can derive what is true. can be proven using consistency + +# Basic modal logic +E.g. "whatever is necessary is possible" == □φ → ◇φ + +□ can also mean "I know", e.g. "I know that someone appreciates me" == ∃x.□A(x, M) + +Loeb's formula: □ (□ p → p) → □ p + +Veridicality: □ φ → φ + +Truth s relative to current situation/world/environment: +- formulas evaluated in given structure +- necessity (□): truth in all accessible worlds. if there are no accessible worlds, it's true. +- possibility (◇): truth in some accessible world (at least one). if there are no accessible worlds, it's false. + +## Frames +A situation is set by a frame F = (W,R) +- W ≠ ∅ set of possible worlds/states +- R ⊆ W × W an accessibility/transition relation + +A frame is just the states and transitions between them, without a valuation (i.e. without saying what's true in each state). + +A frame could be (ℕ, <), or ({1,2,3,4}, {(1,2), (2,4), (1,3), (3,4), (2,2)}) + +## Models +model: pair M = (F, V) +- a frame F = (W,R) +- a valuation V : Var → W → {0,1}, or V : Var → P(W) + - the valuation says which letters/formulas are true in which states + +pointed model: pair (M,w) of model M and w a world in M + + + +◇T holds if at least one successor. +□⊥ holds if there is no successor. + +Dualities: +- ◇ φ := ¬ □ ¬ φ +- □ φ := ¬ ◇ ¬ φ diff --git a/content/advanced-logic-notes/lecture-1/local-truth-definitions.png b/content/advanced-logic-notes/intro-to-modal-logic-operators-frames-models-tautologies/local-truth-definitions.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-1/index.md b/content/advanced-logic-notes/lecture-1/index.md @@ -1,76 +0,0 @@ -+++ -title = 'Lecture 1' -+++ - -# Intro - -Basic model logic operators: -- □: necessary, known, provable -- ◇: possible, considered possible - -In a diagram, one of these symbols is exactly one transition step (use multiple for multiple steps). - -- ◇ φ ⇔ ¬□ ¬φ -- □ φ ⇔ ¬◇ ¬φ - -# First-order propositional logic -Includes variables, T, ⊥, not, and, or, implication. -Proofs are given by structural induction. -Precedence is ¬, then ∧∨, then →. - -a valuation v : Var → {0,1} maps propositional variables to truth values. - -the semantics of a formula under a valuation is defined with ⟦p⟧ᵥ = v(p), with p ∈ Var - -if ⟦φ⟧ᵥ = 1, we write v ⊨ φ (read "v models φ") -- that is, if φ is true in the model v -- then, φ has a model, so φ is satisfiable - -If every model of all φᵢ is a model of ψ, we write φ₁,...,φn ⊨ ψ -- then ψ is a semantic consequence of φ₁,...,φn - -If v ⊨ φ for all valuations of v, then ⊨ φ (φ is a tautology) - -Soundness: ⊢ implies ⊨ -- what we can derive is true. proved by induction on length of proof - -Completeness: ⊨ implies ⊢ -- we can derive what is true. can be proven using consistency - -# Basic modal logic -E.g. "whatever is necessary is possible" == □φ → ◇φ - -□ can also mean "I know", e.g. "I know that someone appreciates me" == ∃x.□A(x, M) - -Loeb's formula: □ (□ p → p) → □ p - -Veridicality: □ φ → φ - -Truth s relative to current situation/world/environment: -- formulas evaluated in given structure -- necessity (□): truth in all accessible worlds. if there are no accessible worlds, it's true. -- possibility (◇): truth in some accessible world (at least one). if there are no accessible worlds, it's false. - -## Frames -A situation is set by a frame F = (W,R) -- W ≠ ∅ set of possible worlds/states -- R ⊆ W × W an accessibility/transition relation - -A frame is just the states and transitions between them, without a valuation (i.e. without saying what's true in each state). - -A frame could be (ℕ, <), or ({1,2,3,4}, {(1,2), (2,4), (1,3), (3,4), (2,2)}) - -## Models -model: pair M = (F, V) -- a frame F = (W,R) -- a valuation V : Var → W → {0,1}, or V : Var → P(W) - - the valuation says which letters/formulas are true in which states - -pointed model: pair (M,w) of model M and w a world in M - - - -◇T holds if at least one successor. -□⊥ holds if there is no successor. - -Dualities: -- ◇ φ := ¬ □ ¬ φ -- □ φ := ¬ ◇ ¬ φ diff --git a/content/advanced-logic-notes/lecture-10/index.md b/content/advanced-logic-notes/lecture-10/index.md @@ -1,64 +0,0 @@ -+++ -title = 'Lecture 10' -+++ -# Lecture 10 -## Multi-modal logic -Assume set of labels I (which in a diagram are on the arrows). -For every label i there is modality 〈i〉 so the formulas of multi-modal logic are, given I, defined for i in ∈ I. - -I-frame is pair (W, {Rᵢ | i ∈ I}). -Rᵢ ⊆ W × W for every i ⊆ I. - -I-model is triple (W, {Rᵢ | i ⊆ I}, V). - -### Truth and validity -For M an I-model, M,w ⊨ φ is defined by induction on the definition of formulas. - -Clauses: -- M,w ⊨ 〈a〉φ iff M,v ⊨ φ for some v with Rₐwv -- M,w ⊨ [a]φ iff M,v ⊨ φ for all v with Rₐwv - -### Example -Use index set I = {a, b, c}. -Give model with a world where the formula 〈a〉(〈b〉[a] p ∧ [c] ¬ 〈a〉p) is true. - - - -<details> -<summary>Graphviz code</summary> - -<!-- :Tangle(dot) example-multimodal-logic-formula.dot --> -```dot -digraph g { -rankdir=LR -1 -> 2 [label="a"] -2 -> 3 [label="b"] -} -``` - -</details> - - -For a bisimulation, when you do a step between states, they have to be with the same label (so the mimic step must have the same label). - -### Geach axiom -◇ □ p → □ ◇ p. - -Valid in frame iff for every r ← s → u there is r → v ← u. - -## Program correctness -Prove that a program meets its specification. - -Correctness specification: formal description of how program is supposed to behave - -Program is correct: its executions satisfy the specification - -### Verification - Hoare approach -Prove statements of form `{precondition} program {postcondition}` -- pre/postcondition are formulas -- program is a while-program -- we have proof rules for showing {φ} α {ψ} - -Partial correctness: if program starts satisfying φ, and if it halts, then when it halts ψ is satisfied - -Total correctness: partially correct, and terminates whenever started while satisfying φ diff --git a/content/advanced-logic-notes/lecture-11/index.md b/content/advanced-logic-notes/lecture-11/index.md @@ -1,29 +0,0 @@ -+++ -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-12/index.md b/content/advanced-logic-notes/lecture-12/index.md @@ -1,93 +0,0 @@ -+++ -title = 'Lecture 12' -template = 'page-math.html' -+++ -# Lecture 12 -- composition "R;S" = {(x, z) | ∃ y : Rxy ∧ Syz} -- union "R ∪ S" = {(x, y) | Rxy ∨ Sxy} -- R\*: repeat R one or more times - -A model M is a PDL-model if the frame is a PDL-frame and $R_{\phi ?} = \\{ (w,w) \\;|\\; M, w \models \phi\\}$ - -The R of the frame is all sets of Rₐ where _a_ is a program (i.e. a label on an arrow). - -<details> -<summary>Proof example of 〈α, β〉 p → 〈α〉〈β〉p</summary> - -- Take a PDL model and a state x. -- Assume x ⊨ 〈α, β〉 p -- That is, there is a state y such that $(x, y) \in R_{\alpha;\beta}$ and y ⊨ p. -- $R_{\alpha;\beta} = R_{\alpha}; R_{\beta}$ -- That is, there is a state u such that $(x, u) \in R_{\alpha}$ and $(u,y) \in R_{\beta}$. -- Because $(u,y) ∈ R_{\beta}$ and y ⊨ p, we have u ⊨ 〈β〉 p -- Because $(x,u) ∈ R_{\alpha}$, we have and u ⊨ 〈β〉p we have x ⊨ 〈α〉〈β〉p. -</details> - -If then else: -- program: `if p then a else b` -- encoding: (p?; a) ∪ (¬ p? ; b) - -<details> -<summary>Example</summary> - - - -<details> -<summary>Graphviz code</summary> - -<!-- :Tangle(dot) model-if-then-else.dot --> -```dot -digraph g { -rankdir=LR -1 [xlabel="[p]"] -1 -> 2 [label="a"] -4 -> 2 [label="b"] -1 -> 3 [label="b"] -4 -> 3 [label="a"] -} - -``` - -</details> - -Calculate the relation for `if p then a else b`, which is encoded as `(p?; a) ∪ (¬ p?; b)`: - - -</details> - -While: -- program: `while p do a` -- encoding: (P?; a)\*; ¬ p? - -<details> -<summary>Example</summary> - - - -<details> -<summary>Graphviz code</summary> - -<!-- :Tangle(dot) model-while.dot --> -```dot -digraph g { -rankdir=LR -1 -> 2 [label="a"] -2 -> 3 [label="a"] -3 -> 4 [label="a"] -4 -> 5 [label="a"] -5 -> 6 [label="a"] -1 [xlabel="[p]"] -2 [xlabel="[p]"] -3 [xlabel="[p]"] -4 [xlabel="[p]"] -} -``` - -</details> - -Calculating the relation `while p do a`, encoded as `(p?; a)*; ¬ p?`: - - -</details> - -If E is a bisimulation between two A-models, then it is a bisimulation for the models' PDL-extensions. diff --git a/content/advanced-logic-notes/lecture-2/index.md b/content/advanced-logic-notes/lecture-2/index.md @@ -1,132 +0,0 @@ -+++ -title = 'Lecture 2' -+++ -# Lecture 2 -## Semantics: local truth -Valuation notation: -- V : Var → P(W) means Var → W → {0,1} -- V(p,w) = 1 is the same as w ∈ V(p) - -A formula φ _characterizes_ a state x in model M if φ is true in x but not in other states of M. - -A formula φ _distinguishes_ state x from state y in a model M if φ is true in x but not in y. - - - -Above: -- the formula 3 ⊨ □ ⊥ characterizes state 3 -- the formula 2 ⊨ ◇ □ ⊥ characterizes state 2 - -## Game semantics -This is an approach to determine if a formula φ holds in a pointed model M, w. - -We have: -- model M = ((W,R), V), world w ∈ W, formula φ -- two players: - - Verifier V claims that φ is true in w (sort of like ∀) - - Falsifier F claims that φ is false in w (sort of like ∃, try to find a _witness_) -- position: pair (w, φ) with w ∈ W a world and φ a formula -- move: from position (w, φ), determined by main operator of φ - -Assume that negation only applied to prop. variables. -Transform formulas from ¬ □ p to ◇ ¬ p, ¬(p ∧ q) to ¬p ∨ ¬q. - -The position determines the move, e.g. in a position (t, ◇ φ), V chooses a successor _u_ of _t_, and play continues with (u, φ). -For (t,p), if p is true in t then V wins, otherwise F wins. -For (t, ¬p), if p is false in t then V wins, otherwise F wins. -If a player should but cannot choose a successor, they lose. - -Who starts: -- V: ∨, ◇ -- F: ∧, □ - -A complete game tree for φ and (M,w) starts with (w,φ) and contains all possible moves. -A strategy for player P is subset of steps for P, and it's a winning strategy if it ensures that P wins the game. -φ is true in M in s ⇔ V has a winning strategy for M,s,φ. - -### Example -Diagram: - - - -<details> -<summary>Graphviz code</summary> - -<!-- :Tangle(dot) states.dot --> -```dot -digraph states { -1 -> 2 -1 -> 3 -2 -> 3 -3 -> 2 -3 -> 4 -4 -> 2 -4 -> 3 -} -``` - -</details> - -Given: -- formula ◇ p ∨ □ ◇ p, in state 2. -- p is true in state 3. - -Complete game tree: - - - -<details> -<summary>Graphviz code</summary> - -<!-- :Tangle(dot) tree.dot --> -```dot -digraph gametree { - top [label="[V] ◇ p ∨ □ ◇ p, 2"] - l11 [label="[V] ◇ p, 2"] - l12 [label="[F] □ ◇ p, 2"] - top -> l11 - top -> l12 - l21 [label="p 3"] - l22 [label="[V] ◇ p, 3"] - l11 -> l21 - l12 -> l22 - l31 [label="Verifier wins"] - l32 [label="p, 2"] - l33 [label="p, 4"] - l21 -> l31 - l22 -> l32 - l22 -> l33 - l41 [label="Falsifier wins."] - l42 [label="Falsifier wins."] - l32 -> l41 - l33 -> l42 -} -``` - -</details> - -## Truth and validity -(((W,R),V),w) ⊨ φ means φ is valid in a point w. -(W,R) ⊨ φ means φ is valid in a frame (W,R). -⊨ φ means φ is valid/tautology. -If a part is omitted, it's implicitly universally quantified. - -Satisfiability: -- φ _satisfiable in model M_ if there's a world w ∈ M such that M,w ⊨ φ -- φ _satisfiable_ if there's a model M and a world w ∈ M such that M,w ⊨ φ -- φ and ψ _semantically equivalent_ if ∀ M,w: M,w ⊨ φ ⇔ M,w ⊨ ψ -- φ valid iff ¬ φ not satisfiable - -### Example -Show universal validity of □ (φ → ψ) → (□ φ → □ ψ) - -1. let F = (W,R) be frame, V valuation on F, let x ∈ W. -2. Assume a1: F,V,x ⊨ □ (φ → ψ) -3. Assume a2: F,V,x ⊨ □ φ -4. Aim to show F,V,x ⊨ □ ψ. -5. □ is universal quantification, so take an arbitrary successor y ∈ W. -6. If Rxy, aim to show y ⊨ ψ. If not, □ ψ holds. -7. Have y ⊨ φ → ψ and y ⊨ φ. -8. From a2, have y ⊨ φ. -9. From a1, have have y ⊨ ψ. -10. Hence x ⊨ □ ψ, hence x ⊨ □ φ → □ ψ. Hence formula is valid. diff --git a/content/advanced-logic-notes/lecture-3.md b/content/advanced-logic-notes/lecture-3.md @@ -1,50 +0,0 @@ -+++ -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 ⊨ φ. -If you need to prove that a formula characterizes a property, you need to prove this bi-implication in _both_ directions. - -## Modal equivalence -Two states M, w and M', w' are modally equivalent if they satisfy the same formulas. diff --git a/content/advanced-logic-notes/lecture-4/index.md b/content/advanced-logic-notes/lecture-4/index.md @@ -1,139 +0,0 @@ -+++ -title = 'Lecture 4' -template = 'page-math.html' -+++ - -# Lecture 4 -## Bisimulations -A non-empty relation Z ⊆ W × W' is bisimulation ($Z : M \underline{\leftrightarrow} M'$) if for all pairs (w, w') ∈ Z we have: -- w ∈ V(p) iff w' ∈ V'(p) -- if Rwv then for some v' ∈ W' we have R'w'v' and vZv' -- if R'w'v' then for some v ∈ W we have Rwv and vZv' - -Two models are bisimilar ($M \underline{\leftrightarrow} M'$) if there exists a bisimulation Z ∈ W × W'. - -Basically, models are bisimilar if they are, in essence, the same (there may be extra states or relations in one of the models but those states/relations do not add any new information compared to the other model). A bisimulation then is the set of states that are bisimilar between two models. - -Two pointed models are bisimilar if there exists a bisimulation such that (w,w') ∈ Z - -Two states are modally equivalent if they satisfy exactly the same formulas. -So if M,w and M',w' are bisimilar, then they are modally equivalent. - -If two states are modally equivalent, then they are bisimilar. - -### Example -It's a bit hard to describe this in words, but intuitive if you see it. -Here's an example: - - - -You see that from the top state, you can get to a terminal state in one or two steps, in both models. -Therefore, the top states of both models are _bisimilar_. -Since all of the states in the models are bisimilar, _the two models are bisimilar_. -The dotted lines connect the pairs that make up the _bisimulation_. - -### Example: finding bisimulations - -Take two example models: - -<table> -<thead> -<th>A</th> <th>B</th> -</thead> - -<tbody> -<tr> - -<td> - - - -<details> -<summary>Graphviz code</summary> - -<!-- :Tangle(dot) model-a.dot --> -```dot -digraph g { -1 -> 2 -2 -> 3 -3 -> 4 -3 -> 5 -1 [xlabel="p"] -2 [xlabel="q"] -3 [xlabel="q"] -4 [xlabel="q"] -5 [xlabel="q"] -} -``` - -</details> -</td> - -<td> - - - -<details> -<summary>Graphviz code</summary> - -<!-- :Tangle(dot) model-b.dot --> -```dot -digraph g { -a -> b -a -> c -c -> d -b -> d -d -> e -a [xlabel="p"] -b [xlabel="q"] -c [xlabel="q"] -d [xlabel="q"] -e [xlabel="q"] -} -``` - -</details> -</td> - -</tr> -</table> - -The claim is that states (A,1) and (B,a) are bisimilar. -How do you prove or refute the claim? - -Well, we need to find a bisimulation with the pair (1, a). -1. Start with pair (1, a) -2. In A, move from 1 to 2. Have to mimic the move in B, can do so by moving from a to b or from a to c. - Yields the pairs (2, b) and (2, c). -3. In A, move from 2 to 3. Have to mimic the move in B, can move from both b and c to d. - Yields the pair (3, d). -4. In A, two options: - - move from 3 to 4. Have to mimic the move in B, can move from d to e. - Yields the pair (4, e). - - move from 3 to 5. Have to mimic the move in B, can move from d to e. - Yields the pair (5, e). - -Since for any move in the first model, we can mimic it in the second model, we have a bisimulation. -The bisimulation contains exactly the pairs we just listed. -So there is a bisimulation Z = {(1, a), (2, b), (2, c), (3, d), (4, e), (5, e)}. -Since (1, a) ∈ Z, we can say that states (A, 1) and (B, a) are bisimilar. - -## Transforming and constructing models -Disjoint union of models: combine models by union of states, relations, and valuations. -A state in one of the models is modally equivalent with the state in the union. - -Generated submodel: starting from state w, only take its future. - -Tree unravelling: unravelling of world s in (W,R,V) is: -- $W' : (s_{1} \dots s_{n})$ with $s_{1} = s$ and $Rs_{i} s_{i+1}$ -- $R'$ relates ($s_{1} \dots s_{n}$) to ($s_{1} \dots s_{n+1}$) if $Rs_{n} s_{n+1}$ -- $V'(p) = \{ (s_{1} \dots s_{n} | s_{n} \in V(p) \}$ -- a state in (W',R',V') is bisimilar to $s_{n}$ in (W,R,V) -- if φ is satisfiable in M,w it is satisfiable in tree unravelling of s in M - -Bisimulation contraction -- W' consists of equivalence classes |s| = { t such that $s \underline{\leftrightarrow} t$ } -- R' relates |s| to |t| if Ruv for some u ∈ |s| and some v ∈ |t| -- V'(p) = { |s| | s ∈ V(p) } - -More on this, with examples, in [lecture 5](../lecture-5/#transforming-and-constructing-models). diff --git a/content/advanced-logic-notes/lecture-5/index.md b/content/advanced-logic-notes/lecture-5/index.md @@ -1,127 +0,0 @@ -+++ -title = 'Lecture 5' -template = 'page-math.html' -+++ -# Lecture 5 -If two states are bisimilar, then they are modally equivalent. -Prove by induction on definition of formulas. - -For finitely branching models, if two states modally equivalent, then they are bisimilar. -Prove by taking modal equivalence as bisimulation. - -Let Z := {(x, x') | for all φ: x ⊨ φ iff x' ⊨ φ}. -Z is a bisimulation. -- Local harmony is satisfied. -- zig: suppose (x, x') ∈ Z and x → y. - Because x ⊨ ◇ T also x' ⊨ ◇ T. - So x' has finitely many successors y'₁...y'n with n ≥ 1. - Suppose for all i: y is not modally equivalent to y'ᵢ. - There are φ₁...φn such that y ⊨ φᵢ and y'ᵢ ⊭ φᵢ. - x ⊨ ◇(φ₁ ∧ ... ∧ φn) so also x' ⊨ ◇ (φ₁ ∧ ... ∧ φn). - Contradiction. - - -Asymmetry is not modally definable. -To deal with only frames, we can use surjective bounded morphisms. - -Function f : W → W' is bounded morphism from (W,R) to (W',R') if: -- for all w,v ∈ W: if Rwv then Rf(w)f(v) -- for all w ∈ W and for all v' ∈ W': if R'f(w)v' then there exists v ∈ W such that f(v) = v' and Rwv - -A bounded morphism f is surjective if for every w' ∈ W' there exists w ∈ W such that f(w) = w' - -If f: W → W' is surjective bounded morphism from (W,R) to (W',R'), then if (W,R) ⊨ φ then (W', R') ⊨ φ - -### Bisimulation games for two players -Spoiler S claims M,s an N,t to be different. -Duplicator D claims they are similar. - -Play consists of sequence of links, starting with link s ~ t. - -At current link m ~ n (with m in M and n in N): -- if m an n different in their atoms, then S wins -- if not, then S picks a successor x either of m or of n -- then D has to find a matching transition to y in the other model -- play continues with next link x ~ y (or y ~ x) - -If player cannot make a move, he loses. -D wins infinite games. - -Modal depth of formulas. -Modal formulas are 'nearsighted': -- md(p) = md(⊥) = md(T) = 0 -- md(¬φ) = md(φ) -- md(φ ∨ ψ) = md(φ ∧ ψ) = max{md(φ), md(ψ)} -- md(□ φ) = md(◇ φ) = md(φ) + 1 - -We need a formula of model depth k to distinguish states x and y. -Spoiler can win bisimulation game in k rounds. -Every winning strategy for Spoiler corresponds to a distinguishing formula. -Games of less than k rounds can be won by Duplicator. -Formulas of modal depth less than k cannot distinguish between x and y. - -M,s and N,t satisfy the same formulas up to modal depth k iff duplicator has winning strategy in the k-round game starting in s ~ t. -If Spoiler can win in k rounds, then there is a distinguishing formula of modal depth k. - -### Transforming and constructing models -#### Tree unraveling -Basically taking the states with possible paths between them, and drawing a tree. - -Example: - -<table> -<tr> <th>Model</th> <th>Tree unraveling</th> </tr> - -<tr> -<td> - - - -<details> -<summary>Graphviz code</summary> - -<!-- :Tangle(dot) model-diagram.dot --> -```dot -digraph g { -1 -> 2 -1 -> 1 -} -``` - -</details> -</td> -<td> - - - -<details> -<summary>Graphviz code</summary> - -<!-- :Tangle(dot) tree-unraveling.dot --> -```dot -digraph g { -a [label="(1)"] -b [label="(1,2)"]; a -> b -c [label="(1,1)"]; a -> c -d [label="(1,1,2)"]; c -> d -e [label="(1,1,1)"]; c -> e -f [label="(1,1,1,2)"]; e -> f -g [label="..."]; e -> g -} -``` - -</details> - -</td> -</tr> -</table> - -If two trees have the same structure, they're bisimilar. - -#### Model contraction -Basically getting rid of 'unnecessary' states. - - - -### Validity and satisfiability -If φ is satisfiable, then it is satisfiable using a model with at most $2^{s(\phi)}$ elements with s(φ) the number of subformulas of φ. diff --git a/content/advanced-logic-notes/lecture-6/index.md b/content/advanced-logic-notes/lecture-6/index.md @@ -1,52 +0,0 @@ -+++ -title = 'Lecture 6' -+++ -# Lecture 6 -## Sequents -φ₁...φn ⇒ ψ₁...ψm valid if in every model, in every world in that model, the conjunction of the φᵢ implies the disjunction of the ψᵢ. - -Empty conjunction is true, empty disjunction is false. - -Reducing modal sequents: - - - -φ valid iff the sequent (⇒ φ) valid. - -For modal logic: -- If we get a sequent of the form p₁...n, ◇φ₁..◇φm ⇒ q₁..qk, ◇ψ₁...◇ψl -- Such a sequent only valid iff either pᵢ = qj for some i and j, or φᵢ ⇒ ψ₁...ψl is valid for some i ∈ {1...m} - -Start with intended conclusion, try to build a proof while moving upwards. -Formula is valid iff it is derivable in sequent calculus. -Validity using sequents: -1. Rewrite formula - - (a → b) to (¬ a ∨ b) - - (¬ □ a) to (◇ ¬ a) - - (□ a) to (¬ ◇ ¬ a) - -2. Rewrite sequent, based on rules above -3. Maybe rewrite formula again -4. Decide on validity of sequent -5. Conclude on validity of formula - -## Tableaux -Tableau is finite tree of sequents. -If all solid branches close, yields validity of initial sequent. -If at least one branch does not close, yields a counterexample. - -The dot separates assumptions on the left from what's true on the right. -A branch closes if what's assumed also holds in the state. - - - -In modal logic: - - - -Example: - - - -It's not valid because in the two red states, the letters on the left of the dot are not on the right. -The countermodel comes from taking the numbers next to each step (the numbers are states), connecting them, and creating a valuation where the letters on the left side of the dot (the assumptions) are true. diff --git a/content/advanced-logic-notes/lecture-7/index.md b/content/advanced-logic-notes/lecture-7/index.md @@ -1,53 +0,0 @@ -+++ -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-8/index.md b/content/advanced-logic-notes/lecture-8/index.md @@ -1,190 +0,0 @@ -+++ -title = 'Lecture 8' -+++ -# Lecture 8 -## Modal tautologies - - - -## Proof systems -Hilbert systems: -- proof is sequence of numbered formulas -- every formula is: an axiom, or result of applying a derivation rule - -Sufficient to have 2 axioms and a rule: -- K: φ → ψ → φ -- S: (φ → ψ → θ) → (φ → ψ) → (φ → θ) -- modus ponens: if φ and (φ → ψ), then ψ - -Rules will be given, don't need to be memorized. - -Admissible rule: - - - -Proof system K is sound and complete with respect to all frames, ⊢K φ iff ⊨ φ. - -<!-- TODO: add this to anki --> -Need to memorize soundness and completeness results -- K sound and complete for all frames -- T sound and complete for all _reflexive_ frames - - T: K with □ p → p -- S4 sound and complete for all _reflexive-transitive_ frames - - S4: T with □ p → □ □ p -- S5 sound and complete for all frames with R an equivalence relation - - S5: S4 with ¬ □ p → □ ¬ □ p - -## Example of derivation -Give derivation in K of ◇ φ ∧ □ (φ → ψ) → ◇ ψ. -Same as example in book <abbr title='Modal Logic for Open Minds (Benthem)'>MLOM</abbr> page 52. - -First, work backwards from the goal towards an axiom or tautology: - -``` -◇ φ ∧ □ (φ → ψ) → ◇ ψ ≡ □ (φ → ψ) → (◇ φ → ◇ ψ) [you can rewrite a conjunction as an implication] - ≡ □ (φ → ψ) → (¬ □ ¬ φ → ¬ □ ¬ ψ) [rewrite diamond to ¬ □ ¬] - ≡ □ (φ → ψ) → (□ ¬ ψ → □ ¬ φ) [rewrite contrapositive (¬ a → ¬ b) to (b → a)] - ≡ □ (φ → ψ) → □ (¬ ψ → ¬ φ) [box distribution over implication] - ≡ □ (φ → ψ) → □ (φ → ψ) [again contrapositive] - ≡ (φ → ψ) → (φ → ψ) [because if derivable (a → b), then derivable (□ a → □ b)] -``` - -We arrive at a tautology. - -Then you write it out in a Hilbert-style proof, starting with the tautology/axiom. -PROP means rewriting in propositional logic. - -1. (φ → ψ) → (¬ ψ → ¬ φ). PROP. -2. □ (φ → ψ) → □ (¬ ψ → ¬ φ). DISTR, 1. -3. □ (p → q) → □ p → □ q. modal distribution (i.e., this is an axiom in K that we use) -4. □ (¬ ψ → ¬ φ) → □ ¬ ψ → □ ¬ φ. substitution, 3 (i.e., substitute stuff in the axiom). -5. □ (φ → ψ) → □ ¬ ψ → □ ¬ φ. PROP, 2, 4. -6. □ (φ → ψ) → ¬ ◇ ψ → ¬ ◇ φ. definition of ◇, □. -7. □ (φ → ψ) → ◇ φ → ◇ ψ. PROP, 6. -8. ◇ φ ∧ □ (φ → ψ) → ◇ ψ. PROP, 7. - -<details> -<summary>Why you can rewrite a conjunction as an implication</summary> - -You can safely rewrite a conjunction to an implication: (a ∧ b → c) ≡ a → (b → c). -Remember that implication is right-associative! - -If you don't trust me, I didn't trust myself either so I made a truth table: - -<table> -<thead> -<tr> -<th>a</th> -<th>b</th> -<th>c</th> -<th>b → c</th> -<th>a ∧ b</th> -<th>a → c</th> -<th>a ∧ b → c</th> -<th>b → (a → c)</th> -<th>a → (b → c)</th> -</tr> -</thead> -<tbody> -<tr> -<td>0</td> -<td>0</td> -<td>0</td> -<td>1</td> -<td>0</td> -<td>1</td> -<td>1</td> -<td>1</td> -<td>1</td> -</tr> - -<tr> -<td>0</td> -<td>0</td> -<td>1</td> -<td>1</td> -<td>0</td> -<td>1</td> -<td>1</td> -<td>1</td> -<td>1</td> -</tr> - -<tr> -<td>0</td> -<td>1</td> -<td>0</td> -<td>0</td> -<td>0</td> -<td>1</td> -<td>1</td> -<td>1</td> -<td>1</td> -</tr> - -<tr> -<td>0</td> -<td>1</td> -<td>1</td> -<td>1</td> -<td>0</td> -<td>1</td> -<td>1</td> -<td>1</td> -<td>1</td> -</tr> - -<tr> -<td>1</td> -<td>0</td> -<td>0</td> -<td>1</td> -<td>0</td> -<td>0</td> -<td>1</td> -<td>1</td> -<td>1</td> -</tr> - -<tr> -<td>1</td> -<td>0</td> -<td>1</td> -<td>1</td> -<td>0</td> -<td>1</td> -<td>1</td> -<td>1</td> -<td>1</td> -</tr> - -<tr> -<td>1</td> -<td>1</td> -<td>0</td> -<td>0</td> -<td>1</td> -<td>0</td> -<td>0</td> -<td>0</td> -<td>0</td> -</tr> - -<tr> -<td>1</td> -<td>1</td> -<td>1</td> -<td>1</td> -<td>1</td> -<td>1</td> -<td>1</td> -<td>1</td> -<td>1</td> -</tr> -</tbody> -</table> - -You see that the right three columns all have the same values, so semantically the formulas are the same. - -</details> - diff --git a/content/advanced-logic-notes/lecture-9/index.md b/content/advanced-logic-notes/lecture-9/index.md @@ -1,126 +0,0 @@ -+++ -title = 'Lecture 9' -+++ -# Lecture 9 -## Temporal logic using temporal frames -Linear time logic: events along a single computation path. 'at some point we will have p' - -Branching time logic: quantify over possible paths. 'there is a path where eventually p' - -A frame F = (T, <) is a temporal frame if both: -- < is irreflexive: not t < t for all t -- < is transitive: if t < u and u < v then t < v - -Truth and validity: - - - -Right-linearity: -- "all future points are related" -- definition: ∀ x,y,z: (x < y) ∧ (x < z) → (y < z) ∨ (y = z) ∨ (z < y) -- is modally definable - -Right-branching: -- "right-branching is _not_ right-linear, so some point has two unrelated points in the future" -- definition: there exist x,y,z such that x < y and x < z but ¬ (y < z) ∧ y ≠ z ∧ ¬ (z < y) -- is _not_ modally definable - -Discrete: -- "every point with a successor has an immediate successor -- definition: (x < y ) → ∃ z : x < z ∧ ¬ ∃ u: ( x < u) ∧ (u < z) -- is modally definable in basic temporal logic - -Dense: -- "between any two points is a third one" -- definition: x < z → ∃ y (x < y ∧ y < z) -- is modally definable - -Operator next: -- symbol ⊗ -- M,t ⊨ ⊗ φ iff ∃ v : t < v ∧ (¬ ∃ u : t < u < v) ∧ M,v ⊨ φ - - e.g. x ⊨ ⊗p: there a future we can reach only in 1 step from x where p holds - - you can go directly from centraal to Utrecht, but Amstelstation is still there -- next not definable in basic modal logic - -Operator until: -- symbol U -- M,t ⊨ φ U ψ iff ∃ v : t < v ∧ M,v ⊨ ψ ∧ ∀ u : t < u < v → M,u ⊨ φ - - if we have a future where ψ holds, then φ holds in all points between now and that future -- not definable in basic modal logic - -Examples of until: - -<table> -<tr> -<td> - - - -<details> -<summary>Graphviz code</summary> - -<!-- :Tangle(dot) until-1.dot --> -```dot -digraph g { -rankdir=BT -a -> b -a -> c -c -> d -b -> d -c -> e -c [xlabel="p"] -d [xlabel="q"] -e [xlabel="q"] -} -``` -</details> - -</td> -<td> - - - -<details> -<summary>Graphviz code</summary> - -<!-- :Tangle(dot) until-2.dot --> -```dot -digraph g { -rankdir=BT -a -> b -a -> c -c -> d -b -> d -d [xlabel="q"] -c [xlabel="p"] -} -``` - -</details> -</td> -</tr> - -<tr> -<td> -a ⊨ p U q. e.g. state e, we have q, and in any paths we have to go through states that have p. -</td> - -<td> -a ⊭ p U q. because we do not have p in state b. -</td> -</tr> -</table> - -In a temporal frame: -- ◇ p is equivalent to T U p -- ⊗ p i equivalent to ⊥ U p - -<!-- -TODO: Things to look at: -- until not definable in basic modal logic in temporal frames -- until not definable in temporal modal logic in temporal frames -- next not definable in basic modal logic in temporal frames -- define discrete in temporal logic -- use next to define discrete in temporal logic -- define right-linearity in temporal logic ---> diff --git a/content/advanced-logic-notes/model-transformations-tree-unravelling-bisimulation-contraction/index.md b/content/advanced-logic-notes/model-transformations-tree-unravelling-bisimulation-contraction/index.md @@ -0,0 +1,85 @@ ++++ +title = 'Model transformations (tree unravelling, bisimulation contraction)' +template = 'page-math.html' ++++ +# Lecture 5 +## Transforming and constructing models +Disjoint union of models: combine models by union of states, relations, and valuations. +A state in one of the models is modally equivalent with the state in the union. + +Generated submodel: starting from state w, only take its future. + +### Transforming and constructing models +#### Tree unraveling +Tree unravelling: unravelling of world s in (W,R,V) is: +- $W' : (s_{1} \dots s_{n})$ with $s_{1} = s$ and $Rs_{i} s_{i+1}$ +- $R'$ relates ($s_{1} \dots s_{n}$) to ($s_{1} \dots s_{n+1}$) if $Rs_{n} s_{n+1}$ +- $V'(p) = \{ (s_{1} \dots s_{n} | s_{n} \in V(p) \}$ +- a state in (W',R',V') is bisimilar to $s_{n}$ in (W,R,V) +- if φ is satisfiable in M,w it is satisfiable in tree unravelling of s in M + +Basically taking the states with possible paths between them, and drawing a tree. + +Example: + +<table> +<tr> <th>Model</th> <th>Tree unraveling</th> </tr> + +<tr> +<td> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) model-diagram.dot --> +```dot +digraph g { +1 -> 2 +1 -> 1 +} +``` + +</details> +</td> +<td> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) tree-unraveling.dot --> +```dot +digraph g { +a [label="(1)"] +b [label="(1,2)"]; a -> b +c [label="(1,1)"]; a -> c +d [label="(1,1,2)"]; c -> d +e [label="(1,1,1)"]; c -> e +f [label="(1,1,1,2)"]; e -> f +g [label="..."]; e -> g +} +``` + +</details> + +</td> +</tr> +</table> + +If two trees have the same structure, they're bisimilar. + +#### Model contraction +Bisimulation contraction +- W' consists of equivalence classes |s| = { t such that $s \underline{\leftrightarrow} t$ } +- R' relates |s| to |t| if Ruv for some u ∈ |s| and some v ∈ |t| +- V'(p) = { |s| | s ∈ V(p) } + +Basically getting rid of 'unnecessary' states. + + + +### Validity and satisfiability +If φ is satisfiable, then it is satisfiable using a model with at most $2^{s(\phi)}$ elements with s(φ) the number of subformulas of φ. diff --git a/content/advanced-logic-notes/lecture-5/model-contraction.png b/content/advanced-logic-notes/model-transformations-tree-unravelling-bisimulation-contraction/model-contraction.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-5/model-diagram.dot b/content/advanced-logic-notes/model-transformations-tree-unravelling-bisimulation-contraction/model-diagram.dot diff --git a/content/advanced-logic-notes/lecture-5/model-diagram.dot.svg b/content/advanced-logic-notes/model-transformations-tree-unravelling-bisimulation-contraction/model-diagram.dot.svg diff --git a/content/advanced-logic-notes/lecture-5/tree-unraveling.dot b/content/advanced-logic-notes/model-transformations-tree-unravelling-bisimulation-contraction/tree-unraveling.dot diff --git a/content/advanced-logic-notes/lecture-5/tree-unraveling.dot.svg b/content/advanced-logic-notes/model-transformations-tree-unravelling-bisimulation-contraction/tree-unraveling.dot.svg diff --git a/content/advanced-logic-notes/lecture-10/example-multimodal-logic-formula.dot b/content/advanced-logic-notes/multi-modal-logic/example-multimodal-logic-formula.dot diff --git a/content/advanced-logic-notes/lecture-10/example-multimodal-logic-formula.dot.svg b/content/advanced-logic-notes/multi-modal-logic/example-multimodal-logic-formula.dot.svg diff --git a/content/advanced-logic-notes/multi-modal-logic/index.md b/content/advanced-logic-notes/multi-modal-logic/index.md @@ -0,0 +1,47 @@ ++++ +title = 'Multi-modal logic' ++++ +# Lecture 10 +## Multi-modal logic +Assume set of labels I (which in a diagram are on the arrows). +For every label i there is modality 〈i〉 so the formulas of multi-modal logic are, given I, defined for i in ∈ I. + +I-frame is pair (W, {Rᵢ | i ∈ I}). +Rᵢ ⊆ W × W for every i ⊆ I. + +I-model is triple (W, {Rᵢ | i ⊆ I}, V). + +### Truth and validity +For M an I-model, M,w ⊨ φ is defined by induction on the definition of formulas. + +Clauses: +- M,w ⊨ 〈a〉φ iff M,v ⊨ φ for some v with Rₐwv +- M,w ⊨ [a]φ iff M,v ⊨ φ for all v with Rₐwv + +### Example +Use index set I = {a, b, c}. +Give model with a world where the formula 〈a〉(〈b〉[a] p ∧ [c] ¬ 〈a〉p) is true. + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) example-multimodal-logic-formula.dot --> +```dot +digraph g { +rankdir=LR +1 -> 2 [label="a"] +2 -> 3 [label="b"] +} +``` + +</details> + + +For a bisimulation, when you do a step between states, they have to be with the same label (so the mimic step must have the same label). + +### Geach axiom +◇ □ p → □ ◇ p. + +Valid in frame iff for every r ← s → u there is r → v ← u. diff --git a/content/advanced-logic-notes/program-correctness.md b/content/advanced-logic-notes/program-correctness.md @@ -0,0 +1,19 @@ ++++ +title = 'Program correctness' ++++ +## Program correctness +Prove that a program meets its specification. + +Correctness specification: formal description of how program is supposed to behave + +Program is correct: its executions satisfy the specification + +### Verification - Hoare approach +Prove statements of form `{precondition} program {postcondition}` +- pre/postcondition are formulas +- program is a while-program +- we have proof rules for showing {φ} α {ψ} + +Partial correctness: if program starts satisfying φ, and if it halts, then when it halts ψ is satisfied + +Total correctness: partially correct, and terminates whenever started while satisfying φ diff --git a/content/advanced-logic-notes/lecture-8/Screenshot 2022-03-05 at 12.06.06.png b/content/advanced-logic-notes/proof-systems-and-derivation/Screenshot 2022-03-05 at 12.06.06.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-8/admissible-rule.png b/content/advanced-logic-notes/proof-systems-and-derivation/admissible-rule.png Binary files differ. diff --git a/content/advanced-logic-notes/proof-systems-and-derivation/index.md b/content/advanced-logic-notes/proof-systems-and-derivation/index.md @@ -0,0 +1,190 @@ ++++ +title = 'Proof systems and derivation' ++++ +# Lecture 8 +## Modal tautologies + + + +## Proof systems +Hilbert systems: +- proof is sequence of numbered formulas +- every formula is: an axiom, or result of applying a derivation rule + +Sufficient to have 2 axioms and a rule: +- K: φ → ψ → φ +- S: (φ → ψ → θ) → (φ → ψ) → (φ → θ) +- modus ponens: if φ and (φ → ψ), then ψ + +Rules will be given, don't need to be memorized. + +Admissible rule: + + + +Proof system K is sound and complete with respect to all frames, ⊢K φ iff ⊨ φ. + +<!-- TODO: add this to anki --> +Need to memorize soundness and completeness results +- K sound and complete for all frames +- T sound and complete for all _reflexive_ frames + - T: K with □ p → p +- S4 sound and complete for all _reflexive-transitive_ frames + - S4: T with □ p → □ □ p +- S5 sound and complete for all frames with R an equivalence relation + - S5: S4 with ¬ □ p → □ ¬ □ p + +## Example of derivation +Give derivation in K of ◇ φ ∧ □ (φ → ψ) → ◇ ψ. +Same as example in book <abbr title='Modal Logic for Open Minds (Benthem)'>MLOM</abbr> page 52. + +First, work backwards from the goal towards an axiom or tautology: + +``` +◇ φ ∧ □ (φ → ψ) → ◇ ψ ≡ □ (φ → ψ) → (◇ φ → ◇ ψ) [you can rewrite a conjunction as an implication] + ≡ □ (φ → ψ) → (¬ □ ¬ φ → ¬ □ ¬ ψ) [rewrite diamond to ¬ □ ¬] + ≡ □ (φ → ψ) → (□ ¬ ψ → □ ¬ φ) [rewrite contrapositive (¬ a → ¬ b) to (b → a)] + ≡ □ (φ → ψ) → □ (¬ ψ → ¬ φ) [box distribution over implication] + ≡ □ (φ → ψ) → □ (φ → ψ) [again contrapositive] + ≡ (φ → ψ) → (φ → ψ) [because if derivable (a → b), then derivable (□ a → □ b)] +``` + +We arrive at a tautology. + +Then you write it out in a Hilbert-style proof, starting with the tautology/axiom. +PROP means rewriting in propositional logic. + +1. (φ → ψ) → (¬ ψ → ¬ φ). PROP. +2. □ (φ → ψ) → □ (¬ ψ → ¬ φ). DISTR, 1. +3. □ (p → q) → □ p → □ q. modal distribution (i.e., this is an axiom in K that we use) +4. □ (¬ ψ → ¬ φ) → □ ¬ ψ → □ ¬ φ. substitution, 3 (i.e., substitute stuff in the axiom). +5. □ (φ → ψ) → □ ¬ ψ → □ ¬ φ. PROP, 2, 4. +6. □ (φ → ψ) → ¬ ◇ ψ → ¬ ◇ φ. definition of ◇, □. +7. □ (φ → ψ) → ◇ φ → ◇ ψ. PROP, 6. +8. ◇ φ ∧ □ (φ → ψ) → ◇ ψ. PROP, 7. + +<details> +<summary>Why you can rewrite a conjunction as an implication</summary> + +You can safely rewrite a conjunction to an implication: (a ∧ b → c) ≡ a → (b → c). +Remember that implication is right-associative! + +If you don't trust me, I didn't trust myself either so I made a truth table: + +<table> +<thead> +<tr> +<th>a</th> +<th>b</th> +<th>c</th> +<th>b → c</th> +<th>a ∧ b</th> +<th>a → c</th> +<th>a ∧ b → c</th> +<th>b → (a → c)</th> +<th>a → (b → c)</th> +</tr> +</thead> +<tbody> +<tr> +<td>0</td> +<td>0</td> +<td>0</td> +<td>1</td> +<td>0</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +</tr> + +<tr> +<td>0</td> +<td>0</td> +<td>1</td> +<td>1</td> +<td>0</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +</tr> + +<tr> +<td>0</td> +<td>1</td> +<td>0</td> +<td>0</td> +<td>0</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +</tr> + +<tr> +<td>0</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>0</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +</tr> + +<tr> +<td>1</td> +<td>0</td> +<td>0</td> +<td>1</td> +<td>0</td> +<td>0</td> +<td>1</td> +<td>1</td> +<td>1</td> +</tr> + +<tr> +<td>1</td> +<td>0</td> +<td>1</td> +<td>1</td> +<td>0</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +</tr> + +<tr> +<td>1</td> +<td>1</td> +<td>0</td> +<td>0</td> +<td>1</td> +<td>0</td> +<td>0</td> +<td>0</td> +<td>0</td> +</tr> + +<tr> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +<td>1</td> +</tr> +</tbody> +</table> + +You see that the right three columns all have the same values, so semantically the formulas are the same. + +</details> + diff --git a/content/advanced-logic-notes/lecture-8/modal-tautologies.png b/content/advanced-logic-notes/proof-systems-and-derivation/modal-tautologies.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-11/formula-examples.png b/content/advanced-logic-notes/propositional-dynamic-logic-pdl/formula-examples.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-12/if-then-else-calculation.png b/content/advanced-logic-notes/propositional-dynamic-logic-pdl/if-then-else-calculation.png Binary files differ. diff --git a/content/advanced-logic-notes/propositional-dynamic-logic-pdl/index.md b/content/advanced-logic-notes/propositional-dynamic-logic-pdl/index.md @@ -0,0 +1,121 @@ ++++ +title = 'Propositional dynamic logic (PDL)' +template = 'page-math.html' ++++ +# 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. + +Operators: +- composition "R;S" = {(x, z) | ∃ y : Rxy ∧ Syz} +- union "R ∪ S" = {(x, y) | Rxy ∨ Sxy} +- R\*: repeat R one or more times + +A model M is a PDL-model if the frame is a PDL-frame and $R_{\phi ?} = \\{ (w,w) \\;|\\; M, w \models \phi\\}$ + +The R of the frame is all sets of Rₐ where _a_ is a program (i.e. a label on an arrow). + +<details> +<summary>Proof example of 〈α, β〉 p → 〈α〉〈β〉p</summary> + +- Take a PDL model and a state x. +- Assume x ⊨ 〈α, β〉 p +- That is, there is a state y such that $(x, y) \in R_{\alpha;\beta}$ and y ⊨ p. +- $R_{\alpha;\beta} = R_{\alpha}; R_{\beta}$ +- That is, there is a state u such that $(x, u) \in R_{\alpha}$ and $(u,y) \in R_{\beta}$. +- Because $(u,y) ∈ R_{\beta}$ and y ⊨ p, we have u ⊨ 〈β〉 p +- Because $(x,u) ∈ R_{\alpha}$, we have and u ⊨ 〈β〉p we have x ⊨ 〈α〉〈β〉p. +</details> + +If then else: +- program: `if p then a else b` +- encoding: (p?; a) ∪ (¬ p? ; b) + +<details> +<summary>Example</summary> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) model-if-then-else.dot --> +```dot +digraph g { +rankdir=LR +1 [xlabel="[p]"] +1 -> 2 [label="a"] +4 -> 2 [label="b"] +1 -> 3 [label="b"] +4 -> 3 [label="a"] +} + +``` + +</details> + +Calculate the relation for `if p then a else b`, which is encoded as `(p?; a) ∪ (¬ p?; b)`: + + +</details> + +While: +- program: `while p do a` +- encoding: (P?; a)\*; ¬ p? + +<details> +<summary>Example</summary> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) model-while.dot --> +```dot +digraph g { +rankdir=LR +1 -> 2 [label="a"] +2 -> 3 [label="a"] +3 -> 4 [label="a"] +4 -> 5 [label="a"] +5 -> 6 [label="a"] +1 [xlabel="[p]"] +2 [xlabel="[p]"] +3 [xlabel="[p]"] +4 [xlabel="[p]"] +} +``` + +</details> + +Calculating the relation `while p do a`, encoded as `(p?; a)*; ¬ p?`: + + +</details> + +If E is a bisimulation between two A-models, then it is a bisimulation for the models' PDL-extensions. +However, intersection and inverse are not safe for bisimulation. diff --git a/content/advanced-logic-notes/lecture-12/model-if-then-else.dot b/content/advanced-logic-notes/propositional-dynamic-logic-pdl/model-if-then-else.dot diff --git a/content/advanced-logic-notes/lecture-12/model-if-then-else.dot.svg b/content/advanced-logic-notes/propositional-dynamic-logic-pdl/model-if-then-else.dot.svg diff --git a/content/advanced-logic-notes/lecture-12/model-while.dot b/content/advanced-logic-notes/propositional-dynamic-logic-pdl/model-while.dot diff --git a/content/advanced-logic-notes/lecture-12/model-while.dot.svg b/content/advanced-logic-notes/propositional-dynamic-logic-pdl/model-while.dot.svg diff --git a/content/advanced-logic-notes/lecture-12/while-calculation.png b/content/advanced-logic-notes/propositional-dynamic-logic-pdl/while-calculation.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-2/example-characterizing.png b/content/advanced-logic-notes/semantics-truth-and-validity-game-semantics-for-formula-validity/example-characterizing.png Binary files differ. diff --git a/content/advanced-logic-notes/semantics-truth-and-validity-game-semantics-for-formula-validity/index.md b/content/advanced-logic-notes/semantics-truth-and-validity-game-semantics-for-formula-validity/index.md @@ -0,0 +1,179 @@ ++++ +title = 'Semantics: truth and validity, game semantics for formula validity' +template = 'page-math.html' ++++ +# Lecture 2 +## Semantics: local truth +Valuation notation: +- V : Var → P(W) means Var → W → {0,1} +- V(p,w) = 1 is the same as w ∈ V(p) + +A formula φ _characterizes_ a state x in model M if φ is true in x but not in other states of M. + +A formula φ _distinguishes_ state x from state y in a model M if φ is true in x but not in y. + + + +Above: +- the formula 3 ⊨ □ ⊥ characterizes state 3 +- the formula 2 ⊨ ◇ □ ⊥ characterizes state 2 + +## Game semantics +This is an approach to determine if a formula φ holds in a pointed model M, w. + +We have: +- model M = ((W,R), V), world w ∈ W, formula φ +- two players: + - Verifier V claims that φ is true in w (sort of like ∀) + - Falsifier F claims that φ is false in w (sort of like ∃, try to find a _witness_) +- position: pair (w, φ) with w ∈ W a world and φ a formula +- move: from position (w, φ), determined by main operator of φ + +Assume that negation only applied to prop. variables. +Transform formulas from ¬ □ p to ◇ ¬ p, ¬(p ∧ q) to ¬p ∨ ¬q. + +The position determines the move, e.g. in a position (t, ◇ φ), V chooses a successor _u_ of _t_, and play continues with (u, φ). +For (t,p), if p is true in t then V wins, otherwise F wins. +For (t, ¬p), if p is false in t then V wins, otherwise F wins. +If a player should but cannot choose a successor, they lose. + +Who starts: +- V: ∨, ◇ +- F: ∧, □ + +A complete game tree for φ and (M,w) starts with (w,φ) and contains all possible moves. +A strategy for player P is subset of steps for P, and it's a winning strategy if it ensures that P wins the game. +φ is true in M in s ⇔ V has a winning strategy for M,s,φ. + +### Example +Diagram: + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) states.dot --> +```dot +digraph states { +1 -> 2 +1 -> 3 +2 -> 3 +3 -> 2 +3 -> 4 +4 -> 2 +4 -> 3 +} +``` + +</details> + +Given: +- formula ◇ p ∨ □ ◇ p, in state 2. +- p is true in state 3. + +Complete game tree: + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) tree.dot --> +```dot +digraph gametree { + top [label="[V] ◇ p ∨ □ ◇ p, 2"] + l11 [label="[V] ◇ p, 2"] + l12 [label="[F] □ ◇ p, 2"] + top -> l11 + top -> l12 + l21 [label="p 3"] + l22 [label="[V] ◇ p, 3"] + l11 -> l21 + l12 -> l22 + l31 [label="Verifier wins"] + l32 [label="p, 2"] + l33 [label="p, 4"] + l21 -> l31 + l22 -> l32 + l22 -> l33 + l41 [label="Falsifier wins."] + l42 [label="Falsifier wins."] + l32 -> l41 + l33 -> l42 +} +``` + +</details> + +## Truth and validity +(((W,R),V),w) ⊨ φ means φ is valid in a point w. +(W,R) ⊨ φ means φ is valid in a frame (W,R). +⊨ φ means φ is valid/tautology. +If a part is omitted, it's implicitly universally quantified. + +Satisfiability: +- φ _satisfiable in model M_ if there's a world w ∈ M such that M,w ⊨ φ +- φ _satisfiable_ if there's a model M and a world w ∈ M such that M,w ⊨ φ +- φ and ψ _semantically equivalent_ if ∀ M,w: M,w ⊨ φ ⇔ M,w ⊨ ψ +- φ valid iff ¬ φ not satisfiable + +### Example +Show universal validity of □ (φ → ψ) → (□ φ → □ ψ) + +1. let F = (W,R) be frame, V valuation on F, let x ∈ W. +2. Assume a1: F,V,x ⊨ □ (φ → ψ) +3. Assume a2: F,V,x ⊨ □ φ +4. Aim to show F,V,x ⊨ □ ψ. +5. □ is universal quantification, so take an arbitrary successor y ∈ W. +6. If Rxy, aim to show y ⊨ ψ. If not, □ ψ holds. +7. Have y ⊨ φ → ψ and y ⊨ φ. +8. From a2, have y ⊨ φ. +9. From a1, have have y ⊨ ψ. +10. Hence x ⊨ □ ψ, hence x ⊨ □ φ → □ ψ. Hence formula is valid. + +## 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 ⊨ φ. +If you need to prove that a formula characterizes a property, you need to prove this bi-implication in _both_ directions. + +## Modal equivalence +Two states M, w and M', w' are modally equivalent if they satisfy the same formulas. diff --git a/content/advanced-logic-notes/lecture-2/states.dot b/content/advanced-logic-notes/semantics-truth-and-validity-game-semantics-for-formula-validity/states.dot diff --git a/content/advanced-logic-notes/lecture-2/states.dot.svg b/content/advanced-logic-notes/semantics-truth-and-validity-game-semantics-for-formula-validity/states.dot.svg diff --git a/content/advanced-logic-notes/lecture-2/tree.dot b/content/advanced-logic-notes/semantics-truth-and-validity-game-semantics-for-formula-validity/tree.dot diff --git a/content/advanced-logic-notes/lecture-2/tree.dot.svg b/content/advanced-logic-notes/semantics-truth-and-validity-game-semantics-for-formula-validity/tree.dot.svg diff --git a/content/advanced-logic-notes/standard-translation-mapping-basic-modal-logic-to-first-order-predicate-logic/index.md b/content/advanced-logic-notes/standard-translation-mapping-basic-modal-logic-to-first-order-predicate-logic/index.md @@ -0,0 +1,53 @@ ++++ +title = 'Standard translation: mapping basic modal logic to first-order predicate logic' ++++ +# 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/standard-translation-mapping-basic-modal-logic-to-first-order-predicate-logic/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/standard-translation-mapping-basic-modal-logic-to-first-order-predicate-logic/standard-translation-rules.png Binary files differ. diff --git a/content/advanced-logic-notes/temporal-logic/index.md b/content/advanced-logic-notes/temporal-logic/index.md @@ -0,0 +1,126 @@ ++++ +title = 'Temporal logic' ++++ +# Lecture 9 +## Temporal logic using temporal frames +Linear time logic: events along a single computation path. 'at some point we will have p' + +Branching time logic: quantify over possible paths. 'there is a path where eventually p' + +A frame F = (T, <) is a temporal frame if both: +- < is irreflexive: not t < t for all t +- < is transitive: if t < u and u < v then t < v + +Truth and validity: + + + +Right-linearity: +- "all future points are related" +- definition: ∀ x,y,z: (x < y) ∧ (x < z) → (y < z) ∨ (y = z) ∨ (z < y) +- is modally definable + +Right-branching: +- "right-branching is _not_ right-linear, so some point has two unrelated points in the future" +- definition: there exist x,y,z such that x < y and x < z but ¬ (y < z) ∧ y ≠ z ∧ ¬ (z < y) +- is _not_ modally definable + +Discrete: +- "every point with a successor has an immediate successor +- definition: (x < y ) → ∃ z : x < z ∧ ¬ ∃ u: ( x < u) ∧ (u < z) +- is modally definable in basic temporal logic + +Dense: +- "between any two points is a third one" +- definition: x < z → ∃ y (x < y ∧ y < z) +- is modally definable + +Operator next: +- symbol ⊗ +- M,t ⊨ ⊗ φ iff ∃ v : t < v ∧ (¬ ∃ u : t < u < v) ∧ M,v ⊨ φ + - e.g. x ⊨ ⊗p: there a future we can reach only in 1 step from x where p holds + - you can go directly from centraal to Utrecht, but Amstelstation is still there +- next not definable in basic modal logic + +Operator until: +- symbol U +- M,t ⊨ φ U ψ iff ∃ v : t < v ∧ M,v ⊨ ψ ∧ ∀ u : t < u < v → M,u ⊨ φ + - if we have a future where ψ holds, then φ holds in all points between now and that future +- not definable in basic modal logic + +Examples of until: + +<table> +<tr> +<td> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) until-1.dot --> +```dot +digraph g { +rankdir=BT +a -> b +a -> c +c -> d +b -> d +c -> e +c [xlabel="p"] +d [xlabel="q"] +e [xlabel="q"] +} +``` +</details> + +</td> +<td> + + + +<details> +<summary>Graphviz code</summary> + +<!-- :Tangle(dot) until-2.dot --> +```dot +digraph g { +rankdir=BT +a -> b +a -> c +c -> d +b -> d +d [xlabel="q"] +c [xlabel="p"] +} +``` + +</details> +</td> +</tr> + +<tr> +<td> +a ⊨ p U q. e.g. state e, we have q, and in any paths we have to go through states that have p. +</td> + +<td> +a ⊭ p U q. because we do not have p in state b. +</td> +</tr> +</table> + +In a temporal frame: +- ◇ p is equivalent to T U p +- ⊗ p i equivalent to ⊥ U p + +<!-- +TODO: Things to look at: +- until not definable in basic modal logic in temporal frames +- until not definable in temporal modal logic in temporal frames +- next not definable in basic modal logic in temporal frames +- define discrete in temporal logic +- use next to define discrete in temporal logic +- define right-linearity in temporal logic +--> diff --git a/content/advanced-logic-notes/lecture-9/truth-and-validity.png b/content/advanced-logic-notes/temporal-logic/truth-and-validity.png Binary files differ. diff --git a/content/advanced-logic-notes/lecture-9/until-1.dot b/content/advanced-logic-notes/temporal-logic/until-1.dot diff --git a/content/advanced-logic-notes/lecture-9/until-1.dot.svg b/content/advanced-logic-notes/temporal-logic/until-1.dot.svg diff --git a/content/advanced-logic-notes/lecture-9/until-2.dot b/content/advanced-logic-notes/temporal-logic/until-2.dot diff --git a/content/advanced-logic-notes/lecture-9/until-2.dot.svg b/content/advanced-logic-notes/temporal-logic/until-2.dot.svg
