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 .
123-416: 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: A formula ϕ {\displaystyle \phi } is said to be stratified if there exists
246-521: A , b ) ) = b {\displaystyle \pi _{2}((a,b))=b} (in Holmes' axiomatization of NFU, the comprehension schema that asserts the existence of { x ∣ ϕ } {\displaystyle \{x\mid \phi \}} for any stratified formula ϕ {\displaystyle \phi } is considered a theorem and only proved later, so expressions like π 1 = { ( (
369-457: A , b ) , a ) ∣ a , b ∈ V } {\displaystyle \pi _{1}=\{((a,b),a)\mid a,b\in V\}} are not considered proper definitions). Fortunately, whether the ordered pair is type-level by definition or by assumption (i.e., taken as primitive) usually does not matter. The usual form of the axiom of infinity is based on the von Neumann construction of
492-561: 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 ). NF can be finitely axiomatized . One advantage of such
615-443: A tree whose leaf nodes are variables, constants, function constants or predicate constants and whose non-leaf nodes are logical operators. This expression can then be determined by doing an inorder traversal of the tree. Variable-binding operators are logical operators that occur in almost every formal language. A binding operator Q takes two arguments: a variable v and an expression P , and when applied to its arguments produces
738-407: A wildcard character that stands for an unspecified symbol. In computer programming , the term free variable refers to variables used in a function that are neither local variables nor parameters of that function. The term non-local variable is often a synonym in this context. An instance of a variable symbol is bound , in contrast, if the value of that variable symbol has been bound to
861-477: A contradiction when A = V {\displaystyle A=V} . Of course there is an injection from P ( V ) {\displaystyle P(V)} into V {\displaystyle V} since V {\displaystyle V} is the universal set, so it must be that Cantor's theorem (in its original form) does not hold in NF. Indeed, the proof of Cantor's theorem uses
984-402: A different female person. In this example, the variable herself is bound to the noun Jane that occurs in subject position. Indicating the coindexation, the first interpretation with Jane and herself coindexed is permissible, but the other interpretation where they are not coindexed is ungrammatical : The coreference binding can be represented using a lambda expression as mentioned in
1107-423: 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
1230-924: A finite set is not equinumerous with any of its proper subsets), n + 1 = S ( n ) = ∅ {\displaystyle n+1=S(n)=\varnothing } , and each subsequent natural number would be ∅ {\displaystyle \varnothing } too, causing arithmetic to break down. To prevent this, one can introduce the axiom of infinity for NF: ∅ ∉ N . {\displaystyle \varnothing \notin \mathbf {N} .} It may intuitively seem that one should be able to prove Infinity in NF(U) by constructing any "externally" infinite sequence of sets, such as ∅ , { ∅ } , { { ∅ } } , … {\displaystyle \varnothing ,\{\varnothing \},\{\{{\varnothing }\}\},\ldots } . However, such
1353-510: A formula ϕ 1 {\displaystyle \phi _{1}} in the language of the nonstandard model of Zermelo set theory with automorphism j using the definition of membership in the model of NFU. Application of any power of j to both sides of an equation or membership statement preserves its truth value because j is an automorphism. Make such an application to each atomic formula in ϕ 1 {\displaystyle \phi _{1}} in such
SECTION 10
#17328631145601476-608: A formula comes in several parts. First, the set of terms is defined recursively. Terms, informally, are expressions that represent objects from the domain of discourse . The next step is to define the atomic formulas . Finally, the set of formulas is defined to be the smallest set containing the set of atomic formulas such that the following holds: If a formula has no occurrences of ∃ x {\displaystyle \exists x} or ∀ x {\displaystyle \forall x} , for any variable x {\displaystyle x} , then it
1599-722: A formula, then the set { x n ∣ ϕ ( x n ) } n + 1 {\displaystyle \{x^{n}\mid \phi (x^{n})\}^{n+1}\!} exists. In other words, given any formula ϕ ( x n ) {\displaystyle \phi (x^{n})\!} , the formula ∃ A n + 1 ∀ x n [ x n ∈ A n + 1 ↔ ϕ ( x n ) ] {\displaystyle \exists A^{n+1}\forall x^{n}[x^{n}\in A^{n+1}\leftrightarrow \phi (x^{n})]}
1722-402: A formula. The formulas of propositional calculus , also called propositional formulas , are expressions such as ( A ∧ ( B ∨ C ) ) {\displaystyle (A\land (B\lor C))} . Their definition begins with the arbitrary choice of a set V of propositional variables . The alphabet consists of the letters in V along with the symbols for
1845-447: A function where t is an expression. t may contain some, all or none of the x 1 , …, x n and it may contain other variables. In this case we say that function definition binds the variables x 1 , …, x n . In this manner, function definition expressions of the kind shown above can be thought of as the variable binding operator, analogous to the lambda expressions of lambda calculus . Other binding operators, like
1968-572: A further development of mathematics in NFU, with a comparison to the development of the same in ZFC, see implementation of mathematics in set theory . Relations and functions are defined in TST (and in NF and NFU) as sets of ordered pairs in the usual way. For purposes of stratification, it is desirable that a relation or function is merely one type higher than the type of the members of its field. This requires defining
2091-436: A least member, and thus cannot be a set. More concretely, the monotonicity of T implies Ω > T 2 ( Ω ) > T 4 ( Ω ) … {\displaystyle \Omega >T^{2}(\Omega )>T^{4}(\Omega )\ldots } , a "descending sequence" in the ordinals which also cannot be a set. One might assert that this result shows that no model of NF(U)
2214-424: A natural number. The well-formed atomic formulas are x n = y n {\displaystyle x^{n}=y^{n}} and x m ∈ y n {\displaystyle x^{m}\in y^{n}} where m < n {\displaystyle m<n} . The axioms of TTT are those of TST where each variable of type i {\displaystyle i}
2337-420: A new expression Q( v , P ). The meaning of binding operators is supplied by the semantics of the language and does not concern us here. Variable binding relates three things: a variable v , a location a for that variable in an expression and a non-leaf node n of the form Q( v , P ). Note: we define a location in an expression as a leaf node in the syntax tree. Variable binding occurs when that location
2460-417: A precise definition of free variable and bound variable, the following are some examples that perhaps make these two concepts clearer than the definition would: In the expression n is a free variable and k is a bound variable; consequently the value of this expression depends on the value of n , but there is nothing called k on which it could depend. In the expression y is a free variable and x
2583-743: A sequence could only be constructed through unstratified constructions (evidenced by the fact that TST itself has finite models), so such a proof could not be carried out in NF(U). In fact, Infinity is logically independent of NFU: There exists models of NFU where | V | {\displaystyle |V|} is a non-standard natural number . In such models, mathematical induction can prove statements about | V | {\displaystyle |V|} , making it impossible to "distinguish" | V | {\displaystyle |V|} from standard natural numbers. However, there are some cases where Infinity can be proven (in which cases it may be referred to as
SECTION 20
#17328631145602706-596: A set with the largest cardinality . In NF, the universal set V {\displaystyle V} is obviously a set with the largest cardinality. However, Cantor's theorem says (given ZFC) that the power set P ( A ) {\displaystyle P(A)} of any set A {\displaystyle A} is larger than A {\displaystyle A} (there can be no injection (one-to-one map) from P ( A ) {\displaystyle P(A)} into A {\displaystyle A} ), which seems to imply
2829-465: A set, because the membership relation is not a set relation. Some mathematicians have questioned the consistency of NF, partly because it is not clear why it avoids the known paradoxes. A key issue was that Specker proved NF combined with the Axiom of Choice is inconsistent. The proof is complex and involves T-operations. However, since 2010, Holmes has claimed to have shown that NF is consistent relative to
2952-407: A specific value or range of values in the domain of discourse or universe . This may be achieved through the use of logical quantifiers, variable-binding operators, or an explicit statement of allowed values for the variable (such as, "...where n {\displaystyle n} is a positive integer".) A variable symbol overall is bound if at least one occurrence of it is bound. Since
3075-492: A truth value or the numerical result of a calculation, or, more generally, an element of an image set of a function. While the domain of discourse in many contexts is understood, when an explicit range of values for the bound variable has not been given, it may be necessary to specify the domain in order to properly evaluate the expression. For example, consider the following expression in which both variables are bound by logical quantifiers: This expression evaluates to false if
3198-447: A type problem is to replace A {\displaystyle A} with P 1 ( A ) {\displaystyle P_{1}(A)} , the set of one-element subsets of A {\displaystyle A} . Indeed, the correctly typed version of Cantor's theorem | P 1 ( A ) | < | P ( A ) | {\displaystyle |P_{1}(A)|<|P(A)|}
3321-481: A type-respecting manner). Given an embedding of T 0 {\displaystyle T_{0}} into T 1 {\displaystyle T_{1}} (identifying elements of the base "type" with subsets of the base type), embeddings may be defined from each "type" into its successor in a natural way. This can be generalized to transfinite sequences T α {\displaystyle T_{\alpha }} with care. Note that
3444-455: A variable may be said to be either free or bound. Some older books use the terms real variable and apparent variable for free variable and bound variable , respectively. A free variable is a notation (symbol) that specifies places in an expression where substitution may take place and is not a parameter of this or any container expression. The idea is related to a placeholder (a symbol that will later be replaced by some value), or
3567-472: A variable of type n . Type 0 consists of individuals otherwise undescribed. For each (meta-) natural number n , type n +1 objects are sets of type n objects; objects connected by identity have equal types and sets of type n have members of type n -1. The axioms of TST are extensionality, on sets of the same (positive) type, and comprehension, namely that if ϕ ( x n ) {\displaystyle \phi (x^{n})} is
3690-629: A way that each variable x assigned type i occurs with exactly N − i {\displaystyle N-i} applications of j . This is possible thanks to the form of the atomic membership statements derived from NFU membership statements, and to the formula being stratified. Each quantified sentence ( ∀ x ∈ V α . ψ ( j N − i ( x ) ) ) {\displaystyle (\forall x\in V_{\alpha }.\psi (j^{N-i}(x)))} can be converted to
3813-405: A well-ordering in NFU (all well-orderings of NFU are well-orderings in the nonstandard model of Zermelo set theory, but not vice versa, due to the formation of urelements in the construction of the model), and W has type α in NFU, then j ( W ) will be a well-ordering of type T (α) in NFU. In fact, j is coded by a function in the model of NFU. The function in the nonstandard model which sends
New Foundations - Misplaced Pages Continue
3936-694: A whole in the proof. The following are some common variable-binding operators . Each of them binds the variable x for some set S . Many of these are operators which act on functions of the bound variable. In more complicated contexts, such notations can become awkward and confusing. It can be useful to switch to notations which make the binding explicit, such as for sums or for differentiation. Variable-binding mechanisms occur in different contexts in mathematics, logic and computer science. In all cases, however, they are purely syntactic properties of expressions and variables in them. For this section we can summarize syntax by identifying an expression with
4059-452: Is " standard ", since the ordinals in any model of NFU are externally not well-ordered. This is a philosophical question, not a question of what can be proved within the formal theory. Note that even within NFU it can be proven that any set model of NFU has non-well-ordered "ordinals"; NFU does not conclude that the universe V {\displaystyle V} is a model of NFU, despite V {\displaystyle V} being
4182-401: Is a type-level ordered pair , and the order type (equivalence class) β = { S ∣ S ∼ R α } {\displaystyle \beta =\{S\mid S\sim R_{\alpha }\}} is one type higher than R α {\displaystyle R_{\alpha }} . If ( x , y ) {\displaystyle (x,y)}
4305-486: Is a bound variable; consequently the value of this expression depends on the value of y , but there is nothing called x on which it could depend. In the expression x is a free variable and h is a bound variable; consequently the value of this expression depends on the value of x , but there is nothing called h on which it could depend. In the expression z is a free variable and x and y are bound variables, associated with logical quantifiers ; consequently
4428-435: Is a formula in which there are no free occurrences of any variable . If A is a formula of a first-order language in which the variables v 1 , …, v n have free occurrences, then A preceded by ∀ v 1 ⋯ ∀ v n is a universal closure of A . In earlier works on mathematical logic (e.g. by Church ), formulas referred to any strings of symbols and among these strings, well-formed formulas were
4551-454: Is a formula, because it is grammatically correct. The sequence of symbols is not a formula, because it does not conform to the grammar. A complex formula may be difficult to read, owing to, for example, the proliferation of parentheses. To alleviate this last phenomenon, precedence rules (akin to the standard mathematical order of operations ) are assumed among the operators, making some operators more binding than others. For example, assuming
4674-417: Is a model of NFU. Let ϕ {\displaystyle \phi } be a stratified formula in the language of NFU. Choose an assignment of types to all variables in the formula which witnesses the fact that it is stratified. Choose a natural number N greater than all types assigned to variables by this stratification. Expand the formula ϕ {\displaystyle \phi } into
4797-574: Is a natural number n , one gets a model of NFU which claims that the universe is finite (it is externally infinite, of course). If α {\displaystyle \alpha } is infinite and the Choice holds in the nonstandard model of ZFC, one obtains a model of NFU + Infinity + Choice . For philosophical reasons, it is important to note that it is not necessary to work in ZFC or any related system to carry out this proof. A common argument against
4920-460: Is a syntactical sentence in NF(U), and as shown above one can talk about its truth value for specific values of A {\displaystyle A} (e.g. when A = V {\displaystyle A=V} it is false). A set A {\displaystyle A} which satisfies the intuitively appealing | A | = | P 1 ( A ) | {\displaystyle |A|=|P_{1}(A)|}
5043-544: Is a theorem in TST (thanks to the diagonalization argument), and thus also a theorem in NF. In particular, | P 1 ( V ) | < | P ( V ) | {\displaystyle |P_{1}(V)|<|P(V)|} : there are fewer one-element sets than sets (and so fewer one-element sets than general objects, if we are in NFU). The "obvious" bijection x ↦ { x } {\displaystyle x\mapsto \{x\}} from
New Foundations - Misplaced Pages Continue
5166-420: Is a well-ordering of O r d {\displaystyle \mathrm {Ord} } . By definition of ordinals, this well-ordering also belongs to an ordinal Ω ∈ O r d {\displaystyle \Omega \in \mathrm {Ord} } . In naive set theory, one would go on to prove by transfinite induction that each ordinal α {\displaystyle \alpha }
5289-401: Is always less than Ω {\displaystyle \Omega } , the order type of all ordinals. In particular, T 2 ( Ω ) < Ω {\displaystyle T^{2}(\Omega )<\Omega } . Another (stratified) statement that can be proven by transfinite induction is that T is a strictly monotone (order-preserving) operation on
5412-428: Is an axiom where A n + 1 {\displaystyle A^{n+1}\!} represents the set { x n ∣ ϕ ( x n ) } n + 1 {\displaystyle \{x^{n}\mid \phi (x^{n})\}^{n+1}\!} and is not free in ϕ ( x n ) {\displaystyle \phi (x^{n})} . This type theory
5535-399: Is an important variant of NF due to Jensen and clarified by Holmes. Urelements are objects that are not sets and do not contain any elements, but can be contained in sets. One of the simplest forms of axiomatization of NFU regards urelements as multiple, unequal empty sets, thus weakening the extensionality axiom of NF to: In this axiomatization, the comprehension schema is unchanged, although
5658-482: Is at least two types higher than α {\displaystyle \alpha } : The order relation R α = { ( x , y ) ∣ x ≤ y < α } {\displaystyle R_{\alpha }=\{(x,y)\mid x\leq y<\alpha \}} is one type higher than α {\displaystyle \alpha } assuming that ( x , y ) {\displaystyle (x,y)}
5781-431: Is below the node n . In the lambda calculus , x is a bound variable in the term M = λx. T and a free variable in the term T . We say x is bound in M and free in T . If T contains a subterm λx. U then x is rebound in this term. This nested, inner binding of x is said to "shadow" the outer binding. Occurrences of x in U are free occurrences of the new x . Variables bound at
5904-440: Is called quantifier-free . An existential formula is a formula starting with a sequence of existential quantification followed by a quantifier-free formula. An atomic formula is a formula that contains no logical connectives nor quantifiers , or equivalently a formula that has no strict subformulas. The precise form of atomic formulas depends on the formal system under consideration; for propositional logic , for example,
6027-455: Is generally seen as weaker than NF because, in NFU, the collection of all sets (the power set of the universe) can be smaller than the universe itself, especially when urelements are included, as required by NFU with Choice. Jensen's proof gives a fairly simple method for producing models of NFU in bulk. Using well-known techniques of model theory , one can construct a nonstandard model of Zermelo set theory (nothing nearly as strong as full ZFC
6150-588: Is larger than all those ordinals. To formalize the Burali-Forti paradox in NF, it is necessary to first formalize the concept of ordinal numbers. In NF, ordinals are defined (in the same way as in naive set theory ) as equivalence classes of well-orderings under isomorphism . This is a stratified definition, so the set of ordinals O r d {\displaystyle \mathrm {Ord} } can be defined with no problem. Transfinite induction works on stratified statements, which allows one to prove that
6273-565: Is mapped to a variable s ( i ) {\displaystyle s(i)} where s {\displaystyle s} is an increasing function. TTT is considered a "weird" theory because each type is related to each lower type in the same way. For example, type 2 sets have both type 1 members and type 0 members, and extensionality axioms assert that a type 2 set is determined uniquely by either its type 1 members or its type 0 members. Whereas TST has natural models where each type i + 1 {\displaystyle i+1}
SECTION 50
#17328631145606396-465: Is much less complicated than the one first set out in the Principia Mathematica , which included types for relations whose arguments were not necessarily all of the same types. There is a correspondence between New Foundations and TST in terms of adding or erasing type annotations. In NF's comprehension schema, a formula is stratified exactly when the formula can be assigned types according to
6519-420: Is needed for the basic technique) on which there is an external automorphism j (not a set of the model) which moves a rank V α {\displaystyle V_{\alpha }} of the cumulative hierarchy of sets. We may suppose without loss of generality that j ( α ) < α {\displaystyle j(\alpha )<\alpha } . The domain of
6642-807: Is never applied to a bound variable. Choose any free variable y in ϕ {\displaystyle \phi } assigned type i . Apply j i − N {\displaystyle j^{i-N}} uniformly to the entire formula to obtain a formula ϕ 3 {\displaystyle \phi _{3}} in which y appears without any application of j . Now { y ∈ V α ∣ ϕ 3 } {\displaystyle \{y\in V_{\alpha }\mid \phi _{3}\}} exists (because j appears applied only to free variables and constants), belongs to V α + 1 {\displaystyle V_{\alpha +1}} , and contains exactly those y which satisfy
6765-439: Is not a topos . NF may seem to run afoul of problems similar to those in naive set theory , but this is not the case. For example, the existence of the impossible Russell class { x ∣ x ∉ x } {\displaystyle \{x\mid x\not \in x\}} is not an axiom of NF, because x ∉ x {\displaystyle x\not \in x} cannot be stratified. NF steers clear of
6888-421: Is not a stratified formula, so the existence of { x ∣ x ∉ x } {\displaystyle \{x\mid x\not \in x\}} is not asserted by any instance of Comprehension . Quine said that he constructed NF with this paradox uppermost in mind. Cantor's paradox boils down to the question of whether there exists a largest cardinal number , or equivalently, whether there exists
7011-610: Is not stratified. Indeed, if f : P ( V ) → V {\displaystyle f:P(V)\to V} is the trivial injection x ↦ x {\displaystyle x\mapsto x} , then B {\displaystyle B} is the same (ill-defined) set in Russell's paradox. This failure is not surprising since | A | < | P ( A ) | {\displaystyle |A|<|P(A)|} makes no sense in TST:
7134-465: Is not trivial to prove that V {\displaystyle V} is not a "finite set", i.e., that the size of the universe | V | {\displaystyle |V|} is not a natural number. Suppose that | V | = n ∈ N {\displaystyle |V|=n\in \mathbf {N} } . Then n = { V } {\displaystyle n=\{V\}} (it can be shown inductively that
7257-453: Is optional, as both interpretations of the previous example are valid (the ungrammatical interpretation is indicated with an asterisk): However, reflexive pronouns , such as himself , herself , themselves , etc., and reciprocal pronouns , such as each other , act as bound variables. In a sentence like the following: the reflexive herself can only refer to the previously mentioned antecedent , in this case Jane , and can never refer to
7380-455: Is said to be Cantorian : a Cantorian set satisfies the usual form of Cantor's theorem . A set A {\displaystyle A} which satisfies the further condition that ( x ↦ { x } ) ⌈ A {\displaystyle (x\mapsto \{x\})\lceil A} , the restriction of the singleton map to A , is a set is not only Cantorian set but strongly Cantorian . The Burali-Forti paradox of
7503-454: Is the fragment of NF with full extensionality (no urelements) and those instances of comprehension which can be stratified using at most three types. NF 4 is the same theory as NF. Mathematical Logic (ML) is an extension of NF that includes proper classes as well as sets. ML was proposed by Quine and revised by Hao Wang, who proved that NF and the revised ML are equiconsistent. This section discusses some problematic constructions in NF. For
SECTION 60
#17328631145607626-472: Is the order type of the natural order on the ordinals less than α {\displaystyle \alpha } " is not stratified, so the transfinite induction argument does not work in NF. In fact, "the order type β {\displaystyle \beta } of the natural order R α {\displaystyle R_{\alpha }} on the ordinals less than α {\displaystyle \alpha } "
7749-395: Is the order type of the natural order on the ordinals less than α {\displaystyle \alpha } , which would imply an contradiction since Ω {\displaystyle \Omega } by definition is the order type of all ordinals, not any proper initial segment of them. However, the statement " α {\displaystyle \alpha }
7872-510: Is the order type of the order W ι = { ( { x } , { y } ) ∣ x W y } {\displaystyle W^{\iota }=\{(\{x\},\{y\})\mid xWy\}} . Now the lemma on order types may be restated in a stratified manner: Both versions of this statement can be proven by transfinite induction; we assume the type level pair hereinafter. This means that T 2 ( α ) {\displaystyle T^{2}(\alpha )}
7995-493: Is the power set of type i {\displaystyle i} , in TTT each type is being interpreted as the power set of each lower type simultaneously. Regardless, a model of NF can be easily converted to a model of TTT, because in NF all the types are already one and the same. Conversely, with a more complicated argument, it can also be shown that the consistency of TTT implies the consistency of NF. NF with urelements ( NFU )
8118-471: Is the usual Kuratowski ordered pair (two types higher than x {\displaystyle x} and y {\displaystyle y} ), then β {\displaystyle \beta } would be four types higher than α {\displaystyle \alpha } . To correct such a type problem, one needs the T operation , T ( α ) {\displaystyle T(\alpha )} , that "raises
8241-425: The Axiom of Infinity and therefore PA cannot be modeled in NFU, avoiding a contradiction. PA also proves that NFU with Infinity and NFU with both Infinity and Choice are equiconsistent with TST with Infinity and TST with both Infinity and Choice, respectively. Therefore, a stronger theory like ZFC, which proves the consistency of TST, will also prove the consistency of NFU with these additions. In simpler terms, NFU
8364-479: The diagonalization argument by considering the set B = { x ∈ A ∣ x ∉ f ( x ) } {\displaystyle B=\{x\in A\mid x\notin f(x)\}} . In NF, x {\displaystyle x} and f ( x ) {\displaystyle f(x)} should be assigned the same type, so the definition of B {\displaystyle B}
8487-399: The logical value of this expression depends on the value of z , but there is nothing called x or y on which it could depend. More widely, in most proofs, bound variables are used. For example, the following proof shows that all squares of positive even integers are divisible by 4 {\displaystyle 4} not only k but also n have been used as bound variables as
8610-471: The propositional connectives and parentheses "(" and ")", all of which are assumed to not be in V . The formulas will be certain expressions (that is, strings of symbols) over this alphabet. The formulas are inductively defined as follows: This definition can also be written as a formal grammar in Backus–Naur form , provided the set of variables is finite: Using this grammar, the sequence of symbols
8733-438: The summation sign, can be thought of as higher-order functions applying to a function. So, for example, the expression could be treated as a notation for where ∑ S f {\displaystyle \sum _{S}{f}} is an operator with two parameters—a one-parameter function, and a set to evaluate that function over. The other operators listed above can be expressed in similar ways; for example,
8856-447: The theorem of infinity ): Stronger axioms of infinity exist, such as that the set of natural numbers is a strongly Cantorian set, or NFUM = NFU + Infinity + Large Ordinals + Small Ordinals which is equivalent to Morse–Kelley set theory plus a predicate on proper classes which is a κ -complete nonprincipal ultrafilter on the proper class ordinal κ . NF (and NFU + Infinity + Choice , described below and known consistent) allow
8979-617: The universal quantifier ∀ x ∈ S P ( x ) {\displaystyle \forall x\in S\ P(x)} can be thought of as an operator that evaluates to the logical conjunction of the Boolean-valued function P applied over the (possibly infinite) set S . When analyzed in formal semantics , natural languages can be seen to have free and bound variables. In English, personal pronouns like he , she , they , etc. can act as free variables. In
9102-450: The atomic formulas are the propositional variables . For predicate logic , the atoms are predicate symbols together with their arguments, each argument being a term . According to some terminology, an open formula is formed by combining atomic formulas using only logical connectives, to the exclusion of quantifiers. This is not to be confused with a formula which is not closed. A closed formula , also ground formula or sentence ,
9225-491: The book, Quine introduced the system "Mathematical Logic" or "ML", an extension of NF that included proper classes as well as sets . The first edition's set theory married NF to the proper classes of NBG set theory and included an axiom schema of unrestricted comprehension for proper classes. However, J. Barkley Rosser proved that the system was subject to the Burali-Forti paradox. Hao Wang showed how to amend Quine's axioms for ML so as to avoid this problem. Quine included
9348-457: The concrete string representation of formulas (using this or that symbol for connectives and quantifiers, using this or that parenthesizing convention , using Polish or infix notation, etc.) as a mere notational problem. The expression "well-formed formulas" (WFF) also crept into popular culture. WFF is part of an esoteric pun used in the name of the academic game " WFF 'N PROOF : The Game of Modern Logic", by Layman Allen, developed while he
9471-555: The consistency of standard set theory (ZFC). In 2024, Sky Wilshaw confirmed Holmes' proof using the Lean proof assistant . Although NFU resolves the paradoxes similarly to NF, it has a much simpler consistency proof. The proof can be formalized within Peano Arithmetic (PA), a theory weaker than ZF that most mathematicians accept without question. This does not conflict with Gödel's second incompleteness theorem because NFU does not include
9594-547: The construction of such sequences of sets is limited by the size of the type in which they are being constructed; this prevents TSTU from proving its own consistency (TSTU + Infinity can prove the consistency of TSTU; to prove the consistency of TSTU+ Infinity one needs a type containing a set of cardinality ℶ ω {\displaystyle \beth _{\omega }} , which cannot be proved to exist in TSTU+ Infinity without stronger assumptions). Now
9717-424: The construction of two kinds of sets that ZFC and its proper extensions disallow because they are "too large" (some set theories admit these entities under the heading of proper classes ): The category whose objects are the sets of NF and whose arrows are the functions between those sets is not Cartesian closed ; Since NF lacks Cartesian closure, not every function curries as one might intuitively expect, and NF
9840-497: The domain of x {\displaystyle x} and y {\displaystyle y} is the real numbers, but true if the domain is the complex numbers. The term "dummy variable" is also sometimes used for a bound variable (more commonly in general mathematics than in computer science), but this should not be confused with the identically named but unrelated concept of dummy variable as used in statistics, most commonly in regression analysis. Before stating
9963-547: The final formula in the sequence is what is proven. Although the term "formula" may be used for written marks (for instance, on a piece of paper or chalkboard), it is more precisely understood as the sequence of symbols being expressed, with the marks being a token instance of formula. This distinction between the vague notion of "property" and the inductively-defined notion of well-formed formula has roots in Weyl's 1910 paper "Uber die Definitionen der mathematischen Grundbegriffe". Thus
10086-453: The following, with the others provable as theorems: New Foundations is closely related to Russellian unramified typed set theory ( TST ), a streamlined version of the theory of types of Principia Mathematica with a linear hierarchy of types. In this many-sorted theory, each variable and set is assigned a type. It is customary to write the type indices as superscripts: x n {\displaystyle x^{n}} denotes
10209-434: The form ( ∀ x ∈ j N − i ( V α ) . ψ ( x ) ) {\displaystyle (\forall x\in j^{N-i}(V_{\alpha }).\psi (x))} (and similarly for existential quantifiers ). Carry out this transformation everywhere and obtain a formula ϕ 2 {\displaystyle \phi _{2}} in which j
10332-398: The largest ordinal number is resolved in the opposite way: In NF, having access to the set of ordinals does not allow one to construct a "largest ordinal number". One can construct the ordinal Ω {\displaystyle \Omega } that corresponds to the natural well-ordering of all ordinals, but that does not mean that Ω {\displaystyle \Omega }
10455-411: The linear hierarchy of sets in TST. The usual definition of the ordered pair was first proposed by Kuratowski in 1921. Willard Van Orman Quine first proposed NF as a way to avoid the "disagreeable consequences" of TST in a 1937 article titled New Foundations for Mathematical Logic ; hence the name. Quine extended the theory in his book Mathematical Logic , whose first edition was published in 1940. In
10578-583: The model of NFU will be the nonstandard rank V α {\displaystyle V_{\alpha }} . The basic idea is that the automorphism j codes the "power set" V α + 1 {\displaystyle V_{\alpha +1}} of our "universe" V α {\displaystyle V_{\alpha }} into its externally isomorphic copy V j ( α ) + 1 {\displaystyle V_{j(\alpha )+1}} inside our "universe." The remaining objects not coding subsets of
10701-491: The model of NFU). This establishes that Stratified Comprehension holds in the model of NFU. To see that weak Extensionality holds is straightforward: each nonempty element of V j ( α ) + 1 {\displaystyle V_{j(\alpha )+1}} inherits a unique extension from the nonstandard model, the empty set inherits its usual extension as well, and all other objects are urelements. If α {\displaystyle \alpha }
10824-469: The natural numbers , which is not suitable for NF, since the description of the successor operation (and many other aspects of von Neumann numerals) is necessarily unstratified. The usual form of natural numbers used in NF follows Frege's definition , i.e., the natural number n is represented by the set of all sets with n elements. Under this definition, 0 is easily defined as { ∅ } {\displaystyle \{\varnothing \}} , and
10947-417: The natural ordering of ordinals ( α ≤ β {\displaystyle \alpha \leq \beta } iff there exists well-orderings R ∈ α , S ∈ β {\displaystyle R\in \alpha ,S\in \beta } such that S {\displaystyle S} is a continuation of R {\displaystyle R} )
11070-449: The ordered pair (a, b) as a primitive notion , as well as its left and right projections π 1 {\displaystyle \pi _{1}} and π 2 {\displaystyle \pi _{2}} , i.e., functions such that π 1 ( ( a , b ) ) = a {\displaystyle \pi _{1}((a,b))=a} and π 2 ( (
11193-417: The ordered pair so that its type is the same as that of its arguments (resulting in a type-level ordered pair). The usual definition of the ordered pair, namely ( a , b ) K := { { a } , { a , b } } {\displaystyle (a,\ b)_{K}\;:=\ \{\{a\},\ \{a,\ b\}\}} , results in a type two higher than
11316-484: The ordinals, i.e., T ( α ) < T ( β ) {\displaystyle T(\alpha )<T(\beta )} iff α < β {\displaystyle \alpha <\beta } . Hence the T operation is not a function: The collection of ordinals { α ∣ T ( α ) < α } {\displaystyle \{\alpha \mid T(\alpha )<\alpha \}} cannot have
11439-401: The original formula ϕ {\displaystyle \phi } in the model of NFU. j ( { y ∈ V α ∣ ϕ 3 } ) {\displaystyle j(\{y\in V_{\alpha }\mid \phi _{3}\})} has this extension in the model of NFU (the application of j corrects for the different definition of membership in
11562-413: The precedence (from most binding to least binding) 1. ¬ 2. → 3. ∧ 4. ∨. Then the formula may be abbreviated as This is, however, only a convention used to simplify the written representation of a formula. If the precedence was assumed, for example, to be left-right associative, in following order: 1. ¬ 2. ∧ 3. ∨ 4. →, then
11685-414: The previous Formal explanation section . The sentence with the reflexive could be represented as in which Jane is the subject referent argument and λx.x hurt x is the predicate function (a lambda abstraction) with the lambda notation and x indicating both the semantic subject and the semantic object of sentence as being bound. This returns the semantic interpretation JANE hurt JANE with JANE being
11808-407: The property that Endo ( { x } ) = { Endo ( { y } ) | y ∈ x } for each set x . This function can define a type level "membership" relation on the universe, one reproducing the membership relation of the original nonstandard model. In 1914, Norbert Wiener showed how to code the ordered pair as a set of sets, making it possible to eliminate the relation types of Principia Mathematica in favor of
11931-538: The referent can be shown using coindexing subscripts where i indicates one referent and j indicates a second referent (different from i ). Thus, the sentence Lisa found her book has the following interpretations: The distinction is not purely of academic interest, as some languages do actually have different forms for her i and her j : for example, Norwegian and Swedish translate coreferent her i as sin and noncoreferent her j as hennes . English does allow specifying coreference, but it
12054-491: The resulting axiomatization in the second and final edition, published in 1951. Well-formed formulas In mathematical logic , propositional logic and predicate logic , a well-formed formula , abbreviated WFF or wff , often simply formula , is a finite sequence of symbols from a given alphabet that is part of a formal language . The abbreviation wff is pronounced "woof", or sometimes "wiff", "weff", or "whiff". A formal language can be identified with
12177-407: The rules of TST. This can be extended to map every NF formula to a set of corresponding TST formulas with various type index annotations. The mapping is one-to-many because TST has many similar formulas. For example, raising every type index in a TST formula by 1 results in a new, valid TST formula. Tangled Type Theory (TTT) is an extension of TST where each variable is typed by an ordinal rather than
12300-440: The same formula above (without parentheses) would be rewritten as The definition of a formula in first-order logic Q S {\displaystyle {\mathcal {QS}}} is relative to the signature of the theory at hand. This signature specifies the constant symbols, predicate symbols, and function symbols of the theory at hand, along with the arities of the function and predicate symbols. The definition of
12423-510: The same formula may be written more than once, and a formula might in principle be so long that it cannot be written at all within the physical universe. Formulas themselves are syntactic objects. They are given meanings by interpretations. For example, in a propositional formula, each propositional variable may be interpreted as a concrete proposition, so that the overall formula expresses a relationship between these propositions. A formula need not be interpreted, however, to be considered solely as
12546-695: The same person. Pronouns can also behave in a different way. In the sentence below the pronoun her can only refer to a female that is not Ashley. This means that it can never have a reflexive meaning equivalent to Ashley hit herself . The grammatical and ungrammatical interpretations are: The first interpretation is impossible. Only the second interpretation is permitted by the grammar. Thus, it can be seen that reflexives and reciprocals are bound variables (known technically as anaphors ) while true pronouns are free variables in some grammatical structures but variables that cannot be bound in other grammatical structures. The binding phenomena found in natural languages
12669-413: The same results of model theory can be used to build a model of NFU and verify that it is a model of NFU in much the same way, with the T α {\displaystyle T_{\alpha }} 's being used in place of V α {\displaystyle V_{\alpha }} in the usual construction. The final move is to observe that since NFU is consistent, we can drop
12792-436: The same type in the metatheory) with embeddings of each P ( T i ) {\displaystyle P(T_{i})} into P 1 ( T i + 1 ) {\displaystyle P_{1}(T_{i+1})} coding embeddings of the power set of T i {\displaystyle T_{i}} into T i + 1 {\displaystyle T_{i+1}} in
12915-435: The same variable symbol may appear in multiple places in an expression, some occurrences of the variable symbol may be free while others are bound, hence "free" and "bound" are at first defined for occurrences and then generalized over all occurrences of said variable symbol in the expression. However it is done, the variable ceases to be an independent variable on which the value of the expression depends, whether that value be
13038-429: The sentence above, the possessive pronoun her is a free variable. It may refer to the previously mentioned Lisa or to any other female. In other words, her book could be referring to Lisa's book (an instance of coreference ) or to a book that belongs to a different female (e.g. Jane's book). Whoever the referent of her is can be established according to the situational (i.e. pragmatic ) context. The identity of
13161-410: The set { n ∈ N ∣ P ( n ) } {\displaystyle \{n\in \mathbf {N} \mid P(n)\}} can be constructed, and when P ( n ) {\displaystyle P(n)} satisfies the conditions for mathematical induction, this set is an inductive set. Finite sets can then be defined as sets that belong to a natural number. However, it
13284-555: The set { x ∣ ϕ ( x ) } {\displaystyle \{x\mid \phi (x)\}} will not be unique if it is empty (i.e. if ϕ ( x ) {\displaystyle \phi (x)} is unsatisfiable). However, for ease of use, it is more convenient to have a unique, "canonical" empty set. This can be done by introducing a sethood predicate s e t ( x ) {\displaystyle \mathrm {set} (x)} to distinguish sets from atoms. The axioms are then: NF 3
13407-579: The set of formulas in the language. A formula is a syntactic object that can be given a semantic meaning by means of an interpretation . Two key uses of formulas are in propositional logic and predicate logic. A key use of formulas is in propositional logic and predicate logic such as first-order logic . In those contexts, a formula is a string of symbols φ for which it makes sense to ask "is φ true?", once any free variables in φ have been instantiated. In formal logic, proofs can be represented by sequences of formulas with certain properties, and
13530-408: The singleton of any element of V j ( α ) {\displaystyle V_{j(\alpha )}} to its sole element, becomes in NFU a function which sends each singleton { x }, where x is any object in the universe, to j ( x ). Call this function Endo and let it have the following properties: Endo is an injection from the set of singletons into the set of sets, with
13653-407: The strings that followed the formation rules of (correct) formulas. Several authors simply say formula. Modern usages (especially in the context of computer science with mathematical software such as model checkers , automated theorem provers , interactive theorem provers ) tend to retain of the notion of formula only the algebraic concept and to leave the question of well-formedness , i.e. of
13776-505: The successor operation can be defined in a stratified way: S ( A ) = { a ∪ { x } ∣ a ∈ A ∧ x ∉ a } . {\displaystyle S(A)=\{a\cup \{x\}\mid a\in A\wedge x\notin a\}.} Under this definition, one can write down a statement analogous to the usual form of the axiom of infinity. However, that statement would be trivially true, since
13899-392: The three well-known paradoxes of set theory in drastically different ways than how those paradoxes are resolved in well-founded set theories such as ZFC. Many useful concepts that are unique to NF and its variants can be developed from the resolution of those paradoxes. The resolution of Russell's paradox is trivial: x ∉ x {\displaystyle x\not \in x}
14022-449: The top level of a program are technically free variables within the terms to which they are bound but are often treated specially because they can be compiled as fixed addresses. Similarly, an identifier bound to a recursive function is also technically a free variable within its own body but is treated specially. A closed term is one containing no free variables. To give an example from mathematics, consider an expression which defines
14145-449: The type of P ( A ) {\displaystyle P(A)} is one higher than the type of A {\displaystyle A} . In NF, | A | < | P ( A ) | {\displaystyle |A|<|P(A)|} is a syntactical sentence due to the conflation of all the types, but any general proof involving Comprehension is unlikely to work. The usual way to correct such
14268-466: The type of its arguments a and b . Hence for purposes of determining stratification, a function is three types higher than the members of its field. NF and related theories usually employ Quine's set-theoretic definition of the ordered pair, which yields a type-level ordered pair. However, Quine's definition relies on set operations on each of the elements a and b , and therefore does not directly work in NFU. As an alternative approach, Holmes takes
14391-456: The type" of an ordinal α {\displaystyle \alpha } , just like how P 1 ( A ) {\displaystyle P_{1}(A)} "raises the type" of the set A {\displaystyle A} . The T operation is defined as follows: If W ∈ α {\displaystyle W\in \alpha } , then T ( α ) {\displaystyle T(\alpha )}
14514-423: The universal set V {\displaystyle V} would be an inductive set . Since inductive sets always exist, the set of natural numbers N {\displaystyle \mathbf {N} } can be defined as the intersection of all inductive sets. This definition enables mathematical induction for stratified statements P ( n ) {\displaystyle P(n)} , because
14637-509: The universe are treated as urelements . Formally, the membership relation of the model of NFU will be x ∈ N F U y ≡ d e f j ( x ) ∈ y ∧ y ∈ V j ( α ) + 1 . {\displaystyle x\in _{NFU}y\equiv _{def}j(x)\in y\wedge y\in V_{j(\alpha )+1}.} It may now be proved that this actually
14760-781: The universe to the one-element sets is not a set; it is not a set because its definition is unstratified. Note that in all models of NFU + Choice it is the case that | P 1 ( V ) | < | P ( V ) | ≪ | V | {\displaystyle |P_{1}(V)|<|P(V)|\ll |V|} ; Choice allows one not only to prove that there are urelements but that there are many cardinals between | P ( V ) | {\displaystyle |P(V)|} and | V | {\displaystyle |V|} . However, unlike in TST, | A | = | P 1 ( A ) | {\displaystyle |A|=|P_{1}(A)|}
14883-492: The use of NFU as a foundation for mathematics is that the reasons for relying on it have to do with the intuition that ZFC is correct. It is sufficient to accept TST (in fact TSTU). In outline: take the type theory TSTU (allowing urelements in each positive type) as a metatheory and consider the theory of set models of TSTU in TSTU (these models will be sequences of sets T i {\displaystyle T_{i}} (all of
15006-404: The use of absolute types in our metatheory, bootstrapping the metatheory from TSTU to NFU. The automorphism j of a model of this kind is closely related to certain natural operations in NFU. For example, if W is a well-ordering in the nonstandard model (we suppose here that we use Kuratowski pairs so that the coding of functions in the two theories will agree to some extent) which is also
15129-691: Was at Yale Law School (he was later a professor at the University of Michigan ). The suite of games is designed to teach the principles of symbolic logic to children (in Polish notation ). Its name is an echo of whiffenpoof , a nonsense word used as a cheer at Yale University made popular in The Whiffenpoof Song and The Whiffenpoofs . Free variables and bound variables In mathematics , and in other disciplines involving formal languages , including mathematical logic and computer science ,
#559440