A direct proof of Infinity in NF-0
Zuhair A. Al-Johar
math.LO
Oct 17, 2026 · v1
TL;DR
A companion Lean 4 project (Lean 4.24.0, Mathlib v4.24.0) encodes NF-0 as a structure and kernel-checks the Infinity theorem.
Abstract
We give a direct proof of Infinity in the no-empty version of New Foundations, denoted NF-0, by establishing that every model of the specified theory contains an object that is not finite in a precise, internally defined sense. The version considered has extensionality, at least two distinct objects, no empty objects, and inhabited stratified comprehension: a stratified extension is supplied whenever it has a member. Finiteness combines a two-sided internally represented well-order with the exclusion of internally represented nonterminating strict transitive relations on inhabited subsets. Assuming all objects finite, partial bijections yield comparison and finite extrema of positive Frege cardinals. Positive exponentiation, singleton type-raising, and the least orbit of the genuine two-cardinal lead to the equation n = T(n) + 1. We prove separately, and in detail, that adjoining one point reverses internally defined parity: the key ingredients are a graph-rewiring proof of invariance under adjoining two points and one instance of stratified induction derived from the all-finite assumption. Since type-raising preserves parity, the cardinal equation is impossible. We identify the corresponding Lean 4 declarations and make explicit the scope of the formal verification. No model-existence or consistency theorem for ordinary NF is claimed.
Problem
The goal is to prove directly that every model of the no-empty version of New Foundations (NF-0) contains a non-finite object. NF-0 has extensionality, at least two objects, no empty objects, and inhabited stratified comprehension. Finiteness is defined internally.
Approach
The proof assumes all objects are finite and uses partial bijections to compare positive Frege cardinals. It then builds positive exponentiation, singleton type-raising, and the least exponentiation orbit of the two-cardinal, which yields the equation n = T(n) + 1. A separate parity argument shows that adjoining one point reverses internal evenness while type-raising preserves it. This argument uses graph rewiring for two-point invariance and stratified induction. The theory and proof are encoded in a Lean 4 / Mathlib project, and the paper maps its statements to the Lean declarations.
Results
The derived cardinal equation contradicts parity, so some object is not finite. The Lean kernel checks the theorem for the exact encoded axioms. No claim is made about model existence or the consistency of NF.
