definability-and-undefinability-results.wiki (2041B)
1 %template math 2 == Definability and Undefinability results == 3 expressible frame properties in predicate/modal logic: 4 5 {{local:../img/expressible-frame-properties.png|Expressible frame properties}} 6 7 === for model cardinality === 8 model cardinality: 9 10 {{local:../img/model-cardinality-definition.png|Model cardinality definition}} 11 12 13 for all models M and all n ≥ 2 it holds that: 14 * M ⊨ Φn ⇔ A has at least n elements 15 * M ⊨ ψn ⇔ A has at most n elements 16 * M ⊨ Φn ∧ ψn ⇔ A has precisely n elements 17 18 model infiniteness is definable by a set of formulas Δ: 19 * M ⊨ Δ ⇔ M has an infinite domain 20 21 model finiteness is undefinable (single formula): 22 * there's no sentence ψ such that 23 * all M: M ⊨ ψ ⇔ M has a finite domain 24 25 model finiteness is undefinable (set of formulas): 26 * there's no set of formulas Γ such that 27 * all M: M ⊨ Γ ⇔ M has a finite domain 28 29 mode infiniteness is undefinable (single formula) 30 * there's no sentence ψ such that 31 * all M: M ⊨ ψ ⇔ M has infinite domain 32 33 === for reachability === 34 "v is reachable via R from u". thinking of R as arrows, it means that there's a path from v to u. 35 36 search for formulas χn that express reachability in n steps: 37 38 Reachable in n steps: 39 1. u = v 40 2. R(u,v) 41 3. ∃x₁ (RU, x₁) ∧ R(x₁, v)) 42 4. ∃x₁ ∃x₂ (R(u, x₁) ∧ R(x₁, x₂) ∧ R(x₂, v)) 43 5. .... 44 45 shorthand: χ₂(c,d) denotes formula ∃x₁ (R(c, x₁) ∧ R(x₁, d)) 46 47 {{local:../img/theorem-for-reachability.png|Theorem for reachability}} 48 49 reachability is undefinable: 50 51 {{local:../img/reachability-is-undefinable.png|Reachability is undefinable}} 52 53 54 Let R be a binary relation symbol. 55 1. In predicate logic, reachability by R-steps is 56 * not definable by a sentence 57 * not definable by a set of sentences 58 2. In predicate logic, unreachability by R-steps is 59 * not definable by a single sentence 60 * definable by a set of sentences 61 62 === General overview === 63 {{local:../img/undefinability-results-overview.png|Undefinability results overview}} 64