The one-page cheat sheet.md (2048B)
1 +++ 2 title = 'One-page cheat sheet' 3 +++ 4 # One-page cheat sheet 5 ## Definitions 6 * Model is: 7 * set A - domain 8 * interpretation operation for predicate and function symbols 9 * satisfiable: some model & environment where it's true 10 * valid: true in all models and environments 11 * derivable: can be proven without global hypothesis 12 * tautology: true under any truth assignment (valid) 13 * soundness: ⊢ A → ⊨ A (from syntax to semantics) 14 * completeness: ⊨ A → ⊢ A (from semantics to syntax) 15 * partial order: antisymmetric, reflexive, transitive 16 * memo technique -- p**art**ial means **a**ntisymmetric, **r**eflexive, **t**ransitive 17 * strict means irreflexive 18 * total order: partial order & ∀ ab: R(a,b) ∨ R(b,a) 19 * strict: ∀ ab: R(a,b) ∨ a = b ∨ R(b,a) 20 * equivalence relation: has all three properties in the positive (symmetric, reflexive, transitive) 21 22 environment is used to interpret free variables 23 ## Modal logic 24 * □ Φ: true in world if true in all related worlds (if no related, true). 25 * ◇ Φ: true in world if true in some related world (if no related, false). 26 27 M,w ⊩ Φ: Φ true in world w of Kripke model M (true in model if true in every world) 28 29 Φ valid in frame if true with every labelling. 30 31 frame = Kripke - labels 32 33 ## Metatheorems 34 * consistent: has a model 35 * syntactically consistent: can't derive ⊥ 36 * compactness: if Γ is consistent, every finite subset of Γ is also consistent 37 38 ## Definability 39 Model finiteness is undefinable. 40 41 Model infiniteness is definable by a set of formulas. 42 43 In predicate logic, only unreachability by n steps is definable, and only by a set of sentences. 44 45 ## Decidability 46 Y ⊆ I decidable if program can tell for every i ∈ I whether i ∈ Y. I set, Y predicate on set. 47 48 Undecidable: termination, PCP, validity, provability, satisfiability. 49 50 Termination can be reduced to PCP, which can be reduced to validity. 51 52 Incompleteness theorems: every non-trivial formal system is 53 * either incomplete (valid but not derivable) 54 * or inconsistent (doesn't have a model, or entails ⊥) 55