New Foundations (NF) is an axiomatic set theory developed by the American philosopher and logician Willard Van Orman Quine in his 1937 paper "New Foundations for Mathematical Logic," published in The American Mathematical Monthly. It provides a parsimonious foundation for mathematics, relying on just two principles: the axiom of extensionality, which equates sets with identical members, and the axiom schema of stratified comprehension, which permits the formation of sets via formulas that respect a hidden type structure to circumvent paradoxes like Russell's.[1]Unlike the dominant Zermelo–Fraenkel set theory with the axiom of choice (ZFC), which prohibits infinite descending membership chains and large collections to maintain consistency, NF embraces a more permissive ontology.[1] A defining feature is the existence of a universal setV containing all sets, provable directly from the axioms, as the stratified formula "y ∈ x" allows comprehension to yield {y | y ∈ x} interpreted universally. This enables "big sets," such as the set of all cardinals or the set of all singletons, which are impossible in ZFC due to its restrictions on set size and well-foundedness.[1]NF's consistency was a longstanding open question in set theory, with early suspicions of inconsistency arising from models exhibiting pathological behaviors, such as the failure of the axiom of choice in strong forms.[1] However, in 2015, Randall Holmes provided a proof establishing NF's consistency relative to the consistency of a weak set theory such as Mac Lane set theory, using a model based on tangled type theory; this proof has been refined and key parts formalized in the Lean proof assistant by Sky Wilshaw as of 2024.[2] Despite these advances, NF remains less developed than ZFC for formalizing large swaths of mathematics, though it supports key structures like the natural numbers and offers intriguing alternatives in areas such as category theory and permutation models.[1]
Overview and Definition
Core Principles and Axioms
New Foundations (NF) is built upon two primary axioms: extensionality and a stratified comprehension schema, which together provide a foundation for set theory without invoking types or iterative hierarchies. The axiom of extensionality states that two sets are identical if and only if they have precisely the same members: \forall x \forall y \, [x = y \leftrightarrow \forall z (z \in x \leftrightarrow z \in y)]. This principle ensures that sets are determined solely by their membership relations, allowing for the identification of collections based on extensional equivalence rather than internal structure or labels.[3][4]The stratified comprehension schema is the cornerstone of NF, permitting the existence of a set for any stratified formula \phi(x): \exists S \forall x (x \in S \leftrightarrow \phi(x)). A formula is stratified if its variables can be assigned natural number types such that for every subformula u \in v, the type of u is one less than the type of v (i.e., type(u) + 1 = type(v)), and for every subformula u = v, type(u) = type(v). For instance, the power set formula \forall z (z \in y \leftrightarrow z \in x) is stratified by assigning type n+1 to x and y, and type n to z, ensuring a consistent hierarchical typing that aligns with the membership relation. This schema enables the construction of sets like the universal set V = \{x \mid x = x\}, which is stratified under type assignment 0 to all variables.[3][4]Stratification prevents circular or impredicative definitions by enforcing a type-level discipline that avoids self-reference in membership. Consider an attempt to define the Russell set R = \{x \mid x \notin x\}; assigning type n to the outer x requires the inner x \in x (or \notin) to have type n+1 for the membership but type n for the argument, leading to a contradiction in typing. Thus, such unstratified formulas are excluded from comprehension, blocking paradoxical constructions without restricting legitimate set formations. NF assumes classical logic, including the law of excluded middle, which applies to all stratified formulas, ensuring that every such formula is either true or false and supporting bivalent reasoning throughout the theory.[3][1][4]
Finite Axiomatization
The standard formulation of New Foundations (NF) relies on an infinite axiom schema of stratified comprehension, which posits the existence of sets defined by any stratified formula. To address the impracticality of an infinite schema for formal proof systems, finite axiomatizations have been developed that capture the full strength of NF using a bounded number of specific axioms. One such approach, introduced by Theodore Hailperin in 1944, replaces the schema with extensionality and nine carefully chosen instances of stratified comprehension, all formulated relative to the universal set V = \{x \mid x = x\}. These instances ensure that all stratified sets can be derived through logical manipulations and substitutions that preserve stratification.[5][3]A key component in Hailperin's system is the use of restricted comprehension principles that leverage the universal set V to define subsets without requiring type indices. For example, the axioms include comprehensions for basic operations such as the singleton image, which constructs sets of the form \{y \in V \mid \exists z \in X (y = \{z\})\}, anti-intersections \{y \in V \mid \neg (y \in y)\}, and insertions like \{y \in V \mid y = a \lor y \in X\}. Additionally, an axiom asserting the existence of singletons \{a\} for any a is included to support these constructions. This setup exploits the totality of V to avoid paradoxes while enabling the generation of all NF sets.[5][6]Central to these finite versions is the "T operation," introduced as a primitive that simulates type raising for tagging elements with implicit levels. Defined as T(X) = \{ \{z\} \mid z \in X \}, or more precisely in the presence of V as T(X) = \{y \in V \mid \exists z \in X (y = \{z\})\}, the T operation wraps elements in singletons to distinguish "types" without explicit typing, preserving stratification in derived formulas. This allows finite axioms to bootstrap higher-level comprehensions; for instance, applying T iteratively corresponds to ascending type levels in the underlying typed theory. The operation is crucial for proving the existence of sets at successive "ranks" and underpins cardinal arithmetic in NF.[3][6]The equiconsistency of Hailperin's finite axiomatization with the standard infinite schema of NF follows from the fact that the nine instances suffice to derive arbitrary stratified comprehensions. A proof sketch involves induction on the complexity of stratified formulas: base cases are covered directly by the finite axioms, and inductive steps use substitutions (e.g., replacing variables with T-tagged expressions) that maintain stratification, as T increases the type assignment by 1. Ernst Specker established a broader equiconsistency result in 1958, showing that NF (in either formulation) is equiconsistent with Tarski's simple type theory (TST) augmented by the full scheme of typical ambiguity axioms, which allow formulas interpretable at multiple types. This bridges NF's type-free presentation to typed systems, confirming that models of the finite version interpret the infinite schema and vice versa.[3]Compared to the infinite formulation, the finite axiomatization offers greater simplicity for automated theorem proving and metatheoretic analysis, as it reduces NF to a finite list of theorems verifiable in systems like Metamath. However, the infinite schema provides a more uniform and conceptually direct expression of stratified comprehension, avoiding the need to select specific instances. Both versions prove identical theorems, including the existence of V and non-trivial sets, but the finite one highlights NF's suitability for practical implementations while preserving its foundational economy over typed alternatives.[6][3]
Stratified Comprehension
Stratified comprehension is the central axiom scheme of New Foundations (NF), positing that for any stratified formula \Phi in the language of set theory (with the distinguished variable y not free in \Phi), there exists a set z such that \forall y (y \in z \leftrightarrow \Phi(y)). A formula is stratified if there is a function \sigma assigning a natural number (type level) to each variable, satisfying: for every atomic subformula u = v, \sigma(u) = \sigma(v); for every atomic subformula u \in v, \sigma(u) + 1 = \sigma(v); and for complex subformulas, the type is preserved under logical connectives and quantifiers, with the overall formula assignable without contradiction. This condition mimics the type restrictions of simple type theory but applies syntactically to untyped formulas, ensuring well-founded definitions by preventing circular type assignments.[7][8]The formal syntax of stratification in NF involves type levels denoted by ordinals or natural numbers \alpha, where membership x^\alpha \in y^\beta is permitted only if \beta = \alpha + 1. Quantifiers and connectives do not alter types: existential and universal quantifiers bind variables at specified levels, conjunction and disjunction take the maximum type among operands, negation preserves the type of its argument, and the distinguished variable y in comprehension is assigned the type of the resulting set. This syntactic check is decidable and ensures that all instances of the axiom schema produce paradox-free sets, as the type discipline avoids infinite descending membership chains in definitions.[7]A classic example of an unstratified formula is x \notin x, which underlies Russell's paradox: any type assignment \sigma(x) = \alpha for the subformula x \in x requires \alpha + 1 = \alpha, an impossibility. Thus, the comprehension \{x \mid x \notin x\} is blocked in NF. In contrast, alternatives avoiding direct self-reference can be stratified; for instance, the formula \exists y (y \in x \land y \neq x) encounters a similar issue due to conflicting types for y \in x (\sigma(x) = \sigma(y) + 1) and y \neq x (\sigma(y) = \sigma(x)), rendering it unstratified as well. A valid stratified example is x = x, which allows the universal set V = \{x \mid x = x\} with uniform type \alpha for x.[7][8]The stratification condition in NF facilitates limited impredicativity, distinguishing it from predicative systems like ramified type theory. While full impredicativity would allow quantifying over the totality of sets at any level, NF permits impredicative comprehensions that respect type differences, such as the power set \mathcal{P}(x) = \{ z \mid \forall y (y \in z \to y \in x ) \}, stratified by assigning \sigma(z) = \sigma(x), \sigma(y) = \sigma(x) - 1. This enables NF to internalize constructions like Cartesian products and function spaces impredicatively, provided the formula's type structure aligns, thus balancing expressive power with paradox avoidance.[7]
Variants and Extensions
NFU with Urelements
NFU, or New Foundations with Urelements, is a variant of Quine's New Foundations (NF) set theory developed by Ronald Jensen in 1969 to incorporate urelements, or atoms, which are non-set objects devoid of members. This modification addresses challenges in modeling NF by permitting a universe that includes both sets and these atomic elements, thereby facilitating the construction of consistent models. Unlike pure set theories, NFU treats urelements as primitive entities that behave like empty collections but can be distinct from one another and from the empty set.[3]The key adjustment in NFU lies in the axiom of extensionality, which is weakened to accommodate urelements while preserving the core structure of NF. Specifically, the axiom states:\forall x \forall y \left( \forall z (z \in x \leftrightarrow z \in y) \to x = y \lor (\text{$x$ and $y$ are both urelements}) \right)This formulation ensures that sets remain extensional—uniquely determined by their members—but allows multiple urelements to coexist despite sharing the same (empty) extension. The axiom of stratified comprehension, which permits the formation of sets via stratified formulas, remains unchanged from NF, enabling the theory to support a rich hierarchy of sets built upon the urelements. Urelements thus serve as foundational atoms, analogous to individuals in type theory, and enable the theory to model scenarios where not all objects are sets, such as in permutation models inspired by Fraenkel-Mostowski constructions.Jensen demonstrated the consistency of NFU relative to a weak subsystem of second-order arithmetic, constructing a countable model using a hierarchy of types with urelements at the base level. This proof highlights the role of urelements in simplifying model theory, as they allow for symmetric extensions and permutations that preserve the axioms without leading to paradoxes inherent in stronger extensionality. NFU is equiconsistent with NF, achieved through an interpretation that maps urelements in an NFU model to distinct singletons in an NF model, thereby collapsing the urelements into pure sets while maintaining the stratified comprehension structure.The inclusion of urelements in NFU not only aids in consistency proofs but also extends its applicability to independence results via permutation methods, where groups of permutations act on urelements to generate models satisfying additional axioms like infinity or choice. These permutation models of NFU provide insights into the theory's flexibility, allowing for the exploration of set-theoretic properties in a controlled manner with atomic supports, distinct from the pure-set environment of NF.[9]
Tangled Type Theory
Tangled type theory (TTT) is a many-sorted first-order theory designed to capture the structure of Quine's New Foundations (NF) set theory through a hierarchy of types indexed by non-negative integers, where membership relations are restricted to elements of strictly lower types.[10] In TTT, each variable is assigned a type, with equality defined only between objects of the same type and membership well-formed only from lower to higher types, allowing objects to be extensional across multiple lower types simultaneously.[10] This "tangling" arises from a relation that permits the same object to participate in extensions of different types, enabling types to intersect in their membership interpretations unlike in simple typed theories where types are disjoint.[11]The interpretation of NF within TTT maps stratified formulas of NF to well-formed, type-safe expressions in the tangled hierarchy, where a stratification function assigns types to variables such that membership increases type strictly.[10] Specifically, for a stratified formula φ in NF, the corresponding TTT formula φ_s uses a strictly increasing type assignment s, ensuring that comprehension for φ in NF translates to the existence of a set of type s(n) whose extension matches the stratified condition across relevant lower types.[10] This mapping preserves the logical structure, with NF's extensionality axiom directly corresponding to TTT's multi-sorted extensionality axiom, which equates objects of the same type if they have identical extensions in every lower type.[10]A key result is that NF is interpretable in TTT, with the interpretation preserving the stratified comprehension scheme of NF, thereby establishing the equiconsistency of the two theories.[10] Models of NF can be converted to models of TTT by creating disjoint copies of the universe labeled by types, with membership induced naturally between copies of appropriate ranks, and conversely, TTT models yield NF models through quotienting by the tangling relations.[10] This interpretability highlights TTT as a typed framework that embeds NF's untyped comprehension while enforcing stratification via type constraints.Unlike NFU, which incorporates urelements to facilitate consistency proofs and model external atoms, TTT operates solely with pure sets and eschews urelements, relying instead on the tangling mechanism to accommodate complex structures such as sets that effectively model self-membership through supertypes and intersecting extensions.[10] In TTT, self-referential phenomena arise because an object of type τ can include, via its extension in a supertype τ*ι, structures that reference prior types in a looped manner, without direct same-type membership.[11] This pure-set approach distinguishes TTT as a direct analog for NF's stratified universe, emphasizing type intersections over atomic additions.[10]
Other Related Systems
NF3 represents an extension of New Foundations that broadens the stratification condition for comprehension, allowing formulas to be typed using three distinct type symbols rather than the standard two. Introduced by V.N. Grishin in 1969, this variant enables the formation of sets via comprehension for more complex stratified predicates, such as those requiring an additional level of typing to avoid paradoxes while expanding the universe of constructible sets beyond what standard NF permits. Grishin demonstrated the consistency of NF3 relative to a third-order typed set theory with an axiom of ambiguity, establishing that NF3 avoids inconsistency while providing greater expressive power for set constructions.[12]Systems incorporating global choice in NF-style frameworks augment the theory with an axiom asserting the existence of a choice function applicable to all non-empty families of sets, including those indexed by the universal set V. Unlike standard NF, which refutes the axiom of choice due to the availability of sets like the Russell class, variants such as NFU admit global choice consistently relative to Mac Lane set theory, enabling the development of well-behaved cardinalities and ordinal structures without leading to contradiction. This addition addresses limitations in original NF by supporting analytical tools like transfinite induction and measure theory, which are hindered in the choice-free base theory.[13]These systems collectively address gaps in the original NF, particularly in handling structures analogous to proper classes through enhanced stratification or choice principles; for instance, NF3's triple typing facilitates definitions that approximate class-like collections within a set universe, while global choice in NFU variants bridges to ZFC-like mathematics by ensuring selectable elements across all sets, including V.[14]
Historical Development
Origins in Quine's Work
New Foundations (NF) originated with Willard Van Orman Quine's seminal 1937 paper, "New Foundations for Mathematical Logic," published in The American Mathematical Monthly.[15] In this work, Quine sought to establish a robust axiomatic foundation for mathematical logic amid the foundational crises precipitated by set-theoretic paradoxes, particularly Russell's paradox, which revealed contradictions in naive set theory. Quine drew inspiration from Bertrand Russell and Alfred North Whitehead's Principia Mathematica (1910–1913), which addressed these paradoxes through a ramified theory of types imposing strict hierarchies on logical expressions to prevent self-reference. However, Quine viewed this type-theoretic approach as overly restrictive and cumbersome, limiting expressive power and complicating proofs unnecessarily. His system aimed to retain the intuitive freedom of unstratified comprehension while avoiding paradoxes via a more streamlined mechanism.Quine's initial axioms centered on extensionality—asserting that sets are determined by their members—and a novel stratified comprehension schema, which permits the existence of sets defined by formulas that can be assigned consistent type levels without vicious circularity. This stratification condition requires that variables in the defining formula maintain uniform "types" across iterations of membership relations, effectively blocking self-referential constructions like the Russell set while allowing a universal set and broad expressive capacity. Positioned as a compromise between the unrestricted comprehension of naive theories (leading to paradoxes) and the rigid typing of Principia Mathematica, NF's schema enables the formation of most mathematically useful sets without the full overhead of types, fostering a simpler logical framework. Quine argued that this approach adheres to Russell's "vicious circle principle" by prohibiting definitions that presuppose the totality being defined, thus providing a philosophically motivated alternative to both type theory and axiomatic systems like Zermelo's.[15]Upon publication, Quine's NF garnered interest among logicians for its elegance and potential to simplify foundational mathematics, with early explorations confirming its ability to derive basic arithmetic and set operations. However, it faced immediate criticisms regarding the ad hoc nature of the stratification restriction, which some viewed as an arbitrary syntactic imposition lacking deeper ontological justification, merely patching over paradoxes without resolving underlying issues of self-reference. Critics, including figures in the logical community, questioned whether the system's consistency could be proven without appealing to external assumptions, highlighting the stratification's departure from intuitive set formation principles. Despite these concerns, Quine's framework stimulated ongoing debate and refinements in alternative set theories.[16]
Key Developments and Contributors
In 1953, Ernst Specker published a groundbreaking result showing that the axiom of choice is false in New Foundations, as it leads to a contradiction when applied to cardinal numbers defined within the theory. This disproof also established that NF proves the axiom of infinity, since the axiom of choice holds for finite sets in NF.Specker's proof made essential use of the universal set V = {x | x = x}, which exists in NF by stratified comprehension and serves as a set containing all sets, a feature that distinguishes NF from well-founded set theories like ZFC. He further showed that the generalized continuum hypothesis fails in NF.A finite axiomatization of NF was later developed by Theodore Hailperin in 1944, reducing the infinite comprehension scheme to a finite set of axioms, which facilitated formal implementations and consistency investigations.In 1969, Ronald B. Jensen advanced the study of NF variants by proving the consistency of NFU (New Foundations with urelements), using Fraenkel-Mostowski permutation models to construct a model of NFU from a model of ZFC. This relative consistency result was the first major progress toward understanding the consistency of systems related to NF, though Jensen's work remained unpublished.Jensen's models demonstrated that NFU supports standard mathematics, including the natural numbers and much of analysis, while avoiding the paradoxes of NF itself. His approach involved urelements to weaken extensionality, allowing sets to be distinguished only by their elements rather than their identity.During the 1980s, William N. Reinhardt contributed to the consistency problem of NF by analyzing automorphisms of models of type theory, extending Specker's 1962 criterion that NF is consistent if and only if there exists a model of ambiguous type theory admitting type-shifting automorphisms. Reinhardt's investigations clarified the structural requirements for such automorphisms, providing partial insights into potential models of NF.[17]Reinhardt's work emphasized the role of symmetry in type-theoretic models, showing that certain automorphism groups suffice to interpret NF's stratified comprehension without contradiction. His results, though not leading to a full consistency proof, influenced subsequent research on NF's models.[18]In 1998, M. Randall Holmes published Elementary Set Theory with a Universal Set, a comprehensive exploration of NFU and its connections to tangled type theory, a typed system equivalent to NFU. Holmes detailed how NFU admits a universal set and supports Cartesian closed categories, making it suitable for higher-order logic and type theory applications.Holmes' book synthesized Jensen's models with tangled types, showing that NFU interprets much of classical mathematics while maintaining a simple axiomatic basis, and it served as a key reference for later formal verifications of NF-related systems.
Evolution to Modern Variants
During the 1990s and 2000s, research on New Foundations increasingly focused on NFU, a variant incorporating urelements to weaken extensionality, which facilitated the construction of models and addressed some of NF's modeling challenges.[3] This shift emphasized NFU's practicality for exploring NF's implications without the full strength of strict extensionality.[19]Randall Holmes played a central role in these developments, authoring comprehensive treatments of NFU, including the book Elementary Set Theory with a Universal Set (1998) and creating the Watson theorem prover, which demonstrates NFU's equivalence to untyped lambda calculus.[20] Holmes also collaborated on extensions like the TRC system with Thomas Jech, using automated proof tools to investigate NFU's properties.[1]A major gap in NF was the absence of a consistency proof, which remained an open problem for decades, while NFU's consistency was established by Ronald Jensen in 1969 and shown to be equiconsistent with a weak subsystem of ZFC. In a breakthrough, Holmes provided a proof of NF's consistency in 2015 by reducing it to the consistency of tangled type theory relative to a weak variant of ZFC with urelements, with partial formalization in the Lean theorem prover achieved by Sky Wilshaw in 2024.[2][21]NF and NFU have found modern applications in alternative foundations, particularly category theory, where Solomon Feferman proposed NFU-based systems for handling unlimited categories and enriched structures.[22] These variants support conceptual frameworks for toposes and functor categories without relying on well-founded sets.[23]As of 2025, research continues on permutation models for NF and NFU to probe choice principles and symmetries, alongside higher-order variants like tangled type theory for broader foundational inquiries.[24][25]
Set Constructions
Ordered Pairs and Relations
In New Foundations (NF), the ordered pair \langle x, y \rangle is defined using a type-level construction attributed to Quine, such as the Quine-Rosser definition \langle x, y \rangle = \{ x \} \cup \{ \{x, y\} \mid y \notin x \} or equivalent abstractions that ensure the term behaves as a unified entity at the same type level as its components. [3] This differs from the standard Kuratowski definition \{\{x\}, \{x, y\}\}, which raises the type by 2 and is not type-neutral. The NF definition allows the formula \langle x, y \rangle = z to be stratified with all free variables x, y, and z assigned the same type level \sigma, where atomic formulas satisfy u \in v implying \sigma(u) + 1 = \sigma(v) and u = v implying \sigma(u) = \sigma(v). Specifically, the abstraction term for the pair is homogeneous at type \sigma, facilitating its use in higher-level constructions without type mismatches.Binary relations in NF are sets of such ordered pairs, formalized via stratified comprehension as R = \{ z \mid \exists x \exists y (z = \langle x, y \rangle \land \phi(x, y)) \}, where \phi(x, y) is a stratified formula.[3] The stratification of the defining formula \exists x \exists y (z = \langle x, y \rangle \land \phi(x, y)) follows from the type-neutral property of the ordered pair definition, as the equality z = \langle x, y \rangle preserves type equality for x, y, and z when they are intended at the same level, and \phi is assumed stratified. Thus, any stratified predicate \phi yields a relation R as a legitimate set, enabling the representation of arbitrary binary relations—such as equality—directly within NF's axiomatic framework. For relations involving type shifts, like membership, bound variables are assigned differing types (e.g., \sigma(x) = i, \sigma(y) = i+1), and the pair abstraction accommodates this via the overall formula's stratification.Functions emerge as particular relations that are left-total (defined for every element in a domain) and right-unique (each domain element maps to exactly one codomain element).[3] For a function f, its graph is the relation G_f = \{ \langle x, y \rangle \mid x \in A \land y \in B \land y = f(x) \}, where the formula defining membership is stratified if f(x) = y assigns types consistently, typically with x and y at the same level and \langle x, y \rangle neutral thereto. Total functions require the domain A to be specified such that the comprehension formula covers all elements, while injective mappings are those where the relation additionally satisfies \langle x_1, y \rangle \in G_f \land \langle x_2, y \rangle \in G_f \to x_1 = x_2, again stratified without issue.[3]The stratified nature of these constructions proves that NF supports binary relations and functions without type-level inconsistencies, as all components—pairs, relations, and functional restrictions—adhere to consistent type assignments for their free and bound variables, bypassing the rigid hierarchies of type theories while still preventing paradoxes through comprehension restrictions. For instance, the membership relation itself, \{ \langle x, y \rangle \mid x \in y \}, is stratified by assigning bound x type i and y type i+1, with z at i+1 or adjusted per the pair definition, confirming NF's capacity for foundational relational structures.[3][2]
Natural Numbers and Infinity
In New Foundations (NF), the axiom of infinity asserts the existence of an inductive set I, which contains the empty set \emptyset and is closed under the successor operation defined by x \mapsto x \cup \{x\}.[13] Specifically, there exists a set I such that \emptyset \in I and \forall x \in I \, (x \cup \{x\} \in I).[26] This axiom is not primitive in NF but is provable as a theorem, with Ernst Specker's 1953 demonstration establishing that NF implies the existence of infinite sets by showing the negation of the axiom of choice for finite sets, which presupposes infinity.[26]The set of natural numbers, denoted \omega, is defined inductively as the smallest inductive set: \omega = \bigcap \{ I \mid \emptyset \in I \land \forall x \in I \, (x \cup \{x\} \in I) \}.[13] This construction ensures \omega is the intersection of all inductive sets and has no infinite descending membership chains, making it well-founded in the sense of finite descending sequences.[3] The elements of \omega are the von Neumann ordinals: $0 = \emptyset, $1 = \{ \emptyset \}, $2 = \{ \emptyset, \{ \emptyset \} \}, and so on, with each successor n+1 = n \cup \{n\}. NF proves the existence of \omega directly from its axioms of extensionality and stratified comprehension.[26]The structure (\omega, \emptyset, s), where s(x) = x \cup \{x\} is the successor function, embeds Peano arithmetic in NF.[3] The Peano axioms are satisfied: \emptyset is not a successor, distinct numbers have distinct successors, and \omega is closed under successor with no additional elements. Addition and multiplication on \omega are defined via recursion, leveraging the inductive nature of \omega. For addition, the functions are specified by the schemes:m + 0 = m, \quad m + s(n) = s(m + n)for all m, n \in \omega. Similarly, for multiplication:m \times 0 = 0, \quad m \times s(n) = (m \times n) + m.These recursive definitions are justified in NF by stratified comprehension, allowing the construction of the required function sets.[3] The arithmetic operations thus inherit the standard properties, such as commutativity and distributivity, provable by induction on \omega.NF further proves that \omega is Dedekind-infinite, meaning there exists an injection from \omega to a proper subset of itself, such as the map n \mapsto s(n).[26] This property underscores the infinite cardinality of \omega without relying on the axiom of choice, which NF refutes.[3]
Large Sets and Cardinals
In New Foundations (NF), the universal set V exists as the set defined by the stratified formula \{x \mid x = x\}, which encompasses all sets due to the axiom of stratified comprehension.[3] This construction assigns type 0 to the variable x, ensuring stratification, and thus V contains every entity as a member, serving as the totality of the set-theoretic universe.[3]The power set \mathcal{P}(x) of a set x is constructed via the stratified comprehension axiom using the formula \{y \mid \forall z (z \in y \to z \in x)\}.[3] Stratification is achieved by assigning type k to x, type k+1 to y, and type k+1 to z, allowing the relative types to align properly (with the membership relation \in treated as increasing type by 1).[3] This ensures that \mathcal{P}(x) exists as a set comprising all subsets of x.[3]Cardinalities in NF are defined through equinumerosity, where two sets have the same cardinality if there exists a bijection between them, following Frege's classical approach.[3] Infinite cardinals, denoted as alephs, are constructed analogously via ordinal-like structures and bijections, but the presence of the universal set V implies a maximal cardinality, as |V| bounds all others.[27]In NF, Cantorian sets are those equinumerous to their power sets, a property that contrasts with Zermelo-Fraenkel set theory (ZFC), where no set equals its power set in cardinality.[3] The universal set V exemplifies this, satisfying |V| = |\mathcal{P}(V)| due to the stratified framework permitting such bijections.[27] This feature arises from the theory's tolerance of non-well-founded sets and the absence of a strict cumulative hierarchy.[3]
Cartesian Closure and Function Spaces
In New Foundations (NF), the Cartesian product of two sets x and y, denoted x \times y, is constructed as the set of all ordered pairs \langle a, b \rangle where a \in x and b \in y. This relies on a stratified definition of ordered pairs, such as Quine's type-level pairing, which ensures the comprehension formula z \in x \times y \iff \exists a \in x \, \exists b \in y \, (z = \langle a, b \rangle) can be assigned consistent types (e.g., type i to a and b, type i to z when same-level). The stratification condition is satisfied because the atomic formulas involving membership and equality align under this typing, allowing the axiom of stratified comprehension to guarantee the existence of x \times y as a set for any sets x and y.[28][29]The function space y^x, representing the set of all functions from x to y, is defined as a subset of the power set \mathcal{P}(x \times y) consisting of those relations f that are functional with domain exactly x and range contained in y. Formally, this is given by the stratified comprehension for the formula f \in y^x \iff f \subseteq x \times y \land \forall u \in x \, \exists ! v \in y \, (\langle u, v \rangle \in f), provided the formula admits a stratification (e.g., assigning type i to elements of x and y, type i to pairs and f). However, for arbitrary sets x and y, the required type assignments for quantifiers like \forall u \in x and \exists u \in x may conflict, preventing stratification and thus the existence of y^x as a set in general. As a result, while NF supports the construction of Cartesian products universally, it does not prove full Cartesian closure, meaning the category of sets and functions in NF lacks exponential objects for all pairs of sets.[30][28]Despite the absence of general exponentiation, NF permits the construction of specific function spaces when the defining formula is stratified, enabling support for higher-order mathematics in restricted contexts. For instance, the set \omega^\omega of functions from the set of natural numbers \omega to itself exists in NF, as the comprehension formula aligns under a uniform typing (treating elements of \omega at base type i, pairs at i, and functions at i). This construction, along with finite products, allows NF to interpret typed lambda calculi and simple type theory via its equivalence to a tangled type theory, where function types are built hierarchically without paradoxes.[29]
Paradox Resolution
Handling Russell's Paradox
Russell's paradox arises in naive set theory from the attempt to comprehend the set R = \{ x \mid x \notin x \}, which leads to a contradiction: assuming R \in R implies R \notin R, and assuming R \notin R implies R \in R.[3][31]In New Foundations (NF), this paradox is avoided through the axiom of stratified comprehension, which permits the formation of sets only from stratified formulas—those assignable to a type function \sigma where, for any subformula u \in v, \sigma(v) = \sigma(u) + 1, and atomic formulas other than membership receive type 0 or match variable types. The defining formula x \notin x for the Russell set is unstratified, as no such \sigma exists: the outer x would require type i, but the inner x in x \in x (negated) demands type i - 1, creating an inconsistency since negation preserves type. Thus, R cannot be comprehended as a set in NF, blocking the paradoxical reasoning.[3]Stratified alternatives allow safe definitions approximating aspects of the Russell class without self-reference. For instance, the formula \{ x \mid \exists y (y \in x \land y \neq x) \} is stratified by assigning \sigma(x) = i+1, \sigma(y) = i, ensuring membership relates consecutive types while the inequality matches types appropriately, yielding a proper class rather than a paradoxical set. Such constructions highlight NF's restriction to well-typed expressions.[3]This mechanism renders NF sets inherently "type-safe," implicitly enforcing type distinctions without an explicit hierarchy, thereby resolving self-referential paradoxes while permitting a universal set V = \{ x \mid x = x \}.[3]
Addressing Cantor's Paradox
Cantor's paradox arises in naive set theory from the existence of a universal set V, the set of all sets, which leads to a contradiction via Cantor's theorem. Cantor's theorem states that for any set A, there is no surjection from A onto its power set P(A), implying |A| < |P(A)|. However, if V exists, then P(V) \subseteq V, so |P(V)| \leq |V|, while the injection x \mapsto \{x\} from V to P(V) suggests |V| \leq |P(V)|, but Cantor's theorem would require |V| < |P(V)|, yielding |V| < |V|, a contradiction.[3]In New Foundations (NF), the universal set V = \{x : x = x\} exists by stratified comprehension, as the formula x = x is stratified with type level 0. Unlike Zermelo-Fraenkel set theory (ZF), where no universal set exists, NF accommodates V without immediate contradiction because the power set P(V) = \{y : \forall z (z \in y \leftrightarrow z \in V)\} also equals V. This equality holds since every subset of V is itself a set (hence in V), and V \subseteq P(V) via the empty set and singletons, establishing a bijection. The key restriction is NF's stratified comprehension axiom, which only allows sets defined by stratified formulas—those assignable consistent type levels where membership u \in v raises the type of u by 1 relative to v. This prevents unstratified self-referential definitions that fuel paradoxes.[7][3]NF resolves the paradox by failing to prove Cantor's theorem in full generality; the standard diagonal argument proof does not apply to arbitrary sets, particularly V. The diagonal construction attempts to define a set D = \{x \in A : x \notin f(x)\} for a purported surjection f: A \to P(A), but the formula x \in A \land x \notin f(x) is unstratified: assigning type \sigma(x) = k for x \in A requires \sigma(x) = \sigma(f(x)) + 1 for x \notin f(x), leading to inconsistent type levels since f(x) \subseteq A implies \sigma(f(x)) = k + 1. Thus, no such D exists via comprehension for general A, blocking the proof that no surjection exists. For V, an injection V \to P(V) via singletons exists, but no surjection does, as any function f: V \to V (since P(V) = V) cannot cover all subsets due to stratification limits.[3][7]Sets equaling their power sets, termed Cantorian sets, are provable in NF, with V as a prime example. A set A is Cantorian if there is a bijection between A and P(A); for V, the identity function serves as this bijection given P(V) = V. More generally, NF proves that the set of natural numbers \mathbb{N} is Cantorian, as |\mathbb{N}| = |P(\mathbb{N})| via explicit bijections, contrasting ZF where no finite or infinite set equals its power set. This demonstrates NF's accommodation of "large" cardinalities without explosion.[7]The diagonal argument adapts in NF to show that stratified functions from V to P(V) form proper subsets of P(V). Consider a stratified function f: V \to P(V); its graph is stratified, but extending it to a surjection fails because potential diagonal elements like \{x \in V : x \notin f(x)\} are unstratified. Thus, the image f``V is a proper subclass of P(V), ensuring no bijection beyond the identity while maintaining P(V) = V. This stratification enforces that while V injects into itself via singletons, full surjectivity onto subsets is curtailed, avoiding cardinality contradictions.[7][3]
Resolving Burali-Forti Paradox
The Burali-Forti paradox arises in naive set theory from the assumption that the collection Ord of all ordinal numbers forms a set, which would then itself be an ordinal greater than any of its elements, leading to Ord ∈ Ord and a violation of well-ordering properties.[3]In New Foundations (NF), this paradox is resolved through the stratified comprehension axiom, which requires formulas to respect type levels assigned to variables, ensuring that membership relations align with increasing types (σ(x) + 1 = σ(y) for x ∈ y). Ordinals in NF are defined as equivalence classes of well-orderings under isomorphism, and the defining formula is stratified, allowing the existence of the set Ω of all ordinals. However, these are inherently stratified: a well-ordering of type i has order type i + 4, placing ordinals at distinct type levels.[7]The T operation provides a key mechanism for type-raising ordinals while preserving order structure, defined for an ordinal λ as the order type of the well-ordering ⟨X₁, R₁⟩, where X is the domain of a representative well-ordering ⟨X, R⟩ of λ, X₁ = {{x} | x ∈ X}, and R₁ = {⟨{x}, {y}⟩ | ⟨x, y⟩ ∈ R}. This construction encodes the original ordering using singletons, effectively raising the type by four levels and avoiding self-referential cycles that could lead to paradoxical inclusions.[32]As a result, although the set Ω of all ordinals exists, the order type of Ω under the ordinal ordering ≤_ord is T⁴(Ω), and T⁴(Ω) < Ω, defusing the paradox by showing that Ω is not greater than itself in terms of order type. The universal set V functions as an "ordinal" in a tangled sense, where the membership relation induces a well-ordering on V, but the stratified types introduce non-standard tangles without undermining consistency.[7][3]
Consistency and Models
Models of NF and NFU
Jensen demonstrated the consistency of NFU in 1969 by constructing a model using the Fraenkel-Mostowski permutation method on a universe of Zermelo-Fraenkel set theory with atoms (ZFA), where the atoms serve as urelements. In this construction, the model comprises the hereditarily symmetric sets with respect to a group of permutations acting on the urelements, ensuring that the stratified comprehension axiom and weakened extensionality hold while preserving key set-theoretic structures like infinity. This approach yields a countable model of NFU + Infinity + Choice if the ambient ZFA model satisfies those axioms, highlighting the flexibility of permutation models in capturing NFU's stratified nature.A canonical or universal model for NFU arises from an HOD-like structure, consisting of the class of hereditarily ordinal-definable sets relative to a base model of ZFA equipped with urelements.[33] This construction parallels the hereditarily ordinal-definable (HOD) class in ZFC, providing a transitive inner model where sets are definable using ordinal parameters and permutations, thus supporting NFU's axioms without introducing inconsistencies from full extensionality.[3] Such models allow for the interpretation of strong axioms of infinity within NFU, extending its consistency strength while maintaining definability.[34]An explicit model of full NF has been constructed by Randall Holmes in 2015 (refined through 2025), using a model of tangled type theory (TTT); NF is equiconsistent with NFU augmented by the axiom of infinity, as established by adapting Jensen's permutation techniques to eliminate urelements in a stratified manner. This relative consistency relies on interpreting NF's strong extensionality within NFU models via ambiguity schemes, confirming that NF's proof power does not exceed that of simple type theory with infinity.[35] The proof has been partially formalized in the Lean proof assistant by Sky Wilshaw as of 2024.[21]NFU models admit an interpretation as Tarski universes in the context of type theory, where the universe of discourse functions as a typed hierarchy of sets and urelements, with comprehension stratified by types to avoid paradoxes. This perspective aligns NFU's structure with cumulative type theories, treating urelements as base types and sets as higher-type constructors, thereby embedding NFU's semantics into a framework of self-contained universes.[10]
Consistency Strength Hierarchy
The consistency strength of New Foundations (NF) and its variant NFU (New Foundations with urelements) lies well below that of Zermelo-Fraenkel set theory with Choice (ZFC), positioning both systems as relatively weak in the hierarchy of axiomatic set theories. NFU, introduced by Jensen in 1969, has a consistency strength weaker than that of Peano arithmetic, allowing its consistency to be established without invoking full replacement or power set axioms from ZFC. Adding the axiom of infinity and choice to NFU yields a system equiconsistent with Mac Lane set theory (also known as structured sets) and the elementary theory of the category of sets (ETCS), which aligns with the strength of Zermelo set theory (Z without replacement). This extension supports a robust development of mathematics but falls short of proving the existence of certain large ordinals like \aleph_\omega that ZFC handles routinely.[36]In contrast, the original NF system, proposed by Quine in 1937, remained of undetermined consistency until Holmes' 2015 proof. Randall Holmes established that NF is consistent relative to Zermelo set theory (Z) via a reduction to the consistency of tangled type theory (TTT), a typed system whose strength matches Zermelo set theory with bounded separation and infinity. Thus, Con(NF) follows from Con(Z) and does not require stronger assumptions like replacement schemes. The proof was refined and partially formalized in Lean by Sky Wilshaw as of 2024. NF proves the axiom of infinity but disproves the axiom of choice, and its models feature non-standard set-theoretic structures without the cumulative hierarchy of ZFC. While NFU provides a lower bound for NF's strength (since NFU is interpretable in NF), the equiconsistency with TTT + infinity places NF above basic arithmetic but below full ZFC.[19][2]The following table summarizes the known consistency strengths of NF, NFU, and related systems relative to established benchmarks, focusing on lower and upper bounds without invoking large cardinals, as neither NF nor NFU reaches such levels (e.g., no implications for the continuum hypothesis or inaccessibles).
Theory
Lower Bound
Upper Bound
Key Reference(s)
NFU
Finite set theory
Peano arithmetic (PA)
Jensen (1969)
NFU + Infinity + Choice
Second-order arithmetic
Zermelo set theory (Z)
Holmes (1995)
NF
TST + Infinity
Zermelo set theory (Z)
Holmes (2015)
ZFC
ZFC
ZFC + inaccessible cardinal
Gödel (1930)
As of 2025, the exact consistency strength of NF is resolved to align with Zermelo set theory, though fine-grained comparisons (e.g., precise fragments of replacement needed for TTT models) remain subjects of ongoing refinement. No results link NF's consistency to advanced phenomena like 0^# or Reinhardt cardinals, which pertain to stronger extensions of ZFC or constructive set theories like CZF.[36]
Automorphisms and Structural Properties
In New Foundations with urelements (NFU), Reinhardt's automorphism j provides a non-trivial automorphism of the universe V, defined as a one-to-one map from the collection of singletons P_1(V) to the power set P(V), satisfying j(\{B\}) = \{ j(\{A\}) \mid A \in B \} for any set B.[37] This automorphism also functions as an endomorphism, mapping P_1(V) into P(V) via \mathrm{Endo}(\{B\}) = \{ \mathrm{Endo}(\{A\}) \mid A \in B \}, and its consistency with NFU axioms is provable.[37]A key property of j is its action on urelements, the non-set atoms in NFU, where it permutes them non-trivially, potentially leaving no urelement fixed in certain interpretations, while assigning set-theoretic structure to atoms through j(\{a\}) to enable stratified membership relations like x \, E \, y if j(\{x\}) \in y.[37] Meanwhile, j fixes all sets pointwise, including those without urelements, preserving their membership structure and distinguishing them from urelements in the model.[37] This fixing behavior implies that the universe V coincides with the class of hereditarily ordinal-definable sets (HOD), as every element is definable using ordinal parameters under the automorphism's symmetry.[37]The presence of j underscores NFU's self-sufficiency, allowing the theory to develop mathematics internally through a pseudo-membership relation \epsilon that codes NFU axioms without relying on external assumptions from other set theories like ZFC; this enables consistent extensions such as the axiom of choice while maintaining the theory's internal coherence.[37] On ordinals, j acts rigidly, fixing them pointwise and preserving their order as the identity map, ensuring ordinal structures remain invariant under the automorphism.[37]Furthermore, j generates a group of automorphisms that act as permutations on V, particularly permuting urelements and levels of the cumulative hierarchy in interpretations like Z₀, where it serves as an external automorphism to support NFU's stratified comprehension.[37] This permutation group structure highlights the symmetric properties inherent to NFU models, facilitating the theory's non-well-founded yet consistent framework for set-theoretic constructions.[37]