arXiv:2610.35928v1 Announce Type: new 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.
Continue to arXiv Mathematics →You are being forwarded in 6s — stay on this page