first-order-logic.html (11526B)
1 <html> 2 <head> 3 <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/highlight.min.js"></script> 4 <script type="text/javascript" async src="https://cdn.jsdelivr.net/gh/mathjax/MathJax@2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script> 5 <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/styles/default.min.css"> 6 <link rel="Stylesheet" type="text/css" href="style.css" /> 7 <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> 8 <script> 9 document.addEventListener('DOMContentLoaded', function() { 10 document.querySelectorAll('pre.code').forEach(function(item) { 11 hljs.highlightBlock(item) 12 }) 13 }); 14 </script> 15 <title>first-order-logic</title> 16 </head> 17 <body> 18 <style type="text/css"> 19 nav a { 20 text-align: left; 21 } 22 nav #name { 23 text-align: right; 24 float: right; 25 font-style: italic; 26 } 27 </style> 28 <nav> 29 <a href="index.html">Index</a> 30 <span id="name">Alex Balgavy</span> 31 </nav> 32 <hr> 33 <div class="content"> 34 35 <div id="First order logic"><h2 id="First order logic" class="header"><a href="#First order logic">First order logic</a></h2></div> 36 <div id="First order logic-Functions, predicates, relations"><h3 id="Functions, predicates, relations" class="header"><a href="#First order logic-Functions, predicates, relations">Functions, predicates, relations</a></h3></div> 37 <p> 38 functions: take different numbers of arguments, returns a result. e.g. \(mul(x,y)\), \(square(x)\) 39 </p> 40 41 <p> 42 predicates, relations: takes one or more arguments, is either true or false. e.g. \(even(x)\), \(divides(x,y)\) 43 </p> 44 45 <p> 46 formulas: say things. make assertions about objects in the domain. 47 </p> 48 49 <div id="First order logic-Quantifiers, binding"><h3 id="Quantifiers, binding" class="header"><a href="#First order logic-Quantifiers, binding">Quantifiers, binding</a></h3></div> 50 <p> 51 Quantifiers: 52 </p> 53 <ul> 54 <li> 55 ∀x: "for all x" 56 57 <li> 58 ∃x: "there exists an x" 59 60 </ul> 61 62 <p> 63 Generally bind tightly: ∀x P ∨ Q == (∀x P) ∨ Q 64 </p> 65 66 <p> 67 free variable: variable that's not bound 68 </p> 69 70 <p> 71 sentence: a formula that has no free variables 72 </p> 73 74 <div id="First order logic-Quantifiers, binding-Natural deduction rules"><h4 id="Natural deduction rules" class="header"><a href="#First order logic-Quantifiers, binding-Natural deduction rules">Natural deduction rules</a></h4></div> 75 76 <table> 77 <tr> 78 <th> 79 Universal quantification 80 </th> 81 <th> 82 Existential quantification 83 </th> 84 <th> 85 Equality 86 </th> 87 </tr> 88 <tr> 89 <td> 90 <img src="img/universal-introduction.png" alt="Universal introduction" /> 91 </td> 92 <td> 93 <img src="img/existential-introduction.png" alt="Existential introduction" /> 94 </td> 95 <td rowspan="2"> 96 <img src="img/equality-rules.png" alt="Equality rules" /> 97 </td> 98 </tr> 99 <tr> 100 <td> 101 <img src="img/universal-elimination.png" alt="Universal elimination" /> 102 </td> 103 <td> 104 <img src="img/existential-elimination.png" alt="Existential elimination" /> 105 </td> 106 </tr> 107 </table> 108 109 110 <div id="First order logic-Relativization and sorts"><h3 id="Relativization and sorts" class="header"><a href="#First order logic-Relativization and sorts">Relativization and sorts</a></h3></div> 111 <p> 112 You can use implication to relativize quantification (put it into a specific domain). 113 </p> 114 115 <p> 116 Universal quantification, e.g. "every prime number greater than two is odd": 117 </p> 118 119 <p> 120 ∀x (prime(x) ∧ x > 2 → odd(x)) 121 </p> 122 123 <p> 124 Existential quantification, e.g. "some woman is strong": 125 </p> 126 127 <p> 128 ∃x (woman(x) ∧ strong(x)) 129 </p> 130 131 <p> 132 Remember to use ∧ with ∃, and not →. 133 </p> 134 135 <div id="First order logic-Models"><h3 id="Models" class="header"><a href="#First order logic-Models">Models</a></h3></div> 136 <p> 137 Let F be a set of function symbols, P a set of predicate symbols. 138 </p> 139 140 <p> 141 Model M for (F, P) consists of: 142 </p> 143 <ul> 144 <li> 145 non-empty set A ("domain", "universe") 146 147 <li> 148 interpretation operation \((\cdot)^M\) for for symbols in F, P 149 150 </ul> 151 152 <p> 153 Universe A can be any non-empty set. 154 </p> 155 156 <p> 157 only constraint: \(F^M\) and \(P^M\) have same number of arguments as F and P. 158 </p> 159 160 <div id="First order logic-Interpreting formulas without quantifiers"><h3 id="Interpreting formulas without quantifiers" class="header"><a href="#First order logic-Interpreting formulas without quantifiers">Interpreting formulas without quantifiers</a></h3></div> 161 <p> 162 Truth definition for formula Φ without quantifiers and free variables in model M by induction on the structure of Φ: 163 </p> 164 <ul> 165 <li> 166 M ⊨ ¬Φ ↔ not: M ⊨ Φ ↔ M ⊭ Φ 167 168 <li> 169 M ⊨ Æ∧ Ψ ↔ M ⊨ Φ and M ⊨ Ψ 170 171 <li> 172 M ⊨ Φ ∨ Ψ ↔ M ⊨ Φ or M ⊨ Ψ 173 174 <li> 175 M ⊨ Φ → Ψ : if M ⊨ Φ then M ⊨ Ψ 176 177 <li> 178 M ⊨ P(t₁, .., tn) ↔ (\(t_1^M,\ldots,t_n^M) \in P^M\) 179 180 </ul> 181 182 <p> 183 Interpretation of terms \(t^M\): 184 </p> 185 <ul> 186 <li> 187 if t = c for constant c, then \(t^M = c^M\) 188 189 <li> 190 if \(t = f(t_1,\ldots, t_n)\), then \(t^M = f^M(t_1^M,\ldots,t_n^M)\) 191 192 </ul> 193 194 <div id="First order logic-Interpretation of formulas with quantifiers and free variables"><h3 id="Interpretation of formulas with quantifiers and free variables" class="header"><a href="#First order logic-Interpretation of formulas with quantifiers and free variables">Interpretation of formulas with quantifiers and free variables</a></h3></div> 195 <p> 196 to interpret free variables, you use an environment. 197 </p> 198 199 <p> 200 an environment <code>l: var → A</code> (look up function) interprets free variables in the domain 201 </p> 202 203 <div id="First order logic-Interpreting terms in model with environment"><h3 id="Interpreting terms in model with environment" class="header"><a href="#First order logic-Interpreting terms in model with environment">Interpreting terms in model with environment</a></h3></div> 204 <p> 205 terms are built from variables, constants, function symbols 206 </p> 207 <ul> 208 <li> 209 variables are interpreted according to environment 210 211 <li> 212 constants are interpreted according to \((\cdot)^M\) 213 214 <li> 215 function symbols are interpreted according to \((\cdot)^M\) 216 217 </ul> 218 219 220 <p> 221 Truth of formula Φ in model M with universe A with respect to environment e is defined by induction on the structure of Φ. 222 </p> 223 224 <p> 225 Interpretation \(t^{M,l}\) of term t is 226 </p> 227 228 \begin{align} 229 t^{M, l} = \begin{cases} 230 l(x) &&\text{if } t = x \text{ for a variable } x \\ 231 c^M &&\text{if } t = c \text{ for a constant } c \\ 232 f^M (t_1^{M, l}, \ldots, t_n^{M, l}) &&\text{if } t = f(t_1, \ldots, t_n) 233 \end{cases} 234 \end{align} 235 <p> 236 by induction on term structure. 237 </p> 238 239 <p> 240 M ⊨l ∀x HI ↔ for all a ∈ A it holds that \( M \models_{l [x \to a]} \phi \) 241 </p> 242 243 <p> 244 M ⊨l ∃x Φ ↔ for some a ∈ A it holds that \( M \models_{l [x \to a]} \phi \) 245 </p> 246 247 <div id="First order logic-Semantical entailment in predicate logic"><h3 id="Semantical entailment in predicate logic" class="header"><a href="#First order logic-Semantical entailment in predicate logic">Semantical entailment in predicate logic</a></h3></div> 248 <p> 249 For all models M and all environments e, 250 such that M ⊨l Φ₁ and ... and M ⊨l Φn hold, 251 it also holds that M ⊨l ψ 252 </p> 253 254 <div id="First order logic-Logical equivalence"><h3 id="Logical equivalence" class="header"><a href="#First order logic-Logical equivalence">Logical equivalence</a></h3></div> 255 <p> 256 Formulas φ and ψ are logically equivalent (φ ≡ ψ) if for all models M and environments l, M ⊨l φ ↔ M ⊨l ψ 257 </p> 258 259 <p> 260 i.e. φ and ψ are true in precisely the same models when interpreted with the same environments. 261 </p> 262 263 <p> 264 theorem: φ ≡ ψ ↔ φ ⊨ ψ and ψ ⊨ φ 265 </p> 266 267 <div id="First order logic-Satisfiability, validity, consistency"><h3 id="Satisfiability, validity, consistency" class="header"><a href="#First order logic-Satisfiability, validity, consistency">Satisfiability, validity, consistency</a></h3></div> 268 <p> 269 Let φ be a formula, and Γ be a set of formulas. 270 </p> 271 272 <p> 273 φ is satisfiable iff there is <em>some</em> model M and <em>some</em> environment l such that M ⊨l φ 274 </p> 275 276 <p> 277 φ is valid iff M ⊨l φ holds for <em>all</em> models M and <em>all</em> environments l in which φ can be checked. 278 </p> 279 280 <p> 281 Γ is consistent/satisfiable iff there is <em>some</em> model M and <em>some</em> environment l such tat M ⊨l ψ for all ψ ∈ Γ 282 </p> 283 284 <p> 285 for all formulas φ, ψ: φ ≡ ψ means that φ ↔ ψ is valid 286 </p> 287 288 <div id="First order logic-Translating into predicate logic"><h3 id="Translating into predicate logic" class="header"><a href="#First order logic-Translating into predicate logic">Translating into predicate logic</a></h3></div> 289 <p> 290 Example: "Marie and Jan are clever." 291 </p> 292 293 <p> 294 Specification and model used: 295 </p> 296 297 <p> 298 two predicates: 299 </p> 300 <ul> 301 <li> 302 CC(x): x is clever 303 304 <li> 305 LL(x): x has learned logic 306 307 </ul> 308 309 <p> 310 two constants: 311 </p> 312 <ul> 313 <li> 314 m: Marie 315 316 <li> 317 j: Jan 318 319 </ul> 320 321 <p> 322 model M: 323 </p> 324 <ul> 325 <li> 326 domain A = the set of all humans 327 328 <li> 329 \(C^M\) = { x ∈ A | x is clever } 330 331 <li> 332 \(LL^M\) = { x ∈ A | x has learned logic } 333 334 <li> 335 \(j^M \)= Jan 336 337 <li> 338 \(m^M\) = Marie 339 340 </ul> 341 342 <p> 343 Then: 344 </p> 345 <ul> 346 <li> 347 "Marie and Jan are clever": C(m) ∧ C(j) 348 349 <li> 350 "Not everybody is clever": ¬∀x C(x) 351 352 <li> 353 "Somebody has learned logic": ∃x LL(x) 354 355 <li> 356 "Not everybody has learned logic, but Marie and Jan have": ¬∀x LL(x) ∧ LL(m) ∧ LL(j) 357 358 </ul> 359 360 <p> 361 ∀ and →: 362 </p> 363 <ul> 364 <li> 365 ∀x(LL(x) → C(x)): "everyone who has learned logic is clever" 366 367 <li> 368 not the same as ∀x LL(x) → ∀x C(x): "if everyone has learned logic, everyone is clever" 369 370 </ul> 371 372 <p> 373 ∃ and ∧: 374 </p> 375 <ul> 376 <li> 377 ∃x(L(x) ∧ C(x)): "some logicians are clever" 378 379 <li> 380 not the same as ∃x(L(x) → C(x)): "if someone is a logician, they are clever" 381 382 </ul> 383 384 <p> 385 Formulas with free variables express properties and relations: 386 </p> 387 <ul> 388 <li> 389 no free variables: a sentence 390 391 <li> 392 one free variable: a property 393 394 <li> 395 two or more free variables: a relation 396 397 </ul> 398 399 <div id="First order logic-Rules for quantifiers and connectives"><h3 id="Rules for quantifiers and connectives" class="header"><a href="#First order logic-Rules for quantifiers and connectives">Rules for quantifiers and connectives</a></h3></div> 400 <p> 401 If you move a negation around ∀, it becomes ∃, and vice versa. 402 </p> 403 404 <p> 405 It also holds that: 406 </p> 407 <ul> 408 <li> 409 ∀x(φ ∧ ψ) ≡ ∀x φ ∧ ∀x ψ 410 411 <ul> 412 <li> 413 BUT in general doesn't hold for ∨ 414 415 </ul> 416 <li> 417 ∃x(φ ∨ ψ) ≡ ∃x φ ∨ ∃x ψ 418 419 <ul> 420 <li> 421 BUT in general doesn't hold for ∧ 422 423 </ul> 424 </ul> 425 426 <p> 427 In general, you can't move quantifiers through an implication. 428 </p> 429 430 <p> 431 Order of <em>repeated</em> ∀ or ∃ doesn't matter. But if you have <em>both</em> ∃ and ∀, the order is important. 432 </p> 433 434 <div id="First order logic-Semantics of first order logic"><h3 id="Semantics of first order logic" class="header"><a href="#First order logic-Semantics of first order logic">Semantics of first order logic</a></h3></div> 435 <p> 436 Interpretation: specifying the meaning of a predicate symbol. 437 </p> 438 <ul> 439 <li> 440 unary predicate P: set of elements of domain D for which P is true. 441 442 <li> 443 constant c: an element of domain D 444 445 <li> 446 function f with arity n: function mapping n elements of domain D to another element of D 447 448 <li> 449 relation R with arity n: set of n tuples of elements of domain D for which R is true 450 451 </ul> 452 453 <p> 454 You can find the truth value of sentences intuitively. 455 </p> 456 457 <p> 458 Completeness: if formula A is logical consequence of set of sentences Γ, then A is provable from Γ. 459 </p> 460 461 <p> 462 Soundness: if A is provable from Γ then A is true in any model of Γ 463 </p> 464 465 </div> 466 </body> 467 </html>