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