@Reuben - Excellent you should mention that. That's some excellent intuition.

John Harrison's compute proof system HOL-Light uses the Knaster-Tarski theorem to construct the natural numbers. Here is the source code: https://github.com/jrh13/hol-light/blob/master/nums.ml

It's a little hard to read, so I will attempt to translate it.

In *Higher Order Logic* (like HOL-Light, Isabelle/HOL or HOL5), the axiom of choice is defined in terms of the *Hilbert choice operator* \\(\epsilon\\). It was introduced by [David Hilbert (1926)](https://eudml.org/doc/159124). It is a higher order function \\(\epsilon : (p \to \mathbf{Bool}) \to p\\). It obeys "The (Hilbert) Axiom of Choice":

$$

\exists x. P(x) \Longleftrightarrow P (\epsilon P)

$$

This is one of the three axioms of HOL-Light. One of the others is "The Axiom of Infinity":

$$

\text{there exists a type } \tau \text{ with a function } succ: \tau \to \tau \text{ that is injective but not surjective}

$$

Since \\(succ\\) is not surjective, there is some number that is not in the range of \\(succ\\). Symbolically, this is \\(\exists x . \forall y. succ(y) \neq x\\). So consider the predicate \\(R(x) : \tau \to \mathbf{Bool} := \forall y. succ(y) \neq x\\). This expresses "\\(x\\) not in the range of \\(succ\\)". HOL-Light defines zero using Hilbert's choice operator and this predicate:

$$

0 := \epsilon R

$$

Zero exists as a consequence of Hilbert's axiom of choice.

Next Harrison defines his monotone map. He uses \\(S(X) := succ_!(X) \cup \\{0\\}\\) where I'm using John Baez's notation \\(succ_!\\) to mean the image of \\(succ\\). \\(S\\) is monotone because \\(succ\\) is injective.

He finally defines

$$

\mathbb{N} := \bigcap \\{X\ :\ S(X) \subseteq X\\}

$$

Now Harrison actually uses a function he wrote called `new_inductive_definition`. The presentation here is more like [Isabelle/HOL's construction](http://isabelle.in.tum.de/website-Isabelle2013/dist/library/HOL/Nat.html). In Isabelle/HOL inductive definitions directly wraps the Knaster-Tarski fixed point contruction. However Isabelle/HOL doesn't do the other nice things Harrison does which follow the discussion above.

John Harrison's compute proof system HOL-Light uses the Knaster-Tarski theorem to construct the natural numbers. Here is the source code: https://github.com/jrh13/hol-light/blob/master/nums.ml

It's a little hard to read, so I will attempt to translate it.

In *Higher Order Logic* (like HOL-Light, Isabelle/HOL or HOL5), the axiom of choice is defined in terms of the *Hilbert choice operator* \\(\epsilon\\). It was introduced by [David Hilbert (1926)](https://eudml.org/doc/159124). It is a higher order function \\(\epsilon : (p \to \mathbf{Bool}) \to p\\). It obeys "The (Hilbert) Axiom of Choice":

$$

\exists x. P(x) \Longleftrightarrow P (\epsilon P)

$$

This is one of the three axioms of HOL-Light. One of the others is "The Axiom of Infinity":

$$

\text{there exists a type } \tau \text{ with a function } succ: \tau \to \tau \text{ that is injective but not surjective}

$$

Since \\(succ\\) is not surjective, there is some number that is not in the range of \\(succ\\). Symbolically, this is \\(\exists x . \forall y. succ(y) \neq x\\). So consider the predicate \\(R(x) : \tau \to \mathbf{Bool} := \forall y. succ(y) \neq x\\). This expresses "\\(x\\) not in the range of \\(succ\\)". HOL-Light defines zero using Hilbert's choice operator and this predicate:

$$

0 := \epsilon R

$$

Zero exists as a consequence of Hilbert's axiom of choice.

Next Harrison defines his monotone map. He uses \\(S(X) := succ_!(X) \cup \\{0\\}\\) where I'm using John Baez's notation \\(succ_!\\) to mean the image of \\(succ\\). \\(S\\) is monotone because \\(succ\\) is injective.

He finally defines

$$

\mathbb{N} := \bigcap \\{X\ :\ S(X) \subseteq X\\}

$$

Now Harrison actually uses a function he wrote called `new_inductive_definition`. The presentation here is more like [Isabelle/HOL's construction](http://isabelle.in.tum.de/website-Isabelle2013/dist/library/HOL/Nat.html). In Isabelle/HOL inductive definitions directly wraps the Knaster-Tarski fixed point contruction. However Isabelle/HOL doesn't do the other nice things Harrison does which follow the discussion above.