In mathematical logic, New Foundations (NF) is a non-well-founded, finitely axiomatizable set theory conceived by Willard Van Orman Quine as a simplification of the theory of types of Principia Mathematica.
Definition The well-formed formulas of NF are the standard formulas of propositional calculus with two primitive predicates equality ( = {\displaystyle =} ) and membership ( ∈ {\displaystyle \in } ). NF can be presented with only two axiom schemata:
Extensionality: Two objects with the same elements are the same object; formally, given any set A and any set B, if for every set X, X is a member of A if and only if X is a member of B, then A is equal to B. A restricted axiom schema of comprehension: { x ∣ ϕ } {\displaystyle \{x\mid \phi \}} exists for each stratified formula ϕ {\displaystyle \phi } . A formula ϕ {\displaystyle \phi } is said to be stratified if there exists a function f from pieces of ϕ {\displaystyle \phi } 's syntax to the natural numbers, such that for any atomic subformula x ∈ y {\displaystyle x\in y} of ϕ {\displaystyle \phi } we have f(y) = f(x) + 1, while for any atomic subformula x = y {\displaystyle x=y} of ϕ {\displaystyle \phi } , we have f(x) = f(y).
Finite axiomatization NF can be finitely axiomatized. One advantage of such a finite axiomatization is that it eliminates the notion of stratification. The axioms in a finite axiomatization correspond to natural basic constructions, whereas stratified comprehension is powerful but not necessarily intuitive. In his introductory book, Holmes opted to take the finite axiomatization as basic, and prove stratified comprehension as a theorem. The precise set of axioms can vary, but includes most of the following, with the others provable as theorems:
… excerpt ends here. Continue reading the full article.
