Rice's theorem for acceptable numberings

TheoremRogers's fixed-point theorem for acceptable numberings#✓fully proved

Let \(\varphi\) assign to each natural number \(e\) a partial function \(\varphi_e : \mathbb{N} \rightharpoonup \mathbb{N}\), and suppose that the universal function \((e, n) \mapsto \varphi_e(n)\) is partial computable, that every partial computable function \(f : \mathbb{N} \rightharpoonup \mathbb{N}\) equals \(\varphi_e\) for some \(e\), and that for every partial computable \(g : \mathbb{N} \times \mathbb{N} \rightharpoonup \mathbb{N}\) there is a total computable \(s : \mathbb{N} \to \mathbb{N}\) with \(\varphi_{s(e)}(n) = g(e, n)\) for all \(e\) and \(n\). Then for every total computable \(h : \mathbb{N} \to \mathbb{N}\) there is an \(e\) with \(\varphi_e(n) = \varphi_{h(e)}(n)\) for all \(n\).

theorem acceptableNumbering_fixed_point (φ : ℕ → ℕ →. ℕ)
    (huniv : Nat.Partrec (fun p => φ (Nat.unpair p).1 (Nat.unpair p).2))
    (hidx : ∀ f : ℕ →. ℕ, Nat.Partrec f → ∃ e, ∀ n, φ e n = f n)
    (hsmn : ∀ g : ℕ → ℕ →. ℕ,
      Nat.Partrec (fun p => g (Nat.unpair p).1 (Nat.unpair p).2) →
      ∃ s : ℕ → ℕ, Nat.Partrec (fun n => Part.some (s n)) ∧
        ∀ e n, φ (s e) n = g e n)
    {h : ℕ → ℕ} (hh : Computable h) : ∃ e, ∀ n, φ e n = φ (h e) n

Used by 1

Used byRice's theorem for acceptable numberings

TheoremRice's theorem for acceptable numberings#✓fully proved

Let \(\varphi\) assign to each natural number \(e\) a partial function \(\varphi_e : \mathbb{N} \rightharpoonup \mathbb{N}\), and suppose that every \(\varphi_e\) is partial computable, that the universal function \((e, n) \mapsto \varphi_e(n)\) is partial computable, that every partial computable function \(f : \mathbb{N} \rightharpoonup \mathbb{N}\) equals \(\varphi_e\) for some \(e\), and that for every partial computable \(g : \mathbb{N} \times \mathbb{N} \rightharpoonup \mathbb{N}\) there is a total computable \(s : \mathbb{N} \to \mathbb{N}\) with \(\varphi_{s(e)}(n) = g(e, n)\) for all \(e\) and \(n\). Let \(C \subseteq \mathbb{N}\) be a set of indices closed under extensional equality, that is, if \(\varphi_a(n) = \varphi_b(n)\) for all \(n\), then \(a \in C\) if and only if \(b \in C\); and suppose that \(C\) is neither empty nor all of \(\mathbb{N}\). Then there is no total computable \(d : \mathbb{N} \to \mathbb{N}\) such that, for every \(e\), \(e \in C\) if and only if \(d(e) = 1\), and \(e \notin C\) if and only if \(d(e) = 0\).

Proof: The standard argument first derives Kleene's recursion theorem for the acceptable numbering, then diagonalizes a putative decider, following Rice (1953), Rogers §11.2, and Soare II.3.1.

theorem rice_theorem : ∀ (φ : ℕ → ℕ →. ℕ),
    (∀ e, Nat.Partrec (φ e)) →
    Nat.Partrec (fun p => φ (Nat.unpair p).1 (Nat.unpair p).2) →
    (∀ f : ℕ →. ℕ, Nat.Partrec f → ∃ e, ∀ n, φ e n = f n) →
    (∀ g : ℕ → ℕ →. ℕ,
      Nat.Partrec (fun p => g (Nat.unpair p).1 (Nat.unpair p).2) →
      ∃ s : ℕ → ℕ, Nat.Partrec (fun n => Part.some (s n)) ∧
        ∀ e n, φ (s e) n = g e n) →
    ∀ (C : Set ℕ),
      (∀ a b, (∀ n, φ a n = φ b n) → (a ∈ C ↔ b ∈ C)) →
      (∃ a, a ∈ C) → (∃ b, b ∉ C) →
      ¬ ∃ dec : ℕ → ℕ, Nat.Partrec (fun n => Part.some (dec n)) ∧
        ∀ e, (e ∈ C ↔ dec e = 1) ∧ (e ∉ C ↔ dec e = 0)

Sources

• H. G. Rice, Classes of recursively enumerable sets and their decision problems, Transactions of the American Mathematical Society 74(2) (1953), 358-366.

Uses 1

Proof usesRogers's fixed-point theorem for acceptable numberings

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.