Arithmetical hierarchy

DefinitionThe class Δₙ of the arithmetical hierarchy#✓fully proved

Let \(n\) be a natural number. A set \(P\) of natural numbers is in \(\Delta_n\) when it is in both classes \(\Sigma_n\) and \(\Pi_n\) of the arithmetical hierarchy.

def IsDelta (n : ℕ) (P : ℕ → Prop) : Prop :=
  IsSigma n P ∧ IsPi n P

Sources

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

Used by 1

Used byΣₙ and Πₙ predicates are Δₙ₊₁

TheoremComputable predicates are closed under computable precomposition#✓fully proved

If \(P\) is a decidable set of natural numbers and \(g : \mathbb{N} \to \mathbb{N}\) is a computable function, then the set \(\{w \in \mathbb{N} : g(w) \in P\}\) is decidable.

theorem computablePred_comp {P : ℕ → Prop} (hP : ComputablePred P) {g : ℕ → ℕ}
    (hg : Computable g) : ComputablePred (fun w ↦ P (g w))

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Lemma 4.2.

Uses 2 · Used by 2

Proof usesCharacteristic function of a set of naturals · A set is decidable iff its characteristic function is partial recursive

Used byThe hierarchy is closed under computable precomposition · Monotonicity of the hierarchy

TheoremThe first projection of the pairing function is computable#✓fully proved

Let \(\langle a, b \rangle\) denote the pairing bijection \(\mathbb{N} \times \mathbb{N} \to \mathbb{N}\), \(\langle a, b \rangle = b^2 + a\) if \(a < b\) and \(\langle a, b \rangle = a^2 + a + b\) otherwise. The function sending \(z \in \mathbb{N}\) to the first component \(a\) of the unique pair \((a, b)\) with \(\langle a, b \rangle = z\) is computable.

theorem computable_unpair_fst : Computable (fun z : ℕ ↦ z.unpair.1)

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.3.

Used by 5

Used byThe hierarchy is closed under computable precomposition · Monotonicity of the hierarchy · Every Πₙ set is Σₙ₊₁ · Σ₁ is the class of recursively enumerable predicates · Every Σₙ predicate is Πₙ₊₁

TheoremThe second projection of the pairing function is computable#✓fully proved

Let \(\langle a, b \rangle\) denote the pairing bijection \(\mathbb{N} \times \mathbb{N} \to \mathbb{N}\), \(\langle a, b \rangle = b^2 + a\) if \(a < b\) and \(\langle a, b \rangle = a^2 + a + b\) otherwise. The function sending \(z \in \mathbb{N}\) to the second component \(b\) of the unique pair \((a, b)\) with \(\langle a, b \rangle = z\) is computable.

theorem computable_unpair_snd : Computable (fun z : ℕ ↦ z.unpair.2)

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.3.

Used by 2

Used byThe hierarchy is closed under computable precomposition · Σ₁ is the class of recursively enumerable predicates

TheoremThe pairing function is computable#✓fully proved

The pairing bijection \(\langle \cdot, \cdot \rangle : \mathbb{N} \times \mathbb{N} \to \mathbb{N}\), given by \(\langle a, b \rangle = b^2 + a\) if \(a < b\) and \(\langle a, b \rangle = a^2 + a + b\) otherwise, is a computable function of its two arguments.

theorem computable_pair : Computable₂ Nat.pair

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.3.

Used by 2

Used byThe hierarchy is closed under computable precomposition · Computable predicates are closed under precomposition with pairing

TheoremComputable predicates are closed under precomposition with pairing#✓fully proved

Let \(\langle a, b \rangle\) denote the pairing bijection \(\mathbb{N} \times \mathbb{N} \to \mathbb{N}\), \(\langle a, b \rangle = b^2 + a\) if \(a < b\) and \(\langle a, b \rangle = a^2 + a + b\) otherwise. If \(Q\) is a decidable set of natural numbers, then the set of pairs \((a, b) \in \mathbb{N} \times \mathbb{N}\) with \(\langle a, b \rangle \in Q\) is decidable.

theorem computablePred_comp_prod {Q : ℕ → Prop} (hQ : ComputablePred Q) :
    ComputablePred (fun p : ℕ × ℕ ↦ Q (Nat.pair p.1 p.2))

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Lemma 4.2.

Uses 1 · Used by 1

Proof usesThe pairing function is computable

Used byΣ₁ is the class of recursively enumerable predicates

TheoremThe hierarchy is closed under computable precomposition#✓fully proved

Let \(n\) be a natural number and let \(g : \mathbb{N} \to \mathbb{N}\) be computable. If a set \(P\) of natural numbers is in the class \(\Sigma_n\) of the arithmetical hierarchy, then so is \(\{w \in \mathbb{N} : g(w) \in P\}\); and if \(P\) is in the class \(\Pi_n\), then so is \(\{w \in \mathbb{N} : g(w) \in P\}\).

theorem comp_closure (n : ℕ) :
    (∀ P : ℕ → Prop, IsSigma n P → ∀ g : ℕ → ℕ, Computable g →
      IsSigma n (fun w ↦ P (g w))) ∧
    (∀ P : ℕ → Prop, IsPi n P → ∀ g : ℕ → ℕ, Computable g →
      IsPi n (fun w ↦ P (g w)))

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Lemma 4.2.

Uses 4 · Used by 2

Proof usesComputable predicates are closed under computable precomposition · The pairing function is computable · The first projection of the pairing function is computable · The second projection of the pairing function is computable

Used byEvery Πₙ set is Σₙ₊₁ · Every Σₙ predicate is Πₙ₊₁

TheoremEvery Σₙ predicate is Πₙ₊₁#✓fully proved

Let \(\Sigma_n\) and \(\Pi_n\) be the levels of the arithmetical hierarchy of predicates on \(\mathbb{N}\): \(\Sigma_0 = \Pi_0\) is the class of computable predicates, \(P \in \Sigma_{n+1}\) when for some \(Q \in \Pi_n\) and all \(x\), \(P(x)\) holds iff \(Q(\langle x, y \rangle)\) holds for some \(y\), and \(P \in \Pi_{n+1}\) when for some \(Q \in \Sigma_n\) and all \(x\), \(P(x)\) holds iff \(Q(\langle x, y \rangle)\) holds for all \(y\); here \(\langle x, y \rangle\) is the standard pairing function of \(\mathbb{N}\). Then for every \(n\), every predicate in \(\Sigma_n\) is in \(\Pi_{n+1}\).

The proof adds a dummy universal quantifier.

theorem sigma_subset_pi_succ {n : ℕ} {P : ℕ → Prop} (h : IsSigma n P) :
    IsPi (n + 1) P

Sources

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

Uses 2 · Used by 1

Proof usesThe hierarchy is closed under computable precomposition · The first projection of the pairing function is computable

Used byΣₙ and Πₙ predicates are Δₙ₊₁

TheoremEvery Πₙ set is Σₙ₊₁#✓fully proved

For every natural number \(n\), every set of natural numbers in the class \(\Pi_n\) of the arithmetical hierarchy is also in \(\Sigma_{n+1}\); that is, \(\Pi_n \subseteq \Sigma_{n+1}\), by adding a dummy existential quantifier.

theorem pi_subset_sigma_succ {n : ℕ} {P : ℕ → Prop} (h : IsPi n P) :
    IsSigma (n + 1) P

Sources

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

Uses 2 · Used by 1

Proof usesThe hierarchy is closed under computable precomposition · The first projection of the pairing function is computable

Used byΣₙ and Πₙ predicates are Δₙ₊₁

TheoremMonotonicity of the hierarchy#✓fully proved

For every natural number \(n\), writing \(\Sigma_n\) and \(\Pi_n\) for the classes of the arithmetical hierarchy, every \(\Sigma_n\) set of natural numbers is in \(\Sigma_{n+1}\) and every \(\Pi_n\) set of natural numbers is in \(\Pi_{n+1}\).

The two inclusions are proved together by induction on \(n\): the step case of each uses the other at the previous level.

theorem mono_aux : ∀ n : ℕ,
    (∀ P : ℕ → Prop, IsSigma n P → IsSigma (n + 1) P) ∧
    (∀ P : ℕ → Prop, IsPi n P → IsPi (n + 1) P)

Sources

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

Uses 2 · Used by 2

Proof usesComputable predicates are closed under computable precomposition · The first projection of the pairing function is computable

Used byMonotonicity of the Π hierarchy · Every Σₙ predicate is Σₙ₊₁

TheoremEvery Σₙ predicate is Σₙ₊₁#✓fully proved

Let \(\Sigma_n\) and \(\Pi_n\) be the levels of the arithmetical hierarchy of predicates on \(\mathbb{N}\): \(\Sigma_0 = \Pi_0\) is the class of computable predicates, \(P \in \Sigma_{n+1}\) when for some \(Q \in \Pi_n\) and all \(x\), \(P(x)\) holds iff \(Q(\langle x, y \rangle)\) holds for some \(y\), and \(P \in \Pi_{n+1}\) when for some \(Q \in \Sigma_n\) and all \(x\), \(P(x)\) holds iff \(Q(\langle x, y \rangle)\) holds for all \(y\); here \(\langle x, y \rangle\) is the standard pairing function of \(\mathbb{N}\). Then for every \(n\), every predicate in \(\Sigma_n\) is in \(\Sigma_{n+1}\).

theorem sigma_mono {n : ℕ} {P : ℕ → Prop} (h : IsSigma n P) : IsSigma (n + 1) P

Sources

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

Uses 1 · Used by 1

Proof usesMonotonicity of the hierarchy

Used byΣₙ and Πₙ predicates are Δₙ₊₁

TheoremMonotonicity of the Π hierarchy#✓fully proved

For every natural number \(n\), every set of natural numbers in the class \(\Pi_n\) of the arithmetical hierarchy is also in \(\Pi_{n+1}\); that is, \(\Pi_n \subseteq \Pi_{n+1}\).

theorem pi_mono {n : ℕ} {P : ℕ → Prop} (h : IsPi n P) : IsPi (n + 1) P

Sources

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

Uses 1 · Used by 1

Proof usesMonotonicity of the hierarchy

Used byΣₙ and Πₙ predicates are Δₙ₊₁

TheoremΣₙ and Πₙ predicates are Δₙ₊₁#✓fully proved

Let \(\Sigma_n\) and \(\Pi_n\) be the levels of the arithmetical hierarchy of predicates on \(\mathbb{N}\): \(\Sigma_0 = \Pi_0\) is the class of computable predicates, \(P \in \Sigma_{n+1}\) when for some \(Q \in \Pi_n\) and all \(x\), \(P(x)\) holds iff \(Q(\langle x, y \rangle)\) holds for some \(y\), and \(P \in \Pi_{n+1}\) when for some \(Q \in \Sigma_n\) and all \(x\), \(P(x)\) holds iff \(Q(\langle x, y \rangle)\) holds for all \(y\); here \(\langle x, y \rangle\) is the standard pairing function of \(\mathbb{N}\). Then for every \(n\), every predicate in \(\Sigma_n\) or in \(\Pi_n\) is in \(\Delta_{n+1}\), that is, in both \(\Sigma_{n+1}\) and \(\Pi_{n+1}\).

theorem sigma_pi_subset_delta_succ {n : ℕ} {P : ℕ → Prop}
    (h : IsSigma n P ∨ IsPi n P) : IsDelta (n + 1) P

Sources

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

Uses 5

Statement usesThe class Δₙ of the arithmetical hierarchy

Proof usesMonotonicity of the Π hierarchy · Every Πₙ set is Σₙ₊₁ · Every Σₙ predicate is Σₙ₊₁ · Every Σₙ predicate is Πₙ₊₁

TheoremΣ₁ is the class of recursively enumerable predicates#✓fully proved

A predicate \(P\) on \(\mathbb{N}\) is recursively enumerable if and only if it is in \(\Sigma_1\), that is, if and only if there is a computable predicate \(Q\) on \(\mathbb{N}\) such that for all \(x\), \(P(x)\) holds iff \(Q(\langle x, y \rangle)\) holds for some \(y\), where \(\langle x, y \rangle\) is the standard pairing function of \(\mathbb{N}\).

This is the first level of Post's theorem.

theorem sigma_one_eq_re {P : ℕ → Prop} : IsSigma 1 P ↔ REPred P

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Theorem 4.4 (Post).

Uses 4

Proof usesComputable predicates are closed under precomposition with pairing · The first projection of the pairing function is computable · The second projection of the pairing function is computable · Existential projection preserves recursive enumerability

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.