Title: Logic & Modelling

Q: satisfiable
A: true in some model and environment

Q: valid
A: true in all models and environments

Q: derivable
A: can be proven without a global hypothesis

Q: tautology
A: true under any truth assignment

Q: soundness
A: |- A -> |= A

Q: completeness
A: |= A -> |- A

Q: partial order
A: antisymmetric, reflexive, transitive

Q: strict partial order
A: partial order but irreflexive

Q: total order
A: partial order & all ab: R(a,b) v R(b,a)

Q: strict total order
A: total order & all ab: R(a,b) v a = b v R(b,a)

Q: equivalence relation
A: symmetric, reflexive, transitive

Q: box A
A: A true in world if true in all related worlds. if none, true.

Q: diamond A
A: A true in world if true in some related world. if none, false

Q: M,w ||- A
A: A true in world w of Kripke model M

Q: A valid in [...] if [...]
A: frame; true with every labelling

Q: consistent
A: has a model

Q: syntactically consistent
A: can't derive false

Compactness: if G is consistent, every finite subset of G is also consistent

Q: Model
A: set A domain, interpretation operation for predicate and function symbols

Q: [...] is used to [...]
A: Environment; interpret free variables

Q: Model finiteness is [...].
A: undefinable

Q: Model [...] is definable by [...].
A: infiniteness; a set of formulas

Q: In predicate logic reachability, only [...] is [...], and only by [...].
A: unreachability by n steps; definable; a set of sentences

Q: Decision problem: \(Y \subseteq I\) [...] if program can tell for every [...] whether [...].
A: decidable; i in I; i in Y

Q: Decision problem \(Y \subseteq I\): I is the [...], Y is [...].
A: input set; predicate on set

Q: [...] can be reduced to [...], which can be reduced to [...].
A: Termination; PCP; validity

Q: Undecidable problems
A: Termination, PCP, validity, provability, satisfiability.

Q: [...]: every non-trivial formal system is either [...] or [...].
A: Incompleteness theorems; incomplete; inconsistent