decidability-and-undecidability.html (5627B)
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>decidability-and-undecidability</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="Decidability and Undecidability"><h2 id="Decidability and Undecidability" class="header"><a href="#Decidability and Undecidability">Decidability and Undecidability</a></h2></div> 36 <div id="Decidability and Undecidability-Decision problems"><h3 id="Decision problems" class="header"><a href="#Decidability and Undecidability-Decision problems">Decision problems</a></h3></div> 37 <p> 38 Decision problem consists of set I and a predicate Y ⊆ I 39 </p> 40 41 <p> 42 Examples: 43 </p> 44 <ul> 45 <li> 46 determine whether a number is prime: 47 48 <ul> 49 <li> 50 input: natural number n 51 52 <ul> 53 <li> 54 I = N 55 56 </ul> 57 <li> 58 output: yes if n is prime, no otherwise 59 60 <ul> 61 <li> 62 Y = { n ∈ N | n is prime } 63 64 </ul> 65 </ul> 66 <li> 67 termination problem (whether a program terminates): 68 69 <ul> 70 <li> 71 input: program P, input w 72 73 <ul> 74 <li> 75 I = set of all pairs <program, input> 76 77 </ul> 78 <li> 79 output: yes if P started with input w terminates, no otherwise 80 81 <ul> 82 <li> 83 Y = { <P, w> | P terminates on input w } 84 85 </ul> 86 </ul> 87 <li> 88 validity problem (determine whether a formula is valid): 89 90 <ul> 91 <li> 92 input: formula Φ of predicate logic 93 94 <ul> 95 <li> 96 I = set of formulas of predicate logic 97 98 </ul> 99 <li> 100 output: yes if Φ is valid, no otherwise 101 102 <ul> 103 <li> 104 Y = set of valid formulas in predicate logic 105 106 </ul> 107 </ul> 108 </ul> 109 110 <p> 111 A decision problem Y ⊆ I is decidable if there is a program that tells for every i ∈ I whether i ∈ Y. 112 </p> 113 114 <div id="Decidability and Undecidability-Decision problems-Termination problem"><h4 id="Termination problem" class="header"><a href="#Decidability and Undecidability-Decision problems-Termination problem">Termination problem</a></h4></div> 115 <p> 116 This problem is undecidable. 117 </p> 118 119 <p> 120 steps: 121 </p> 122 <ul> 123 <li> 124 T outputs yes on input <P, w> ⇔ P halts on input w 125 126 <li> 127 Tself outputs yes on input P ⇔ P halts on input P 128 129 <li> 130 Z halts on input P ⇔ P does not halt on input P 131 132 <li> 133 Z halts on input Z ⇔ Z does not halt on input Z 134 135 <li> 136 contradiction. 137 138 </ul> 139 140 <div id="Decidability and Undecidability-Decision problems-Post's Correspondence Problem"><h4 id="Post's Correspondence Problem" class="header"><a href="#Decidability and Undecidability-Decision problems-Post's Correspondence Problem">Post's Correspondence Problem</a></h4></div> 141 <p> 142 Given n pairs of words: <w1, v1> , ..., <wn, vn> 143 </p> 144 145 <p> 146 are there indices \(i_1, i_2, ..., i_k\) (k ≥ 1) s.t. when concatenated, \(wi_1 wi_2 ... wi_k = vi_1 vi_2 ... vi_k \)? 147 </p> 148 149 <p> 150 as a decision problem: 151 </p> 152 <ul> 153 <li> 154 \(PCP = \{ < <w_1, v_1>, ..., <w_k, v_k> > | k ≥ 1, w_i, v_i \; \text{binary words} \}\) 155 156 <li> 157 Y = { i ∈ PCP | i has a solution } 158 159 </ul> 160 161 <p> 162 it's undecidable. 163 </p> 164 165 <p> 166 the termination problem can be reduced to PCP -- there is a computable function r that maps instances of termination problem to instances of PCP such that it holds: \(P\text{ terminates on input w} \iff I_{<P, w>}\text{ has a solution}\) 167 </p> 168 169 <p> 170 the validity problem in predicate logic is undecidable (no program that, given formula Φ, decides whether or not ⊨ Φ holds). PCP can be reduced to validity problem: 171 </p> 172 <ul> 173 <li> 174 I (instance of PCP) has a solution ⇔ ⊨ ΦI (instance of validity problem is valid) 175 176 </ul> 177 178 <p> 179 Then if we had program deciding validity for predicate logic, we would obtain PCP-solver. Not gonna work. 180 </p> 181 182 <div id="Decidability and Undecidability-Undecidability of Validity and Provability"><h3 id="Undecidability of Validity and Provability" class="header"><a href="#Decidability and Undecidability-Undecidability of Validity and Provability">Undecidability of Validity and Provability</a></h3></div> 183 <p> 184 The validity problem in predicate logic is undecidable. 185 There cannot be a program that, given any formula Φ, decides whether or not ⊨Φ holds. 186 </p> 187 188 <p> 189 The provability in predicate logic is undecidable. 190 There cannot be a program that, given any formula Φ, decides whether or not ⊢ Φ holds. 191 This follows from soundness and completeness theorem. 192 </p> 193 194 <div id="Decidability and Undecidability-Undecidability of Satisfiability"><h3 id="Undecidability of Satisfiability" class="header"><a href="#Decidability and Undecidability-Undecidability of Satisfiability">Undecidability of Satisfiability</a></h3></div> 195 <p> 196 for sentences Φ it holds: 197 </p> 198 <ul> 199 <li> 200 Φ is unsatisfiable ⇔ ¬ Φ is valid 201 202 <li> 203 Φ is satisfiable ⇔ ¬ Φ is not valid 204 205 </ul> 206 207 <p> 208 there's an easy reduction of validity problem to satisfiability problem. 209 </p> 210 211 <p> 212 The relations ⊨ and ⊢ in predicate logic are undecidable. 213 </p> 214 215 </div> 216 </body> 217 </html>