index.md (6662B)
1 +++ 2 template = 'page-math.html' 3 title = 'First order logic' 4 +++ 5 # First order logic 6 ## Functions, predicates, relations 7 functions: take different numbers of arguments, returns a result. e.g. $mul(x,y)$, $square(x)$ 8 9 predicates, relations: takes one or more arguments, is either true or false. e.g. $even(x)$, $divides(x,y)$ 10 11 formulas: say things. make assertions about objects in the domain. 12 13 ## Quantifiers, binding 14 Quantifiers: 15 * ∀x: "for all x" 16 * ∃x: "there exists an x" 17 18 Generally bind tightly: ∀x P ∨ Q == (∀x P) ∨ Q 19 20 free variable: variable that's not bound 21 22 sentence: a formula that has no free variables 23 24 ### Natural deduction rules 25 26 <table> 27 <tr><td>Universal quantification</td><td>Existential quantification</td><td>Equality</td></tr> 28 <tr><td><img alt="Universal introduction" src="universal-introduction.png"></td><td><img alt="Existential introduction" src="existential-introduction.png"></td><td rowspan="2"><img alt="Equality rules" src="equality-rules.png"></td></tr> 29 <tr><td><img alt="Universal elimination" src="universal-elimination.png"></td><td><img alt="Existential elimination" src="existential-elimination.png"></td></td></tr> 30 </table> 31 32 33 ## Relativization and sorts 34 You can use implication to relativize quantification (put it into a specific domain). 35 36 Universal quantification, e.g. "every prime number greater than two is odd": 37 38 ∀x (prime(x) ∧ x > 2 → odd(x)) 39 40 Existential quantification, e.g. "some woman is strong": 41 42 ∃x (woman(x) ∧ strong(x)) 43 44 Remember to use ∧ with ∃, and not →. 45 46 ## Models 47 Let F be a set of function symbols, P a set of predicate symbols. 48 49 Model M for (F, P) consists of: 50 * non-empty set A ("domain", "universe") 51 * interpretation operation $(\cdot)^M$ for for symbols in F, P 52 53 Universe A can be any non-empty set. 54 55 only constraint: $F^M$ and $P^M$ have same number of arguments as F and P. 56 57 ## Interpreting formulas without quantifiers 58 Truth definition for formula Φ without quantifiers and free variables in model M by induction on the structure of Φ: 59 * M ⊨ ¬Φ ↔ not: M ⊨ Φ ↔ M ⊭ Φ 60 * M ⊨ Æ∧ Ψ ↔ M ⊨ Φ and M ⊨ Ψ 61 * M ⊨ Φ ∨ Ψ ↔ M ⊨ Φ or M ⊨ Ψ 62 * M ⊨ Φ → Ψ : if M ⊨ Φ then M ⊨ Ψ 63 * M ⊨ P(t₁, .., tn) ↔ ($t_1^M,\ldots,t_n^M) \in P^M$ 64 65 Interpretation of terms $t^M$: 66 * if t = c for constant c, then $t^M = c^M$ 67 * if $t = f(t_1,\ldots, t_n)$, then $t^M = f^M(t_1^M,\ldots,t_n^M)$ 68 69 ## Interpretation of formulas with quantifiers and free variables 70 to interpret free variables, you use an environment. 71 72 an environment `l: var → A` (look up function) interprets free variables in the domain 73 74 ## Interpreting terms in model with environment 75 terms are built from variables, constants, function symbols 76 * variables are interpreted according to environment 77 * constants are interpreted according to $(\cdot)^M$ 78 * function symbols are interpreted according to $(\cdot)^M$ 79 80 81 Truth of formula Φ in model M with universe A with respect to environment e is defined by induction on the structure of Φ. 82 83 Interpretation $t^{M,l}$ of term t is 84 85 $ 86 \begin{aligned} 87 t^{M, l} = \begin{cases} 88 l(x) &&\text{if } t = x \text{ for a variable } x \\\\ 89 c^M &&\text{if } t = c \text{ for a constant } c \\\\ 90 f^M (t_1^{M, l}, \ldots, t_n^{M, l}) &&\text{if } t = f(t_1, \ldots, t_n) 91 \end{cases} 92 \end{aligned} 93 $ 94 95 by induction on term structure. 96 97 M ⊨l ∀x HI ↔ for all a ∈ A it holds that $ M \models_{l [x \to a]} \phi $ 98 99 M ⊨l ∃x Φ ↔ for some a ∈ A it holds that $ M \models_{l [x \to a]} \phi $ 100 101 ## Semantical entailment in predicate logic 102 For all models M and all environments e, 103 such that M ⊨l Φ₁ and ... and M ⊨l Φn hold, 104 it also holds that M ⊨l ψ 105 106 ## Logical equivalence 107 Formulas φ and ψ are logically equivalent (φ ≡ ψ) if for all models M and environments l, M ⊨l φ ↔ M ⊨l ψ 108 109 i.e. φ and ψ are true in precisely the same models when interpreted with the same environments. 110 111 theorem: φ ≡ ψ ↔ φ ⊨ ψ and ψ ⊨ φ 112 113 ## Satisfiability, validity, consistency 114 Let φ be a formula, and Γ be a set of formulas. 115 116 φ is satisfiable iff there is _some_ model M and _some_ environment l such that M ⊨l φ 117 118 φ is valid iff M ⊨l φ holds for _all_ models M and _all_ environments l in which φ can be checked. 119 120 Γ is consistent/satisfiable iff there is _some_ model M and _some_ environment l such tat M ⊨l ψ for all ψ ∈ Γ 121 122 for all formulas φ, ψ: φ ≡ ψ means that φ ↔ ψ is valid 123 124 ## Translating into predicate logic 125 Example: "Marie and Jan are clever." 126 127 Specification and model used: 128 129 two predicates: 130 * CC(x): x is clever 131 * LL(x): x has learned logic 132 133 two constants: 134 * m: Marie 135 * j: Jan 136 137 model M: 138 * domain A = the set of all humans 139 * $C^M$ = { x ∈ A | x is clever } 140 * $LL^M$ = { x ∈ A | x has learned logic } 141 * $j^M $= Jan 142 * $m^M$ = Marie 143 144 Then: 145 * "Marie and Jan are clever": C(m) ∧ C(j) 146 * "Not everybody is clever": ¬∀x C(x) 147 * "Somebody has learned logic": ∃x LL(x) 148 * "Not everybody has learned logic, but Marie and Jan have": ¬∀x LL(x) ∧ LL(m) ∧ LL(j) 149 150 ∀ and →: 151 * ∀x(LL(x) → C(x)): "everyone who has learned logic is clever" 152 * not the same as ∀x LL(x) → ∀x C(x): "if everyone has learned logic, everyone is clever" 153 154 ∃ and ∧: 155 * ∃x(L(x) ∧ C(x)): "some logicians are clever" 156 * not the same as ∃x(L(x) → C(x)): "if someone is a logician, they are clever" 157 158 Formulas with free variables express properties and relations: 159 * no free variables: a sentence 160 * one free variable: a property 161 * two or more free variables: a relation 162 163 ## Rules for quantifiers and connectives 164 If you move a negation around ∀, it becomes ∃, and vice versa. 165 166 It also holds that: 167 * ∀x(φ ∧ ψ) ≡ ∀x φ ∧ ∀x ψ 168 * BUT in general doesn't hold for ∨ 169 * ∃x(φ ∨ ψ) ≡ ∃x φ ∨ ∃x ψ 170 * BUT in general doesn't hold for ∧ 171 172 In general, you can't move quantifiers through an implication. 173 174 Order of _repeated_ ∀ or ∃ doesn't matter. But if you have _both_ ∃ and ∀, the order is important. 175 176 ## Semantics of first order logic 177 Interpretation: specifying the meaning of a predicate symbol. 178 * unary predicate P: set of elements of domain D for which P is true. 179 * constant c: an element of domain D 180 * function f with arity n: function mapping n elements of domain D to another element of D 181 * relation R with arity n: set of n tuples of elements of domain D for which R is true 182 183 You can find the truth value of sentences intuitively. 184 185 Completeness: if formula A is logical consequence of set of sentences Γ, then A is provable from Γ. 186 187 Soundness: if A is provable from Γ then A is true in any model of Γ 188