the-finite-model-property.md (1084B)
1 +++ 2 title = 'Finite model property' 3 +++ 4 # Finite model property 5 If φ is satisfiable, then φ is satisfiable on a finite model. 6 7 Effective finite model property: if φ is satisfiable, then φ is satisfiable in a model of size ≤ f(φ) 8 9 Via selection: 10 - suppose there is a model that makes φ true 11 - unravel the model at x to a tree model 12 - φ has finite modal depth n, so restrict tree model to height n 13 - rewrite φ to a conjunction of first-order propositional logic formulas and diamonds 14 - take for every diamond formula a successor 15 16 Via filtration: 17 - suppose there is a model that makes φ true 18 - consider set S of all subformulas of φ 19 - define equivalence relation on S: u ~ v iff u and v are modally equivalent 20 - i.e., if they agree on letters/formulas 21 - define W' to consist of equivalence classes [u] of states from W 22 - define V' using u ∈ V(p) iff [u] ∈ V'(p) for every p in S 23 - define a R' using R'[u][v] if Ruv, and requiring: 24 - if R'[u][v] and ◇ ψ ∈ S and [v] ⊨ ψ, then [u] ⊨ ◇ φ 25 - then (W', R'), V' is finite and (W', R'), V', [x] ⊨ φ 26 27