definability-and-undefinability-results.html (4207B)
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>definability-and-undefinability-results</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="Definability and Undefinability results"><h2 id="Definability and Undefinability results" class="header"><a href="#Definability and Undefinability results">Definability and Undefinability results</a></h2></div> 36 <p> 37 expressible frame properties in predicate/modal logic: 38 </p> 39 40 <p> 41 <img src="img/expressible-frame-properties.png" alt="Expressible frame properties" /> 42 </p> 43 44 <div id="Definability and Undefinability results-for model cardinality"><h3 id="for model cardinality" class="header"><a href="#Definability and Undefinability results-for model cardinality">for model cardinality</a></h3></div> 45 <p> 46 model cardinality: 47 </p> 48 49 <p> 50 <img src="img/model-cardinality-definition.png" alt="Model cardinality definition" /> 51 </p> 52 53 54 <p> 55 for all models M and all n ≥ 2 it holds that: 56 </p> 57 <ul> 58 <li> 59 M ⊨ Φn ⇔ A has at least n elements 60 61 <li> 62 M ⊨ ψn ⇔ A has at most n elements 63 64 <li> 65 M ⊨ Φn ∧ ψn ⇔ A has precisely n elements 66 67 </ul> 68 69 <p> 70 model infiniteness is definable by a set of formulas Δ: 71 </p> 72 <ul> 73 <li> 74 M ⊨ Δ ⇔ M has an infinite domain 75 76 </ul> 77 78 <p> 79 model finiteness is undefinable (single formula): 80 </p> 81 <ul> 82 <li> 83 there's no sentence ψ such that 84 85 <li> 86 all M: M ⊨ ψ ⇔ M has a finite domain 87 88 </ul> 89 90 <p> 91 model finiteness is undefinable (set of formulas): 92 </p> 93 <ul> 94 <li> 95 there's no set of formulas Γ such that 96 97 <li> 98 all M: M ⊨ Γ ⇔ M has a finite domain 99 100 </ul> 101 102 <p> 103 mode infiniteness is undefinable (single formula) 104 </p> 105 <ul> 106 <li> 107 there's no sentence ψ such that 108 109 <li> 110 all M: M ⊨ ψ ⇔ M has infinite domain 111 112 </ul> 113 114 <div id="Definability and Undefinability results-for reachability"><h3 id="for reachability" class="header"><a href="#Definability and Undefinability results-for reachability">for reachability</a></h3></div> 115 <p> 116 "v is reachable via R from u". thinking of R as arrows, it means that there's a path from v to u. 117 </p> 118 119 <p> 120 search for formulas χn that express reachability in n steps: 121 </p> 122 123 <p> 124 Reachable in n steps: 125 </p> 126 <ol> 127 <li> 128 u = v 129 130 <li> 131 R(u,v) 132 133 <li> 134 ∃x₁ (RU, x₁) ∧ R(x₁, v)) 135 136 <li> 137 ∃x₁ ∃x₂ (R(u, x₁) ∧ R(x₁, x₂) ∧ R(x₂, v)) 138 139 <li> 140 .... 141 142 </ol> 143 144 <p> 145 shorthand: χ₂(c,d) denotes formula ∃x₁ (R(c, x₁) ∧ R(x₁, d)) 146 </p> 147 148 <p> 149 <img src="img/theorem-for-reachability.png" alt="Theorem for reachability" /> 150 </p> 151 152 <p> 153 reachability is undefinable: 154 </p> 155 156 <p> 157 <img src="img/reachability-is-undefinable.png" alt="Reachability is undefinable" /> 158 </p> 159 160 161 <p> 162 Let R be a binary relation symbol. 163 </p> 164 <ol> 165 <li> 166 In predicate logic, reachability by R-steps is 167 168 <ul> 169 <li> 170 not definable by a sentence 171 172 <li> 173 not definable by a set of sentences 174 175 </ul> 176 <li> 177 In predicate logic, unreachability by R-steps is 178 179 <ul> 180 <li> 181 not definable by a single sentence 182 183 <li> 184 definable by a set of sentences 185 186 </ul> 187 </ol> 188 189 <div id="Definability and Undefinability results-General overview"><h3 id="General overview" class="header"><a href="#Definability and Undefinability results-General overview">General overview</a></h3></div> 190 <p> 191 <img src="img/undefinability-results-overview.png" alt="Undefinability results overview" /> 192 </p> 193 194 </div> 195 </body> 196 </html>