Completeness of the halting set

TheoremComposing a code with a constant code ignores the input#✓fully proved

Let \(c\) be a code of a partial recursive function and let \(n, m \in \mathbb{N}\). The code that first computes the constant function with value \(n\) and then applies \(c\), evaluated at \(m\), gives the same partial value as \(c\) evaluated at \(n\): one is defined exactly when the other is, and then they are equal.

theorem eval_comp_const (c : Code) (n m : ℕ) : (Code.comp c (Code.const n)).eval m = c.eval n

Used by 1

Used byEvery recognizable predicate one-one reduces to the halting set

TheoremRecognizability transfers down many-one reductions#✓fully proved

Let \(\alpha\) and \(\beta\) be types with primitive recursive encodings into \(\mathbb{N}\), and let \(p\) and \(q\) be predicates on \(\alpha\) and on \(\beta\). Suppose that \(p\) many-one reduces to \(q\), that is, there is a computable function \(f : \alpha \to \beta\) such that for every \(a \in \alpha\), \(p(a)\) holds if and only if \(q(f(a))\) holds. If \(q\) is recognizable (recursively enumerable: the domain of a partial computable function on \(\beta\)), then \(p\) is recognizable.

theorem REPred.of_manyOneReducible {α β : Type*} [Primcodable α] [Primcodable β] {p : α → Prop}
    {q : β → Prop} (h : ManyOneReducible p q) (hq : REPred q) : REPred p

Used by 2

Used byA predicate is recognizable iff it many-one reduces to the halting set · A predicate is recognizable iff it one-one reduces to the halting set

TheoremThe halting set is recognizable#✓fully proved

The halting set, the set of numbers \(n\) such that the code with number \(n\) halts on input \(0\), is recursively enumerable: it is the domain of a partial computable function on \(\mathbb{N}\).

theorem rePred_haltingSet : REPred haltingSet

Uses 1 · Used by 2

Statement usesHalting set

Used byA predicate is recognizable iff it many-one reduces to the halting set · A predicate is recognizable iff it one-one reduces to the halting set

TheoremEvery recognizable predicate one-one reduces to the halting set#✓fully proved

Let \(\alpha\) be a type with a primitive recursive encoding into \(\mathbb{N}\), and let \(p\) be a recognizable (recursively enumerable) predicate on \(\alpha\), that is, the domain of a partial computable function on \(\alpha\). Here the halting set is the set of \(n \in \mathbb{N}\) such that the partial recursive function with code number \(n\) halts on input \(0\). Then there is an injective computable function \(f : \alpha \to \mathbb{N}\) such that for every \(a \in \alpha\), \(p(a)\) holds if and only if \(f(a)\) lies in the halting set.

The proof takes for \(f(a)\) the number of the code that ignores its input and runs a code for \(p\) on the number encoding \(a\); distinct \(a\) give distinct codes.

theorem oneOneReducible_haltingSet {α : Type*} [Primcodable α] {p : α → Prop} (hp : REPred p) :
    OneOneReducible p haltingSet

Uses 2 · Used by 2

Statement usesHalting set

Proof usesComposing a code with a constant code ignores the input

Used byEvery recognizable predicate many-one reduces to the halting set · A predicate is recognizable iff it one-one reduces to the halting set

TheoremEvery recognizable predicate many-one reduces to the halting set#✓fully proved

Let \(\alpha\) be a type with a primitive recursive encoding into \(\mathbb{N}\), and let \(p\) be a recognizable (recursively enumerable) predicate on \(\alpha\), that is, the domain of a partial computable function on \(\alpha\). Here the halting set is the set of \(n \in \mathbb{N}\) such that the partial recursive function with code number \(n\) halts on input \(0\). Then there is a computable function \(f : \alpha \to \mathbb{N}\) such that for every \(a \in \alpha\), \(p(a)\) holds if and only if \(f(a)\) lies in the halting set.

theorem manyOneReducible_haltingSet {α : Type*} [Primcodable α] {p : α → Prop} (hp : REPred p) :
    ManyOneReducible p haltingSet

Uses 2 · Used by 1

Statement usesHalting set

Proof usesEvery recognizable predicate one-one reduces to the halting set

Used byA predicate is recognizable iff it many-one reduces to the halting set

TheoremA predicate is recognizable iff it many-one reduces to the halting set#✓fully proved

Let \(\alpha\) be a type with a primitive recursive encoding into \(\mathbb{N}\) and let \(p\) be a predicate on \(\alpha\). Here the halting set is the set of \(n \in \mathbb{N}\) such that the partial recursive function with code number \(n\) halts on input \(0\). Then \(p\) is recognizable (recursively enumerable: the domain of a partial computable function on \(\alpha\)) if and only if there is a computable function \(f : \alpha \to \mathbb{N}\) such that for every \(a \in \alpha\), \(p(a)\) holds if and only if \(f(a)\) lies in the halting set.

theorem rePred_iff_manyOneReducible_haltingSet {α : Type*} [Primcodable α] {p : α → Prop} :
    REPred p ↔ ManyOneReducible p haltingSet

Uses 4

Statement usesHalting set

Proof usesRecognizability transfers down many-one reductions · Every recognizable predicate many-one reduces to the halting set · The halting set is recognizable

TheoremA predicate is recognizable iff it one-one reduces to the halting set#✓fully proved

Let \(\alpha\) be a type with a primitive recursive encoding into \(\mathbb{N}\) and let \(p\) be a predicate on \(\alpha\). Here the halting set is the set of \(n \in \mathbb{N}\) such that the partial recursive function with code number \(n\) halts on input \(0\). Then \(p\) is recognizable (recursively enumerable: the domain of a partial computable function on \(\alpha\)) if and only if there is an injective computable function \(f : \alpha \to \mathbb{N}\) such that for every \(a \in \alpha\), \(p(a)\) holds if and only if \(f(a)\) lies in the halting set.

theorem rePred_iff_oneOneReducible_haltingSet {α : Type*} [Primcodable α] {p : α → Prop} :
    REPred p ↔ OneOneReducible p haltingSet

Uses 4

Statement usesHalting set

Proof usesRecognizability transfers down many-one reductions · Every recognizable predicate one-one reduces to the halting set · The halting set is recognizable

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.