Yannick Forster

Fabian Kunze

Nils Lauermann

Nils Lauermann Synthetic Kolmogorov

Synthetic Kolmogorov Complexity in Coq

Keywords: 2012 ACM Subject Classification Theory of computation → Constructive mathematics; Theory of computation → Type theory Kolmogorov complexity, computability theory, random numbers, constructive matemathics, synthetic computability theory, constructive type theory, Coq Digital Object Identifier 10.4230/LIPIcs.ITP.2022.12

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Kolmogorov complexity1 as a subject of computability and information theory is usually presented in the abstract rather than using spelled-out definitions (e.g. [START_REF] Shen | Kolmogorov Complexity and Algorithmic Randomness[END_REF][START_REF] Li | An Introduction to Kolmogorov Complexity and Its Applications[END_REF]). This is no oversight: Kolmogorov complexity is a general concept, invariant in the concrete definition as long as some structural properties are fulfilled. The Kolmogorov complexity of a number x is the length of the shortest bitstring s s.t. decoding s terminates with x, based on a certain decoding function called description mode (which can and will be left abstract at first). the effective topos. In contrast to the work of Richman, Bridges, and Bauer, developing synthetic computability in the constructive type theory underlying the Coq proof assistant is compatible with classical logic, i.e. the law of excluded middle can be assumed alongside Synthetic Church's Thesis without immediately introducing an inconsistency.

Synthetic computability in the Calculus of Inductive Constructions (CIC [START_REF] Coquand | The calculus of constructions[END_REF][START_REF] Paulin-Mohring | Inductive definitions in the system Coq rules and properties[END_REF][START_REF] Paulin-Mohring | Introduction to the Calculus of Inductive Constructions[END_REF]), the constructive type theory underlying the Coq proof assistant [START_REF]The Coq proof assistant version 8[END_REF], is based on two facts: First, that all functions definable in CIC can be shown computable in CIC (thus allowing the assumption of a universal function, implementable as the universal µ-recursive function). Secondly, that CIC has a strict separation between function spaces such as N → N or N ⇀ N and logic, carried out in the impredicative universe of propositions P. Thus, assuming the law of excluded middle (LEM) does not leak into the function space and does not allow the definition of an uncomputable function. In this setting, one has the choice between three equivalent axioms to develop results: SCT, based on total functions N → N → N, EPF, based on partial functions N → N ⇀ N, and EA, based on parametrically enumerable predicates N → N → P. Forster, Jahn, and Smolka [14] use EA to construct Post's simple predicate.

Coming back to Kolmogorov complexity, the noncomputability of Kolmogorov complexity can also be proved by showing that nonrandom numbers (numbers which can be efficiently described, i.e. which are longer than their Kolmogorov complexity) form a simple predicate. We give a machine-checked proof of this result using the definition of simple predicates by Forster, Jahn, and Smolka [14] based on the axiom EPF [START_REF] Forster | Parametric church's thesis: Synthetic computability without choice[END_REF], which seems most natural for Kolmogorov complexity due to the frequent use of partial functions.

We structure the paper to be instructive for similar future endeavours: First, we give the high-level proof idea in Section 2, without formal definitions and without bothering about the use of classical logic. Then, we introduce the relevant aspects of CIC in Section 3: Total and partial functions (treated as computable functions), partial relations (which are not necessarily computable), total relations (also not provably computable, but where a constructive totality proof is possible if and only if the relation is computable), and classically total relations (which can be proved total using classical logic and are not necessarily computable).

We recap the formalities of synthetic computability in CIC in Section 4 and discuss provable versions of choice principles in Section 5. We then observe that Kolmogorov complexity has to be formalised as a partial, classically total relation and introduce the notion formally in Section 6. In Section 7 we introduce nonrandom and random numbers, suitably formalised to allow a constructive enumerability proof, and show that the nonrandom numbers form a simple predicate. For infinity of random numbers, we rely on the definition by Forster, Jahn, Smolka [14] and explain how to insert double negations in the formalised statements of the intuitive proofs to get rid of uses of the law of excluded middle. To show that nonrandom numbers are immune (a necessary condition to show nonrandom numbers simple) we rely on Markov's principle (MP), which simplifies the proof.

We then discuss the role of MP in Section 8 and show a general technique how the specific way how MP is used in the proof, which also occurs in other proofs, can be eliminated to obtain a fully constructive proof that nonrandom numbers form a simple predicate.

In Section 9 we then instantiate our general definition of Kolmogorov complexity to the definition used by Catt and Norrish (while still staying in the synthetic setting). We also instantiate to a definition similar to the definition used in Odifreddi's book [START_REF] Odifreddi | Classical recursion theory: The theory of functions and sets of natural numbers[END_REF] in Section 10.

We claim that we obtain elegant proofs of all results and that our proofs do not lose elegance either due to formalising, due to mechanising them in a proof assistant, or due to presenting them in constructive logic. The machine-checked development3 is accessible to any Coq user and no knowledge of tedious details regarding models of computation is necessary.

12:4

Synthetic Kolmogorov Complexity in Coq 2

Intuition: Nonrandom numbers form a simple predicate

The Kolmogorov complexity C(x) of a number x is the size of its shortest description. We call a partial function δ : N ⇀ N a description mode. We call y a description of x if δy ▷ x.

The size of descriptions is the length of its interpretation as bitstring. We write |n| for the length of the bit string representing n. We will assume that the interpretation as bitstring works such that the size of n is at most as long as the logarithm (by 2) of n plus 1.

As a consequence, we obtain the following.

▶ Fact 1. For all d, there is n with n > |n| + d.

▶ Fact 2. There are exactly 2 k descriptions with size k and, 2 k -1 descriptions with size less than k.

Proof. The first follows since there are exactly 2 k bit strings of length k. The second is by usual arithmetical arguments. ◀

We only assume one property of δ, namely that it is optimal up to a constant. I.e. for every computable function δ ′ there is a constant d s.t.

∀y ′ x. δ ′ y ′ ▷ x → ∃y. δy ▷ x ∧ |y| < |y ′ | + d.
Using the optimality on δ ′ y := y we obtain that δ is surjective:

▶ Fact 3.

Every number has a description.

A number is nonrandom if its shortest description is shorter than the number itself. Formally, N (x) := C(x) < x. Intuitively (but because we do not go into detail how δ is defined, not formally), the following number is nonrandom: 001 001 001 001 001 001 001 001 001 001 001 001 001 001 001 001 001 This is because it can be written more compactly as "repeat 001 for 17 times". On the other hand, the terminology random seems intuitive when looking at a number like We now prove that nonrandom numbers form a simple predicate, a result that first appeared in [START_REF] Zvonkin | The complexity of finite objects and the development of the concepts of information and randomness by means of the theory of algorithms[END_REF] and is there attributed to Janis Barzdins. A predicate is simple if it is enumerable and its complement is infinite but does not contain an enumerable, infinite subpredicate.

▶ Lemma 4. Nonrandom numbers are enumerable.

Proof. Try all possible inputs y and evaluate δy for all possible step numbers n. If δy evaluates to a value x in n steps and |y| < |x|, then output x. ◀ ▶ Lemma 5. Random numbers are infinite.

Proof. Suppose all 2 k many numbers x i of size k would be nonrandom. This means that they would have 2 k many distinct descriptions y i , all with size smaller than k. But there are at most 2 k -1 numbers of size smaller than k. Contradiction. ◀

The third part of the definition of simpleness, which is often called immunity, is easiest to explain with some more formulas. ▶ Lemma 6. There is no enumerable infinite sub-predicate of random numbers.

Proof. Assume such a predicate q. Since q is infinite, in particular, for every k it contains x with |x| > k. Now since q is enumerable, we can define a computable function f computing these x, i.e. for all k, f k is in q. Since q is a subpredicate of random numbers, in particular f k is random.

∀k. k < |f k|.
Since δ is optimal, we have a constant d and descriptions y k for every f k at most as long as |k| + d, i.e.:

∀k. |y k | ≤ |k| + d.
Since f k is random, its size is shorter than its shortest description, and in particular it is shorter than its description y k , i.e.

Constructive Logic in Coq's Type Theory

In the previous section, we informally defined Kolmogorov complexity as the size of the least description. Since every number has a description, Kolmogorov complexity was treated as a total function. Later, we showed that this total function is however not computable.

When we now want to define Kolmogorov complexity in CIC, we cannot define it as a function, because all definable functions in CIC always are, by definition, computable. Thus, we will define Kolmogorov complexity as a functional relation. While in set theory the notion of a function and a functional relation are conflated they are strictly separate in CIC.

We make use of this separation and introduce the following general leastness-predicate transformer: For every predicate p: N → P one can define the predicate y is (µx. px) being satisfied exactly if y is the least number satisfying p.

y is (µx. px) := py ∧ ∀y ′ . py ′ → y ≤ y ′
We can then prove that the predicate is functional.

Fact 8. y 1 is (µx. px) → y 2 is (µx. px) → y 1 = y 2
As we have defined it, we cannot prove that whenever p is satisfied there is a least element satisfying it. To see this, we can look again at Kolmogorov complexity: After defining Kolmogorov complexity using µ, we could then show that Kolmogorov complexity is a total relation. This, however, is impossible: A constructive totality proof ∀x.∃y. would correspond via the Curry-Howard interpretation to a definable function computing Kolmogorov complexity, which we know cannot exist because Kolmogorov complexity is uncomputable.

I T P 2 0 2 2 12:6 Synthetic Kolmogorov Complexity in Coq

Since we know that a totality proof cannot be constructive, we will use classical totality: A relation X → Y → P is classically total if ∀x.¬¬∃y. Rxy.

When proving the ¬¬∃ part of classical totality, one can use classical logic. This is because one can think of double negation as a modality with the following proof rules. We can indeed prove that whenever p is satisfied it does not not have a least element:

Fact 10. py → ¬¬∃y. y is (µx. px)
The well-known axioms of the law of excluded middle LEM and Markov's principle MP can be thought of as extending the proof rules for the double negation modality.

LEM := ∀P : P. P ∨ ¬P MP := ∀f : N → B. ¬¬(∃n. f n = true) → ∃n. f n = true
MP allows entering the double negation modality whenever the goal is a Σ 0 1 formula. The following states that LEM allows entering the double negation modality for every goal.

Fact 11. LEM → ¬¬Q → Q

Using LEM, one can prove that least elements for inhabited predicates always exist. Furthermore, in constructive mathematics, it is standard practice to also analyse whether made classical assumptions are necessary, and in this case one can indeed prove that the existence of least elements for inhabited predicates implies LEM.

Lastly, we need a good, constructive definition of infinite predicates. The definition cannot be too weak, which might mean that we cannot show that simple predicates are undecidable. The definition cannot be too strong either, which might mean that it is impossible to establish random numbers to be infinite. We can here just follow Forster, Jahn, and Smolka [14] in using non-finite predicates. We use the type of lists over X, written LX, with [] being the empty list and x :: l being the list with element x added to a list l. A predicate p:

X → P is finite if ∃l: LX. ∀x. px ↔ x ∈ l. A predicate p: X → P is subfinite if ∃l: LX. ∀x. px → x ∈ l.
A predicate is non-finite if it is not finite.

Fact 12. A predicate is non-finite if and only if it is not subfinite.

Non-finiteness for predicates on natural numbers can be expressed as a ∀¬¬∃ version of having elements of arbitrary size. Computability theory is usually presented with respect to an effective enumeration ϕ of all computable function, i.e. ϕ c denotes the c-th computable function, and for every computable function f there is a code c s.t. f and ϕ c agree. By appeal to the (informal) Church Turing thesis, ϕ has the following informal universal property:

∀f : N ⇀ N. f is intuitively computable → ∃c.∀xv. ϕ c x ▷ v ↔ f x ▷ v.
In synthetic computability theory [START_REF] Forster | Parametric church's thesis: Synthetic computability without choice[END_REF], one uses essentially the same approach, but (1) abstracts against an abstract function ϕ rather than a concrete enumeration, and (2) assumes all functions N ⇀ N of the meta-theory to be intuitively computable. Thus, we obtain an axiom assuming a function ϕ: N → N ⇀ N with the following formal universality property:

∀f : N ⇀ N. ∃c.∀xv. ϕ c x ▷ v ↔ f x ▷ v
This axiom is called EPF in [START_REF] Forster | Church's Thesis and Related Axioms in Coq's Type Theory[END_REF] and is a consequence of the axiom EPF in [START_REF] Forster | Parametric church's thesis: Synthetic computability without choice[END_REF]. 4 Consistency of such an axiom is a consequence of the consistency of the axiom CT in CIC, see [13, Appendix A] and [START_REF] Forster | Church's Thesis and Related Axioms in Coq's Type Theory[END_REF].

The first simplification entailed by synthetic computability becomes obvious when defining standard notions of computability, which do not need to rely on a model of computation [START_REF] Forster | On synthetic undecidability in Coq, with an application to the entscheidungsproblem[END_REF]. A predicate p: X → P is decidable if there exists a decider: ∃f : X → B.∀x. px ↔ f x = true enumerable if there exists an enumerator: ∃f :

N → OX.∀x. px ↔ ∃n. f n = Some x
Here, OX is the type with constructors None and Some x where x : X and B has elements true and false.

The intuition behind decidability should be immediately clear. Enumerability captures the definition that a predicate is "r.e." ("recursively enumerable") if it is the co-domain of a function. Equivalent domain-based definitions can be given [START_REF] Forster | Computability in Constructive Type Theory[END_REF] but we do not require them.

If a predicate p is enumerable we write Ep. We write ER for a relation R: N → N → P if the predicate λ(x, y). Rxy is enumerable. We call a type X discrete if λ(x 1 , x 1 ). x 1 = x 2 is decidable and enumerable if λx: X. ⊤ is enumerable.

One can give various definitions of partial functions in CIC with enumerable graph [12, §4.5]. We abstractly use a function type N ⇀ N and write f x ▷ y if f : N ⇀ N on input x evaluates to y. This type can for instance be inhabited by stationary functions N → (N → ON), i.e. where f xn 1 = Some x → ∀n 2 ≥ n 1 . f xn 2 = Some x. We just need the following fact and only need more constructions for partial functions in Fact 37.

Fact 14. One can define an enumeration function graph:

(N ⇀ N) → N → O(N × N) s.t. ∀f xy. f x ▷ y ↔ ∃n. graphf n = Some (x, y).
Following Forster, Jahn, and Smolka [14] one can also define reducibility, e.g. many-one, one-one, or truth-table reducibility. We refrain from doing so here and just use their definition of simpleness. A predicate p: N → P is simple if 1. p is enumerable, 2. the complement of p is not finite, 3. the complement of p has no non-finite, enumerable sub-predicate q (i.e. ∀x. qx → ¬px).

12:8

Synthetic Kolmogorov Complexity in Coq 5

Choice Functions

In computability theory, unbounded search is a crucial tool to define functions. In CIC, we have two options for unbounded search: First, we can implement an unbounded search operator yielding partial functions (e.g. of type N ⇀ N). Secondly, we can make use of the fact that a choice principle for enumerable relations is provable. This means that for enumerable relations (often also called Σ 0 1 -relations) one can extract a function from a totality proof.

Kolmogorov Complexity

Recall that the Kolmogorov complexity of a number x is the size of the least description of x.

To formally capture the notion, we need to formally capture size and description.

We will model descriptions using the type of natural numbers. To define the size of a description we parameterise our development against a bijection between natural numbers and binary strings, i. [false, false, false] are then binary strings. We write len(l) for the length of a binary string.

To see that such a bijection exists, we can define one which identifies a natural number n with the binary expansion of n + 1 with the most significant bit left out. I.e. this bijection associates the following numbers and lists:

0 ∼ [] 1 ∼ [false] 2 ∼ [true] 3 ∼ [false, false] 4 ∼ [false, true] . . .
It is then routine to prove the above properties, we do not go into detail here.

Y. Forster, F. Kunze, and N. Lauermann

12:9

We now turn back to working with any bijection fulfilling the above four properties and define the size of a number n as the length of its interpretation as binary string, i.e.

|n| := len(⌈n⌉).

We can use concatenation to define a pairing function on natural numbers: ⟨x, y⟩ := ⌊⌈x⌉ + + ⌈y⌉⌋ Note that ⟨x, y⟩ is surjective, but injectivity or the existence of a (left-)inverse function depend on the concrete definition of ⌈•⌉ and ⌊•⌋, because x and y are not necessarily reconstructible from ⌈x⌉ + + ⌈y⌉. We however do not rely on either. The following fact will become important later, because it restricts the amount of possible descriptions with a certain size.

Fact 20. There are exactly 2 k distinct lists of booleans x with lenx = k:

∃l: L(LB). (∀x. x ∈ l ↔ len(x) = k) ∧ #l ∧ len(l) = 2 k
We write #l to indicate that l does not contain any duplicates. One can find various definitions of what constitutes a description of a number x. We will just assume a description mode δ: N ⇀ N. As in the intuitive explanation, we will assume that δ is optimal, i.e. that As before, using optimality on the identity function, we can obtain that every number has a description.

Nonrandom Numbers

In this section, we introduce nonrandom numbers and prove that they form a simple predicate.

Recall that a number is nonrandom if it has a description shorter than its own size. Formally, we have three options to define nonrandom numbers:

N 1 (x) := ∃s. s is C δ (x) ∧ s < |x| N 2 (x) := ∃y. δy ▷ x ∧ |y| < |x| N 3 (x) := ∀s. s is C δ (x) → s < |x|
Note that we cannot simply use C δ (x) < |x|, because C is not a total function. Options N 1 and N 3 capture the two possible ways to talk about the values of a functional relation. Option N 2 circumvents mentioning C, because if some description y has smaller size than x, then surely the smallest description (i.e. C δ (x)) has smaller size as well. All definitions have different constructive strength, but are classically equivalent. We emphasise that, counter-intuitively perhaps given the naming, random numbers are constructively the complement of nonrandom numbers (rather than the other way around):

Fact 24. N 1 (x) → N 2 (x), N 2 (x) → N 3 (x), N 3 (x) → ¬¬N 1 (x).
Fact 26. R(x) ↔ ¬N (x).
Classically, a number is random if it is shorter than or as long as its shortest description, again for surjective description functions:

Fact 27. Given ∀x.∃y. δy ▷ x we have Let R 1 (x) := ∃s. s is C δ (x) ∧ |x| ≤ s and R 3 (x) := ∀s. s is C δ (x) → |x| ≤ s. Then R 1 (x) → R(x), R(x) → R 3 (x) and R 3 (x) → ¬¬R 1 (x).
We have already proved that N is enumerable. To prove that it is simple, we need to prove that R (being the complement of N ) is not finite and to prove that R has no enumerable, non-finite subpredicate. We will do so in the following sections.

The Random Numbers are Non-Finite

Recall Fact 20 stating that there are exactly 2 k distinct lists of numbers l: LB with length k. We can immediately lift this to the following:

∀k.¬¬∃x. |x| = k ∧ R(x)
Corollary 32. R is not finite.

The Nonrandom Numbers are Simple

Recall that we have assumed δ to be an optimal description function. Restricting optimality to total functions yields the following. We only need this fact, not full optimality, for the following central result.

Lemma 34. Given MP, R does not have an enumerable, non-finite subpredicate.

Proof. Let q be enumerable, non-finite, and ∀x. qx → R(x). We have to obtain a contradiction.

Since q is non-finite the relation λkx. k < |x| ∧ qx is classically total, i.e. ∀k.¬¬∃x. k < |x| ∧ qx. Thus, by MP and Corollary 17 there is a function f : N → N s.t. for all k < |f k| (1) and q(f k). In particular, due to the latter and since q is a subpredicate of random numbers, ∀ky. δy ▷ f k → |f k| ≤ |y| [START_REF] Bauer | On fixed-point theorems in synthetic computability[END_REF].

By optimality for total functions there exists d such that for all k there is y k with δy k ▷ f k and |y k | < |k| + d (3). Thus we have for all k: Enumerable relations can equivalently be characterised using partial choice functions. This approach is not very common in type theory because partial functions are usually avoided, but in the setting of Kolmogorov complexity we have been relying on partial functions all along. We say that a partial We can then use optimality to prove the following result applying to every classically total, enumerable relation R. The rest of the proof then proceeds exactly as before:

k (1) < |f k| (2) ≤ |y k | (3) ≤ |k| + d.
Lemma 39. R does not have an enumerable, non-finite sub-predicate.

Proof. Let q be enumerable, non-finite, and ∀x. qx → R(x). We have to obtain a contradiction.

Since q is non-finite λky. y is µx. k < |x| ∧ qx is classically total, i.e. for all k, there classically exists x k s.t. k < |x k | (1) and qx k . In particular, due to the latter, x k is random:

∀y. δy ▷ x k → |x k | ≤ |y|.
By Lemma 38 there exists d such that for all k there exist y k and there classically exists

x k with k < |x k | (1), qx k , thus ∀y. δy ▷ x k → |x k | ≤ |y| (2), δy k ▷ x k and |y k | < |k| + d (3).
We now prove ∀k. k < |k| + d, a contradiction by Fact 19.

Let k be given. We prove k < |k| + d. Since < is decidable, we can obtain y k and x k with properties (1) -( 3) from above and have the wanted contradiction to Fact 19:

k (1) < |x k | (2) ≤ |y k | (3) < |k| + d ◀
Note that overall, it would have been shorter to just explain the proof without MP in the paper. However, the proof becomes arguably a little more indirect by eliminating MP. We consciously decided to show both versions, because we think that being able to transparently compare both approaches can be helpful to eliminate uses of MP from other theorems not exclusively but especially in computability theory.

12:15

Other machine-checked proofs regarding Kolmogorov complexity. In Section 9 we discuss a synthetic version of the definition used by Catt and Norrish [START_REF] Catt | On the formalisation of Kolmogorov complexity[END_REF].

There are various differences in the approaches: First, Catt and Norrish define ϕ in terms of the λ-calculus. In order to obtain c s.t. ϕ c computes f they have to explicitly construct a λ-term computing f . Terms of the λ-calculus constitute about 200 lines of code of their HOL4 formalisation (not accounting for proofs about these terms) which has approximately 6000 lines in total. For comparison of the magnitude, our whole development has around 800 lines of Coq code. Note that we just give these numbers for comparison of magnitude and do not want to relate the complexity of Coq code and HOL4 code via line numbers.

Catt and Norrish use an operation MIN_SET computing the least element of a non-empty set to define a Kolmogorov complexity function. In general, such an operation requires at least a unique choice operator and the law of excluded middle. We instead work with functional relations, which poses no problems and avoids the operator. They also use classical logic, i.e. rely on LEM. While classical logic would be available in our setting, our result also shows that it is not needed. Classical logic is only available in our synthetic setting because we avoid (unique) choice operators [START_REF] Forster | Church's Thesis and Related Axioms in Coq's Type Theory[END_REF]. Note that Catt and Norrish do not consider random or nonrandom numbers and prove instead that C is uncomputable. This is a direct consequence of the proof that N is simple, but the proof idea is exactly the same.

Other results on Kolmogorov complexity. Catt and Norrish [START_REF] Catt | On the formalisation of Kolmogorov complexity[END_REF] also prove the Kraft and Kolmogorov-Kraft inequalities and various other information-theoretic properties from the book by Hutter [START_REF] Hutter | Universal Artificial Intellegence[END_REF]Theorem 2.10]. We do not see any hurdles in adding them on top of our development, but leave them for future work as we focus on computability-theoretic properties. Regarding computability Kummer [START_REF] Kummer | On the complexity of random strings[END_REF] proves that N is truth-table complete, i.e. that every enumerable predicate p, and in particular the halting problem K truth-table reduces to N . The proof is highly involved and would pose an interesting challenge for interactive theorem proving. Forster, Jahn, and Smolka [14] give a machine-checked construction of a simple but truth-table complete predicate following Post, which is easier.

Other machine-checked proofs in computability and complexity theory. Norrish [START_REF] Norrish | Mechanised computability theory[END_REF] proves Rice's theorem in HOL4 based on the full λ calculus, the development is now underlying the work on Kolmogorov complexity with Catt.

Forster and Smolka [START_REF] Forster | Weak call-by-value lambda calculus as a model of computation in Coq[END_REF] prove Rice's theorem in Coq based on the weak call-by-value λ calculus. Forster, Kunze, Smolka, and Wuttke [START_REF] Forster | A mechanised proof the time invariance thesis for the weak call-by-value λ-calculus[END_REF] prove that the weak call-by-value λ calculus and Turing machines can simulate each other with polynomial overhead in time. Gäher and Kunze [START_REF] Gäher | Mechanising complexity theory: The cook-levin theorem in Coq[END_REF] prove the Cook-Levin theorem stating that SAT is NP-complete with a definition of NP in the weak call-by-value λ-calculus, but by employing the simulation of the λ-calculus on Turing machines to encode computation as boolean circuits.

Xu, Zhang, and Urban [START_REF] Xu | Mechanising Turing machines and computability theory in Isabelle/HOL[END_REF] prove that the halting problem of Turing machines is undecidable in Isabelle. Larchey-Wendling [START_REF] Larchey-Wendling | Typing total recursive functions in Coq[END_REF] proves that every total µ-recursive function gives rise to a Coq function. Carneiro [START_REF] Carneiro | Formalizing Computability Theory via Partial Recursive Functions[END_REF] proves Rice's theorem in Lean based on µ-recursive functions. Ramos et al. [START_REF] Mendonça | Formalization of rice's theorem over a functional language model[END_REF] prove Rice's theorem in PVS based on PVS0 and assuming a fixed-point theorem. Forster, Jahn, and Smolka [14] prove a synthetic version of Myhill's isomorphism theorem and a synthetic computational version of the Cantor-Bernstein theorem without assuming any axioms. Lastly, Forster [START_REF] Forster | Parametric church's thesis: Synthetic computability without choice[END_REF][START_REF] Forster | Computability in Constructive Type Theory[END_REF] proves Rice's theorem and Forster, Jahn, and Smolka [14] develop the theory of one-one, many-one, and truth-table degrees and construct simple and hypersimple sets, based on the axiom EA, equivalent to EPF. We conclude by discussing several more general points concerning machine-checked proofs, synthetic computability, and constructive mathematics.

For the scope of this project, translating from textbook proofs to the synthetic settings was barely noticable: The look and feel is like working in a textbook setting. Classical logic is available and the axiom of choice, albeit being explicitly acknowledged as foundation e.g. by Rogers [START_REF] Rogers | Theory of Recursive Functions and Effective Computability[END_REF], does not play any practical role. Instead of using (unique) choice operators to obtain functions one can work with the -often anyways more convenient -(classically) total functional relation directly.

The original textbook proofs on Kolmogorov complexity are heavily classical. The first steps of the present paper were undertaken as part of the third author's Bachelor's thesis [START_REF] Lauermann | A formalization of Kolmogorov complexity in synthetic computability theory[END_REF], and explicitly used the law of excluded middle. The agnosticism of constructive type theory and Coq w.r.t classical provided very helpful in this regard: Require Import Classical. turns Coq into a classical proof assistant and basic logical automation tactics like tauto use classical logic immediately.

In a second pass, also part of the mentioned Bachelor's thesis, the uses of LEM were analysed one by one and either circumvented by a constructivisation of the statement, or by a use of Markov's principle where no immediate constructivisation was possible. For instance, the usual definition "There exist members of every size." (∀s.∃n ≥ s. pn) to define infinite sets has to be translated to the constructively weaker definition of infinity, "For every size, the subset of members of this size is not non-empty." (∀n.¬(¬∃n. n ≥ s ∧ pn)). Here, Coq serves as a true proof assistant: It helps in keeping track of details and assumptions and keeps its user honest by forcing them to apply classical axioms explicitly. Manually constructivising proofs on paper would be more time-intensive, as proofs have to be checked repeatedly on axiom usage to be sure.

In the case of Kolmogorov complexity, obtaining fully constructive proofs directly from textbook proofs seems unfeasible. Even obtaining proofs based solely on MP requires a great deal of experience with constructive proofs. Thus it is crucial that both Coq and our setting of synthetic computability are compatible with classical reasoning: First working up to LEM, then up to MP and only then re-working the proofs to not use MP turned out to be feasible.

Overall, our paper can be seen as a case study substantiating various points often found in papers on interactive theorem proving:

First, giving a machine-checked proof has benefits distinct from the question of correctness. The ITP forces users to think about the most concise and elegant ways to express definitions, statements, and proofs and to isolate the properties of structures necessary to prove the wanted results. In our case, we can isolate that the assumption of an optimal description function suffices to prove the existence of a simple predicate, no other properties of the description function or the subsequent definition of Kolmogorov complexity are needed.

Secondly, thinking about constructive proofs has benefits distinct from the question which axioms are necessary for a result. Constructive logic enforces direct arguments, thus making presentations easier to follow, and makes proofs by contradiction explicit already in theorem statements, thus making presentations more transparent.

Thirdly, having the possibility to assume classical axioms is vital. Nowadays, few (if any) constructive mathematicians outright reject axioms like the law of excluded middle, but rather emphasise the benefits for presentations on the one hand, and on the other hand the academic curiosity motivating the analysis of which assumptions constitute the minimal set of assumptions necessary for any given theorem. The circumstance that our setting of synthetic computability theory allows classical axioms, in contrast to previous approaches forming an anti-classical endeavour, was crucial for the present paper, which as already mentioned started out as a Bachelor's thesis project: Due to the pioneering work by Catt and Norrish it was clear that a machine-checked proof based on classical axioms is in reach, the first task was just to translate it to the simpler setting of synthetic computability theory. Probably, we would not have dared posing a simultaneous constructivisation and translation to the synthetic setting for a thesis project on Bachelor's level.

  833 256 052 501 225 207 711 246 773 401 191 432 051 794 357 674 718

Fact 9 .

 9 The following hold: 1. P → ¬¬P 2. ¬¬P → (P → ¬¬Q) → ¬¬Q 3. (P ∨ ¬P → ¬¬Q) → ¬¬Q Item 1 states that the double negation modality can be left at any time (it has the type of the return of a monad). 2 states how to combine different double negated proofs (it has the type of the bind of a monad). 3 states that in the double negation modality, arbitrary case disctinctions are allowed.

Fact 13 .

 13 Let f : N → N be a size function which assigns only finitely many elements the same size. A predicate p : N → P is infinite if and only if ∀n. ∃x. f x ≥ n ∧ px. Synthetic Computability Theory

Fact 15 .Fact 16 .

 1516 Every total enumerable relation R: N → N → P has a choice function: ER → (∀x.∃y. Rxy) → ∃f.∀x. Rx(f x) Proof. Due to the fact that whenever ∃n: N. f n = true also Σn: N. f n = true, discovered independently by Benjamin Werner and Jean-François Monin and part of Coq's standard library as constructive ground description operator. ◀ As discussed it is however not always possible to prove totality of a relation without classical logic. For enumerable relations, MP suffices to obtain full classical power for the totality proof. Given MP, every classically total enumerable relation R: N → N → P is total: MP → ER → (∀x.¬¬∃y. Rxy) → ∀x.∃y. Rxy Corollary 17. Given MP, every classically total enumerable relation R: N → N → P has a choice function: MP → ER → (∀x.¬¬∃y. Rxy) → ∃f.∀x. Rx(f x)

  e. against functions ⌈•⌉: N → LB and ⌊•⌋: LB → N s.t. 1. ∀l. ⌈⌊l⌋⌉ = l 2. ∀n. ⌊⌈n⌉⌋ = n 3. ∀n. len(⌈n⌉) ≤ log 2 (n) + 1 4. ∀xy. x ≤ y → len(⌈x⌉) ≤ len(⌈y⌉) We model binary strings formally as lists of booleans LB, for instance [], [true, false],

Fact 18 .Fact 19 .

 1819 |⟨x, y⟩| = |x| + |y| Since the size behaves logarithmically, there (classically) exist numbers n which are larger than |n|. Formally: For all d, ¬¬∃n. n > |n| + d. Equivalently: For all d, ¬∀n.n ≤ |n| + d.

  ∀δ ′ : N ⇀ N.∃d: N.∀y ′ x. δ ′ y ′ ▷ x → ∃y. δy ▷ x ∧ |y| < |y ′ | + d.

Fact 21 .

 21 ∀x.∃y. δy ▷ xIn Sections 9 and 10 we give several possible definitions for description modes frequently found in the literature.We define the Kolmogorov complexity C(x) of a number x to be the least number s s.t. s is a size of a description of x, i.e. we define a functional relation C: N → N → P as followsC(x)s := s is µs. ∃y. s = |y| ∧ δy ▷ xWe also write s is C(x) for C(x)s. Surjectivity of δ suffices to prove that C(x) is classically total.Fact 22. ∀x. ¬¬∃s. s is C(x)We can also use optimality of δ to prove that a definition of C using any other description operator δ ′ yields a similar definition of Kolmogorov complexity, only differing in a constant. In this so-called invariance theorem we write C δ and C δ ′ for the two respective definitions of Kolmogorov complexity. Theorem 23. If δ is an optimal description mode we have that for every δ ′ : N ⇀ N there exists d: N s.t. whenever s is C δ (x) and s ′ is C δ ′ (x) we have s ≤ s ′ + d.

Proof.

  Relying on surjectivity of δ. ◀ Since only N 2 can be proved enumerable constructively, we choose it as definition. N (x) := ∃y. δy ▷ x ∧ |y| < |x| Fact 25. N is enumerable. Proof. Let f : N → ON enumerate the graph of δ, i.e. δy ▷ x ↔ ∃n. f n = Some (x, y). Then λn. if f n is Some (x ′ , y) then if x ′ = x ∧ |y| < |x| then Some y else None else None enumerates N . ◀ The complement of nonrandom numbers is formed by random or incompressible numbers: R(x) := ∀y. δy ▷ x → |x| ≤ |y|

Corollary 28 .Corollary 29 . 1 Lemma 30 .Corollary 31 .

 282913031 There are exactly 2 k distinct numbers y with |y| = k: ∃l: LN. (∀y. y ∈ l ↔ |y| = k) ∧ #l ∧ len(l) = 2 k There are at most 2 k -1 distinct numbers y with |y| < k:∀l: LN. (∀x. x ∈ l → |y| < k) → #llen(l) < 2 k -Not every number of size k is nonrandom: ∀k: N.¬∀x: N. |x| = k → N (x)Proof. Suppose all 2 k many numbers of size k would be nonrandom, i.e. we have distinct x i for 0 ≤ i < 2 k s.t. there is y i with|y i | < |x i | = k and δy i ▷ x i .Note that we have |y| i < k and all y i are distinct (because y i = y j implies x i = x j ). But by the last corollary, there are at most 2 k -1 numbers y with |y| < k. Contradiction.◀ There classically exist random numbers of every size:

Fact 33 .

 33 ∀f : N → N.∃d: N.∀x: N.∃y x . δy x ▷ f x ∧ |y x | < |x| + d

Theorem 35 .▶ Corollary 36 .

 3536 This is a contradiction to Fact 19.◀ Given MP, N is simple. The following hold given MP:1. R is undecidable. 2. N is undecidable. 3. C is uncomputable.principle MP is used to prove that R has no enumerable, non-finite subpredicate in the proof of simpleness of R. The simpleness proof of nonrandom numbers uses MP to obtain a choice function f for the classically total, enumerable relation λkx. k < |x| ∧ qx. Then optimality is applied to f to obtain an upper bound for C δ (f x), i.e. d with ∀x. C δ (f x) < |x| + d. However, optimality would readily apply to partial functions f .

  function f : X ⇀ Y is a partial choice function for a relation R : X → Y → P if values computed by f are in the relation. A partial choice function has the same domain as R if ∀x.(∃y. Rxy) ↔ ∃y. f x ▷ y. For functional relations, the conditions are equivalent to Rxy ↔ f x ▷ y. A relation is enumerable if and only if it has a partial choice function with the same domain.

Fact 37 .

 37 Every enumerable relation R: N → N → P has a partial choice function with the same domain, and vice versa: ER ↔ ∃f : N ⇀ N. (∀xy. f x ▷ y → Rxy) ∧ ∀x. (∃y. Rxy) → (∃y. f x ▷ y) If R is functional, then ER ↔ ∃f : N ⇀ N. ∀xy. f x ▷ y ↔ Rxy.

Lemma 38 .

 38 Let R: N → N → P be a classically total, enumerable relation. Then ∃d: N.∀x: N.∃y x .¬¬∃v x . Rxv x ∧ δy x ▷ v x ∧ |y| x < |x| + d. Proof. By Fact 37 R has a partial choice function f : N ⇀ N s.t. f x ▷ v x → Rxv x and Rxv x → ∃v ′ x . f x ▷ v ′ x . Optimality of δ used on f immediately yields the result. ◀

  ∀k. |f k| ≤ |y k |.

	But now ∀k. k < |f k| ≤ |y k | ≤ |k| + d, a contradiction to Fact 1.	◀
	▶ Corollary 7.
	1. Nonrandom numbers are simple.
	2. Both random and nonrandom numbers are undecidable.
	3. Kolmogorov complexity is noncomputable.
	Proof. Simple predicates can be shown undecidable [14]. If there would be a function f
	computing Kolmogorov complexity, λx.f x < |x| would decide nonrandomness.	◀

The origins of the complexity notion are complicated, see Li and Vitányi's book for an overview[30, §1.13]. It is often also called Solomonoff-Kolmogorov-Chaitin complexity, crediting the influential work by Ray Solmonoff[START_REF] Ray | A preliminary report on a general theory of inductive inference (revision of report v-131)[END_REF][START_REF] Solomonoff | A formal theory of inductive inference. part i[END_REF][START_REF] Solomonoff | A formal theory of inductive inference. part II[END_REF], Andrej Kolmogorov[24,

[START_REF] Kolmogorov | Three approaches to the quantitative definition of information[END_REF], and Gregory Chaitin[START_REF] Chaitin | On the simplicity and speed of programs for computing infinite sets of natural numbers[END_REF]

The given reference is usually used for Post's theorem, but just constitutes a short abstract containing neither the theorem or a proof. Standard textbook references give modern proofs[41,

[START_REF] Odifreddi | Classical recursion theory: The theory of functions and sets of natural numbers[END_REF].

The development is hyperlinked with the present paper, always indicated by a clickable -symbol.I T P 2 0 2 2

This is not a typo, both axioms are unfortunately indeed named the same.I T P 2 0 2 2

Acknowledgements

We want to thank Dominik Kirst and Gert Smolka for many fruitful discussions.

1

Funding Yannick Forster: received funding from the European Union's Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 101024493.

: https://github.com/uds-psl/coq-synthetic-computability/tree/kolmogorov archived at swh:1:dir:172c753027deabef87ce303e73dc98fc14745a89

12:13 [START_REF] Dudenhefner | Constructive many-one reduction from the halting problem to semiunification[END_REF]

Universal codes

We now instantiate the definition of Kolmogorov complexity to a definition based on universal codes as used by Catt and Norrish [START_REF] Catt | On the formalisation of Kolmogorov complexity[END_REF]. We call a code u universal if ∀c. ∃x. ∀y. ϕ c y ≡ ϕ u ⟨x, y⟩ and define Proof. Let a code u be strongly universal if ∀ci. ϕ c i ≡ ϕ u ⟨c, i⟩. It is immediate that every strongly universal code is universal and that every strongly universal code fulfils the properties.

Thus, it suffices to prove that there exists a strongly universal code: Define

By universality of ϕ there exists a code u s.t. ∀x.

Catt and Norrish define pairing as ⌊Ix + + ⌈x⌉ + + ⌈y⌉⌋ with I being the function from the proof of Lemma 41, which makes pairing immediately computationally invertible. For our definition of pairing, we do not know how to define such an inversion operation, but the whole development in this paper does not depend on the concrete definition of pairing and could as well be carried out with Catt and Norrish's definition.

Fixed inputs

Odifreddi [START_REF] Odifreddi | Classical recursion theory: The theory of functions and sets of natural numbers[END_REF] defines the Kolmogorov complexity of x as the smallest c such that the c-th Turing machine (w.r.t. an effective enumeration of Turing machines) outputs x when ran on a blank tape. That is, he defines the description operator to simulate on input c the c-th Turing machine on blank tape, and then defines the size of a Turing machine as exactly its code. Thus, there is exactly one Turing machine of size k, rather than exponentially many. This non-conventional approach allows Odifreddi to obtain an elegant proof of simpleness of nonrandom numbers using Rogers' fixed-point theorem. However, Odifreddi's definition is not invariant w.r.t. other definitions (in the sense of Theorem 23) since there are strings with Kolmogorov complexity exponentially larger than using our definition.

However, one can use the first part of the definition to instantiate our definition as well. That is, we can define δ in terms of ϕ for an arbitrary fixed input i.

The assumed universality of ϕ does not suffice to prove that N is simple using this definition. We need to adapt it in order to make statements on the size of γx for certain functions as follows.

Note that this is strictly stronger than the universality condition, but it can similarly be proved consistent by showing that a formulation of CT L as discussed by Forster [13, §7, Appendix A] also implies this version.

Related Work

Vitanyi [START_REF] Paul | How incomputable is Kolmogorov complexity?[END_REF] attributes the first complete, spelled-out undecidability proof to Zvonkin and Levin in 1970 [START_REF] Zvonkin | The complexity of finite objects and the development of the concepts of information and randomness by means of the theory of algorithms[END_REF]. Zvonkin and Levin themselves refer to Kolmogorov who claimed the uncomputability of Kolmogorov complexity in 1965 by pointing to the undecidability of the halting problem [START_REF] Kolmogorov | Three approaches to the quantitative definition of information[END_REF], however without a real proof. Furthermore, the paper by Zvonkin and Levin seems to contain the first proof that that the nonrandom numbers are simple, but attribute the result to Janis Barzdins.

Other definitions of Kolmogorov complexity. Odifreddi [34] defines Kolmogorov complexity as C(x) := µc. ϕ c 0 ▷ x, i.e. assuming |c| = c. Our theory cannot be instantiated to such definitions of Kolmogorov complexity, because it contradicts property 3 of the encoding of numbers as binary strings. In particular, there are just k many numbers x with |x| < k and just one number with exactly size k, so our proof cannot be used directly. Odifreddis' proof seems to be about as complicated as our proof, but not considering a size function allows a very elegant use of Roger's fixed-point theorem [START_REF] Rogers | Theory of Recursive Functions and Effective Computability[END_REF], of which Forster [START_REF] Forster | Parametric church's thesis: Synthetic computability without choice[END_REF] gives a machine-checked proof. Thus, everything would be in place to also give a machine-checked proof that nonrandom numbers form a simple predicate based on Odifreddi's definition in our setting, but we leave this to future work.