decidability-and-undecidability.md (2900B)
1 +++ 2 template = 'page-math.html' 3 title = 'Decidability and Undecidability' 4 +++ 5 6 # Decidability and Undecidability 7 ## Decision problems 8 Decision problem consists of set I and a predicate Y ⊆ I 9 10 Examples: 11 * determine whether a number is prime: 12 * input: natural number n 13 * I = N 14 * output: yes if n is prime, no otherwise 15 * Y = { n ∈ N | n is prime } 16 * termination problem (whether a program terminates): 17 * input: program P, input w 18 * I = set of all pairs <program, input> 19 * output: yes if P started with input w terminates, no otherwise 20 * Y = { <P, w> | P terminates on input w } 21 * validity problem (determine whether a formula is valid): 22 * input: formula Φ of predicate logic 23 * I = set of formulas of predicate logic 24 * output: yes if Φ is valid, no otherwise 25 * Y = set of valid formulas in predicate logic 26 27 A decision problem Y ⊆ I is decidable if there is a program that tells for every i ∈ I whether i ∈ Y. 28 29 ### Termination problem 30 This problem is undecidable. 31 32 steps: 33 * T outputs yes on input <P, w> ⇔ P halts on input w 34 * Tself outputs yes on input P ⇔ P halts on input P 35 * Z halts on input P ⇔ P does not halt on input P 36 * Z halts on input Z ⇔ Z does not halt on input Z 37 * contradiction. 38 39 ### Post's Correspondence Problem 40 Given n pairs of words: <w1, v1> , ..., <wn, vn> 41 42 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 $? 43 44 as a decision problem: 45 * $PCP = \{ < <w_1, v_1>, ..., <w_k, v_k> > | k ≥ 1, w_i, v_i \; \text{binary words} \}$ 46 * Y = { i ∈ PCP | i has a solution } 47 48 it's undecidable. 49 50 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}$ 51 52 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: 53 * I (instance of PCP) has a solution ⇔ ⊨ ΦI (instance of validity problem is valid) 54 55 Then if we had program deciding validity for predicate logic, we would obtain PCP-solver. Not gonna work. 56 57 ## Undecidability of Validity and Provability 58 The validity problem in predicate logic is undecidable. 59 There cannot be a program that, given any formula Φ, decides whether or not ⊨Φ holds. 60 61 The provability in predicate logic is undecidable. 62 There cannot be a program that, given any formula Φ, decides whether or not ⊢ Φ holds. 63 This follows from soundness and completeness theorem. 64 65 ## Undecidability of Satisfiability 66 for sentences Φ it holds: 67 * Φ is unsatisfiable ⇔ ¬ Φ is valid 68 * Φ is satisfiable ⇔ ¬ Φ is not valid 69 70 there's an easy reduction of validity problem to satisfiability problem. 71 72 The relations ⊨ and ⊢ in predicate logic are undecidable. 73