Upper semicomputability of Kolmogorov complexity, and incompressible strings

TheoremThe description relation is recognizable#✓fully proved

Let \(U\) be the universal description method. The set of pairs \((x, p)\) of binary strings such that \(U(p)\) is defined and equal to \(x\) is recursively enumerable (recognizable).

theorem rePred_mem_U : REPred fun q : List Bool × List Bool ↦ q.1 ∈ U q.2

Uses 2 · Used by 1

Statement usesThe universal description method

Proof usesThe universal description method is partial recursive

Used byKolmogorov complexity is upper semicomputable

TheoremKolmogorov complexity is upper semicomputable#✓fully proved

Let \(K\) denote Kolmogorov complexity. The set of pairs \((x, n)\) of a binary string \(x\) and a natural number \(n\) with \(K(x) \le n\) is recursively enumerable (recognizable).

theorem rePred_K_le : REPred fun q : List Bool × ℕ ↦ K q.1 ≤ q.2

Uses 7

Statement usesKolmogorov complexity

Proof usesA description bounds the complexity · The universal description method · Shortest descriptions exist · The description relation is recognizable · Recursively enumerable predicates are closed under conjunction · Existential projection preserves recursive enumerability

TheoremA partial recursive map raises complexity by at most a constant#✓fully proved

Let \(K\) denote Kolmogorov complexity and let \(f\) be a partial recursive function from binary strings to binary strings. Then there is a natural number \(c\) such that \(K(y) \le K(x) + c\) for all binary strings \(x\) and \(y\) such that \(f(x)\) is defined and equal to \(y\).

theorem exists_K_map_le {f : List Bool →. List Bool} (hf : Partrec f) :
    ∃ c, ∀ x y : List Bool, y ∈ f x → K y ≤ K x + c

Uses 5 · Used by 1

Statement usesKolmogorov complexity

Proof usesThe universal description method · Optimality (the invariance theorem) · Shortest descriptions exist · The universal description method is partial recursive

Used byShortest descriptions are incompressible

TheoremShortest descriptions are incompressible#✓fully proved

Let \(U\) be the universal description method, \(K\) Kolmogorov complexity, and \(|p|\) the length of a binary string \(p\). There is a natural number \(b\) such that for all binary strings \(x\) and \(p\), if \(p\) is a shortest description of \(x\), that is, \(U(p)\) is defined and equal to \(x\) and \(|p| = K(x)\), then \(|p| \le K(p) + b\).

theorem exists_shortest_incompressible :
    ∃ b, ∀ x p : List Bool, p.length = K x → x ∈ U p → p.length ≤ K p + b

Uses 4

Statement usesKolmogorov complexity · The universal description method

Proof usesA partial recursive map raises complexity by at most a constant · The universal description method is partial recursive

TheoremChaitin's incompleteness theorem#✓fully proved

Let \(K\) denote Kolmogorov complexity, and let \(S\) be a recursively enumerable (recognizable) set of pairs \((x, n)\) of a binary string \(x\) and a natural number \(n\) such that \(n \le K(x)\) for every \((x, n) \in S\). Then there is a natural number \(B\) with \(n \le B\) for every \((x, n) \in S\).

This is the abstract form of the theorem: think of \(S\) as the statements \(K(x) \ge n\) that a sound formal system proves. The proof searches \(S\) for a pair with a large bound \(n\) and applies optimality of the universal description method (Berry's paradox).

theorem exists_bound_of_rePred_le_K {S : List Bool × ℕ → Prop} (hS : REPred S)
    (hsound : ∀ q, S q → q.2 ≤ K q.1) : ∃ B, ∀ q, S q → q.2 ≤ B

Uses 4 · Used by 3

Statement usesKolmogorov complexity

Proof usesOptimality (the invariance theorem) · Recursively enumerable predicates are closed under conjunction · Selection for r.e. relations

Used byA computable lower bound of Kolmogorov complexity is bounded · Kolmogorov complexity is not lower semicomputable · No recognizable set with arbitrarily long members consists of incompressible strings

TheoremA computable lower bound of Kolmogorov complexity is bounded#✓fully proved

Let \(K\) denote Kolmogorov complexity. If \(f\) is a computable function from binary strings to natural numbers with \(f(x) \le K(x)\) for every binary string \(x\), then there is a natural number \(B\) with \(f(x) \le B\) for every binary string \(x\).

theorem exists_bound_of_computable_le_K {f : List Bool → ℕ} (hf : Computable f)
    (hle : ∀ x, f x ≤ K x) : ∃ B, ∀ x, f x ≤ B

Uses 2

Statement usesKolmogorov complexity

Proof usesChaitin's incompleteness theorem

TheoremKolmogorov complexity is not lower semicomputable#✓fully proved

Let \(K\) denote Kolmogorov complexity. The set of pairs \((x, n)\) of a binary string \(x\) and a natural number \(n\) with \(n \le K(x)\) is not recursively enumerable (recognizable).

theorem not_rePred_le_K : ¬REPred fun q : List Bool × ℕ ↦ q.2 ≤ K q.1

Uses 3

Statement usesKolmogorov complexity

Proof usesChaitin's incompleteness theorem · Incompressible strings exist at every length

TheoremNo recognizable set with arbitrarily long members consists of incompressible strings#✓fully proved

Let \(K\) denote Kolmogorov complexity and \(|x|\) the length of a binary string \(x\). There is no recursively enumerable (recognizable) set \(S\) of binary strings such that for every natural number \(n\) some \(x \in S\) has \(|x| \ge n\), and every \(x \in S\) satisfies \(|x| \le K(x)\).

theorem not_rePred_of_forall_incompressible {S : List Bool → Prop} (hS : REPred S)
    (hlong : ∀ n, ∃ x, S x ∧ n ≤ x.length) (hinc : ∀ x, S x → x.length ≤ K x) : False

Uses 3 · Used by 1

Statement usesKolmogorov complexity

Proof usesChaitin's incompleteness theorem · Recursively enumerable predicates are closed under conjunction

Used byThe incompressible strings are not recognizable

TheoremThe incompressible strings are not recognizable#✓fully proved

Let \(K\) denote Kolmogorov complexity and \(|x|\) the length of a binary string \(x\). The set of incompressible binary strings, that is, of binary strings \(x\) with \(|x| \le K(x)\), is not recursively enumerable (recognizable).

theorem not_rePred_incompressible : ¬REPred fun x : List Bool ↦ x.length ≤ K x

Uses 3 · Used by 1

Statement usesKolmogorov complexity

Proof usesIncompressible strings exist at every length · No recognizable set with arbitrarily long members consists of incompressible strings

Used byThe incompressible strings are not decidable

TheoremThe incompressible strings are not decidable#✓fully proved

Let \(K\) denote Kolmogorov complexity and \(|x|\) the length of a binary string \(x\). The set of incompressible binary strings, that is, of binary strings \(x\) with \(|x| \le K(x)\), is not decidable.

theorem not_computablePred_incompressible : ¬ComputablePred fun x : List Bool ↦ x.length ≤ K x

Uses 2

Statement usesKolmogorov complexity

Proof usesThe incompressible strings are not recognizable

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.