The Hereditarily Finite Universe

§1

What is verified

Two things the note says are checkable, and both have been checked. Its opening intuition about digit places (§2–§3) is taken up in §2 below. Its claim about the axioms (§5) — that if you remove Infinity, the remaining axioms are satisfied by the hereditarily finite sets, a perfectly coherent universe in which every set is finite — is the subject of the rest of this page.

Lean 4.23.0, core only — no mathlib, no `sorry`.
Claim	Result	Status
Digits.lean — the digit argument
n digit places express at most 10ⁿ values	finite_of_uniform_digit_bound	holds
at most n digits is exactly “below 10ⁿ”	numDigits_le_iff	holds
every natural has a finite digit count	each_has_finite_digits	holds
one bound covers every natural	no_uniform_digit_bound	refuted
an infinite set uses unboundedly many digit places	unbounded_digit_lengths	holds
HF.lean — the finite universe
Extensionality	ext	holds
Empty set	empty_exists	holds
Pairing	pairing_exists	holds
Union	mem_sUnion	holds
Separation	mem_sep	holds
Power set	mem_powerset	holds
Replacement	mem_repl	holds
Foundation	regularity, mem_induction	holds
Infinity	infinity_fails	refuted

Separation and Replacement are stated for arbitrary predicates and functions, not merely decidable or definable ones. Two further results sit alongside these. cantor_diagonal is the diagonal argument over an arbitrary type, finite or not, using no infinity whatsoever — which is the formal counterpart of the note’s “I am not claiming Cantor made an error.” Rejecting Infinity leaves the construction untouched; it only removes the infinite object to apply it to. And no_universal_set: nothing contains everything.

§2

The digit argument

The note opens with an intuition: a finite number of digit places can only express finitely many distinct values — ten digits per place, n places, at most 10ⁿ values — so if a set contains infinitely many distinct elements, infinitely many digit places must be in use somewhere.

The premise is exactly right, and it is a theorem. finite_of_uniform_digit_bound shows that if a single n bounds the digit count of every member of a set, that set has at most 10ⁿ members — witnessed by an explicit list of that length. numDigits_le_iff makes the correspondence exact rather than a mere upper bound: having at most n digits is the condition of being below 10ⁿ.

What does not follow is the conclusion, and the gap is one quantifier.

∀x ∃n every natural has some finite digit count true
∃n ∀x one bound covers every natural false

Both halves are proved in the_quantifier_swap. The argument needs the second. The naturals supply only the first.

So the claim as literally stated — that there can be no infinite set all of whose members have finitely many digits — is false in standard mathematics, and the counterexample is the first set anyone would reach for. unbounded_set_of_finite_digit_numbers: the naturals are unbounded, every member has a finite digit count, and no member has infinitely many digits, because there is no such natural number.

Where the digit places are

The note ends that passage with a question: where, then, are the infinitely many digit places? Inside standard mathematics it has an exact answer. unbounded_digit_lengths proves that an infinite set of naturals must contain a number of more than n digits, for every n.

So the unboundedly many digit places are real, and they are in the set — distributed across its members, never accumulated inside any one of them. Each member stops; the lengths do not. That is the whole of the distinction the note’s §3 draws between unbounded and infinite, and it is the precise sense in which the original intuition was tracking something true.

Not support for the thesis — and not a refutation of it

This is the formal shape of a concession the note already makes. It settles nothing in the note’s favour; what it adds is precision about which half of the intuition holds in every framework, and exactly where the other half stops being a proof and becomes a choice.

Nor does it meet the note’s deeper objection. To say the digit places are in the set presupposes a completed set to hold them — which is exactly what the note declines to grant. The answer is given inside the framework it defends. To a reader who denies completed infinity, it restates unboundedness rather than answering the objection.

§3

The model

The universe is the natural numbers. Membership is read straight off the binary expansion: a is a member of b exactly when the a-th bit of b is set. So the members of a number are literally the positions of its ones.

codebits, index 0 firstmembers

0 no bits set ∅

1 {0}

3 {0, 1}

11 {0, 1, 3}

2059 {0, 1, 3, 11}

The von Neumann naturals. Each row’s members are exactly the rows above it — the construction is visible in the bits. Every code is finite, and the codes grow without bound, so no code can have all of them as members. That is infinity_fails.

The whole development turns on one lemma. Call it mem_lt: a member always has a strictly smaller code, because a set bit at position a forces the number to be at least 2^a, which already exceeds a. Membership therefore descends, every set is finite, and Foundation comes free. The same lemma is what defeats Infinity: an inductive set would have to contain codes larger than itself.

§4

What this establishes

A theory with a model is consistent. So ZF−Infinity does not prove Infinity: Infinity is not a theorem but an axiom, exactly as the note says. The position the note describes is not confused, and it is not a mistake about mathematics. There is a universe in which every set is finite, it can be written down, and a machine can check it.

§5

What it does not

Not established, and not establishable

This does not show that completed infinity is incoherent, and no formal development could. If ZF is consistent then Infinity cannot be refuted, so on the narrow formal reading the record runs the other way.

That is worth stating flatly, because it is the thing a reader might hope a page headed “machine-checked” would deliver. It does not. What it delivers is the weaker and more useful thing: the disagreement is located precisely, at an axiom, which is where the note always said it was.

§6

Three caveats

Soundness is not formalized here. Lean verifies that this structure satisfies these sentences. The step from there to “the first-order theory does not prove Infinity” is the soundness theorem. It is entirely standard, but it is taken outside the machine, and nothing here checks it.
Semantic, not schematic. Separation and Replacement are axiom schemas over formulas in the language of set theory. What is verified is the semantic version, quantifying over arbitrary Lean predicates and functions. For this purpose that is at least as strong — every definable predicate is in particular a predicate — but it is a statement in Lean’s type theory about a structure, not a derivation inside a formalized first-order calculus.
The independence is two-sided, and only one side is cheap. That ZF−Infinity cannot prove Infinity is witnessed here: the finite universe can be written down and checked. That it cannot refute Infinity needs a model of ZF, and by Gödel’s second incompleteness theorem ZF cannot prove one exists; that half rests on assuming the consistency of ZF and cannot be exhibited the way this file exhibits the finite universe. The asymmetry is real, and mildly congenial to the note. But it is an asymmetry about the cost of exhibiting models of weaker against stronger theories, which is generic, and it is not evidence that the stronger theory describes nothing.

§7

Consistent is not coherent

The note’s thesis is that a completed infinite totality is incoherent. Formal consistency is a different and weaker notion. This work shows that denying Infinity is consistent. It says nothing about whether asserting it is coherent, and on the narrow formal reading “incoherent” cannot mean “inconsistent” here at all.

Formal work can locate a disagreement exactly. It cannot settle one.

§8

Checking it yourself

The file is self-auditing. A clean run prints the axiom dependencies of every result and nothing else; any gap, any sorry, or any appeal to an extra axiom would appear in that output.

# Lean 4.23.0, no other dependencies
elan toolchain install leanprover/lean4:v4.23.0
lean formal/HF.lean

The audit it prints names only Lean’s own propext and Quot.sound, plus Classical.choice exactly where classical reasoning was used on purpose. sorryAx — the marker for anything assumed rather than proved — appears nowhere.

'HF.infinity_fails' depends on axioms: [propext, Quot.sound]
'HF.cantor_diagonal' depends on axioms: [propext]

A sanity section computes small cases — P(∅) = {∅}, succ 3 = 11, powerset 7 = 255 — so the theorems cannot be vacuously true of a mis-stated encoding.