commit f07aa866ac886d5053ff42bcbb10277e163801b4 parent 64f1d6e8b559cc9961cfa05b27d9b08d9271e559 Author: Alex Balgavy <alex@balgavy.eu> Date: Thu, 24 Mar 2022 21:45:46 +0100 Add clarifications to advanced logic notes Diffstat:
15 files changed, 157 insertions(+), 142 deletions(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md @@ -8,6 +8,7 @@ title = 'Advanced Logic' - [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/) +- [The finite model property](the-finite-model-property/) - [Proof systems and derivation](proof-systems-and-derivation/) - [Temporal logic](temporal-logic/) - [Multi-modal logic](multi-modal-logic/) @@ -17,12 +18,12 @@ title = 'Advanced 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/) +- [Exercise 1](exercise-1/): validity, game semantics (verifier/falsifier) +- [Exercise 3](exercise-3/): bisimulation game semantics, sequents, tableaux +- [Exercise 4](exercise-4/): derivation in proof systems, temporal logic +- [Exercise 5](exercise-5/): PDL +- [Homework 1](homework-1/): misc topics +- [Some midterm solutions](some-midterm-solutions/): validity, bisimulation, definability in BML 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/bisimulations/index.md b/content/advanced-logic-notes/bisimulations/index.md @@ -3,8 +3,7 @@ title = 'Bisimulations' template = 'page-math.html' +++ -# Lecture 4 -## Bisimulations +# 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' @@ -12,18 +11,18 @@ A non-empty relation Z ⊆ W × W' is bisimulation ($Z : M \underline{\leftright 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. +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 pairs of states that are bisimilar between two models. -Two pointed models are bisimilar if there exists a bisimulation such that (w,w') ∈ Z +Two pointed models are bisimilar if there exists a bisimulation Z 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 +## Example of a bisimulation It's a bit hard to describe this in words, but intuitive if you see it. -Here's an example: +Here's an example with two models:  @@ -32,7 +31,7 @@ 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 +## Example: finding bisimulations Take two example models: @@ -121,9 +120,12 @@ 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. +For finitely branching models, if two states are modally equivalent, then they are bisimilar. Prove by taking modal equivalence as bisimulation. +<details> +<summary>Proof of modal equivalence implying bisimilar</summary> + Let Z := {(x, x') | for all φ: x ⊨ φ iff x' ⊨ φ}. Z is a bisimulation. - Local harmony is satisfied. @@ -135,6 +137,7 @@ Z is a bisimulation. x ⊨ ◇(φ₁ ∧ ... ∧ φn) so also x' ⊨ ◇ (φ₁ ∧ ... ∧ φn). Contradiction. +</details> Asymmetry is not modally definable. To deal with only frames, we can use surjective bounded morphisms. @@ -147,14 +150,21 @@ A bounded morphism f is surjective if for every w' ∈ W' there exists w ∈ W s 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 +## 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 + +## A bisimulation game 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 m and 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) @@ -162,12 +172,7 @@ At current link m ~ n (with m in M and n in N): 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 +There's an example of this [in exercise class 3](../exercise-3/#a). We need a formula of model depth k to distinguish states x and y. Spoiler can win bisimulation game in k rounds. diff --git a/content/advanced-logic-notes/epistemic-logic.md b/content/advanced-logic-notes/epistemic-logic.md @@ -1,8 +1,7 @@ +++ title = 'Epistemic logic' +++ -# Lecture 13 -Epistemic logic: +# Epistemic logic - □ φ: 'we know that φ is true' (also written Kφ) - ◇ φ: 'we consider φ possible' - [i] φ: 'agent i knows that φ is true' (also written Kᵢφ) 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 @@ -1,7 +1,12 @@ +++ title = 'Formula validity using sequents and tableaux' +++ -# Lecture 6 +# Formula validity using sequents and tableaux +Sequents and tableaux are two ways to determine validity of formulas. +Tableaux also conveniently provide a countermodel if a formula is not valid. + +Some examples in [exercise class 3](../exercise-3/#sequents-and-tableaux-exercise-5). + ## Sequents φ₁...φn ⇒ ψ₁...ψm valid if in every model, in every world in that model, the conjunction of the φᵢ implies the disjunction of the ψᵢ. @@ -44,7 +49,7 @@ In modal logic:  -Example: +### Example  diff --git a/content/advanced-logic-notes/semantics-truth-and-validity-game-semantics-for-formula-validity/example-characterizing.png b/content/advanced-logic-notes/intro-to-modal-logic-operators-frames-models-tautologies/example-characterizing.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 @@ -2,52 +2,59 @@ 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 +# Intro to Modal Logic (operators, frames, models, tautologies) +## 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. +i.e., it tells you what variables are true. 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 ⟦φ⟧ᵥ = 1 (i.e. φ is true in v), we write v ⊨ φ (read "v models φ"). +- then also: φ has a model, namely the model with state _v_, 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) +If v ⊨ φ for all valuations of v, then universally ⊨ φ (φ is a tautology) -Soundness: ⊢ implies ⊨ -- what we can derive is true. proved by induction on length of proof +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 +Completeness: ⊨ implies ⊢ ("what is true can be derived"). can be proven using consistency -# Basic modal logic -E.g. "whatever is necessary is possible" == □φ → ◇φ +## Basic modal logic +Basic model logic operators: +- □: necessary, known, provable +- ◇: possible, considered possible -□ can also mean "I know", e.g. "I know that someone appreciates me" == ∃x.□A(x, M) +In a diagram, one of these symbols is exactly one transition step (use multiple for multiple steps). + +- ◇ φ ⇔ ¬□ ¬φ +- □ φ ⇔ ¬◇ ¬φ + +Examples in natural language: +- "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 +Truth is relative to current situation/world/environment: +- formulas evaluated in given structure (i.e. world, model, frame, or universally) - necessity (□): truth in all accessible worlds. if there are no accessible worlds, it's true. + - □ T: holds always + - □ ⊥: holds in blind states (those without a successor) - possibility (◇): truth in some accessible world (at least one). if there are no accessible worlds, it's false. + - ◇ ⊥: never holds (can never do a step to a state where ⊥ holds) + - ◇ T: holds in states with a successor + +Dualities: +- ◇ φ ≡ ¬ □ ¬ φ +- □ φ ≡ ¬ ◇ ¬ φ ## Frames A situation is set by a frame F = (W,R) @@ -63,14 +70,28 @@ 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 + - possible notation: + - V : Var → P(W) means Var → W → {0,1} + - V(p,w) = 1 is the same as w ∈ V(p) + -pointed model: pair (M,w) of model M and w a world in M +pointed model: pair (M,w) of model M and w a world in M (i.e. you zoom in to a specific state in M)  -◇T holds if at least one successor. -□⊥ holds if there is no successor. -Dualities: -- ◇ φ := ¬ □ ¬ φ -- □ φ := ¬ ◇ ¬ φ +## Distinguishing and characterizing states +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. + +<details> +<summary>Example</summary> + + + +Above: +- the formula 3 ⊨ □ ⊥ characterizes state 3 +- the formula 2 ⊨ ◇ □ ⊥ characterizes state 2 + +</details> 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 @@ -2,15 +2,13 @@ title = 'Model transformations (tree unravelling, bisimulation contraction)' template = 'page-math.html' +++ -# Lecture 5 -## Transforming and constructing models +# 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 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}$ @@ -69,17 +67,18 @@ g [label="..."]; e -> g </tr> </table> -If two trees have the same structure, they're bisimilar. +If two trees have the same structure, the models are bisimilar. -#### Model contraction +## 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. +See in this diagram, model on the left and contraction on the right:  -### Validity and satisfiability +## 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/multi-modal-logic/index.md b/content/advanced-logic-notes/multi-modal-logic/index.md @@ -1,8 +1,7 @@ +++ title = 'Multi-modal logic' +++ -# Lecture 10 -## Multi-modal logic +# 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. @@ -11,14 +10,14 @@ Rᵢ ⊆ W × W for every i ⊆ I. I-model is triple (W, {Rᵢ | i ⊆ I}, V). -### Truth and validity +## 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 +## 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. @@ -41,7 +40,7 @@ rankdir=LR 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 +## 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/proof-systems-and-derivation/index.md b/content/advanced-logic-notes/proof-systems-and-derivation/index.md @@ -1,11 +1,7 @@ +++ title = 'Proof systems and derivation' +++ -# Lecture 8 -## Modal tautologies - - - +# Proof systems and derivation ## Proof systems Hilbert systems: - proof is sequence of numbered formulas @@ -24,8 +20,7 @@ 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 +Soundness and completeness results (**note:** the frame classes _do_ need to be memorized) - K sound and complete for all frames - T sound and complete for all _reflexive_ frames - T: K with □ p → p @@ -40,14 +35,14 @@ Same as example in book <abbr title='Modal Logic for Open Minds (Benthem)'>MLOM< First, work backwards from the goal towards an axiom or tautology: -``` +<pre> ◇ φ ∧ □ (φ → ψ) → ◇ ψ ≡ □ (φ → ψ) → (◇ φ → ◇ ψ) [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)] -``` +</pre> We arrive at a tautology. diff --git a/content/advanced-logic-notes/proof-systems-and-derivation/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/propositional-dynamic-logic-pdl/index.md b/content/advanced-logic-notes/propositional-dynamic-logic-pdl/index.md @@ -2,7 +2,7 @@ title = 'Propositional dynamic logic (PDL)' template = 'page-math.html' +++ -# Lecture 11 +# Propositional dynamic logic (PDL) 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. 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 @@ -2,22 +2,7 @@ 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 - +# Semantics: truth and validity, game semantics for formula validity ## Game semantics This is an approach to determine if a formula φ holds in a pointed model M, w. @@ -43,9 +28,12 @@ Who starts: 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 +To determine validity: φ is true in M in s ⇔ V has a winning strategy for M,s,φ. + +<details> +<summary>Example: complete game tree</summary> + Diagram:  @@ -69,7 +57,7 @@ digraph states { </details> Given: -- formula ◇ p ∨ □ ◇ p, in state 2. +- question: formula ◇ p ∨ □ ◇ p, is it valid in state 2? - p is true in state 3. Complete game tree: @@ -105,20 +93,26 @@ digraph gametree { ``` </details> +</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. +There are different levels of validity: +- (((W,R),V),w) ⊨ φ means φ is valid in a state/world w. +- (W,R) ⊨ φ means φ is valid in a frame (W,R). +- ⊨ φ means φ is valid universally (a 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 +φ and ψ _semantically equivalent_ if they're only valid in the same worlds, i.e. ∀ M,w: M,w ⊨ φ ⇔ M,w ⊨ ψ + +<details> +<summary>Example: showing universal validity</summary> + Show universal validity of □ (φ → ψ) → (□ φ → □ ψ) 1. let F = (W,R) be frame, V valuation on F, let x ∈ W. @@ -132,17 +126,17 @@ Show universal validity of □ (φ → ψ) → (□ φ → □ ψ) 9. From a1, have have y ⊨ ψ. 10. Hence x ⊨ □ ψ, hence x ⊨ □ φ → □ ψ. Hence formula is valid. +</details> + ## 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}$ +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 σ. +But validity in a _frame_ is preserved 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. @@ -159,20 +153,17 @@ 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}$ +- ⊨ □ (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 ⊨ φ. +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 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 @@ -1,8 +1,7 @@ +++ title = 'Standard translation: mapping basic modal logic to first-order predicate logic' +++ -# Lecture 7 -## Standard translation +# Standard translation: mapping basic modal logic to first-order predicate logic 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* @@ -26,28 +25,3 @@ 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/temporal-logic/index.md b/content/advanced-logic-notes/temporal-logic/index.md @@ -1,8 +1,7 @@ +++ title = 'Temporal logic' +++ -# Lecture 9 -## Temporal logic using temporal frames +# 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' diff --git a/content/advanced-logic-notes/the-finite-model-property.md b/content/advanced-logic-notes/the-finite-model-property.md @@ -0,0 +1,27 @@ ++++ +title = 'Finite model property' ++++ +# 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] ⊨ φ + +
