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