Productive, creative, simple and immune sets

DefinitionStandard enumeration of the recursively enumerable sets#✓fully proved

For natural numbers \(e\) and \(n\), \(n\) belongs to \(W_e\), the \(e\)-th recursively enumerable set, when the partial recursive function \(\varphi_e\) computed by the program with index \(e\) in the standard numbering of partial recursive programs is defined at \(n\); thus \(W_e\) is the domain of \(\varphi_e\).

def enumRE (e n : ℕ) : Prop :=
  (Nat.Partrec.Code.eval (Denumerable.ofNat Nat.Partrec.Code e) n).Dom

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (standard enumeration of the partial recursive functions).

Used by 2

Used byProductive set · A productive set is not recursively enumerable

DefinitionProductive set#✓fully proved

A set \(A\) of natural numbers is productive when there is a partial recursive function \(f\) such that for every natural number \(e\) with \(W_e \subseteq A\), where \(W_e\) is the \(e\)-th recursively enumerable set in the standard enumeration, \(f(e)\) is defined, \(f(e) \in A\) and \(f(e) \notin W_e\).

def Productive (P : ℕ → Prop) : Prop :=
  ∃ f : ℕ →. ℕ, Partrec f ∧ ∀ e, (∀ n, enumRE e n → P n) →
    ∃ h : (f e).Dom, P ((f e).get h) ∧ ¬ enumRE e ((f e).get h)

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Definition 5.1.

Uses 1 · Used by 4

Statement usesStandard enumeration of the recursively enumerable sets

Used byCreative set · A creative set is not computable · A creative set is recursively enumerable · A productive set is not recursively enumerable

DefinitionCreative set#✓fully proved

A set \(A\) of natural numbers is creative when it is recursively enumerable and its complement \(\mathbb{N} \setminus A\) is productive.

def Creative (P : ℕ → Prop) : Prop :=
  REPred P ∧ Productive (fun n ↦ ¬ P n)

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Definition 5.2.

Uses 1 · Used by 2

Statement usesProductive set

Used byA creative set is not computable · A creative set is recursively enumerable

DefinitionImmune set#✓fully proved

A set \(A\) of natural numbers is immune when it is infinite and every recursively enumerable set \(B \subseteq A\) is finite.

def Immune (P : ℕ → Prop) : Prop :=
  Set.Infinite {n | P n} ∧ ∀ A : ℕ → Prop, REPred A → (∀ n, A n → P n) →
    Set.Finite {n | A n}

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Definition 5.4.

Used by 5

Used byAn immune set is not recursively enumerable · Simple set · The complement of a simple set is immune · A simple set is not computable · A simple set is recursively enumerable

DefinitionSimple set#✓fully proved

A set \(P\) of natural numbers is simple when it is recursively enumerable and its complement \(\{n \mid \neg P(n)\}\) is immune.

def Simple (P : ℕ → Prop) : Prop :=
  REPred P ∧ Immune (fun n ↦ ¬ P n)

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Definition 5.3.

Uses 1 · Used by 3

Statement usesImmune set

Used byThe complement of a simple set is immune · A simple set is not computable · A simple set is recursively enumerable

TheoremA productive set is not recursively enumerable#✓fully proved

No productive set of natural numbers is recursively enumerable: if it were the \(e\)-th recursively enumerable set \(W_e\), its productive function would produce a member of it outside \(W_e\).

theorem productive_not_re {P : ℕ → Prop} (hP : Productive P) : ¬ REPred P

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Theorem 5.5.

Uses 2 · Used by 1

Statement usesProductive set

Proof usesStandard enumeration of the recursively enumerable sets

Used byA creative set is not computable

TheoremAn immune set is not recursively enumerable#✓fully proved

It would be an infinite RE subset of itself.

theorem immune_not_re {P : ℕ → Prop} (hP : Immune P) : ¬ REPred P

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Theorem 5.6.

Uses 1

Statement usesImmune set

TheoremA simple set is not computable#✓fully proved

Its complement would be an infinite RE set, contradicting immunity.

theorem simple_not_computable {P : ℕ → Prop} (hP : Simple P) : ¬ ComputablePred P

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Theorem 5.6.

Uses 2

Statement usesSimple set

Proof usesImmune set

TheoremA simple set is recursively enumerable#✓fully proved

A simple set is recursively enumerable, by definition.

theorem simple_re {P : ℕ → Prop} (hP : Simple P) : REPred P

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Definition 5.3.

Uses 2

Statement usesSimple set

Proof usesImmune set

TheoremThe complement of a simple set is immune#✓fully proved

The complement of a simple set is immune, by definition.

theorem simple_complement_immune {P : ℕ → Prop} (hP : Simple P) :
    Immune (fun n ↦ ¬ P n)

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Definition 5.3.

Uses 2

Statement usesImmune set · Simple set

TheoremA creative set is recursively enumerable#✓fully proved

A creative set is recursively enumerable, by definition.

theorem creative_re {P : ℕ → Prop} (hP : Creative P) : REPred P

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Definition 5.2.

Uses 2

Statement usesCreative set

Proof usesProductive set

TheoremA creative set is not computable#✓fully proved

Its complement is productive, hence not RE, but the complement of a computable set is RE.

theorem creative_not_computable {P : ℕ → Prop} (hP : Creative P) :
    ¬ ComputablePred P

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Theorem 5.7.

Uses 3

Statement usesCreative set

Proof usesProductive set · A productive set is not recursively enumerable

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.