@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.