A direct proof of Infinity in NF-0
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.
Related
- A Direct Proof of the Locally Dense Graphon Inequality
- A direct proof of the equivalence of the A2 and the Helson--Szego conditions
- A direct inductive proof of the sharp Merino--Welsh threshold for matroids
- A Direct Proof of the Simplicity of Non-Trivial Zeros of the Riemann Zeta Function
- The Order Mass Identity of Rooted Forests, with a Direct Proof of the Extended Aldous-Broder Theorem
BibTeX
@misc{aljohar2026direct,
title = {{A direct proof of Infinity in NF-0}},
author = {Zuhair A. Al-Johar},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.35928},
eprint = {2610.35928},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.35928},
}
RIS
TY - UNPB
TI - A direct proof of Infinity in NF-0
AU - Zuhair A. Al-Johar
PY - 2026
DA - 2026/10/17
PB - arXiv
DO - 10.48550/arxiv.2610.35928
UR - https://arxiv.org/abs/2610.35928
AB - 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.
ER -