14663:
12315:
426:. 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:
3922:, 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.
10794:) are allowed to have the type of the set asserted to exist by an instance of comprehension. He called the result "predicative NF" (NFP); it is, of course, doubtful whether any theory with a self-membered universe is truly predicative. Holmes has shown that NFP has the same consistency strength as the predicative theory of types of
3940:) 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:
9008:", 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
10823:
is consistent relative to ZF with atoms but without choice (ZFA) by constructing a class model of ZFA which includes "tangled webs of cardinals" in ZF with atoms and choice (ZFA+C). These proofs were "difficult to read, insanely involved, and involve the sort of elaborate bookkeeping which makes it
10789:
restriction, though NFI is not a predicative theory: it admits enough impredicativity to define the set of natural numbers (defined as the intersection of all inductive sets; note that the inductive sets quantified over are of the same type as the set of natural numbers being defined). Crabbé also
10780:
consistent. Specker additionally showed that NF is equiconsistent with TST plus the axiom scheme of "typical ambiguity". NF is also equiconsistent with TST augmented with a "type shifting automorphism", an operation (external to the theory) which raises type by one, mapping each type onto the next
3681:
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 the rules of TST. This can be extended to map every NF formula to a set of
10189:
or any related system to carry out this proof. A common argument against 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
9088:
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 is generally seen as weaker than NF because, in NFU, the
4589:
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 the ordered pair so that its type is the same as that of its arguments (resulting in a
4376:
10569:
so that the coding of functions in the two theories will agree to some extent) which is also 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
9064:
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 the consistency of standard set theory (ZFC). In 2024, Sky
Wilshaw confirmed Holmes' proof using the
4057:
10828:, finally resolving the question of NF's consistency. Timothy Chow characterized Wilshaw's work as showing that the reluctance of peer reviewers to engage with a difficult to understand proof can be addressed with the help of proof assistants.
10784:
In 1983, Marcel Crabbé proved consistent a system he called NFI, whose axioms are unrestricted extensionality and those instances of comprehension in which no variable is assigned a type higher than that of the set asserted to exist. This is a
4542:
6131:
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.
3682:
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.
9429:
2414:
5602:
2574:
1710:
5027:, 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
2886:
8999:
5604:. However, such 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,
5143:
825:
3194:
9752:
9673:
8111:
10416:(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
1311:
4558:
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.
4238:
4680:
1498:
10057:
8932:
8603:
4249:
1190:
10811:
database implemented
Hailperin's finite axiomatization for New Foundations. Since 2015, several candidate proofs by Randall Holmes of the consistency of NF relative to ZF were available both on
5009:
2692:
9935:
8218:
3628:
3382:
5538:
10539:
in the usual construction. The final move is to observe that since NFU is consistent, we can drop the use of absolute types in our metatheory, bootstrapping the metatheory from TSTU to NFU.
3089:
2999:
2244:
2161:
5274:
6546:
3955:
3525:
7215:
1020:
10446:
Note that 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 +
8808:
7844:
684:
7742:
7553:
9453:
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
8859:
1398:
5145:
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 the universal set
9179:
6206:
6095:
5483:
5400:
1576:
7089:
7018:
2787:
7704:
4422:
4101:
9596:. 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
8885:
4876:
4822:
4170:
2311:
10479:
10114:
9315:
5063:
5011:
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.
3872:
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
4908:
206:
10631:
10300:
8742:
8702:
8666:
7810:
7674:
7481:
7353:
7124:
3768:
3419:
10485:
without stronger assumptions). Now 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
9972:
9246:
6864:
6760:
5802:
1858:
8499:
5503:
5192:
4566:
This section discusses some problematic constructions in NF. For a further development of mathematics in NFU, with a comparison to the development of the same in ZFC, see
3668:
3313:
11604:
10537:
10510:
10441:
9273:
9209:
9140:
8630:
8245:
7998:
6656:
6168:
6121:
3728:
2023:
1799:
9089:
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.
8528:
8397:
6682:
9875:
9783:
9556:
9502:
3559:
2733:
917:
891:
10749:
showed how to amend Quine's axioms for ML so as to avoid this problem. Quine included the resulting axiomatization in the second and final edition, published in 1951.
10251:
8453:
7589:
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
6927:
4768:
4741:
4451:
4130:
1056:
11624:
10360:
10161:
10137:
9848:
8762:
8417:
8361:
8131:
8042:
8018:
7951:
7931:
7904:
7884:
7864:
7627:
7607:
6013:
5432:
8337:
7971:
7258:
3794:
310:
10414:
10387:
10327:
10215:
9996:
9811:
9475:
9451:
8277:
8163:
4928:
3250:
1973:
392:
330:
284:
253:
229:
7632:
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
6789:
6595:
6443:
6361:
6288:
5303:
5225:
4456:
3843:
118:
9590:
7399:
7288:
6407:
5907:
5704:
5674:
5640:
5356:
3900:
2075:
2049:
1082:
594:
372:
10815:
and on the logician's home page. His proofs were based on demonstrating the equiconsistency of a "weird" variant of TST, "tangled type theory with λ-types" (TTT
9046:
9026:
8473:
8317:
8297:
7782:
7762:
7509:
7419:
7373:
6947:
6891:
6809:
6702:
6615:
6566:
6483:
6463:
6381:
6328:
6308:
6252:
5770:
5747:
5326:
5163:
3920:
3863:
3814:
3112:
2909:
2810:
2614:
2594:
2477:
2457:
2434:
2334:
1941:
1921:
1901:
1881:
1819:
1750:
1730:
1639:
1619:
1596:
1523:
1331:
1233:
1210:
1105:
940:
865:
845:
747:
727:
704:
617:
568:
548:
528:
508:
488:
468:
448:
94:
3690:
Tangled Type Theory (TTT) is an extension of TST where each variable is typed by an ordinal rather than a natural number. The well-formed atomic formulas are
10753:
5028:
4690:. Hence for purposes of determining stratification, a function is three types higher than the members of its field. NF and related theories usually employ
10689:. This function can define a type level "membership" relation on the universe, one reproducing the membership relation of the original nonstandard model.
10190:(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
4551:
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
13042:
9084:
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
10725:, whose first edition was published in 1940. In the book, Quine introduced the system "Mathematical Logic" or "ML", an extension of NF that included
9324:
6485:
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 the
2339:
10116:
inherits a unique extension from the nonstandard model, the empty set inherits its usual extension as well, and all other objects are urelements.
5549:
7126:
from 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 +
13717:
12779:
2482:
2246:
exist (these are the relations which an ordered pair has to its first and second terms, which are technically referred to as its projections).
1644:
4135:
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
13800:
12941:
11789:
10954:(1981) uses "three primitive notational devices: membership, joint denial, and quantification", then defines = in this fashion (pp.134–136)
2815:
4694:
of the ordered pair, which yields a type-level ordered pair. However, Quine's definition relies on set operations on each of the elements
10857:
10847:
5729:
is false. Since it can be proved through induction that every finite set has a choice function (a stratified condition), it follows that
5024:
4567:
9077:
8937:
5068:
3218:
752:
8708:
Both versions of this statement can be proven by transfinite induction; we assume the type level pair hereinafter. This means that
7091:: there are fewer one-element sets than sets (and so fewer one-element sets than general objects, if we are in NFU). The "obvious"
3117:
9678:
9599:
9060:
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
8047:
14114:
9072:
Although NFU resolves the paradoxes similarly to NF, it has a much simpler consistency proof. The proof can be formalized within
12032:, 2nd ed., revised. Harvard Univ. Press: 80–101. The definitive version of where it all began, namely Quine's 1937 paper in the
5820:
interprets NFU + "there is a type-level ordered pair" (they are not quite the same theory, but the differences are inessential).
1238:
11853:, Cahiers du Centre de Logique, vol. 10, Louvain-la-Neuve: Université Catholique de Louvain, Département de Philosophie,
10597:
is coded by a function in the model of NFU. The function in the nonstandard model which sends the singleton of any element of
14272:
11549:
5868:
and its proper extensions disallow because they are "too large" (some set theories admit these entities under the heading of
4371:{\displaystyle \forall yz.(\mathrm {set} (y)\wedge \mathrm {set} (z)\wedge (\forall x.x\in y\leftrightarrow x\in z))\to y=z.}
4179:
13060:
4597:
1403:
14127:
13450:
12468:
12281:
10738:
10001:
8890:
11753:, Oxford Science Publications, Oxford Logic Guides, vol. 20, New York: The Clarendon Press, Oxford University Press,
8533:
1110:
12221:
4933:
2624:
9888:
8172:
5824:
Stronger axioms of infinity exist, such as that the set of natural numbers is a strongly
Cantorian set, or NFUM = NFU +
3564:
3318:
14132:
14122:
13859:
13712:
13065:
12796:
10791:
3631:
13056:
5512:
14268:
12051:
12009:
11858:
11758:
5609:
3004:
2914:
2166:
2083:
13610:
5230:
14702:
14365:
14109:
12934:
6492:
5643:
73:
5308:
Finite sets can then be defined as sets that belong to a natural number. However, it is not trivial to prove that
3424:
13670:
13363:
12774:
12368:
7355:
is a syntactical sentence in NF(U), and as shown above one can talk about its truth value for specific values of
7133:
3279:-1. The axioms of TST are extensionality, on sets of the same (positive) type, and comprehension, namely that if
945:
13104:
12654:
10824:
easy to introduce errors". In 2024, Sky
Wilshaw formalized a version of Holmes' proof using the proof assistant
10709:
in favor of the linear hierarchy of sets in TST. The usual definition of the ordered pair was first proposed by
9097:
Jensen's proof gives a fairly simple method for producing models of NFU in bulk. Using well-known techniques of
14687:
14626:
14328:
14091:
14086:
13911:
13332:
13016:
8771:
7815:
622:
10143:, one gets a model of NFU which claims that the universe is finite (it is externally infinite, of course). If
7709:
7514:
14621:
14404:
14321:
14034:
13965:
13842:
13084:
12548:
12427:
11875:
Holmes, M. Randall (2008). "Symmetry as a
Criterion for Comprehension Motivating Quine's 'New Foundations'".
8820:
1339:
173:
9076:(PA), a theory weaker than ZF that most mathematicians accept without question. This does not conflict with
7020:
is a theorem in TST (thanks to the diagonalization argument), and thus also a theorem in NF. In particular,
14546:
14372:
14058:
13692:
13291:
12791:
12233:
9149:
6173:
6062:
6032:
The category whose objects are the sets of NF and whose arrows are the functions between those sets is not
5441:
5361:
1528:
423:
7023:
6952:
2077:. This and larger tuples can be a definition rather than an axiom if an ordered pair construction is used.
14424:
14419:
14029:
13768:
13697:
13026:
12927:
12784:
12422:
12385:
7953:" is not stratified, so the transfinite induction argument does not work in NF. In fact, "the order type
5937:
5837:
2738:
32:
7683:
4386:
4065:
14353:
13943:
13337:
13305:
12996:
9105:(nothing nearly as strong as full ZFC is needed for the basic technique) on which there is an external
8864:
4827:
4773:
4138:
2252:
12439:
10457:
10077:
9278:
5042:
4052:{\displaystyle \forall xyw.(w\in x)\to (x=y\leftrightarrow (\forall z.z\in x\leftrightarrow z\in y)))}
14643:
14592:
14489:
13987:
13948:
13425:
13070:
12473:
12358:
12346:
12341:
11807:
8934:
cannot have a least member, and thus cannot be a set. More concretely, the monotonicity of T implies
7556:
6033:
4881:
179:
13099:
10717:
first proposed NF as a way to avoid the "disagreeable consequences" of TST in a 1937 article titled
10600:
10256:
8711:
8671:
8635:
7787:
7651:
7424:
7296:
7097:
3733:
3387:
14484:
14414:
13953:
13805:
13788:
13511:
12991:
12274:
11523:
11449:
9944:
9218:
8813:
Another (stratified) statement that can be proven by transfinite induction is that T is a strictly
6814:
6710:
6486:
5775:
4714:
4691:
1824:
8478:
6866:
is a syntactical sentence due to the conflation of all the types, but any general proof involving
5488:
5175:
3637:
3282:
14316:
14293:
14254:
14140:
14081:
13727:
13647:
13491:
13435:
13048:
12893:
12811:
12686:
12638:
12452:
12375:
11582:
10714:
10557:
of a model of this kind is closely related to certain natural operations in NFU. For example, if
10515:
10488:
10419:
9251:
9187:
9118:
9005:
8612:
8223:
7976:
7680:
works on stratified statements, which allows one to prove that the natural ordering of ordinals (
7560:
7221:
allows one not only to prove that there are urelements but that there are many cardinals between
6620:
6147:
6100:
5933:
3693:
1978:
1758:
419:
43:
36:
10063:
corrects for the different definition of membership in the model of NFU). This establishes that
8504:
8373:
6661:
97:
14606:
14333:
14311:
14278:
14171:
14017:
14002:
13975:
13926:
13810:
13745:
13570:
13536:
13531:
13405:
13236:
13213:
12845:
12726:
12538:
12351:
12248:
11905:
10837:
10825:
9853:
9761:
9755:
9534:
9480:
9317:
inside our "universe." The remaining objects not coding subsets of the universe are treated as
9066:
5970:
5195:
4582:
4578:
3675:
3530:
2697:
896:
870:
260:
69:
10220:
8422:
6896:
4746:
4719:
4427:
4106:
1025:
14536:
14389:
14181:
13899:
13635:
13541:
13400:
13385:
13266:
13241:
12761:
12731:
12675:
12595:
12575:
12553:
12041:
11609:
10801:
10796:
10332:
10146:
10122:
9820:
8747:
8402:
8346:
8116:
8027:
8003:
7936:
7916:
7889:
7869:
7849:
7677:
7612:
7592:
5992:
5405:
4537:{\displaystyle \exists A.\mathrm {set} (A)\wedge (\forall x.x\in A\leftrightarrow \phi (x)).}
52:
39:
11371:
8322:
7956:
7224:
3773:
289:
14692:
14509:
14471:
14348:
14152:
13992:
13916:
13894:
13722:
13680:
13579:
13546:
13410:
13198:
13109:
12835:
12825:
12659:
12590:
12543:
12483:
12363:
12190:
12121:
12090:
12019:
11993:
11868:
11768:
10842:
10392:
10365:
10305:
10193:
9981:
9796:
9460:
9436:
9143:
8250:
8136:
7846:. In naive set theory, one would go on to prove by transfinite induction that each ordinal
7609:
that corresponds to the natural well-ordering of all ordinals, but that does not mean that
7581:
6141:
6057:
4913:
3228:
1946:
377:
315:
269:
238:
214:
65:
12254:
11714:
10776:
to NF yields a theory (NFU) that is provably consistent. That same year, Grishin proved NF
6765:
6571:
6419:
6337:
6264:
5279:
5201:
4878:(in Holmes' axiomatization of NFU, the comprehension schema that asserts the existence of
3819:
103:
8:
14697:
14638:
14529:
14514:
14494:
14451:
14338:
14288:
14214:
14159:
14096:
13889:
13884:
13832:
13600:
13589:
13261:
13161:
13089:
13080:
13076:
13011:
13006:
12830:
12741:
12649:
12644:
12458:
12400:
12331:
12267:
10852:
10746:
9569:
7488:
7378:
7263:
6386:
6255:
6220:
5886:
5864:, described below and known consistent) allow the construction of two kinds of sets that
5679:
5649:
5615:
5331:
3879:
3876:
its type 1 members or its type 0 members. Whereas TST has natural models where each type
2054:
2028:
1061:
573:
351:
12125:
11640:
Crabbé, Marcel (1982). "On the consistency of an impredicative fragment of Quine's NF".
11626:
because we do not want to assume that every ordinal in the model is the index of a rank.
10741:
and included an axiom schema of unrestricted comprehension for proper classes. However,
9457:
greater than all types assigned to variables by this stratification. Expand the formula
14667:
14436:
14399:
14384:
14377:
14360:
14164:
14146:
14012:
13938:
13921:
13874:
13687:
13596:
13430:
13415:
13375:
13327:
13312:
13300:
13256:
13231:
13001:
12950:
12753:
12748:
12533:
12488:
12395:
12194:
12178:
12144:
12109:
12094:
12078:
11973:
11944:
11936:
11892:
11832:
11824:
11737:
11665:
11657:
11394:
10726:
10658:
10185:
For philosophical reasons, it is important to note that it is not necessary to work in
9505:
9102:
9031:
9011:
8814:
8458:
8302:
8282:
7767:
7747:
7494:
7404:
7358:
6932:
6876:
6794:
6687:
6600:
6551:
6468:
6448:
6413:
6366:
6331:
6313:
6293:
6237:
5958:
5910:
5755:
5732:
5311:
5148:
3905:
3848:
3799:
3097:
2894:
2795:
2599:
2579:
2462:
2442:
2419:
2319:
1926:
1906:
1886:
1866:
1804:
1735:
1715:
1624:
1604:
1581:
1508:
1316:
1218:
1195:
1090:
925:
850:
830:
732:
712:
689:
602:
553:
533:
513:
493:
473:
453:
433:
209:
79:
20:
13620:
11698:
14662:
14602:
14409:
14219:
14209:
14101:
13982:
13817:
13793:
13574:
13558:
13463:
13440:
13317:
13286:
13251:
13146:
12981:
12610:
12447:
12410:
12380:
12304:
12149:
12047:
12005:
11896:
11854:
11754:
10742:
10730:
9113:
9081:
7637:
6016:
5966:
5166:
5020:
12211:
12198:
12098:
11948:
11836:
11741:
11669:
9515:
using the definition of membership in the model of NFU. Application of any power of
422:. One advantage of such a finite axiomatization is that it eliminates the notion of
14616:
14611:
14504:
14461:
14283:
14244:
14239:
14224:
14050:
14007:
13904:
13702:
13652:
13226:
13188:
12898:
12888:
12873:
12868:
12736:
12390:
12215:
12170:
12139:
12129:
12070:
11965:
11928:
11884:
11816:
11729:
11649:
11386:
9073:
7633:
6053:
5965:'s definition of the cardinal numbers works in NF and NFU: a cardinal number is an
5305:
satisfies the conditions for mathematical induction, this set is an inductive set.
4710:
5194:
can be defined as the intersection of all inductive sets. This definition enables
127:: Two objects with the same elements are the same object; formally, given any set
14597:
14587:
14541:
14524:
14479:
14441:
14343:
14263:
14070:
13997:
13970:
13958:
13864:
13778:
13752:
13675:
13476:
13278:
13221:
13171:
13136:
13094:
12705:
12523:
12336:
12186:
12086:
12015:
11989:
11864:
11764:
10928:
10765:
10165:
9061:
6224:
5944:
5726:
4062:
In this axiomatization, the comprehension schema is unchanged, although the set
14582:
14561:
14519:
14499:
14394:
14249:
13847:
13837:
13827:
13822:
13756:
13630:
13506:
13395:
13390:
13368:
12969:
12903:
12700:
12681:
12585:
12570:
12527:
12463:
12405:
10947:
10698:
9528:
9424:{\displaystyle x\in _{NFU}y\equiv _{def}j(x)\in y\wedge y\in V_{j(\alpha )+1}.}
9085:
7586:
5974:
5948:
3257:
3221:
theory, each variable and set is assigned a type. It is customary to write the
867:, exists. This can be restricted to the existence of one of the cross products
147:
124:
11888:
11776:
11733:
5505:
too, causing arithmetic to break down. To prevent this, one can introduce the
3670:. This type theory is much less complicated than the one first set out in the
14681:
14556:
14234:
13741:
13526:
13516:
13486:
13471:
13141:
12908:
12710:
12624:
12619:
12227:
12105:
12025:
11916:
10786:
10761:
10562:
7641:
6232:
6020:
5914:
5878:
5546:
in NF(U) by constructing any "externally" infinite sequence of sets, such as
2409:{\displaystyle \bigcup =\{x|{\text{for some }}B,x\in B{\text{ and }}B\in A\}}
12878:
11845:
5597:{\displaystyle \varnothing ,\{\varnothing \},\{\{{\varnothing }\}\},\ldots }
14456:
14303:
14204:
14196:
14076:
14024:
13933:
13869:
13852:
13783:
13642:
13501:
13203:
12986:
12858:
12853:
12671:
12600:
12558:
12417:
12314:
12242:
12153:
11678:
10734:
10702:
10633:
to its sole element, becomes in NFU a function which sends each singleton {
10566:
10551:
9509:
9106:
9098:
7812:. By definition of ordinals, this well-ordering also belongs to an ordinal
5869:
5435:
4586:
162:
12134:
14566:
14446:
13625:
13615:
13562:
13246:
13166:
13151:
13031:
12976:
12883:
12518:
9520:
9057:
7645:
6228:
6212:. Quine said that he constructed NF with this paradox uppermost in mind.
6056:, but this is not the case. For example, the existence of the impossible
5752:
In NFU with axioms asserting the existence of a type-level ordered pair,
3271:
objects; objects connected by identity have equal types and sets of type
3256:. Type 0 consists of individuals otherwise undescribed. For each (meta-)
47:
11940:
11919:(1969), "On the Consistency of a Slight(?) Modification of Quine's NF",
10705:
as a set of sets, making it possible to eliminate the relation types of
10661:
from the set of singletons into the set of sets, with the property that
2569:{\displaystyle (R|S)=\{(x,y)|{\text{for some }}z,xRz{\text{ and }}zSy\}}
1705:{\displaystyle A\cup B=\{x|x\in A{\text{ or }}x\in B{\text{ or both}}\}}
13496:
13351:
13322:
13128:
12863:
12634:
12290:
12182:
12110:"The axiom of choice in Quine's new foundations for mathematical logic"
12082:
12040:
Quine, Willard Van Orman (1987). "The Inception of "New Foundations"".
11977:
11932:
11828:
11661:
11398:
10710:
8605:. Now the lemma on order types may be restated in a stratified manner:
6128:
10180:
9001:, a "descending sequence" in the ordinals which also cannot be a set.
8887:. Hence the T operation is not a function: The collection of ordinals
286:'s syntax to the natural numbers, such that for any atomic subformula
14648:
14551:
13604:
13521:
13481:
13445:
13381:
13193:
13183:
13156:
12919:
12666:
12629:
12580:
12478:
10773:
10769:
10571:
9318:
7092:
6259:
5986:
5722:
3932:
2881:{\displaystyle \{x|\exists y:(\forall w:w\in x\leftrightarrow w=y)\}}
12212:"Enriched Stratified systems for the Foundations of Category Theory"
12174:
12074:
11969:
11820:
11653:
11390:
10450:
can prove the consistency of TSTU; to prove the consistency of TSTU+
10169:
holds in the nonstandard model of ZFC, one obtains a model of NFU +
9048:
being a set, because the membership relation is not a set relation.
5646:. In such models, mathematical induction can prove statements about
14633:
14431:
13879:
13584:
13178:
11244:
10808:
9519:
to both sides of an equation or membership statement preserves its
9004:
One might assert that this result shows that no model of NF(U) is "
6037:
4930:
is considered a theorem and only proved later, so expressions like
3868:
TTT is considered a "weird" theory because each type is related to
1333:, exists. This can be defined using the operation of type lowering.
9941:
appears applied only to free variables and constants), belongs to
8994:{\displaystyle \Omega >T^{2}(\Omega )>T^{4}(\Omega )\ldots }
5065:, and the successor operation can be defined in a stratified way:
2694:
exists. This is equivalent to complement and union together, with
14229:
13021:
11256:
10760:
is equivalent to a finite conjunction of its instances, In 1953,
10217:(all of the same type in the metatheory) with embeddings of each
9758:). Carry out this transformation everywhere and obtain a formula
7933:
is the order type of the natural order on the ordinals less than
7866:
is the order type of the natural order on the ordinals less than
6124:
3796:. The axioms of TTT are those of TST where each variable of type
12004:(Revised ed.), Cambridge, Mass.: Harvard University Press,
10745:
proved that the system was subject to the Burali-Forti paradox.
9321:. Formally, the membership relation of the model of NFU will be
5138:{\displaystyle S(A)=\{a\cup \{x\}\mid a\in A\wedge x\notin a\}.}
4594:
ordered pair). The usual definition of the ordered pair, namely
12691:
12513:
11956:
Quine, W. V. (1937), "New Foundations for Mathematical Logic",
11268:
11220:
11118:
11070:
11034:
10993:
9789:
is never applied to a bound variable. Choose any free variable
9433:
It may now be proved that this actually is a model of NFU. Let
6227:, or equivalently, whether there exists a set with the largest
5844:-complete nonprincipal ultrafilter on the proper class ordinal
11751:
Set theory with a universal set. Exploring an untyped universe
11338:
11336:
10781:
higher type, and preserves equality and membership relations.
6123:
cannot be stratified. NF steers clear of the three well-known
5172:
Since inductive sets always exist, the set of natural numbers
4682:, results in a type two higher than the type of its arguments
820:{\displaystyle A\times B=\{(a,b)|a\in A{\text{ and }}b\in B\}}
13773:
13119:
12964:
12563:
12323:
12259:
11280:
10812:
6223:
boils down to the question of whether there exists a largest
6041:
5962:
3948:
objects with the same elements are the same object; formally,
3189:{\displaystyle {\text{TL}}(S)=\{z:\forall w:(w,\{z\})\in S\}}
11699:"Why the Sets of NF do not form a Cartesian-closed Category"
9747:{\displaystyle (\forall x\in j^{N-i}(V_{\alpha }).\psi (x))}
9668:{\displaystyle (\forall x\in V_{\alpha }.\psi (j^{N-i}(x)))}
9184:
The domain of the model of NFU will be the nonstandard rank
8279:
is the usual Kuratowski ordered pair (two types higher than
8106:{\displaystyle R_{\alpha }=\{(x,y)\mid x\leq y<\alpha \}}
5014:
3678:
whose arguments were not necessarily all of the same types.
11429:
11333:
10059:
has this extension in the model of NFU (the application of
7574:
6873:
The usual way to correct such a type problem is to replace
5713:
can be proven (in which cases it may be referred to as the
5328:
is not a "finite set", i.e., that the size of the universe
11988:(first ed.), New York: W. W. Norton & Co., Inc.,
7648:. This is a stratified definition, so the set of ordinals
6949:. Indeed, the correctly typed version of Cantor's theorem
6254:
is obviously a set with the largest cardinality. However,
4705:
As an alternative approach, Holmes takes the ordered pair
1306:{\displaystyle {\text{dom}}(R)=\{x|\exists y.(x,y)\in R\}}
596:. This can also be viewed as defining the equality symbol.
11292:
11130:
10186:
9146:
of sets. We may suppose without loss of generality that
6052:
NF may seem to run afoul of problems similar to those in
5865:
5816:
proves the existence of a type-level ordered pair. NFU +
5542:
It may intuitively seem that one should be able to prove
11208:
11046:
10887:
10790:
discussed a subtheory of NFI, in which only parameters (
10721:; hence the name. Quine extended the theory in his book
6047:
5039:
elements. Under this definition, 0 is easily defined as
11232:
11186:
11184:
11169:
11147:
11145:
11094:
11082:
11024:
11022:
11020:
11005:
10877:
10875:
10873:
6597:
should be assigned the same type, so the definition of
6036:; Since NF lacks Cartesian closure, not every function
5936:, and the entire set-theoretic universe under NF has a
4233:{\displaystyle \forall xy.x\in y\to \mathrm {set} (y).}
11353:
11351:
10969:
10565:
in the nonstandard model (we suppose here that we use
6215:
5434:(it can be shown inductively that a finite set is not
4675:{\displaystyle (a,\ b)_{K}\;:=\ \{\{a\},\ \{a,\ b\}\}}
1493:{\displaystyle =\cap (1\times V)=\{(\{x\},y)|x\in y\}}
120:). NF can be presented with only two axiom schemata:
11612:
11585:
11311:
11309:
11307:
10603:
10518:
10491:
10460:
10422:
10395:
10368:
10335:
10308:
10259:
10223:
10196:
10149:
10125:
10080:
10052:{\displaystyle j(\{y\in V_{\alpha }\mid \phi _{3}\})}
10004:
9984:
9947:
9891:
9856:
9823:
9799:
9764:
9681:
9602:
9572:
9537:
9527:
is an automorphism. Make such an application to each
9483:
9463:
9439:
9327:
9281:
9254:
9221:
9190:
9152:
9121:
9034:
9014:
8940:
8927:{\displaystyle \{\alpha \mid T(\alpha )<\alpha \}}
8893:
8867:
8823:
8774:
8750:
8714:
8674:
8638:
8615:
8536:
8507:
8481:
8461:
8425:
8405:
8376:
8349:
8325:
8305:
8285:
8253:
8226:
8175:
8139:
8119:
8050:
8030:
8006:
7979:
7959:
7939:
7919:
7892:
7872:
7852:
7818:
7790:
7770:
7750:
7712:
7686:
7654:
7615:
7595:
7517:
7497:
7427:
7407:
7381:
7361:
7299:
7266:
7227:
7136:
7100:
7026:
6955:
6935:
6899:
6879:
6817:
6797:
6768:
6713:
6690:
6664:
6623:
6603:
6574:
6554:
6495:
6471:
6451:
6422:
6389:
6369:
6340:
6316:
6296:
6267:
6240:
6176:
6150:
6103:
6065:
5995:
5889:
5778:
5758:
5735:
5682:
5652:
5618:
5552:
5515:
5491:
5444:
5408:
5364:
5334:
5314:
5282:
5233:
5204:
5178:
5151:
5071:
5045:
4936:
4916:
4884:
4830:
4776:
4749:
4722:
4600:
4459:
4430:
4389:
4252:
4182:
4172:
to distinguish sets from atoms. The axioms are then:
4141:
4109:
4068:
3958:
3908:
3882:
3851:
3822:
3802:
3776:
3736:
3696:
3640:
3567:
3533:
3427:
3390:
3321:
3285:
3231:
3120:
3100:
3007:
2917:
2897:
2818:
2798:
2741:
2700:
2627:
2602:
2582:
2485:
2465:
2445:
2422:
2342:
2322:
2255:
2169:
2086:
2057:
2031:
1981:
1949:
1929:
1909:
1889:
1869:
1827:
1807:
1761:
1738:
1718:
1647:
1627:
1607:
1584:
1531:
1511:
1406:
1342:
1319:
1241:
1221:
1198:
1113:
1093:
1064:
1028:
948:
928:
899:
873:
853:
833:
755:
735:
715:
692:
625:
605:
576:
556:
536:
516:
496:
476:
456:
436:
380:
354:
318:
292:
272:
241:
217:
182:
106:
82:
12061:
Rosser, Barkley (1942), "The Burali-Forti paradox",
12028:, 1980, "New Foundations for Mathematical Logic" in
11196:
11181:
11157:
11142:
11106:
11058:
11017:
10906:
10904:
10902:
10870:
10362:
in a type-respecting manner). Given an embedding of
9850:
uniformly to the entire formula to obtain a formula
8817:(order-preserving) operation on the ordinals, i.e.,
8609:
The order type of the natural order on the ordinals
8598:{\displaystyle W^{\iota }=\{(\{x\},\{y\})\mid xWy\}}
6704:
is the same (ill-defined) set in Russell's paradox.
1185:{\displaystyle R\iota =\{(\{x\},\{y\})|(x,y)\in R\}}
11550:"Timothy Chow on the NF consistency proof and Lean"
11491:
11405:
11348:
10981:
10957:
10916:
10733:. The first edition's set theory married NF to the
10181:
Self-sufficiency of mathematical foundations in NFU
10074:holds is straightforward: each nonempty element of
5004:{\displaystyle \pi _{1}=\{((a,b),a)\mid a,b\in V\}}
3213:), a streamlined version of the theory of types of
2687:{\displaystyle x|y=\{z:\neg (z\in x\land z\in y)\}}
11805:Hailperin, T (1944). "A set of axioms for logic".
11618:
11598:
11503:
11467:
11321:
11304:
10625:
10531:
10504:
10473:
10435:
10408:
10381:
10354:
10321:
10294:
10245:
10209:
10155:
10131:
10108:
10051:
9990:
9966:
9930:{\displaystyle \{y\in V_{\alpha }\mid \phi _{3}\}}
9929:
9869:
9842:
9805:
9777:
9746:
9667:
9584:
9550:
9496:
9469:
9445:
9423:
9309:
9267:
9240:
9203:
9173:
9134:
9040:
9020:
8993:
8926:
8879:
8853:
8802:
8756:
8736:
8696:
8660:
8624:
8597:
8522:
8493:
8467:
8447:
8411:
8391:
8355:
8331:
8311:
8291:
8271:
8239:
8213:{\displaystyle \beta =\{S\mid S\sim R_{\alpha }\}}
8212:
8157:
8125:
8105:
8036:
8012:
7992:
7965:
7945:
7925:
7910:ordinals, not any proper initial segment of them.
7898:
7878:
7858:
7838:
7804:
7776:
7756:
7736:
7698:
7668:
7621:
7601:
7547:
7503:
7475:
7413:
7393:
7367:
7347:
7282:
7252:
7209:
7118:
7083:
7012:
6941:
6921:
6885:
6858:
6803:
6783:
6754:
6696:
6676:
6650:
6609:
6589:
6560:
6540:
6477:
6457:
6437:
6401:
6375:
6355:
6322:
6302:
6282:
6246:
6200:
6162:
6115:
6089:
6007:
5901:
5796:
5764:
5741:
5698:
5668:
5634:
5596:
5532:
5497:
5477:
5426:
5394:
5350:
5320:
5297:
5268:
5219:
5186:
5157:
5137:
5057:
5003:
4922:
4902:
4870:
4816:
4762:
4735:
4674:
4585:are defined in TST (and in NF and NFU) as sets of
4536:
4445:
4416:
4370:
4232:
4164:
4124:
4095:
4051:
3914:
3894:
3857:
3837:
3808:
3788:
3762:
3722:
3662:
3623:{\displaystyle \{x^{n}\mid \phi (x^{n})\}^{n+1}\!}
3622:
3553:
3519:
3413:
3377:{\displaystyle \{x^{n}\mid \phi (x^{n})\}^{n+1}\!}
3376:
3307:
3244:
3188:
3106:
3083:
2993:
2903:
2880:
2804:
2781:
2727:
2686:
2608:
2588:
2568:
2471:
2451:
2428:
2408:
2328:
2305:
2238:
2155:
2069:
2043:
2017:
1967:
1935:
1915:
1895:
1875:
1852:
1813:
1793:
1744:
1724:
1704:
1633:
1613:
1590:
1570:
1517:
1492:
1392:
1325:
1305:
1227:
1204:
1184:
1099:
1076:
1050:
1014:
934:
911:
885:
859:
839:
819:
741:
721:
698:
678:
611:
588:
562:
542:
522:
502:
482:
462:
442:
386:
366:
324:
304:
278:
247:
223:
200:
112:
88:
11964:(2), Mathematical Association of America: 70–80,
11417:
10899:
10542:
10454:one needs a type containing a set of cardinality
6170:is not a stratified formula, so the existence of
6040:as one might intuitively expect, and NF is not a
5932:. An immediate consequence is that all sets have
3619:
3550:
3410:
3373:
2336:is a set all of whose elements are sets, the set
14679:
12249:Bibliography of Set Theory with a Universal Set.
11790:"Consistency of a fragment of Quine's NF system"
11479:
5533:{\displaystyle \varnothing \notin \mathbf {N} .}
4702:, and therefore does not directly work in NFU.
12114:Proceedings of the National Academy of Sciences
11579:We talk about the automorphism moving the rank
5025:von Neumann construction of the natural numbers
3084:{\displaystyle I_{3}(R)=\{(z,w,t):(z,w)\in R\}}
2994:{\displaystyle I_{2}(R)=\{(z,w,t):(z,t)\in R\}}
2239:{\displaystyle \pi _{2}=\{((x,y),y)|x,y\in V\}}
2156:{\displaystyle \pi _{1}=\{((x,y),x)|x,y\in V\}}
1801:exists. It is straightforward that for any set
12161:Wang, Hao (1950), "A formal system of logic",
8366:To correct such a type problem, one needs the
7487:: a Cantorian set satisfies the usual form of
5953:. In NF (and TST), the set of all sets having
5840:plus a predicate on proper classes which is a
5485:, and each subsequent natural number would be
5269:{\displaystyle \{n\in \mathbf {N} \mid P(n)\}}
4246:with the same elements are the same set, i.e.
1400:exists. Equivalently, we may consider the set
12935:
12275:
11903:
11298:
6541:{\displaystyle B=\{x\in A\mid x\notin f(x)\}}
6383:), which seems to imply a contradiction when
10043:
10011:
9924:
9892:
9504:in the language of the nonstandard model of
8921:
8894:
8592:
8574:
8568:
8562:
8556:
8550:
8475:. The T operation is defined as follows: If
8207:
8182:
8100:
8064:
7539:
7533:
7527:
7113:
7107:
6535:
6502:
6195:
6177:
6084:
6066:
5791:
5785:
5585:
5582:
5574:
5571:
5565:
5559:
5421:
5415:
5263:
5234:
5129:
5102:
5096:
5087:
5052:
5046:
4998:
4950:
4897:
4885:
4669:
4666:
4651:
4642:
4636:
4633:
4411:
4390:
4090:
4069:
3604:
3568:
3520:{\displaystyle \exists A^{n+1}\forall x^{n}}
3358:
3322:
3183:
3171:
3165:
3138:
3078:
3030:
2988:
2940:
2875:
2819:
2681:
2642:
2563:
2506:
2403:
2358:
2300:
2268:
2233:
2183:
2150:
2100:
1788:
1768:
1699:
1660:
1565:
1545:
1487:
1461:
1455:
1449:
1387:
1355:
1300:
1259:
1179:
1147:
1141:
1135:
1129:
1123:
1009:
965:
814:
768:
673:
653:
647:
641:
195:
183:
16:Axiomatic set theory devised by W.V.O. Quine
10858:Set-theoretic definition of natural numbers
10848:Implementation of mathematics in set theory
9101:, one can construct a nonstandard model of
7886:, which would imply an contradiction since
7511:which satisfies the further condition that
7210:{\displaystyle |P_{1}(V)|<|P(V)|\ll |V|}
5035:is represented by the set of all sets with
4568:implementation of mathematics in set theory
4103:will not be unique if it is empty (i.e. if
3217:with a linear hierarchy of types. In this
1015:{\displaystyle R^{-1}=\{(x,y)|(y,x)\in R\}}
13127:
12942:
12928:
12282:
12268:
11847:Elementary set theory with a universal set
10653:and let it have the following properties:
10481:, which cannot be proved to exist in TSTU+
9211:. The basic idea is that the automorphism
8704:, depending on which ordered pair is used.
7421:which satisfies the intuitively appealing
4626:
3384:exists. In other words, given any formula
12143:
12133:
11904:Holmes, M. Randall; Wilshaw, Sky (2024).
11804:
11274:
11250:
11226:
11124:
11100:
11076:
11040:
10999:
10934:
10881:
8803:{\displaystyle T^{2}(\Omega )<\Omega }
8169:, and the order type (equivalence class)
7839:{\displaystyle \Omega \in \mathrm {Ord} }
7567:, is a set is not only Cantorian set but
5612:of NFU: There exists models of NFU where
5015:Natural numbers and the axiom of infinity
3925:
679:{\displaystyle \iota (x)=\{x\}=\{y|y=x\}}
12043:Selected Logic Papers - Enlarged Edition
9056:Some mathematicians have questioned the
7737:{\displaystyle R\in \alpha ,S\in \beta }
7575:Burali-Forti paradox and the T operation
7548:{\displaystyle (x\mapsto \{x\})\lceil A}
5676:, making it impossible to "distinguish"
413:
12104:
11787:
11774:
11748:
11712:
11696:
11497:
11411:
11357:
10574:in the construction of the model), and
9112:(not a set of the model) which moves a
8854:{\displaystyle T(\alpha )<T(\beta )}
8399:, that "raises the type" of an ordinal
5772:is equinumerous with its proper subset
1393:{\displaystyle =\{(x,y)|x\subseteq y\}}
686:exists, and is called the singleton of
348:) + 1, while for any atomic subformula
14680:
12949:
12255:A new pass at the NF consistency proof
12120:(9). National Acad Sciences: 972–975.
12060:
11915:
11874:
11843:
11676:
11639:
11509:
11473:
11435:
11369:
11342:
11327:
11315:
11286:
11262:
11238:
11214:
11202:
11190:
11175:
11163:
11151:
11136:
11112:
11088:
11064:
11052:
11028:
11011:
10987:
10975:
10963:
10922:
10910:
10893:
10772:). In 1969, Jensen showed that adding
10719:New Foundations for Mathematical Logic
10302:coding embeddings of the power set of
5358:is not a natural number. Suppose that
3685:
3207:Russellian unramified typed set theory
3205:New Foundations is closely related to
12923:
12263:
12039:
11999:
11983:
11955:
11521:
11447:
11423:
10819:), with NF, and then showing that TTT
9174:{\displaystyle j(\alpha )<\alpha }
9078:Gödel's second incompleteness theorem
6707:This failure is not surprising since
6201:{\displaystyle \{x\mid x\not \in x\}}
6090:{\displaystyle \{x\mid x\not \in x\}}
6048:Resolution of set-theoretic paradoxes
5989:between them, in which case we write
5961:here is only apparent) exists. Hence
5478:{\displaystyle n+1=S(n)=\varnothing }
5395:{\displaystyle |V|=n\in \mathbf {N} }
2313:exists, called the equality relation.
1571:{\displaystyle A^{c}=\{x|x\notin A\}}
12160:
11697:Forster, Thomas (October 14, 2007).
11679:"New Foundations Explorer Home Page"
11547:
11485:
9275:into its externally isomorphic copy
7084:{\displaystyle |P_{1}(V)|<|P(V)|}
7013:{\displaystyle |P_{1}(A)|<|P(A)|}
6929:, the set of one-element subsets of
6135:
6027:
6015:. Likewise, an ordinal number is an
5709:However, there are some cases where
12222:Stanford Encyclopedia of Philosophy
11781:Stanford Encyclopedia of Philosophy
9978:which satisfy the original formula
9881:appears without any application of
7906:by definition is the order type of
7629:is larger than all those ordinals.
6762:makes no sense in TST: the type of
6216:Cantor's paradox and Cantorian sets
6208:is not asserted by any instance of
5985:are equinumerous if there exists a
4424:exists for each stratified formula
4176:Sets: Only sets have members, i.e.
3200:
2782:{\displaystyle x\cup y=x^{c}|y^{c}}
68:of NF are the standard formulas of
13:
12234:Alternative axiomatic set theories
11372:"Strong axioms of infinity in NFU"
10641:is any object in the universe, to
10586:) will be a well-ordering of type
9685:
9606:
8982:
8960:
8941:
8797:
8788:
8751:
8166:
7893:
7832:
7829:
7826:
7819:
7798:
7795:
7792:
7699:{\displaystyle \alpha \leq \beta }
7662:
7659:
7656:
7616:
7596:
4495:
4476:
4473:
4470:
4460:
4417:{\displaystyle \{x\mid \phi (x)\}}
4317:
4298:
4295:
4292:
4275:
4272:
4269:
4253:
4214:
4211:
4208:
4183:
4149:
4146:
4143:
4096:{\displaystyle \{x\mid \phi (x)\}}
4010:
3959:
3447:
3428:
3315: is a formula, then the set
3147:
2842:
2830:
2651:
1270:
1087:Singleton Image: For any relation
827:, called the Cartesian product of
14:
14714:
12205:
12000:Quine, Willard Van Orman (1951),
11984:Quine, Willard Van Orman (1940),
11958:The American Mathematical Monthly
11715:"The iterative conception of set"
11370:Holmes, M. Randall (March 2001).
9558:in such a way that each variable
9080:because NFU does not include the
8880:{\displaystyle \alpha <\beta }
5562:
5472:
5438:with any of its proper subsets),
5049:
4871:{\displaystyle \pi _{2}((a,b))=b}
4817:{\displaystyle \pi _{1}((a,b))=a}
4165:{\displaystyle \mathrm {set} (x)}
2891:Tuple Insertions: For a relation
2576:, called the relative product of
2306:{\displaystyle =\{(x,x)|x\in V\}}
14661:
12313:
10937:, Definition 1.02 and Axiom PId.
10474:{\displaystyle \beth _{\omega }}
10109:{\displaystyle V_{j(\alpha )+1}}
9310:{\displaystyle V_{j(\alpha )+1}}
9092:
7706:iff there exists well-orderings
7676:can be defined with no problem.
5523:
5388:
5244:
5180:
5058:{\displaystyle \{\varnothing \}}
4713:, as well as its left and right
4692:Quine's set-theoretic definition
4573:
4561:
1712:, called the (Boolean) union of
1192:, called the singleton image of
709:Cartesian Product: For any sets
11906:"New Foundations is consistent"
11573:
11541:
11515:
11441:
11363:
8530:is the order type of the order
6791:is one higher than the type of
6097:is not an axiom of NF, because
5706:from standard natural numbers.
4903:{\displaystyle \{x\mid \phi \}}
201:{\displaystyle \{x\mid \phi \}}
12289:
11522:Smith, Peter (21 April 2024).
11448:Smith, Peter (21 April 2024).
10940:
10626:{\displaystyle V_{j(\alpha )}}
10618:
10612:
10295:{\displaystyle P_{1}(T_{i+1})}
10289:
10270:
10240:
10227:
10095:
10089:
10046:
10008:
9741:
9738:
9732:
9723:
9710:
9682:
9662:
9659:
9656:
9650:
9631:
9603:
9407:
9401:
9375:
9369:
9296:
9290:
9162:
9156:
9051:
8985:
8979:
8963:
8957:
8912:
8906:
8848:
8842:
8833:
8827:
8791:
8785:
8737:{\displaystyle T^{2}(\alpha )}
8731:
8725:
8697:{\displaystyle T^{4}(\alpha )}
8691:
8685:
8661:{\displaystyle T^{2}(\alpha )}
8655:
8649:
8577:
8553:
8517:
8511:
8442:
8436:
8386:
8380:
8266:
8254:
8152:
8140:
8079:
8067:
7805:{\displaystyle \mathrm {Ord} }
7669:{\displaystyle \mathrm {Ord} }
7536:
7524:
7518:
7476:{\displaystyle |A|=|P_{1}(A)|}
7469:
7465:
7459:
7445:
7437:
7429:
7348:{\displaystyle |A|=|P_{1}(A)|}
7341:
7337:
7331:
7317:
7309:
7301:
7276:
7268:
7246:
7242:
7236:
7229:
7203:
7195:
7187:
7183:
7177:
7170:
7162:
7158:
7152:
7138:
7119:{\displaystyle x\mapsto \{x\}}
7104:
7077:
7073:
7067:
7060:
7052:
7048:
7042:
7028:
7006:
7002:
6996:
6989:
6981:
6977:
6971:
6957:
6916:
6910:
6852:
6848:
6842:
6835:
6827:
6819:
6778:
6772:
6748:
6744:
6738:
6731:
6723:
6715:
6668:
6642:
6639:
6633:
6617:is not stratified. Indeed, if
6584:
6578:
6532:
6526:
6432:
6426:
6350:
6344:
6277:
6271:
5725:), Specker has shown that the
5692:
5684:
5662:
5654:
5628:
5620:
5466:
5460:
5374:
5366:
5344:
5336:
5292:
5286:
5260:
5254:
5214:
5208:
5081:
5075:
4977:
4968:
4956:
4953:
4859:
4856:
4844:
4841:
4805:
4802:
4790:
4787:
4617:
4601:
4528:
4525:
4519:
4513:
4492:
4486:
4480:
4440:
4434:
4408:
4402:
4353:
4350:
4347:
4335:
4314:
4308:
4302:
4285:
4279:
4265:
4224:
4218:
4204:
4159:
4153:
4119:
4113:
4087:
4081:
4046:
4043:
4040:
4028:
4007:
4004:
3992:
3989:
3986:
3974:
3832:
3826:
3763:{\displaystyle x^{m}\in y^{n}}
3657:
3644:
3600:
3587:
3514:
3511:
3498:
3492:
3460:
3414:{\displaystyle \phi (x^{n})\!}
3407:
3394:
3354:
3341:
3302:
3289:
3174:
3156:
3132:
3126:
3069:
3057:
3051:
3033:
3024:
3018:
2979:
2967:
2961:
2943:
2934:
2928:
2872:
2860:
2839:
2826:
2765:
2718:
2678:
2654:
2632:
2525:
2521:
2509:
2500:
2493:
2486:
2365:
2352:
2346:
2287:
2283:
2271:
2262:
2256:
2214:
2210:
2201:
2189:
2186:
2131:
2127:
2118:
2106:
2103:
2012:
2000:
1994:
1982:
1962:
1950:
1775:
1667:
1552:
1474:
1470:
1452:
1443:
1431:
1425:
1419:
1413:
1407:
1374:
1370:
1358:
1349:
1343:
1291:
1279:
1266:
1253:
1247:
1170:
1158:
1154:
1150:
1126:
1000:
988:
984:
980:
968:
787:
783:
771:
660:
635:
629:
470:are sets, and for each object
72:with two primitive predicates
1:
14622:History of mathematical logic
12034:American Mathematical Monthly
11642:The Journal of Symbolic Logic
11633:
10543:Facts about the automorphism
9974:, and contains exactly those
9967:{\displaystyle V_{\alpha +1}}
9675:can be converted to the form
9241:{\displaystyle V_{\alpha +1}}
8455:"raises the type" of the set
6859:{\displaystyle |A|<|P(A)|}
6755:{\displaystyle |A|<|P(A)|}
5851:
5797:{\displaystyle V\times \{0\}}
5276:can be constructed, and when
1853:{\displaystyle x\cup x^{c}=V}
174:axiom schema of comprehension
59:
14547:Primitive recursive function
12046:. Harvard University Press.
12030:From a Logical Point of View
11722:The Review of Symbolic Logic
11548:Chow, Timothy (3 May 2024).
8494:{\displaystyle W\in \alpha }
5498:{\displaystyle \varnothing }
5187:{\displaystyle \mathbf {N} }
4770:, i.e., functions such that
3663:{\displaystyle \phi (x^{n})}
3308:{\displaystyle \phi (x^{n})}
3267:+1 objects are sets of type
2416:, called the (set) union of
922:Converse: For each relation
599:Singleton: For every object
7:
11844:Holmes, M. Randall (1998),
11599:{\displaystyle V_{\alpha }}
11253:, p. 10, Axioms P3,P4.
10831:
10532:{\displaystyle V_{\alpha }}
10505:{\displaystyle T_{\alpha }}
10436:{\displaystyle T_{\alpha }}
10067:holds in the model of NFU.
9268:{\displaystyle V_{\alpha }}
9204:{\displaystyle V_{\alpha }}
9135:{\displaystyle V_{\alpha }}
9028:is a model of NFU, despite
8625:{\displaystyle <\alpha }
8240:{\displaystyle R_{\alpha }}
7993:{\displaystyle R_{\alpha }}
6651:{\displaystyle f:P(V)\to V}
6163:{\displaystyle x\not \in x}
6116:{\displaystyle x\not \in x}
5644:non-standard natural number
5031:, i.e., the natural number
4910:for any stratified formula
3865:is an increasing function.
3723:{\displaystyle x^{n}=y^{n}}
3674:, which included types for
3252:denotes a variable of type
3094:Type lowering: For any set
2018:{\displaystyle (a,b)=(c,d)}
1794:{\displaystyle V=\{x|x=x\}}
1578:, called the complement of
46:as a simplification of the
10:
14719:
13611:Schröder–Bernstein theorem
13338:Monadic predicate calculus
12997:Foundations of mathematics
12780:von Neumann–Bernays–Gödel
12243:New Foundations Home Page.
10692:
10512:'s being used in place of
8523:{\displaystyle T(\alpha )}
8392:{\displaystyle T(\alpha )}
8000:on the ordinals less than
6677:{\displaystyle x\mapsto x}
6258:says (given ZFC) that the
5198:for stratified statements
4555:is the same theory as NF.
14657:
14644:Philosophy of mathematics
14593:Automated theorem proving
14575:
14470:
14302:
14195:
14047:
13764:
13740:
13718:Von Neumann–Bernays–Gödel
13663:
13557:
13461:
13359:
13350:
13277:
13212:
13118:
13040:
12957:
12844:
12807:
12719:
12609:
12581:One-to-one correspondence
12497:
12438:
12322:
12311:
12297:
12163:Journal of Symbolic Logic
12063:Journal of Symbolic Logic
11952:With discussion by Quine.
11889:10.1007/s11225-008-9107-8
11808:Journal of Symbolic Logic
11777:"Quine's New Foundations"
11734:10.1017/S1755020308080064
11524:"NF really is consistent"
11450:"NF really is consistent"
11379:Journal of Symbolic Logic
11299:Holmes & Wilshaw 2024
9870:{\displaystyle \phi _{3}}
9778:{\displaystyle \phi _{2}}
9551:{\displaystyle \phi _{1}}
9497:{\displaystyle \phi _{1}}
8768:ordinals. In particular,
6658:is the trivial injection
3944:Weak extensionality: Two
3902:is the power set of type
3554:{\displaystyle A^{n+1}\!}
2728:{\displaystyle x^{c}=x|x}
1505:Complement: For each set
912:{\displaystyle V\times B}
886:{\displaystyle A\times V}
11606:rather than the ordinal
10863:
10768:is false in NF (without
10578:has type α in NFU, then
10246:{\displaystyle P(T_{i})}
10065:Stratified Comprehension
8448:{\displaystyle P_{1}(A)}
8220:is one type higher than
8113:is one type higher than
7913:However, the statement "
7784:) is a well-ordering of
7293:However, unlike in TST,
6922:{\displaystyle P_{1}(A)}
6487:diagonalization argument
4763:{\displaystyle \pi _{2}}
4736:{\displaystyle \pi _{1}}
4446:{\displaystyle \phi (x)}
4125:{\displaystyle \phi (x)}
3816:is mapped to a variable
1051:{\displaystyle xR^{-1}y}
14703:Willard Van Orman Quine
14294:Self-verifying theories
14115:Tarski's axiomatization
13066:Tarski's undefinability
13061:incompleteness theorems
12228:Quine's New Foundations
11788:Grishin, V. N. (1969).
11775:Forster, T. E. (2018).
11749:Forster, T. E. (1992),
11713:Forster, T. E. (2008).
11619:{\displaystyle \alpha }
11277:, p. 10, Axiom P6.
11229:, p. 10, Axiom P8.
11127:, p. 10, Axiom P9.
11079:, p. 10, Axiom P2.
11043:, p. 10, Axiom P7.
11002:, p. 10, Axiom P5.
10715:Willard Van Orman Quine
10701:showed how to code the
10355:{\displaystyle T_{i+1}}
10156:{\displaystyle \alpha }
10132:{\displaystyle \alpha }
9843:{\displaystyle j^{i-N}}
9756:existential quantifiers
8757:{\displaystyle \Omega }
8412:{\displaystyle \alpha }
8356:{\displaystyle \alpha }
8167:type-level ordered pair
8126:{\displaystyle \alpha }
8037:{\displaystyle \alpha }
8013:{\displaystyle \alpha }
7946:{\displaystyle \alpha }
7926:{\displaystyle \alpha }
7899:{\displaystyle \Omega }
7879:{\displaystyle \alpha }
7859:{\displaystyle \alpha }
7622:{\displaystyle \Omega }
7602:{\displaystyle \Omega }
6489:by considering the set
6008:{\displaystyle A\sim B}
5838:Morse–Kelley set theory
5836:which is equivalent to
5427:{\displaystyle n=\{V\}}
2479:are relations, the set
1863:Ordered Pair: For each
1313:, called the domain of
1235:is a relation, the set
44:Willard Van Orman Quine
14668:Mathematics portal
14279:Proof of impossibility
13927:propositional variable
13237:Propositional calculus
12539:Constructible universe
12359:Constructibility (V=L)
11677:Fenton, Scott (2015).
11620:
11600:
10838:Alternative set theory
10649:). Call this function
10627:
10533:
10506:
10475:
10437:
10410:
10383:
10356:
10323:
10296:
10247:
10211:
10157:
10133:
10110:
10053:
9992:
9968:
9931:
9871:
9844:
9807:
9779:
9748:
9669:
9586:
9552:
9498:
9471:
9447:
9425:
9311:
9269:
9242:
9215:codes the "power set"
9205:
9175:
9136:
9042:
9022:
8995:
8928:
8881:
8855:
8804:
8758:
8738:
8698:
8662:
8626:
8599:
8524:
8495:
8469:
8449:
8413:
8393:
8357:
8333:
8332:{\displaystyle \beta }
8313:
8293:
8273:
8241:
8214:
8159:
8127:
8107:
8038:
8014:
7994:
7967:
7966:{\displaystyle \beta }
7947:
7927:
7900:
7880:
7860:
7840:
7806:
7778:
7758:
7738:
7700:
7670:
7623:
7603:
7549:
7505:
7477:
7415:
7395:
7369:
7349:
7284:
7254:
7253:{\displaystyle |P(V)|}
7211:
7120:
7085:
7014:
6943:
6923:
6887:
6860:
6805:
6785:
6756:
6698:
6678:
6652:
6611:
6591:
6562:
6542:
6479:
6459:
6439:
6412:Of course there is an
6403:
6377:
6357:
6334:(one-to-one map) from
6324:
6304:
6284:
6248:
6202:
6164:
6117:
6091:
6009:
5903:
5798:
5766:
5743:
5700:
5670:
5636:
5598:
5534:
5499:
5479:
5428:
5396:
5352:
5322:
5299:
5270:
5221:
5196:mathematical induction
5188:
5159:
5139:
5059:
5019:The usual form of the
5005:
4924:
4904:
4872:
4818:
4764:
4737:
4676:
4538:
4447:
4418:
4372:
4234:
4166:
4126:
4097:
4053:
3926:NFU and other variants
3916:
3896:
3859:
3839:
3810:
3790:
3789:{\displaystyle m<n}
3764:
3724:
3664:
3624:
3555:
3521:
3415:
3378:
3309:
3246:
3190:
3108:
3085:
2995:
2905:
2882:
2806:
2792:Cardinal one: The set
2783:
2729:
2688:
2610:
2590:
2570:
2473:
2453:
2430:
2410:
2330:
2307:
2240:
2157:
2080:Projections: The sets
2071:
2045:
2019:
1969:
1937:
1917:
1903:, the ordered pair of
1897:
1877:
1854:
1815:
1795:
1746:
1726:
1706:
1635:
1615:
1592:
1572:
1519:
1494:
1394:
1327:
1307:
1229:
1206:
1186:
1101:
1078:
1052:
1016:
936:
913:
887:
861:
841:
821:
743:
723:
700:
680:
613:
590:
564:
544:
524:
504:
484:
464:
444:
388:
368:
326:
306:
305:{\displaystyle x\in y}
280:
249:
225:
202:
114:
90:
70:propositional calculus
37:finitely axiomatizable
14688:Systems of set theory
14537:Kolmogorov complexity
14490:Computably enumerable
14390:Model complete theory
14182:Principia Mathematica
13242:Propositional formula
13071:Banach–Tarski paradox
12762:Principia Mathematica
12596:Transfinite induction
12455:(i.e. set difference)
12135:10.1073/pnas.39.9.972
11794:Dokl. Akad. Nauk SSSR
11621:
11601:
10802:axiom of reducibility
10797:Principia Mathematica
10707:Principia Mathematica
10628:
10534:
10507:
10476:
10438:
10411:
10409:{\displaystyle T_{1}}
10384:
10382:{\displaystyle T_{0}}
10357:
10324:
10322:{\displaystyle T_{i}}
10297:
10248:
10212:
10210:{\displaystyle T_{i}}
10158:
10134:
10111:
10054:
9998:in the model of NFU.
9993:
9991:{\displaystyle \phi }
9969:
9932:
9872:
9845:
9808:
9806:{\displaystyle \phi }
9780:
9749:
9670:
9587:
9553:
9499:
9472:
9470:{\displaystyle \phi }
9448:
9446:{\displaystyle \phi }
9426:
9312:
9270:
9243:
9206:
9176:
9137:
9043:
9023:
8996:
8929:
8882:
8856:
8805:
8759:
8739:
8699:
8663:
8627:
8600:
8525:
8496:
8470:
8450:
8414:
8394:
8358:
8334:
8314:
8294:
8274:
8272:{\displaystyle (x,y)}
8242:
8215:
8160:
8158:{\displaystyle (x,y)}
8128:
8108:
8044:: The order relation
8039:
8015:
7995:
7973:of the natural order
7968:
7948:
7928:
7901:
7881:
7861:
7841:
7807:
7779:
7764:is a continuation of
7759:
7739:
7701:
7678:Transfinite induction
7671:
7624:
7604:
7550:
7506:
7478:
7416:
7396:
7370:
7350:
7285:
7255:
7212:
7121:
7086:
7015:
6944:
6924:
6888:
6870:is unlikely to work.
6861:
6806:
6786:
6757:
6699:
6679:
6653:
6612:
6592:
6563:
6543:
6480:
6460:
6440:
6404:
6378:
6358:
6325:
6305:
6285:
6249:
6203:
6165:
6118:
6092:
6010:
5904:
5799:
5767:
5744:
5701:
5671:
5637:
5610:logically independent
5599:
5535:
5500:
5480:
5429:
5397:
5353:
5323:
5300:
5271:
5222:
5189:
5160:
5140:
5060:
5006:
4925:
4923:{\displaystyle \phi }
4905:
4873:
4819:
4765:
4738:
4677:
4539:
4448:
4419:
4373:
4235:
4167:
4127:
4098:
4054:
3917:
3897:
3860:
3840:
3811:
3791:
3765:
3725:
3672:Principia Mathematica
3665:
3625:
3556:
3522:
3416:
3379:
3310:
3275:have members of type
3247:
3245:{\displaystyle x^{n}}
3215:Principia Mathematica
3191:
3109:
3086:
2996:
2906:
2883:
2807:
2784:
2730:
2689:
2611:
2591:
2571:
2474:
2454:
2439:Relative Product: If
2431:
2411:
2331:
2308:
2241:
2158:
2072:
2046:
2020:
1970:
1968:{\displaystyle (a,b)}
1938:
1918:
1898:
1878:
1855:
1816:
1796:
1747:
1727:
1707:
1636:
1616:
1593:
1573:
1520:
1495:
1395:
1328:
1308:
1230:
1207:
1187:
1102:
1079:
1053:
1022:exists; observe that
1017:
937:
914:
888:
862:
842:
822:
744:
724:
701:
681:
614:
591:
565:
545:
525:
505:
485:
465:
445:
414:Finite axiomatization
389:
387:{\displaystyle \phi }
369:
327:
325:{\displaystyle \phi }
307:
281:
279:{\displaystyle \phi }
250:
248:{\displaystyle \phi }
226:
224:{\displaystyle \phi }
203:
115:
91:
53:Principia Mathematica
14485:Church–Turing thesis
14472:Computability theory
13681:continuum hypothesis
13199:Square of opposition
13057:Gödel's completeness
12836:Burali-Forti paradox
12591:Set-builder notation
12544:Continuum hypothesis
12484:Symmetric difference
12236:— by Randall Holmes.
12230:— by Thomas Forster.
11610:
11583:
10843:Axiomatic set theory
10601:
10516:
10489:
10458:
10420:
10393:
10366:
10333:
10306:
10257:
10221:
10194:
10163:is infinite and the
10147:
10139:is a natural number
10123:
10078:
10002:
9982:
9945:
9889:
9854:
9821:
9797:
9762:
9679:
9600:
9570:
9566:occurs with exactly
9535:
9481:
9461:
9437:
9325:
9279:
9252:
9219:
9188:
9150:
9144:cumulative hierarchy
9119:
9067:Lean proof assistant
9032:
9012:
8938:
8891:
8865:
8821:
8772:
8764:, the order type of
8748:
8744:is always less than
8712:
8672:
8636:
8613:
8534:
8505:
8479:
8459:
8423:
8403:
8374:
8347:
8323:
8303:
8283:
8251:
8224:
8173:
8137:
8117:
8048:
8028:
8004:
7977:
7957:
7937:
7917:
7890:
7870:
7850:
7816:
7788:
7768:
7748:
7710:
7684:
7652:
7613:
7593:
7582:Burali-Forti paradox
7515:
7495:
7425:
7405:
7401:it is false). A set
7379:
7359:
7297:
7264:
7225:
7134:
7130:it is the case that
7098:
7024:
6953:
6933:
6897:
6877:
6815:
6795:
6784:{\displaystyle P(A)}
6766:
6711:
6688:
6662:
6621:
6601:
6590:{\displaystyle f(x)}
6572:
6552:
6493:
6469:
6449:
6438:{\displaystyle P(V)}
6420:
6387:
6367:
6356:{\displaystyle P(A)}
6338:
6314:
6294:
6283:{\displaystyle P(A)}
6265:
6238:
6174:
6148:
6101:
6063:
5993:
5887:
5808:. Conversely, NFU +
5776:
5756:
5733:
5680:
5650:
5616:
5550:
5513:
5489:
5442:
5406:
5362:
5332:
5312:
5298:{\displaystyle P(n)}
5280:
5231:
5220:{\displaystyle P(n)}
5202:
5176:
5149:
5069:
5043:
4934:
4914:
4882:
4828:
4774:
4747:
4720:
4598:
4457:
4428:
4387:
4250:
4242:Extensionality: Two
4180:
4139:
4107:
4066:
3956:
3906:
3880:
3849:
3838:{\displaystyle s(i)}
3820:
3800:
3774:
3734:
3694:
3638:
3565:
3531:
3425:
3388:
3319:
3283:
3229:
3118:
3098:
3005:
2915:
2895:
2816:
2796:
2739:
2698:
2625:
2600:
2580:
2483:
2463:
2443:
2420:
2340:
2320:
2253:
2167:
2084:
2055:
2029:
1979:
1947:
1927:
1907:
1887:
1867:
1825:
1805:
1759:
1736:
1716:
1645:
1625:
1605:
1601:(Boolean) Union: If
1582:
1529:
1509:
1404:
1340:
1317:
1239:
1219:
1196:
1111:
1091:
1062:
1026:
946:
926:
897:
871:
851:
831:
753:
733:
713:
690:
623:
603:
574:
554:
534:
514:
494:
474:
454:
434:
420:finitely axiomatized
378:
352:
316:
290:
270:
239:
215:
180:
113:{\displaystyle \in }
104:
80:
66:well-formed formulas
14639:Mathematical object
14530:P versus NP problem
14495:Computable function
14289:Reverse mathematics
14215:Logical consequence
14092:primitive recursive
14087:elementary function
13860:Free/bound variable
13713:Tarski–Grothendieck
13232:Logical connectives
13162:Logical equivalence
13012:Logical consequence
12797:Tarski–Grothendieck
12126:1953PNAS...39..972S
11706:www.dpmms.cam.ac.uk
10853:Positive set theory
9754:(and similarly for
9585:{\displaystyle N-i}
7638:equivalence classes
7394:{\displaystyle A=V}
7283:{\displaystyle |V|}
6402:{\displaystyle A=V}
5902:{\displaystyle x=x}
5715:theorem of infinity
5699:{\displaystyle |V|}
5669:{\displaystyle |V|}
5635:{\displaystyle |V|}
5351:{\displaystyle |V|}
4380:Comprehension: The
4132:is unsatisfiable).
3895:{\displaystyle i+1}
3686:Tangled Type Theory
3561:represents the set
2812:of all singletons,
2621:Anti-intersection:
2070:{\displaystyle b=d}
2044:{\displaystyle a=c}
1336:Inclusion: The set
1077:{\displaystyle yRx}
589:{\displaystyle A=B}
430:Extensionality: If
367:{\displaystyle x=y}
135:, if for every set
14437:Transfer principle
14400:Semantics of logic
14385:Categorical theory
14361:Non-standard model
13875:Logical connective
13002:Information theory
12951:Mathematical logic
12386:Limitation of size
12002:Mathematical logic
11986:Mathematical Logic
11933:10.1007/bf00568059
11616:
11596:
11265:, ax-ins2,ax-ins3.
10952:Mathematical Logic
10754:Theodore Hailperin
10723:Mathematical Logic
10623:
10529:
10502:
10471:
10433:
10406:
10379:
10352:
10319:
10292:
10243:
10207:
10153:
10129:
10106:
10049:
9988:
9964:
9927:
9867:
9840:
9803:
9775:
9744:
9665:
9582:
9548:
9506:Zermelo set theory
9494:
9467:
9443:
9421:
9307:
9265:
9248:of our "universe"
9238:
9201:
9171:
9132:
9103:Zermelo set theory
9038:
9018:
8991:
8924:
8877:
8851:
8800:
8754:
8734:
8694:
8658:
8622:
8595:
8520:
8491:
8465:
8445:
8409:
8389:
8353:
8343:types higher than
8329:
8309:
8289:
8269:
8237:
8210:
8155:
8123:
8103:
8034:
8024:types higher than
8010:
7990:
7963:
7943:
7923:
7896:
7876:
7856:
7836:
7802:
7774:
7754:
7734:
7696:
7666:
7619:
7599:
7569:strongly Cantorian
7545:
7501:
7473:
7411:
7391:
7365:
7345:
7280:
7250:
7207:
7116:
7081:
7010:
6939:
6919:
6883:
6856:
6801:
6781:
6752:
6694:
6674:
6648:
6607:
6587:
6558:
6538:
6475:
6455:
6435:
6399:
6373:
6353:
6320:
6300:
6280:
6244:
6198:
6160:
6140:The resolution of
6113:
6087:
6005:
5969:of sets under the
5911:stratified formula
5899:
5794:
5762:
5739:
5696:
5666:
5632:
5594:
5530:
5495:
5475:
5424:
5392:
5348:
5318:
5295:
5266:
5227:, because the set
5217:
5184:
5155:
5135:
5055:
5029:Frege's definition
5001:
4920:
4900:
4868:
4814:
4760:
4733:
4672:
4534:
4443:
4414:
4368:
4230:
4162:
4122:
4093:
4049:
3912:
3892:
3855:
3835:
3806:
3786:
3760:
3720:
3660:
3620:
3551:
3527:is an axiom where
3517:
3411:
3374:
3305:
3242:
3186:
3104:
3081:
2991:
2901:
2878:
2802:
2779:
2725:
2684:
2606:
2586:
2566:
2469:
2449:
2426:
2406:
2326:
2303:
2249:Diagonal: The set
2236:
2153:
2067:
2041:
2015:
1965:
1933:
1913:
1893:
1873:
1850:
1811:
1791:
1742:
1722:
1702:
1641:are sets, the set
1631:
1611:
1588:
1568:
1515:
1490:
1390:
1323:
1303:
1225:
1202:
1182:
1097:
1074:
1048:
1012:
932:
909:
883:
857:
837:
817:
739:
719:
696:
676:
609:
586:
560:
540:
520:
500:
480:
460:
440:
384:
364:
322:
302:
276:
259:if there exists a
245:
221:
210:stratified formula
198:
110:
86:
21:mathematical logic
14675:
14674:
14607:Abstract category
14410:Theories of truth
14220:Rule of inference
14210:Natural deduction
14191:
14190:
13736:
13735:
13441:Cartesian product
13346:
13345:
13252:Many-valued logic
13227:Boolean functions
13110:Russell's paradox
13085:diagonal argument
12982:First-order logic
12917:
12916:
12826:Russell's paradox
12775:Zermelo–Fraenkel
12676:Dedekind-infinite
12549:Diagonal argument
12448:Cartesian product
12305:Set (mathematics)
12106:Specker, Ernst P.
11178:, pp. 26–27.
10743:J. Barkley Rosser
10070:To see that weak
9082:Axiom of Infinity
9041:{\displaystyle V}
9021:{\displaystyle V}
8468:{\displaystyle A}
8312:{\displaystyle y}
8292:{\displaystyle x}
7777:{\displaystyle R}
7757:{\displaystyle S}
7504:{\displaystyle A}
7414:{\displaystyle A}
7368:{\displaystyle A}
6942:{\displaystyle A}
6886:{\displaystyle A}
6804:{\displaystyle A}
6697:{\displaystyle B}
6610:{\displaystyle B}
6561:{\displaystyle x}
6478:{\displaystyle V}
6458:{\displaystyle V}
6376:{\displaystyle A}
6330:(there can be no
6323:{\displaystyle A}
6303:{\displaystyle A}
6247:{\displaystyle V}
6142:Russell's paradox
6136:Russell's paradox
6028:Cartesian closure
6017:equivalence class
5967:equivalence class
5765:{\displaystyle V}
5742:{\displaystyle V}
5507:axiom of infinity
5321:{\displaystyle V}
5158:{\displaystyle V}
5021:axiom of infinity
4662:
4650:
4632:
4612:
3915:{\displaystyle i}
3858:{\displaystyle s}
3809:{\displaystyle i}
3225:as superscripts:
3124:
3107:{\displaystyle S}
2904:{\displaystyle R}
2805:{\displaystyle 1}
2609:{\displaystyle S}
2589:{\displaystyle R}
2552:
2532:
2472:{\displaystyle S}
2452:{\displaystyle R}
2429:{\displaystyle A}
2392:
2372:
2329:{\displaystyle A}
1936:{\displaystyle b}
1916:{\displaystyle a}
1896:{\displaystyle b}
1876:{\displaystyle a}
1814:{\displaystyle x}
1745:{\displaystyle B}
1725:{\displaystyle A}
1697:
1683:
1634:{\displaystyle B}
1614:{\displaystyle A}
1591:{\displaystyle A}
1518:{\displaystyle A}
1326:{\displaystyle R}
1245:
1228:{\displaystyle R}
1205:{\displaystyle R}
1100:{\displaystyle R}
935:{\displaystyle R}
860:{\displaystyle B}
840:{\displaystyle A}
803:
742:{\displaystyle B}
722:{\displaystyle A}
699:{\displaystyle x}
612:{\displaystyle x}
563:{\displaystyle B}
550:is an element of
543:{\displaystyle x}
523:{\displaystyle A}
510:is an element of
503:{\displaystyle x}
483:{\displaystyle x}
463:{\displaystyle B}
443:{\displaystyle A}
89:{\displaystyle =}
14710:
14666:
14665:
14617:History of logic
14612:Category of sets
14505:Decision problem
14284:Ordinal analysis
14225:Sequent calculus
14123:Boolean algebras
14063:
14062:
14037:
14008:logical/constant
13762:
13761:
13748:
13671:Zermelo–Fraenkel
13422:Set operations:
13357:
13356:
13294:
13125:
13124:
13105:Löwenheim–Skolem
12992:Formal semantics
12944:
12937:
12930:
12921:
12920:
12899:Bertrand Russell
12889:John von Neumann
12874:Abraham Fraenkel
12869:Richard Dedekind
12831:Suslin's problem
12742:Cantor's theorem
12459:De Morgan's laws
12317:
12284:
12277:
12270:
12261:
12260:
12253:Randall Holmes:
12247:Randall Holmes:
12241:Randall Holmes:
12216:Solomon Feferman
12201:
12157:
12147:
12137:
12101:
12057:
12022:
11996:
11980:
11951:
11912:
11910:
11900:
11871:
11852:
11840:
11801:
11784:
11771:
11745:
11719:
11709:
11703:
11693:
11691:
11689:
11673:
11627:
11625:
11623:
11622:
11617:
11605:
11603:
11602:
11597:
11595:
11594:
11577:
11565:
11564:
11562:
11560:
11545:
11539:
11538:
11536:
11534:
11519:
11513:
11507:
11501:
11495:
11489:
11483:
11477:
11471:
11465:
11464:
11462:
11460:
11445:
11439:
11433:
11427:
11421:
11415:
11409:
11403:
11402:
11376:
11367:
11361:
11355:
11346:
11340:
11331:
11325:
11319:
11313:
11302:
11296:
11290:
11284:
11278:
11272:
11266:
11260:
11254:
11248:
11242:
11236:
11230:
11224:
11218:
11212:
11206:
11200:
11194:
11188:
11179:
11173:
11167:
11161:
11155:
11149:
11140:
11134:
11128:
11122:
11116:
11110:
11104:
11098:
11092:
11086:
11080:
11074:
11068:
11062:
11056:
11050:
11044:
11038:
11032:
11026:
11015:
11009:
11003:
10997:
10991:
10985:
10979:
10973:
10967:
10961:
10955:
10944:
10938:
10932:
10926:
10920:
10914:
10908:
10897:
10891:
10885:
10879:
10764:showed that the
10632:
10630:
10629:
10624:
10622:
10621:
10567:Kuratowski pairs
10538:
10536:
10535:
10530:
10528:
10527:
10511:
10509:
10508:
10503:
10501:
10500:
10480:
10478:
10477:
10472:
10470:
10469:
10442:
10440:
10439:
10434:
10432:
10431:
10415:
10413:
10412:
10407:
10405:
10404:
10388:
10386:
10385:
10380:
10378:
10377:
10361:
10359:
10358:
10353:
10351:
10350:
10328:
10326:
10325:
10320:
10318:
10317:
10301:
10299:
10298:
10293:
10288:
10287:
10269:
10268:
10252:
10250:
10249:
10244:
10239:
10238:
10216:
10214:
10213:
10208:
10206:
10205:
10162:
10160:
10159:
10154:
10138:
10136:
10135:
10130:
10115:
10113:
10112:
10107:
10105:
10104:
10058:
10056:
10055:
10050:
10042:
10041:
10029:
10028:
9997:
9995:
9994:
9989:
9973:
9971:
9970:
9965:
9963:
9962:
9937:exists (because
9936:
9934:
9933:
9928:
9923:
9922:
9910:
9909:
9876:
9874:
9873:
9868:
9866:
9865:
9849:
9847:
9846:
9841:
9839:
9838:
9812:
9810:
9809:
9804:
9784:
9782:
9781:
9776:
9774:
9773:
9753:
9751:
9750:
9745:
9722:
9721:
9709:
9708:
9674:
9672:
9671:
9666:
9649:
9648:
9624:
9623:
9592:applications of
9591:
9589:
9588:
9583:
9557:
9555:
9554:
9549:
9547:
9546:
9503:
9501:
9500:
9495:
9493:
9492:
9476:
9474:
9473:
9468:
9452:
9450:
9449:
9444:
9430:
9428:
9427:
9422:
9417:
9416:
9365:
9364:
9346:
9345:
9316:
9314:
9313:
9308:
9306:
9305:
9274:
9272:
9271:
9266:
9264:
9263:
9247:
9245:
9244:
9239:
9237:
9236:
9210:
9208:
9207:
9202:
9200:
9199:
9180:
9178:
9177:
9172:
9141:
9139:
9138:
9133:
9131:
9130:
9074:Peano Arithmetic
9047:
9045:
9044:
9039:
9027:
9025:
9024:
9019:
9000:
8998:
8997:
8992:
8978:
8977:
8956:
8955:
8933:
8931:
8930:
8925:
8886:
8884:
8883:
8878:
8860:
8858:
8857:
8852:
8809:
8807:
8806:
8801:
8784:
8783:
8763:
8761:
8760:
8755:
8743:
8741:
8740:
8735:
8724:
8723:
8703:
8701:
8700:
8695:
8684:
8683:
8667:
8665:
8664:
8659:
8648:
8647:
8631:
8629:
8628:
8623:
8604:
8602:
8601:
8596:
8546:
8545:
8529:
8527:
8526:
8521:
8500:
8498:
8497:
8492:
8474:
8472:
8471:
8466:
8454:
8452:
8451:
8446:
8435:
8434:
8419:, just like how
8418:
8416:
8415:
8410:
8398:
8396:
8395:
8390:
8362:
8360:
8359:
8354:
8338:
8336:
8335:
8330:
8318:
8316:
8315:
8310:
8298:
8296:
8295:
8290:
8278:
8276:
8275:
8270:
8246:
8244:
8243:
8238:
8236:
8235:
8219:
8217:
8216:
8211:
8206:
8205:
8164:
8162:
8161:
8156:
8132:
8130:
8129:
8124:
8112:
8110:
8109:
8104:
8060:
8059:
8043:
8041:
8040:
8035:
8019:
8017:
8016:
8011:
7999:
7997:
7996:
7991:
7989:
7988:
7972:
7970:
7969:
7964:
7952:
7950:
7949:
7944:
7932:
7930:
7929:
7924:
7905:
7903:
7902:
7897:
7885:
7883:
7882:
7877:
7865:
7863:
7862:
7857:
7845:
7843:
7842:
7837:
7835:
7811:
7809:
7808:
7803:
7801:
7783:
7781:
7780:
7775:
7763:
7761:
7760:
7755:
7743:
7741:
7740:
7735:
7705:
7703:
7702:
7697:
7675:
7673:
7672:
7667:
7665:
7634:naive set theory
7628:
7626:
7625:
7620:
7608:
7606:
7605:
7600:
7554:
7552:
7551:
7546:
7510:
7508:
7507:
7502:
7489:Cantor's theorem
7482:
7480:
7479:
7474:
7472:
7458:
7457:
7448:
7440:
7432:
7420:
7418:
7417:
7412:
7400:
7398:
7397:
7392:
7374:
7372:
7371:
7366:
7354:
7352:
7351:
7346:
7344:
7330:
7329:
7320:
7312:
7304:
7289:
7287:
7286:
7281:
7279:
7271:
7259:
7257:
7256:
7251:
7249:
7232:
7216:
7214:
7213:
7208:
7206:
7198:
7190:
7173:
7165:
7151:
7150:
7141:
7125:
7123:
7122:
7117:
7090:
7088:
7087:
7082:
7080:
7063:
7055:
7041:
7040:
7031:
7019:
7017:
7016:
7011:
7009:
6992:
6984:
6970:
6969:
6960:
6948:
6946:
6945:
6940:
6928:
6926:
6925:
6920:
6909:
6908:
6892:
6890:
6889:
6884:
6865:
6863:
6862:
6857:
6855:
6838:
6830:
6822:
6810:
6808:
6807:
6802:
6790:
6788:
6787:
6782:
6761:
6759:
6758:
6753:
6751:
6734:
6726:
6718:
6703:
6701:
6700:
6695:
6683:
6681:
6680:
6675:
6657:
6655:
6654:
6649:
6616:
6614:
6613:
6608:
6596:
6594:
6593:
6588:
6567:
6565:
6564:
6559:
6547:
6545:
6544:
6539:
6484:
6482:
6481:
6476:
6464:
6462:
6461:
6456:
6444:
6442:
6441:
6436:
6408:
6406:
6405:
6400:
6382:
6380:
6379:
6374:
6362:
6360:
6359:
6354:
6329:
6327:
6326:
6321:
6309:
6307:
6306:
6301:
6289:
6287:
6286:
6281:
6256:Cantor's theorem
6253:
6251:
6250:
6245:
6221:Cantor's paradox
6207:
6205:
6204:
6199:
6169:
6167:
6166:
6161:
6122:
6120:
6119:
6114:
6096:
6094:
6093:
6088:
6054:naive set theory
6034:Cartesian closed
6014:
6012:
6011:
6006:
5908:
5906:
5905:
5900:
5804:, which implies
5803:
5801:
5800:
5795:
5771:
5769:
5768:
5763:
5748:
5746:
5745:
5740:
5705:
5703:
5702:
5697:
5695:
5687:
5675:
5673:
5672:
5667:
5665:
5657:
5641:
5639:
5638:
5633:
5631:
5623:
5603:
5601:
5600:
5595:
5581:
5539:
5537:
5536:
5531:
5526:
5504:
5502:
5501:
5496:
5484:
5482:
5481:
5476:
5433:
5431:
5430:
5425:
5401:
5399:
5398:
5393:
5391:
5377:
5369:
5357:
5355:
5354:
5349:
5347:
5339:
5327:
5325:
5324:
5319:
5304:
5302:
5301:
5296:
5275:
5273:
5272:
5267:
5247:
5226:
5224:
5223:
5218:
5193:
5191:
5190:
5185:
5183:
5164:
5162:
5161:
5156:
5144:
5142:
5141:
5136:
5064:
5062:
5061:
5056:
5023:is based on the
5010:
5008:
5007:
5002:
4946:
4945:
4929:
4927:
4926:
4921:
4909:
4907:
4906:
4901:
4877:
4875:
4874:
4869:
4840:
4839:
4823:
4821:
4820:
4815:
4786:
4785:
4769:
4767:
4766:
4761:
4759:
4758:
4742:
4740:
4739:
4734:
4732:
4731:
4711:primitive notion
4681:
4679:
4678:
4673:
4660:
4648:
4630:
4625:
4624:
4610:
4543:
4541:
4540:
4535:
4479:
4452:
4450:
4449:
4444:
4423:
4421:
4420:
4415:
4377:
4375:
4374:
4369:
4301:
4278:
4239:
4237:
4236:
4231:
4217:
4171:
4169:
4168:
4163:
4152:
4131:
4129:
4128:
4123:
4102:
4100:
4099:
4094:
4058:
4056:
4055:
4050:
3921:
3919:
3918:
3913:
3901:
3899:
3898:
3893:
3864:
3862:
3861:
3856:
3844:
3842:
3841:
3836:
3815:
3813:
3812:
3807:
3795:
3793:
3792:
3787:
3769:
3767:
3766:
3761:
3759:
3758:
3746:
3745:
3729:
3727:
3726:
3721:
3719:
3718:
3706:
3705:
3669:
3667:
3666:
3661:
3656:
3655:
3629:
3627:
3626:
3621:
3618:
3617:
3599:
3598:
3580:
3579:
3560:
3558:
3557:
3552:
3549:
3548:
3526:
3524:
3523:
3518:
3510:
3509:
3491:
3490:
3472:
3471:
3459:
3458:
3446:
3445:
3420:
3418:
3417:
3412:
3406:
3405:
3383:
3381:
3380:
3375:
3372:
3371:
3353:
3352:
3334:
3333:
3314:
3312:
3311:
3306:
3301:
3300:
3251:
3249:
3248:
3243:
3241:
3240:
3201:Typed Set Theory
3195:
3193:
3192:
3187:
3125:
3122:
3113:
3111:
3110:
3105:
3090:
3088:
3087:
3082:
3017:
3016:
3000:
2998:
2997:
2992:
2927:
2926:
2910:
2908:
2907:
2902:
2887:
2885:
2884:
2879:
2829:
2811:
2809:
2808:
2803:
2788:
2786:
2785:
2780:
2778:
2777:
2768:
2763:
2762:
2734:
2732:
2731:
2726:
2721:
2710:
2709:
2693:
2691:
2690:
2685:
2635:
2615:
2613:
2612:
2607:
2595:
2593:
2592:
2587:
2575:
2573:
2572:
2567:
2553:
2550:
2533:
2530:
2528:
2496:
2478:
2476:
2475:
2470:
2458:
2456:
2455:
2450:
2435:
2433:
2432:
2427:
2415:
2413:
2412:
2407:
2393:
2390:
2373:
2370:
2368:
2335:
2333:
2332:
2327:
2312:
2310:
2309:
2304:
2290:
2245:
2243:
2242:
2237:
2217:
2179:
2178:
2162:
2160:
2159:
2154:
2134:
2096:
2095:
2076:
2074:
2073:
2068:
2050:
2048:
2047:
2042:
2024:
2022:
2021:
2016:
1974:
1972:
1971:
1966:
1942:
1940:
1939:
1934:
1922:
1920:
1919:
1914:
1902:
1900:
1899:
1894:
1882:
1880:
1879:
1874:
1859:
1857:
1856:
1851:
1843:
1842:
1820:
1818:
1817:
1812:
1800:
1798:
1797:
1792:
1778:
1751:
1749:
1748:
1743:
1731:
1729:
1728:
1723:
1711:
1709:
1708:
1703:
1698:
1695:
1684:
1681:
1670:
1640:
1638:
1637:
1632:
1620:
1618:
1617:
1612:
1597:
1595:
1594:
1589:
1577:
1575:
1574:
1569:
1555:
1541:
1540:
1524:
1522:
1521:
1516:
1499:
1497:
1496:
1491:
1477:
1399:
1397:
1396:
1391:
1377:
1332:
1330:
1329:
1324:
1312:
1310:
1309:
1304:
1269:
1246:
1243:
1234:
1232:
1231:
1226:
1211:
1209:
1208:
1203:
1191:
1189:
1188:
1183:
1157:
1106:
1104:
1103:
1098:
1083:
1081:
1080:
1075:
1057:
1055:
1054:
1049:
1044:
1043:
1021:
1019:
1018:
1013:
987:
961:
960:
941:
939:
938:
933:
918:
916:
915:
910:
892:
890:
889:
884:
866:
864:
863:
858:
846:
844:
843:
838:
826:
824:
823:
818:
804:
801:
790:
748:
746:
745:
740:
728:
726:
725:
720:
705:
703:
702:
697:
685:
683:
682:
677:
663:
618:
616:
615:
610:
595:
593:
592:
587:
569:
567:
566:
561:
549:
547:
546:
541:
529:
527:
526:
521:
509:
507:
506:
501:
489:
487:
486:
481:
469:
467:
466:
461:
449:
447:
446:
441:
393:
391:
390:
385:
373:
371:
370:
365:
331:
329:
328:
323:
311:
309:
308:
303:
285:
283:
282:
277:
254:
252:
251:
246:
230:
228:
227:
222:
208:exists for each
207:
205:
204:
199:
119:
117:
116:
111:
95:
93:
92:
87:
33:non-well-founded
14718:
14717:
14713:
14712:
14711:
14709:
14708:
14707:
14678:
14677:
14676:
14671:
14660:
14653:
14598:Category theory
14588:Algebraic logic
14571:
14542:Lambda calculus
14480:Church encoding
14466:
14442:Truth predicate
14298:
14264:Complete theory
14187:
14056:
14052:
14048:
14043:
14035:
13755: and
13751:
13746:
13732:
13708:New Foundations
13676:axiom of choice
13659:
13621:Gödel numbering
13561: and
13553:
13457:
13342:
13292:
13273:
13222:Boolean algebra
13208:
13172:Equiconsistency
13137:Classical logic
13114:
13095:Halting problem
13083: and
13059: and
13047: and
13046:
13041:Theorems (
13036:
12953:
12948:
12918:
12913:
12840:
12819:
12803:
12768:New Foundations
12715:
12605:
12524:Cardinal number
12507:
12493:
12434:
12318:
12309:
12293:
12288:
12208:
12175:10.2307/2268438
12075:10.2307/2267550
12054:
12012:
11970:10.2307/2300564
11927:(1/2): 250–63,
11908:
11861:
11850:
11821:10.2307/2267307
11761:
11717:
11701:
11687:
11685:
11654:10.2307/2273386
11636:
11631:
11630:
11611:
11608:
11607:
11590:
11586:
11584:
11581:
11580:
11578:
11574:
11569:
11568:
11558:
11556:
11546:
11542:
11532:
11530:
11520:
11516:
11508:
11504:
11496:
11492:
11484:
11480:
11472:
11468:
11458:
11456:
11446:
11442:
11434:
11430:
11422:
11418:
11410:
11406:
11391:10.2307/2694912
11374:
11368:
11364:
11356:
11349:
11341:
11334:
11326:
11322:
11314:
11305:
11297:
11293:
11285:
11281:
11273:
11269:
11261:
11257:
11249:
11245:
11237:
11233:
11225:
11221:
11213:
11209:
11201:
11197:
11189:
11182:
11174:
11170:
11162:
11158:
11150:
11143:
11135:
11131:
11123:
11119:
11111:
11107:
11099:
11095:
11087:
11083:
11075:
11071:
11063:
11059:
11051:
11047:
11039:
11035:
11027:
11018:
11010:
11006:
10998:
10994:
10986:
10982:
10974:
10970:
10962:
10958:
10945:
10941:
10933:
10929:
10921:
10917:
10909:
10900:
10892:
10888:
10880:
10871:
10866:
10834:
10822:
10818:
10779:
10766:axiom of choice
10695:
10685:} for each set
10608:
10604:
10602:
10599:
10598:
10548:
10523:
10519:
10517:
10514:
10513:
10496:
10492:
10490:
10487:
10486:
10465:
10461:
10459:
10456:
10455:
10427:
10423:
10421:
10418:
10417:
10400:
10396:
10394:
10391:
10390:
10373:
10369:
10367:
10364:
10363:
10340:
10336:
10334:
10331:
10330:
10313:
10309:
10307:
10304:
10303:
10277:
10273:
10264:
10260:
10258:
10255:
10254:
10234:
10230:
10222:
10219:
10218:
10201:
10197:
10195:
10192:
10191:
10183:
10148:
10145:
10144:
10124:
10121:
10120:
10085:
10081:
10079:
10076:
10075:
10037:
10033:
10024:
10020:
10003:
10000:
9999:
9983:
9980:
9979:
9952:
9948:
9946:
9943:
9942:
9918:
9914:
9905:
9901:
9890:
9887:
9886:
9861:
9857:
9855:
9852:
9851:
9828:
9824:
9822:
9819:
9818:
9798:
9795:
9794:
9769:
9765:
9763:
9760:
9759:
9717:
9713:
9698:
9694:
9680:
9677:
9676:
9638:
9634:
9619:
9615:
9601:
9598:
9597:
9571:
9568:
9567:
9542:
9538:
9536:
9533:
9532:
9488:
9484:
9482:
9479:
9478:
9477:into a formula
9462:
9459:
9458:
9438:
9435:
9434:
9397:
9393:
9354:
9350:
9335:
9331:
9326:
9323:
9322:
9286:
9282:
9280:
9277:
9276:
9259:
9255:
9253:
9250:
9249:
9226:
9222:
9220:
9217:
9216:
9195:
9191:
9189:
9186:
9185:
9151:
9148:
9147:
9126:
9122:
9120:
9117:
9116:
9095:
9062:Axiom of Choice
9054:
9033:
9030:
9029:
9013:
9010:
9009:
8973:
8969:
8951:
8947:
8939:
8936:
8935:
8892:
8889:
8888:
8866:
8863:
8862:
8822:
8819:
8818:
8779:
8775:
8773:
8770:
8769:
8749:
8746:
8745:
8719:
8715:
8713:
8710:
8709:
8679:
8675:
8673:
8670:
8669:
8643:
8639:
8637:
8634:
8633:
8614:
8611:
8610:
8541:
8537:
8535:
8532:
8531:
8506:
8503:
8502:
8480:
8477:
8476:
8460:
8457:
8456:
8430:
8426:
8424:
8421:
8420:
8404:
8401:
8400:
8375:
8372:
8371:
8348:
8345:
8344:
8324:
8321:
8320:
8304:
8301:
8300:
8284:
8281:
8280:
8252:
8249:
8248:
8231:
8227:
8225:
8222:
8221:
8201:
8197:
8174:
8171:
8170:
8138:
8135:
8134:
8118:
8115:
8114:
8055:
8051:
8049:
8046:
8045:
8029:
8026:
8025:
8005:
8002:
8001:
7984:
7980:
7978:
7975:
7974:
7958:
7955:
7954:
7938:
7935:
7934:
7918:
7915:
7914:
7891:
7888:
7887:
7871:
7868:
7867:
7851:
7848:
7847:
7825:
7817:
7814:
7813:
7791:
7789:
7786:
7785:
7769:
7766:
7765:
7749:
7746:
7745:
7711:
7708:
7707:
7685:
7682:
7681:
7655:
7653:
7650:
7649:
7614:
7611:
7610:
7594:
7591:
7590:
7585:of the largest
7577:
7516:
7513:
7512:
7496:
7493:
7492:
7468:
7453:
7449:
7444:
7436:
7428:
7426:
7423:
7422:
7406:
7403:
7402:
7380:
7377:
7376:
7360:
7357:
7356:
7340:
7325:
7321:
7316:
7308:
7300:
7298:
7295:
7294:
7275:
7267:
7265:
7262:
7261:
7245:
7228:
7226:
7223:
7222:
7202:
7194:
7186:
7169:
7161:
7146:
7142:
7137:
7135:
7132:
7131:
7099:
7096:
7095:
7076:
7059:
7051:
7036:
7032:
7027:
7025:
7022:
7021:
7005:
6988:
6980:
6965:
6961:
6956:
6954:
6951:
6950:
6934:
6931:
6930:
6904:
6900:
6898:
6895:
6894:
6878:
6875:
6874:
6851:
6834:
6826:
6818:
6816:
6813:
6812:
6796:
6793:
6792:
6767:
6764:
6763:
6747:
6730:
6722:
6714:
6712:
6709:
6708:
6689:
6686:
6685:
6663:
6660:
6659:
6622:
6619:
6618:
6602:
6599:
6598:
6573:
6570:
6569:
6553:
6550:
6549:
6494:
6491:
6490:
6470:
6467:
6466:
6450:
6447:
6446:
6421:
6418:
6417:
6388:
6385:
6384:
6368:
6365:
6364:
6339:
6336:
6335:
6315:
6312:
6311:
6310:is larger than
6295:
6292:
6291:
6266:
6263:
6262:
6239:
6236:
6235:
6225:cardinal number
6218:
6175:
6172:
6171:
6149:
6146:
6145:
6138:
6102:
6099:
6098:
6064:
6061:
6060:
6050:
6030:
5994:
5991:
5990:
5888:
5885:
5884:
5854:
5777:
5774:
5773:
5757:
5754:
5753:
5734:
5731:
5730:
5727:axiom of choice
5721:In NF (without
5691:
5683:
5681:
5678:
5677:
5661:
5653:
5651:
5648:
5647:
5627:
5619:
5617:
5614:
5613:
5577:
5551:
5548:
5547:
5522:
5514:
5511:
5510:
5490:
5487:
5486:
5443:
5440:
5439:
5407:
5404:
5403:
5387:
5373:
5365:
5363:
5360:
5359:
5343:
5335:
5333:
5330:
5329:
5313:
5310:
5309:
5281:
5278:
5277:
5243:
5232:
5229:
5228:
5203:
5200:
5199:
5179:
5177:
5174:
5173:
5150:
5147:
5146:
5070:
5067:
5066:
5044:
5041:
5040:
5017:
4941:
4937:
4935:
4932:
4931:
4915:
4912:
4911:
4883:
4880:
4879:
4835:
4831:
4829:
4826:
4825:
4781:
4777:
4775:
4772:
4771:
4754:
4750:
4748:
4745:
4744:
4727:
4723:
4721:
4718:
4717:
4620:
4616:
4599:
4596:
4595:
4576:
4564:
4554:
4550:
4469:
4458:
4455:
4454:
4429:
4426:
4425:
4388:
4385:
4384:
4291:
4268:
4251:
4248:
4247:
4207:
4181:
4178:
4177:
4142:
4140:
4137:
4136:
4108:
4105:
4104:
4067:
4064:
4063:
3957:
3954:
3953:
3928:
3907:
3904:
3903:
3881:
3878:
3877:
3850:
3847:
3846:
3821:
3818:
3817:
3801:
3798:
3797:
3775:
3772:
3771:
3754:
3750:
3741:
3737:
3735:
3732:
3731:
3714:
3710:
3701:
3697:
3695:
3692:
3691:
3688:
3651:
3647:
3639:
3636:
3635:
3607:
3603:
3594:
3590:
3575:
3571:
3566:
3563:
3562:
3538:
3534:
3532:
3529:
3528:
3505:
3501:
3480:
3476:
3467:
3463:
3454:
3450:
3435:
3431:
3426:
3423:
3422:
3401:
3397:
3389:
3386:
3385:
3361:
3357:
3348:
3344:
3329:
3325:
3320:
3317:
3316:
3296:
3292:
3284:
3281:
3280:
3236:
3232:
3230:
3227:
3226:
3203:
3121:
3119:
3116:
3115:
3099:
3096:
3095:
3012:
3008:
3006:
3003:
3002:
2922:
2918:
2916:
2913:
2912:
2896:
2893:
2892:
2825:
2817:
2814:
2813:
2797:
2794:
2793:
2773:
2769:
2764:
2758:
2754:
2740:
2737:
2736:
2717:
2705:
2701:
2699:
2696:
2695:
2631:
2626:
2623:
2622:
2601:
2598:
2597:
2581:
2578:
2577:
2551: and
2549:
2529:
2524:
2492:
2484:
2481:
2480:
2464:
2461:
2460:
2444:
2441:
2440:
2421:
2418:
2417:
2391: and
2389:
2369:
2364:
2341:
2338:
2337:
2321:
2318:
2317:
2286:
2254:
2251:
2250:
2213:
2174:
2170:
2168:
2165:
2164:
2130:
2091:
2087:
2085:
2082:
2081:
2056:
2053:
2052:
2030:
2027:
2026:
1980:
1977:
1976:
1948:
1945:
1944:
1928:
1925:
1924:
1908:
1905:
1904:
1888:
1885:
1884:
1868:
1865:
1864:
1838:
1834:
1826:
1823:
1822:
1806:
1803:
1802:
1774:
1760:
1757:
1756:
1755:Universal Set:
1737:
1734:
1733:
1717:
1714:
1713:
1694:
1680:
1666:
1646:
1643:
1642:
1626:
1623:
1622:
1606:
1603:
1602:
1583:
1580:
1579:
1551:
1536:
1532:
1530:
1527:
1526:
1510:
1507:
1506:
1473:
1405:
1402:
1401:
1373:
1341:
1338:
1337:
1318:
1315:
1314:
1265:
1242:
1240:
1237:
1236:
1220:
1217:
1216:
1197:
1194:
1193:
1153:
1112:
1109:
1108:
1092:
1089:
1088:
1063:
1060:
1059:
1036:
1032:
1027:
1024:
1023:
983:
953:
949:
947:
944:
943:
927:
924:
923:
898:
895:
894:
872:
869:
868:
852:
849:
848:
832:
829:
828:
802: and
800:
786:
754:
751:
750:
734:
731:
730:
714:
711:
710:
691:
688:
687:
659:
624:
621:
620:
604:
601:
600:
575:
572:
571:
555:
552:
551:
535:
532:
531:
530:if and only if
515:
512:
511:
495:
492:
491:
475:
472:
471:
455:
452:
451:
435:
432:
431:
416:
379:
376:
375:
353:
350:
349:
317:
314:
313:
291:
288:
287:
271:
268:
267:
266:from pieces of
240:
237:
236:
216:
213:
212:
181:
178:
177:
153:is a member of
143:is a member of
105:
102:
101:
81:
78:
77:
62:
48:theory of types
25:New Foundations
17:
12:
11:
5:
14716:
14706:
14705:
14700:
14695:
14690:
14673:
14672:
14658:
14655:
14654:
14652:
14651:
14646:
14641:
14636:
14631:
14630:
14629:
14619:
14614:
14609:
14600:
14595:
14590:
14585:
14583:Abstract logic
14579:
14577:
14573:
14572:
14570:
14569:
14564:
14562:Turing machine
14559:
14554:
14549:
14544:
14539:
14534:
14533:
14532:
14527:
14522:
14517:
14512:
14502:
14500:Computable set
14497:
14492:
14487:
14482:
14476:
14474:
14468:
14467:
14465:
14464:
14459:
14454:
14449:
14444:
14439:
14434:
14429:
14428:
14427:
14422:
14417:
14407:
14402:
14397:
14395:Satisfiability
14392:
14387:
14382:
14381:
14380:
14370:
14369:
14368:
14358:
14357:
14356:
14351:
14346:
14341:
14336:
14326:
14325:
14324:
14319:
14312:Interpretation
14308:
14306:
14300:
14299:
14297:
14296:
14291:
14286:
14281:
14276:
14266:
14261:
14260:
14259:
14258:
14257:
14247:
14242:
14232:
14227:
14222:
14217:
14212:
14207:
14201:
14199:
14193:
14192:
14189:
14188:
14186:
14185:
14177:
14176:
14175:
14174:
14169:
14168:
14167:
14162:
14157:
14137:
14136:
14135:
14133:minimal axioms
14130:
14119:
14118:
14117:
14106:
14105:
14104:
14099:
14094:
14089:
14084:
14079:
14066:
14064:
14045:
14044:
14042:
14041:
14040:
14039:
14027:
14022:
14021:
14020:
14015:
14010:
14005:
13995:
13990:
13985:
13980:
13979:
13978:
13973:
13963:
13962:
13961:
13956:
13951:
13946:
13936:
13931:
13930:
13929:
13924:
13919:
13909:
13908:
13907:
13902:
13897:
13892:
13887:
13882:
13872:
13867:
13862:
13857:
13856:
13855:
13850:
13845:
13840:
13830:
13825:
13823:Formation rule
13820:
13815:
13814:
13813:
13808:
13798:
13797:
13796:
13786:
13781:
13776:
13771:
13765:
13759:
13742:Formal systems
13738:
13737:
13734:
13733:
13731:
13730:
13725:
13720:
13715:
13710:
13705:
13700:
13695:
13690:
13685:
13684:
13683:
13678:
13667:
13665:
13661:
13660:
13658:
13657:
13656:
13655:
13645:
13640:
13639:
13638:
13631:Large cardinal
13628:
13623:
13618:
13613:
13608:
13594:
13593:
13592:
13587:
13582:
13567:
13565:
13555:
13554:
13552:
13551:
13550:
13549:
13544:
13539:
13529:
13524:
13519:
13514:
13509:
13504:
13499:
13494:
13489:
13484:
13479:
13474:
13468:
13466:
13459:
13458:
13456:
13455:
13454:
13453:
13448:
13443:
13438:
13433:
13428:
13420:
13419:
13418:
13413:
13403:
13398:
13396:Extensionality
13393:
13391:Ordinal number
13388:
13378:
13373:
13372:
13371:
13360:
13354:
13348:
13347:
13344:
13343:
13341:
13340:
13335:
13330:
13325:
13320:
13315:
13310:
13309:
13308:
13298:
13297:
13296:
13283:
13281:
13275:
13274:
13272:
13271:
13270:
13269:
13264:
13259:
13249:
13244:
13239:
13234:
13229:
13224:
13218:
13216:
13210:
13209:
13207:
13206:
13201:
13196:
13191:
13186:
13181:
13176:
13175:
13174:
13164:
13159:
13154:
13149:
13144:
13139:
13133:
13131:
13122:
13116:
13115:
13113:
13112:
13107:
13102:
13097:
13092:
13087:
13075:Cantor's
13073:
13068:
13063:
13053:
13051:
13038:
13037:
13035:
13034:
13029:
13024:
13019:
13014:
13009:
13004:
12999:
12994:
12989:
12984:
12979:
12974:
12973:
12972:
12961:
12959:
12955:
12954:
12947:
12946:
12939:
12932:
12924:
12915:
12914:
12912:
12911:
12906:
12904:Thoralf Skolem
12901:
12896:
12891:
12886:
12881:
12876:
12871:
12866:
12861:
12856:
12850:
12848:
12842:
12841:
12839:
12838:
12833:
12828:
12822:
12820:
12818:
12817:
12814:
12808:
12805:
12804:
12802:
12801:
12800:
12799:
12794:
12789:
12788:
12787:
12772:
12771:
12770:
12758:
12757:
12756:
12745:
12744:
12739:
12734:
12729:
12723:
12721:
12717:
12716:
12714:
12713:
12708:
12703:
12698:
12689:
12684:
12679:
12669:
12664:
12663:
12662:
12657:
12652:
12642:
12632:
12627:
12622:
12616:
12614:
12607:
12606:
12604:
12603:
12598:
12593:
12588:
12586:Ordinal number
12583:
12578:
12573:
12568:
12567:
12566:
12561:
12551:
12546:
12541:
12536:
12531:
12521:
12516:
12510:
12508:
12506:
12505:
12502:
12498:
12495:
12494:
12492:
12491:
12486:
12481:
12476:
12471:
12466:
12464:Disjoint union
12461:
12456:
12450:
12444:
12442:
12436:
12435:
12433:
12432:
12431:
12430:
12425:
12414:
12413:
12411:Martin's axiom
12408:
12403:
12398:
12393:
12388:
12383:
12378:
12376:Extensionality
12373:
12372:
12371:
12361:
12356:
12355:
12354:
12349:
12344:
12334:
12328:
12326:
12320:
12319:
12312:
12310:
12308:
12307:
12301:
12299:
12295:
12294:
12287:
12286:
12279:
12272:
12264:
12258:
12257:
12251:
12245:
12239:
12238:
12237:
12231:
12219:
12207:
12206:External links
12204:
12203:
12202:
12158:
12102:
12058:
12052:
12037:
12023:
12010:
11997:
11981:
11953:
11913:
11901:
11883:(2): 195–213.
11872:
11859:
11841:
11802:
11785:
11772:
11759:
11746:
11710:
11694:
11674:
11648:(1): 131–136.
11635:
11632:
11629:
11628:
11615:
11593:
11589:
11571:
11570:
11567:
11566:
11540:
11514:
11502:
11490:
11478:
11466:
11440:
11428:
11416:
11404:
11362:
11347:
11332:
11320:
11303:
11291:
11289:, ax-typlower.
11279:
11275:Hailperin 1944
11267:
11255:
11251:Hailperin 1944
11243:
11231:
11227:Hailperin 1944
11219:
11207:
11195:
11180:
11168:
11156:
11141:
11129:
11125:Hailperin 1944
11117:
11105:
11101:Hailperin 1944
11093:
11081:
11077:Hailperin 1944
11069:
11057:
11045:
11041:Hailperin 1944
11033:
11016:
11004:
11000:Hailperin 1944
10992:
10980:
10968:
10956:
10948:W. V. O. Quine
10939:
10935:Hailperin 1944
10927:
10915:
10898:
10886:
10882:Hailperin 1944
10868:
10867:
10865:
10862:
10861:
10860:
10855:
10850:
10845:
10840:
10833:
10830:
10820:
10816:
10792:free variables
10777:
10739:NBG set theory
10735:proper classes
10727:proper classes
10699:Norbert Wiener
10694:
10691:
10620:
10617:
10614:
10611:
10607:
10547:
10541:
10526:
10522:
10499:
10495:
10468:
10464:
10430:
10426:
10403:
10399:
10376:
10372:
10349:
10346:
10343:
10339:
10316:
10312:
10291:
10286:
10283:
10280:
10276:
10272:
10267:
10263:
10242:
10237:
10233:
10229:
10226:
10204:
10200:
10182:
10179:
10152:
10128:
10103:
10100:
10097:
10094:
10091:
10088:
10084:
10072:Extensionality
10048:
10045:
10040:
10036:
10032:
10027:
10023:
10019:
10016:
10013:
10010:
10007:
9987:
9961:
9958:
9955:
9951:
9926:
9921:
9917:
9913:
9908:
9904:
9900:
9897:
9894:
9864:
9860:
9837:
9834:
9831:
9827:
9813:assigned type
9802:
9772:
9768:
9743:
9740:
9737:
9734:
9731:
9728:
9725:
9720:
9716:
9712:
9707:
9704:
9701:
9697:
9693:
9690:
9687:
9684:
9664:
9661:
9658:
9655:
9652:
9647:
9644:
9641:
9637:
9633:
9630:
9627:
9622:
9618:
9614:
9611:
9608:
9605:
9581:
9578:
9575:
9562:assigned type
9545:
9541:
9529:atomic formula
9491:
9487:
9466:
9442:
9420:
9415:
9412:
9409:
9406:
9403:
9400:
9396:
9392:
9389:
9386:
9383:
9380:
9377:
9374:
9371:
9368:
9363:
9360:
9357:
9353:
9349:
9344:
9341:
9338:
9334:
9330:
9304:
9301:
9298:
9295:
9292:
9289:
9285:
9262:
9258:
9235:
9232:
9229:
9225:
9198:
9194:
9170:
9167:
9164:
9161:
9158:
9155:
9129:
9125:
9094:
9091:
9086:equiconsistent
9053:
9050:
9037:
9017:
8990:
8987:
8984:
8981:
8976:
8972:
8968:
8965:
8962:
8959:
8954:
8950:
8946:
8943:
8923:
8920:
8917:
8914:
8911:
8908:
8905:
8902:
8899:
8896:
8876:
8873:
8870:
8850:
8847:
8844:
8841:
8838:
8835:
8832:
8829:
8826:
8799:
8796:
8793:
8790:
8787:
8782:
8778:
8753:
8733:
8730:
8727:
8722:
8718:
8706:
8705:
8693:
8690:
8687:
8682:
8678:
8657:
8654:
8651:
8646:
8642:
8621:
8618:
8594:
8591:
8588:
8585:
8582:
8579:
8576:
8573:
8570:
8567:
8564:
8561:
8558:
8555:
8552:
8549:
8544:
8540:
8519:
8516:
8513:
8510:
8490:
8487:
8484:
8464:
8444:
8441:
8438:
8433:
8429:
8408:
8388:
8385:
8382:
8379:
8352:
8328:
8308:
8288:
8268:
8265:
8262:
8259:
8256:
8234:
8230:
8209:
8204:
8200:
8196:
8193:
8190:
8187:
8184:
8181:
8178:
8154:
8151:
8148:
8145:
8142:
8133:assuming that
8122:
8102:
8099:
8096:
8093:
8090:
8087:
8084:
8081:
8078:
8075:
8072:
8069:
8066:
8063:
8058:
8054:
8033:
8020:" is at least
8009:
7987:
7983:
7962:
7942:
7922:
7895:
7875:
7855:
7834:
7831:
7828:
7824:
7821:
7800:
7797:
7794:
7773:
7753:
7733:
7730:
7727:
7724:
7721:
7718:
7715:
7695:
7692:
7689:
7664:
7661:
7658:
7642:well-orderings
7618:
7598:
7587:ordinal number
7576:
7573:
7544:
7541:
7538:
7535:
7532:
7529:
7526:
7523:
7520:
7500:
7483:is said to be
7471:
7467:
7464:
7461:
7456:
7452:
7447:
7443:
7439:
7435:
7431:
7410:
7390:
7387:
7384:
7364:
7343:
7339:
7336:
7333:
7328:
7324:
7319:
7315:
7311:
7307:
7303:
7278:
7274:
7270:
7248:
7244:
7241:
7238:
7235:
7231:
7205:
7201:
7197:
7193:
7189:
7185:
7182:
7179:
7176:
7172:
7168:
7164:
7160:
7157:
7154:
7149:
7145:
7140:
7115:
7112:
7109:
7106:
7103:
7079:
7075:
7072:
7069:
7066:
7062:
7058:
7054:
7050:
7047:
7044:
7039:
7035:
7030:
7008:
7004:
7001:
6998:
6995:
6991:
6987:
6983:
6979:
6976:
6973:
6968:
6964:
6959:
6938:
6918:
6915:
6912:
6907:
6903:
6882:
6854:
6850:
6847:
6844:
6841:
6837:
6833:
6829:
6825:
6821:
6800:
6780:
6777:
6774:
6771:
6750:
6746:
6743:
6740:
6737:
6733:
6729:
6725:
6721:
6717:
6693:
6673:
6670:
6667:
6647:
6644:
6641:
6638:
6635:
6632:
6629:
6626:
6606:
6586:
6583:
6580:
6577:
6557:
6537:
6534:
6531:
6528:
6525:
6522:
6519:
6516:
6513:
6510:
6507:
6504:
6501:
6498:
6474:
6454:
6434:
6431:
6428:
6425:
6398:
6395:
6392:
6372:
6352:
6349:
6346:
6343:
6319:
6299:
6279:
6276:
6273:
6270:
6243:
6217:
6214:
6197:
6194:
6191:
6188:
6185:
6182:
6179:
6159:
6156:
6153:
6137:
6134:
6112:
6109:
6106:
6086:
6083:
6080:
6077:
6074:
6071:
6068:
6049:
6046:
6029:
6026:
6025:
6024:
6004:
6001:
5998:
5975:equinumerosity
5957:elements (the
5941:
5898:
5895:
5892:
5870:proper classes
5856:NF (and NFU +
5853:
5850:
5834:Small Ordinals
5830:Large Ordinals
5822:
5821:
5793:
5790:
5787:
5784:
5781:
5761:
5750:
5738:
5694:
5690:
5686:
5664:
5660:
5656:
5630:
5626:
5622:
5593:
5590:
5587:
5584:
5580:
5576:
5573:
5570:
5567:
5564:
5561:
5558:
5555:
5529:
5525:
5521:
5518:
5494:
5474:
5471:
5468:
5465:
5462:
5459:
5456:
5453:
5450:
5447:
5423:
5420:
5417:
5414:
5411:
5390:
5386:
5383:
5380:
5376:
5372:
5368:
5346:
5342:
5338:
5317:
5294:
5291:
5288:
5285:
5265:
5262:
5259:
5256:
5253:
5250:
5246:
5242:
5239:
5236:
5216:
5213:
5210:
5207:
5182:
5154:
5134:
5131:
5128:
5125:
5122:
5119:
5116:
5113:
5110:
5107:
5104:
5101:
5098:
5095:
5092:
5089:
5086:
5083:
5080:
5077:
5074:
5054:
5051:
5048:
5016:
5013:
5000:
4997:
4994:
4991:
4988:
4985:
4982:
4979:
4976:
4973:
4970:
4967:
4964:
4961:
4958:
4955:
4952:
4949:
4944:
4940:
4919:
4899:
4896:
4893:
4890:
4887:
4867:
4864:
4861:
4858:
4855:
4852:
4849:
4846:
4843:
4838:
4834:
4813:
4810:
4807:
4804:
4801:
4798:
4795:
4792:
4789:
4784:
4780:
4757:
4753:
4730:
4726:
4671:
4668:
4665:
4659:
4656:
4653:
4647:
4644:
4641:
4638:
4635:
4629:
4623:
4619:
4615:
4609:
4606:
4603:
4575:
4572:
4563:
4560:
4552:
4548:
4545:
4544:
4533:
4530:
4527:
4524:
4521:
4518:
4515:
4512:
4509:
4506:
4503:
4500:
4497:
4494:
4491:
4488:
4485:
4482:
4478:
4475:
4472:
4468:
4465:
4462:
4442:
4439:
4436:
4433:
4413:
4410:
4407:
4404:
4401:
4398:
4395:
4392:
4378:
4367:
4364:
4361:
4358:
4355:
4352:
4349:
4346:
4343:
4340:
4337:
4334:
4331:
4328:
4325:
4322:
4319:
4316:
4313:
4310:
4307:
4304:
4300:
4297:
4294:
4290:
4287:
4284:
4281:
4277:
4274:
4271:
4267:
4264:
4261:
4258:
4255:
4240:
4229:
4226:
4223:
4220:
4216:
4213:
4210:
4206:
4203:
4200:
4197:
4194:
4191:
4188:
4185:
4161:
4158:
4155:
4151:
4148:
4145:
4121:
4118:
4115:
4112:
4092:
4089:
4086:
4083:
4080:
4077:
4074:
4071:
4060:
4059:
4048:
4045:
4042:
4039:
4036:
4033:
4030:
4027:
4024:
4021:
4018:
4015:
4012:
4009:
4006:
4003:
4000:
3997:
3994:
3991:
3988:
3985:
3982:
3979:
3976:
3973:
3970:
3967:
3964:
3961:
3950:
3949:
3927:
3924:
3911:
3891:
3888:
3885:
3854:
3834:
3831:
3828:
3825:
3805:
3785:
3782:
3779:
3757:
3753:
3749:
3744:
3740:
3717:
3713:
3709:
3704:
3700:
3687:
3684:
3659:
3654:
3650:
3646:
3643:
3616:
3613:
3610:
3606:
3602:
3597:
3593:
3589:
3586:
3583:
3578:
3574:
3570:
3547:
3544:
3541:
3537:
3516:
3513:
3508:
3504:
3500:
3497:
3494:
3489:
3486:
3483:
3479:
3475:
3470:
3466:
3462:
3457:
3453:
3449:
3444:
3441:
3438:
3434:
3430:
3421:, the formula
3409:
3404:
3400:
3396:
3393:
3370:
3367:
3364:
3360:
3356:
3351:
3347:
3343:
3340:
3337:
3332:
3328:
3324:
3304:
3299:
3295:
3291:
3288:
3258:natural number
3239:
3235:
3202:
3199:
3198:
3197:
3185:
3182:
3179:
3176:
3173:
3170:
3167:
3164:
3161:
3158:
3155:
3152:
3149:
3146:
3143:
3140:
3137:
3134:
3131:
3128:
3103:
3092:
3080:
3077:
3074:
3071:
3068:
3065:
3062:
3059:
3056:
3053:
3050:
3047:
3044:
3041:
3038:
3035:
3032:
3029:
3026:
3023:
3020:
3015:
3011:
2990:
2987:
2984:
2981:
2978:
2975:
2972:
2969:
2966:
2963:
2960:
2957:
2954:
2951:
2948:
2945:
2942:
2939:
2936:
2933:
2930:
2925:
2921:
2900:
2889:
2877:
2874:
2871:
2868:
2865:
2862:
2859:
2856:
2853:
2850:
2847:
2844:
2841:
2838:
2835:
2832:
2828:
2824:
2821:
2801:
2790:
2776:
2772:
2767:
2761:
2757:
2753:
2750:
2747:
2744:
2724:
2720:
2716:
2713:
2708:
2704:
2683:
2680:
2677:
2674:
2671:
2668:
2665:
2662:
2659:
2656:
2653:
2650:
2647:
2644:
2641:
2638:
2634:
2630:
2618:
2617:
2605:
2585:
2565:
2562:
2559:
2556:
2548:
2545:
2542:
2539:
2536:
2531:for some
2527:
2523:
2520:
2517:
2514:
2511:
2508:
2505:
2502:
2499:
2495:
2491:
2488:
2468:
2448:
2437:
2425:
2405:
2402:
2399:
2396:
2388:
2385:
2382:
2379:
2376:
2371:for some
2367:
2363:
2360:
2357:
2354:
2351:
2348:
2345:
2325:
2316:Set Union: If
2314:
2302:
2299:
2296:
2293:
2289:
2285:
2282:
2279:
2276:
2273:
2270:
2267:
2264:
2261:
2258:
2247:
2235:
2232:
2229:
2226:
2223:
2220:
2216:
2212:
2209:
2206:
2203:
2200:
2197:
2194:
2191:
2188:
2185:
2182:
2177:
2173:
2152:
2149:
2146:
2143:
2140:
2137:
2133:
2129:
2126:
2123:
2120:
2117:
2114:
2111:
2108:
2105:
2102:
2099:
2094:
2090:
2078:
2066:
2063:
2060:
2040:
2037:
2034:
2014:
2011:
2008:
2005:
2002:
1999:
1996:
1993:
1990:
1987:
1984:
1964:
1961:
1958:
1955:
1952:
1932:
1912:
1892:
1872:
1861:
1849:
1846:
1841:
1837:
1833:
1830:
1810:
1790:
1787:
1784:
1781:
1777:
1773:
1770:
1767:
1764:
1753:
1741:
1721:
1701:
1693:
1690:
1687:
1682: or
1679:
1676:
1673:
1669:
1665:
1662:
1659:
1656:
1653:
1650:
1630:
1610:
1599:
1587:
1567:
1564:
1561:
1558:
1554:
1550:
1547:
1544:
1539:
1535:
1514:
1502:
1501:
1489:
1486:
1483:
1480:
1476:
1472:
1469:
1466:
1463:
1460:
1457:
1454:
1451:
1448:
1445:
1442:
1439:
1436:
1433:
1430:
1427:
1424:
1421:
1418:
1415:
1412:
1409:
1389:
1386:
1383:
1380:
1376:
1372:
1369:
1366:
1363:
1360:
1357:
1354:
1351:
1348:
1345:
1334:
1322:
1302:
1299:
1296:
1293:
1290:
1287:
1284:
1281:
1278:
1275:
1272:
1268:
1264:
1261:
1258:
1255:
1252:
1249:
1224:
1213:
1201:
1181:
1178:
1175:
1172:
1169:
1166:
1163:
1160:
1156:
1152:
1149:
1146:
1143:
1140:
1137:
1134:
1131:
1128:
1125:
1122:
1119:
1116:
1096:
1085:
1073:
1070:
1067:
1047:
1042:
1039:
1035:
1031:
1011:
1008:
1005:
1002:
999:
996:
993:
990:
986:
982:
979:
976:
973:
970:
967:
964:
959:
956:
952:
931:
920:
908:
905:
902:
882:
879:
876:
856:
836:
816:
813:
810:
807:
799:
796:
793:
789:
785:
782:
779:
776:
773:
770:
767:
764:
761:
758:
738:
718:
707:
695:
675:
672:
669:
666:
662:
658:
655:
652:
649:
646:
643:
640:
637:
634:
631:
628:
608:
597:
585:
582:
579:
559:
539:
519:
499:
479:
459:
439:
424:stratification
415:
412:
383:
363:
360:
357:
321:
301:
298:
295:
275:
255:is said to be
244:
233:
232:
220:
197:
194:
191:
188:
185:
170:
148:if and only if
125:Extensionality
109:
85:
61:
58:
15:
9:
6:
4:
3:
2:
14715:
14704:
14701:
14699:
14696:
14694:
14691:
14689:
14686:
14685:
14683:
14670:
14669:
14664:
14656:
14650:
14647:
14645:
14642:
14640:
14637:
14635:
14632:
14628:
14625:
14624:
14623:
14620:
14618:
14615:
14613:
14610:
14608:
14604:
14601:
14599:
14596:
14594:
14591:
14589:
14586:
14584:
14581:
14580:
14578:
14574:
14568:
14565:
14563:
14560:
14558:
14557:Recursive set
14555:
14553:
14550:
14548:
14545:
14543:
14540:
14538:
14535:
14531:
14528:
14526:
14523:
14521:
14518:
14516:
14513:
14511:
14508:
14507:
14506:
14503:
14501:
14498:
14496:
14493:
14491:
14488:
14486:
14483:
14481:
14478:
14477:
14475:
14473:
14469:
14463:
14460:
14458:
14455:
14453:
14450:
14448:
14445:
14443:
14440:
14438:
14435:
14433:
14430:
14426:
14423:
14421:
14418:
14416:
14413:
14412:
14411:
14408:
14406:
14403:
14401:
14398:
14396:
14393:
14391:
14388:
14386:
14383:
14379:
14376:
14375:
14374:
14371:
14367:
14366:of arithmetic
14364:
14363:
14362:
14359:
14355:
14352:
14350:
14347:
14345:
14342:
14340:
14337:
14335:
14332:
14331:
14330:
14327:
14323:
14320:
14318:
14315:
14314:
14313:
14310:
14309:
14307:
14305:
14301:
14295:
14292:
14290:
14287:
14285:
14282:
14280:
14277:
14274:
14273:from ZFC
14270:
14267:
14265:
14262:
14256:
14253:
14252:
14251:
14248:
14246:
14243:
14241:
14238:
14237:
14236:
14233:
14231:
14228:
14226:
14223:
14221:
14218:
14216:
14213:
14211:
14208:
14206:
14203:
14202:
14200:
14198:
14194:
14184:
14183:
14179:
14178:
14173:
14172:non-Euclidean
14170:
14166:
14163:
14161:
14158:
14156:
14155:
14151:
14150:
14148:
14145:
14144:
14142:
14138:
14134:
14131:
14129:
14126:
14125:
14124:
14120:
14116:
14113:
14112:
14111:
14107:
14103:
14100:
14098:
14095:
14093:
14090:
14088:
14085:
14083:
14080:
14078:
14075:
14074:
14072:
14068:
14067:
14065:
14060:
14054:
14049:Example
14046:
14038:
14033:
14032:
14031:
14028:
14026:
14023:
14019:
14016:
14014:
14011:
14009:
14006:
14004:
14001:
14000:
13999:
13996:
13994:
13991:
13989:
13986:
13984:
13981:
13977:
13974:
13972:
13969:
13968:
13967:
13964:
13960:
13957:
13955:
13952:
13950:
13947:
13945:
13942:
13941:
13940:
13937:
13935:
13932:
13928:
13925:
13923:
13920:
13918:
13915:
13914:
13913:
13910:
13906:
13903:
13901:
13898:
13896:
13893:
13891:
13888:
13886:
13883:
13881:
13878:
13877:
13876:
13873:
13871:
13868:
13866:
13863:
13861:
13858:
13854:
13851:
13849:
13846:
13844:
13841:
13839:
13836:
13835:
13834:
13831:
13829:
13826:
13824:
13821:
13819:
13816:
13812:
13809:
13807:
13806:by definition
13804:
13803:
13802:
13799:
13795:
13792:
13791:
13790:
13787:
13785:
13782:
13780:
13777:
13775:
13772:
13770:
13767:
13766:
13763:
13760:
13758:
13754:
13749:
13743:
13739:
13729:
13726:
13724:
13721:
13719:
13716:
13714:
13711:
13709:
13706:
13704:
13701:
13699:
13696:
13694:
13693:Kripke–Platek
13691:
13689:
13686:
13682:
13679:
13677:
13674:
13673:
13672:
13669:
13668:
13666:
13662:
13654:
13651:
13650:
13649:
13646:
13644:
13641:
13637:
13634:
13633:
13632:
13629:
13627:
13624:
13622:
13619:
13617:
13614:
13612:
13609:
13606:
13602:
13598:
13595:
13591:
13588:
13586:
13583:
13581:
13578:
13577:
13576:
13572:
13569:
13568:
13566:
13564:
13560:
13556:
13548:
13545:
13543:
13540:
13538:
13537:constructible
13535:
13534:
13533:
13530:
13528:
13525:
13523:
13520:
13518:
13515:
13513:
13510:
13508:
13505:
13503:
13500:
13498:
13495:
13493:
13490:
13488:
13485:
13483:
13480:
13478:
13475:
13473:
13470:
13469:
13467:
13465:
13460:
13452:
13449:
13447:
13444:
13442:
13439:
13437:
13434:
13432:
13429:
13427:
13424:
13423:
13421:
13417:
13414:
13412:
13409:
13408:
13407:
13404:
13402:
13399:
13397:
13394:
13392:
13389:
13387:
13383:
13379:
13377:
13374:
13370:
13367:
13366:
13365:
13362:
13361:
13358:
13355:
13353:
13349:
13339:
13336:
13334:
13331:
13329:
13326:
13324:
13321:
13319:
13316:
13314:
13311:
13307:
13304:
13303:
13302:
13299:
13295:
13290:
13289:
13288:
13285:
13284:
13282:
13280:
13276:
13268:
13265:
13263:
13260:
13258:
13255:
13254:
13253:
13250:
13248:
13245:
13243:
13240:
13238:
13235:
13233:
13230:
13228:
13225:
13223:
13220:
13219:
13217:
13215:
13214:Propositional
13211:
13205:
13202:
13200:
13197:
13195:
13192:
13190:
13187:
13185:
13182:
13180:
13177:
13173:
13170:
13169:
13168:
13165:
13163:
13160:
13158:
13155:
13153:
13150:
13148:
13145:
13143:
13142:Logical truth
13140:
13138:
13135:
13134:
13132:
13130:
13126:
13123:
13121:
13117:
13111:
13108:
13106:
13103:
13101:
13098:
13096:
13093:
13091:
13088:
13086:
13082:
13078:
13074:
13072:
13069:
13067:
13064:
13062:
13058:
13055:
13054:
13052:
13050:
13044:
13039:
13033:
13030:
13028:
13025:
13023:
13020:
13018:
13015:
13013:
13010:
13008:
13005:
13003:
13000:
12998:
12995:
12993:
12990:
12988:
12985:
12983:
12980:
12978:
12975:
12971:
12968:
12967:
12966:
12963:
12962:
12960:
12956:
12952:
12945:
12940:
12938:
12933:
12931:
12926:
12925:
12922:
12910:
12909:Ernst Zermelo
12907:
12905:
12902:
12900:
12897:
12895:
12894:Willard Quine
12892:
12890:
12887:
12885:
12882:
12880:
12877:
12875:
12872:
12870:
12867:
12865:
12862:
12860:
12857:
12855:
12852:
12851:
12849:
12847:
12846:Set theorists
12843:
12837:
12834:
12832:
12829:
12827:
12824:
12823:
12821:
12815:
12813:
12810:
12809:
12806:
12798:
12795:
12793:
12792:Kripke–Platek
12790:
12786:
12783:
12782:
12781:
12778:
12777:
12776:
12773:
12769:
12766:
12765:
12764:
12763:
12759:
12755:
12752:
12751:
12750:
12747:
12746:
12743:
12740:
12738:
12735:
12733:
12730:
12728:
12725:
12724:
12722:
12718:
12712:
12709:
12707:
12704:
12702:
12699:
12697:
12695:
12690:
12688:
12685:
12683:
12680:
12677:
12673:
12670:
12668:
12665:
12661:
12658:
12656:
12653:
12651:
12648:
12647:
12646:
12643:
12640:
12636:
12633:
12631:
12628:
12626:
12623:
12621:
12618:
12617:
12615:
12612:
12608:
12602:
12599:
12597:
12594:
12592:
12589:
12587:
12584:
12582:
12579:
12577:
12574:
12572:
12569:
12565:
12562:
12560:
12557:
12556:
12555:
12552:
12550:
12547:
12545:
12542:
12540:
12537:
12535:
12532:
12529:
12525:
12522:
12520:
12517:
12515:
12512:
12511:
12509:
12503:
12500:
12499:
12496:
12490:
12487:
12485:
12482:
12480:
12477:
12475:
12472:
12470:
12467:
12465:
12462:
12460:
12457:
12454:
12451:
12449:
12446:
12445:
12443:
12441:
12437:
12429:
12428:specification
12426:
12424:
12421:
12420:
12419:
12416:
12415:
12412:
12409:
12407:
12404:
12402:
12399:
12397:
12394:
12392:
12389:
12387:
12384:
12382:
12379:
12377:
12374:
12370:
12367:
12366:
12365:
12362:
12360:
12357:
12353:
12350:
12348:
12345:
12343:
12340:
12339:
12338:
12335:
12333:
12330:
12329:
12327:
12325:
12321:
12316:
12306:
12303:
12302:
12300:
12296:
12292:
12285:
12280:
12278:
12273:
12271:
12266:
12265:
12262:
12256:
12252:
12250:
12246:
12244:
12240:
12235:
12232:
12229:
12226:
12225:
12223:
12220:
12217:
12213:
12210:
12209:
12200:
12196:
12192:
12188:
12184:
12180:
12176:
12172:
12168:
12164:
12159:
12155:
12151:
12146:
12141:
12136:
12131:
12127:
12123:
12119:
12115:
12111:
12107:
12103:
12100:
12096:
12092:
12088:
12084:
12080:
12076:
12072:
12068:
12064:
12059:
12055:
12053:9780674798373
12049:
12045:
12044:
12038:
12035:
12031:
12027:
12024:
12021:
12017:
12013:
12011:0-674-55451-5
12007:
12003:
11998:
11995:
11991:
11987:
11982:
11979:
11975:
11971:
11967:
11963:
11959:
11954:
11950:
11946:
11942:
11938:
11934:
11930:
11926:
11922:
11918:
11917:Jensen, R. B.
11914:
11907:
11902:
11898:
11894:
11890:
11886:
11882:
11878:
11877:Studia Logica
11873:
11870:
11866:
11862:
11860:2-87209-488-1
11856:
11849:
11848:
11842:
11838:
11834:
11830:
11826:
11822:
11818:
11814:
11810:
11809:
11803:
11799:
11795:
11791:
11786:
11782:
11778:
11773:
11770:
11766:
11762:
11760:0-19-853395-0
11756:
11752:
11747:
11743:
11739:
11735:
11731:
11727:
11723:
11716:
11711:
11707:
11700:
11695:
11684:
11680:
11675:
11671:
11667:
11663:
11659:
11655:
11651:
11647:
11643:
11638:
11637:
11613:
11591:
11587:
11576:
11572:
11555:
11554:Logic Matters
11551:
11544:
11529:
11528:Logic Matters
11525:
11518:
11511:
11506:
11499:
11494:
11487:
11482:
11475:
11470:
11455:
11454:Logic Matters
11451:
11444:
11437:
11432:
11425:
11420:
11413:
11408:
11400:
11396:
11392:
11388:
11385:(1): 87–116.
11384:
11380:
11373:
11366:
11359:
11354:
11352:
11344:
11339:
11337:
11329:
11324:
11317:
11312:
11310:
11308:
11300:
11295:
11288:
11283:
11276:
11271:
11264:
11259:
11252:
11247:
11240:
11235:
11228:
11223:
11216:
11211:
11205:, p. 24.
11204:
11199:
11193:, p. 30.
11192:
11187:
11185:
11177:
11172:
11166:, p. 20.
11165:
11160:
11154:, p. 19.
11153:
11148:
11146:
11138:
11133:
11126:
11121:
11115:, p. 44.
11114:
11109:
11103:, p. 10.
11102:
11097:
11090:
11085:
11078:
11073:
11067:, p. 32.
11066:
11061:
11054:
11049:
11042:
11037:
11031:, p. 31.
11030:
11025:
11023:
11021:
11013:
11008:
11001:
10996:
10990:, p. 27.
10989:
10984:
10977:
10972:
10966:, p. 25.
10965:
10960:
10953:
10949:
10943:
10936:
10931:
10925:, p. 16.
10924:
10919:
10912:
10907:
10905:
10903:
10895:
10890:
10883:
10878:
10876:
10874:
10869:
10859:
10856:
10854:
10851:
10849:
10846:
10844:
10841:
10839:
10836:
10835:
10829:
10827:
10814:
10810:
10805:
10803:
10799:
10798:
10793:
10788:
10787:predicativity
10782:
10775:
10771:
10767:
10763:
10762:Ernst Specker
10759:
10758:Comprehension
10755:
10750:
10748:
10744:
10740:
10736:
10732:
10728:
10724:
10720:
10716:
10712:
10708:
10704:
10700:
10690:
10688:
10684:
10680:
10676:
10672:
10668:
10664:
10660:
10656:
10652:
10648:
10644:
10640:
10636:
10615:
10609:
10605:
10596:
10591:
10589:
10585:
10581:
10577:
10573:
10568:
10564:
10563:well-ordering
10560:
10556:
10553:
10546:
10540:
10524:
10520:
10497:
10493:
10484:
10466:
10462:
10453:
10449:
10444:
10428:
10424:
10401:
10397:
10374:
10370:
10347:
10344:
10341:
10337:
10314:
10310:
10284:
10281:
10278:
10274:
10265:
10261:
10235:
10231:
10224:
10202:
10198:
10188:
10178:
10176:
10172:
10168:
10167:
10150:
10142:
10126:
10117:
10101:
10098:
10092:
10086:
10082:
10073:
10068:
10066:
10062:
10038:
10034:
10030:
10025:
10021:
10017:
10014:
10005:
9985:
9977:
9959:
9956:
9953:
9949:
9940:
9919:
9915:
9911:
9906:
9902:
9898:
9895:
9884:
9880:
9862:
9858:
9835:
9832:
9829:
9825:
9816:
9800:
9792:
9788:
9770:
9766:
9757:
9735:
9729:
9726:
9718:
9714:
9705:
9702:
9699:
9695:
9691:
9688:
9653:
9645:
9642:
9639:
9635:
9628:
9625:
9620:
9616:
9612:
9609:
9595:
9579:
9576:
9573:
9565:
9561:
9543:
9539:
9530:
9526:
9522:
9518:
9514:
9511:
9507:
9489:
9485:
9464:
9456:
9440:
9431:
9418:
9413:
9410:
9404:
9398:
9394:
9390:
9387:
9384:
9381:
9378:
9372:
9366:
9361:
9358:
9355:
9351:
9347:
9342:
9339:
9336:
9332:
9328:
9320:
9302:
9299:
9293:
9287:
9283:
9260:
9256:
9233:
9230:
9227:
9223:
9214:
9196:
9192:
9182:
9168:
9165:
9159:
9153:
9145:
9127:
9123:
9115:
9111:
9108:
9104:
9100:
9093:Models of NFU
9090:
9087:
9083:
9079:
9075:
9070:
9068:
9063:
9059:
9049:
9035:
9015:
9007:
9002:
8988:
8974:
8970:
8966:
8952:
8948:
8944:
8918:
8915:
8909:
8903:
8900:
8897:
8874:
8871:
8868:
8845:
8839:
8836:
8830:
8824:
8816:
8811:
8794:
8780:
8776:
8767:
8728:
8720:
8716:
8688:
8680:
8676:
8652:
8644:
8640:
8619:
8616:
8608:
8607:
8606:
8589:
8586:
8583:
8580:
8571:
8565:
8559:
8547:
8542:
8538:
8514:
8508:
8488:
8485:
8482:
8462:
8439:
8431:
8427:
8406:
8383:
8377:
8369:
8364:
8350:
8342:
8326:
8306:
8286:
8263:
8260:
8257:
8232:
8228:
8202:
8198:
8194:
8191:
8188:
8185:
8179:
8176:
8168:
8149:
8146:
8143:
8120:
8097:
8094:
8091:
8088:
8085:
8082:
8076:
8073:
8070:
8061:
8056:
8052:
8031:
8023:
8007:
7985:
7981:
7960:
7940:
7920:
7911:
7909:
7873:
7853:
7822:
7771:
7751:
7731:
7728:
7725:
7722:
7719:
7716:
7713:
7693:
7690:
7687:
7679:
7647:
7643:
7639:
7635:
7630:
7588:
7584:
7583:
7572:
7570:
7566:
7562:
7558:
7542:
7530:
7521:
7498:
7490:
7486:
7462:
7454:
7450:
7441:
7433:
7408:
7388:
7385:
7382:
7362:
7334:
7326:
7322:
7313:
7305:
7291:
7272:
7239:
7233:
7220:
7199:
7191:
7180:
7174:
7166:
7155:
7147:
7143:
7129:
7110:
7101:
7094:
7070:
7064:
7056:
7045:
7037:
7033:
6999:
6993:
6985:
6974:
6966:
6962:
6936:
6913:
6905:
6901:
6880:
6871:
6869:
6868:Comprehension
6845:
6839:
6831:
6823:
6798:
6775:
6769:
6741:
6735:
6727:
6719:
6705:
6691:
6671:
6665:
6645:
6636:
6630:
6627:
6624:
6604:
6581:
6575:
6555:
6529:
6523:
6520:
6517:
6514:
6511:
6508:
6505:
6499:
6496:
6488:
6472:
6452:
6429:
6423:
6415:
6410:
6396:
6393:
6390:
6370:
6347:
6341:
6333:
6317:
6297:
6274:
6268:
6261:
6257:
6241:
6234:
6233:universal set
6231:. In NF, the
6230:
6226:
6222:
6213:
6211:
6210:Comprehension
6192:
6189:
6186:
6183:
6180:
6157:
6154:
6151:
6143:
6133:
6130:
6126:
6110:
6107:
6104:
6081:
6078:
6075:
6072:
6069:
6059:
6058:Russell class
6055:
6045:
6043:
6039:
6035:
6022:
6018:
6002:
5999:
5996:
5988:
5984:
5980:
5976:
5972:
5968:
5964:
5960:
5956:
5952:
5950:
5946:
5942:
5939:
5935:
5931:
5930:Comprehension
5927:
5923:
5919:
5916:
5915:universal set
5912:
5896:
5893:
5890:
5882:
5880:
5879:universal set
5875:
5874:
5873:
5871:
5867:
5863:
5859:
5849:
5847:
5843:
5839:
5835:
5831:
5827:
5819:
5815:
5811:
5807:
5788:
5782:
5779:
5759:
5751:
5736:
5728:
5724:
5720:
5719:
5718:
5716:
5712:
5707:
5688:
5658:
5645:
5624:
5611:
5607:
5591:
5588:
5578:
5568:
5556:
5553:
5545:
5540:
5527:
5519:
5516:
5508:
5492:
5469:
5463:
5457:
5454:
5451:
5448:
5445:
5437:
5418:
5412:
5409:
5384:
5381:
5378:
5370:
5340:
5315:
5306:
5289:
5283:
5257:
5251:
5248:
5240:
5237:
5211:
5205:
5197:
5170:
5168:
5167:inductive set
5152:
5132:
5126:
5123:
5120:
5117:
5114:
5111:
5108:
5105:
5099:
5093:
5090:
5084:
5078:
5072:
5038:
5034:
5030:
5026:
5022:
5012:
4995:
4992:
4989:
4986:
4983:
4980:
4974:
4971:
4965:
4962:
4959:
4947:
4942:
4938:
4917:
4894:
4891:
4888:
4865:
4862:
4853:
4850:
4847:
4836:
4832:
4811:
4808:
4799:
4796:
4793:
4782:
4778:
4755:
4751:
4728:
4724:
4716:
4712:
4708:
4703:
4701:
4697:
4693:
4689:
4685:
4663:
4657:
4654:
4645:
4639:
4627:
4621:
4613:
4607:
4604:
4593:
4588:
4587:ordered pairs
4584:
4580:
4574:Ordered pairs
4571:
4569:
4562:Constructions
4559:
4556:
4531:
4522:
4516:
4510:
4507:
4504:
4501:
4498:
4489:
4483:
4466:
4463:
4437:
4431:
4405:
4399:
4396:
4393:
4383:
4379:
4365:
4362:
4359:
4356:
4344:
4341:
4338:
4332:
4329:
4326:
4323:
4320:
4311:
4305:
4288:
4282:
4262:
4259:
4256:
4245:
4241:
4227:
4221:
4201:
4198:
4195:
4192:
4189:
4186:
4175:
4174:
4173:
4156:
4133:
4116:
4110:
4084:
4078:
4075:
4072:
4037:
4034:
4031:
4025:
4022:
4019:
4016:
4013:
4001:
3998:
3995:
3983:
3980:
3977:
3971:
3968:
3965:
3962:
3952:
3951:
3947:
3943:
3942:
3941:
3939:
3935:
3934:
3923:
3909:
3889:
3886:
3883:
3875:
3871:
3866:
3852:
3829:
3823:
3803:
3783:
3780:
3777:
3755:
3751:
3747:
3742:
3738:
3715:
3711:
3707:
3702:
3698:
3683:
3679:
3677:
3673:
3652:
3648:
3641:
3633:
3614:
3611:
3608:
3595:
3591:
3584:
3581:
3576:
3572:
3545:
3542:
3539:
3535:
3506:
3502:
3495:
3487:
3484:
3481:
3477:
3473:
3468:
3464:
3455:
3451:
3442:
3439:
3436:
3432:
3402:
3398:
3391:
3368:
3365:
3362:
3349:
3345:
3338:
3335:
3330:
3326:
3297:
3293:
3286:
3278:
3274:
3270:
3266:
3262:
3259:
3255:
3237:
3233:
3224:
3220:
3216:
3212:
3208:
3180:
3177:
3168:
3162:
3159:
3153:
3150:
3144:
3141:
3135:
3129:
3101:
3093:
3075:
3072:
3066:
3063:
3060:
3054:
3048:
3045:
3042:
3039:
3036:
3027:
3021:
3013:
3009:
2985:
2982:
2976:
2973:
2970:
2964:
2958:
2955:
2952:
2949:
2946:
2937:
2931:
2923:
2919:
2898:
2890:
2869:
2866:
2863:
2857:
2854:
2851:
2848:
2845:
2836:
2833:
2822:
2799:
2791:
2774:
2770:
2759:
2755:
2751:
2748:
2745:
2742:
2722:
2714:
2711:
2706:
2702:
2675:
2672:
2669:
2666:
2663:
2660:
2657:
2648:
2645:
2639:
2636:
2628:
2620:
2619:
2603:
2583:
2560:
2557:
2554:
2546:
2543:
2540:
2537:
2534:
2518:
2515:
2512:
2503:
2497:
2489:
2466:
2446:
2438:
2423:
2400:
2397:
2394:
2386:
2383:
2380:
2377:
2374:
2361:
2355:
2349:
2343:
2323:
2315:
2297:
2294:
2291:
2280:
2277:
2274:
2265:
2259:
2248:
2230:
2227:
2224:
2221:
2218:
2207:
2204:
2198:
2195:
2192:
2180:
2175:
2171:
2147:
2144:
2141:
2138:
2135:
2124:
2121:
2115:
2112:
2109:
2097:
2092:
2088:
2079:
2064:
2061:
2058:
2038:
2035:
2032:
2009:
2006:
2003:
1997:
1991:
1988:
1985:
1959:
1956:
1953:
1930:
1910:
1890:
1870:
1862:
1847:
1844:
1839:
1835:
1831:
1828:
1808:
1785:
1782:
1779:
1771:
1765:
1762:
1754:
1739:
1719:
1696: or both
1691:
1688:
1685:
1677:
1674:
1671:
1663:
1657:
1654:
1651:
1648:
1628:
1608:
1600:
1585:
1562:
1559:
1556:
1548:
1542:
1537:
1533:
1512:
1504:
1503:
1484:
1481:
1478:
1467:
1464:
1458:
1446:
1440:
1437:
1434:
1428:
1422:
1416:
1410:
1384:
1381:
1378:
1367:
1364:
1361:
1352:
1346:
1335:
1320:
1297:
1294:
1288:
1285:
1282:
1276:
1273:
1262:
1256:
1250:
1222:
1214:
1199:
1176:
1173:
1167:
1164:
1161:
1144:
1138:
1132:
1120:
1117:
1114:
1094:
1086:
1071:
1068:
1065:
1045:
1040:
1037:
1033:
1029:
1006:
1003:
997:
994:
991:
977:
974:
971:
962:
957:
954:
950:
929:
921:
906:
903:
900:
880:
877:
874:
854:
834:
811:
808:
805:
797:
794:
791:
780:
777:
774:
765:
762:
759:
756:
736:
716:
708:
693:
670:
667:
664:
656:
650:
644:
638:
632:
626:
606:
598:
583:
580:
577:
557:
537:
517:
497:
477:
457:
437:
429:
428:
427:
425:
421:
411:
409:
405:
401:
397:
381:
361:
358:
355:
347:
343:
339:
335:
319:
299:
296:
293:
273:
265:
262:
258:
242:
218:
211:
192:
189:
186:
175:
172:A restricted
171:
168:
164:
160:
156:
152:
149:
146:
142:
138:
134:
130:
126:
123:
122:
121:
107:
99:
83:
75:
71:
67:
57:
55:
54:
49:
45:
42:conceived by
41:
38:
34:
30:
26:
22:
14659:
14457:Ultraproduct
14304:Model theory
14269:Independence
14205:Formal proof
14197:Proof theory
14180:
14153:
14110:real numbers
14082:second-order
13993:Substitution
13870:Metalanguage
13811:conservative
13784:Axiom schema
13728:Constructive
13707:
13698:Morse–Kelley
13664:Set theories
13643:Aleph number
13636:inaccessible
13542:Grothendieck
13426:intersection
13313:Higher-order
13301:Second-order
13247:Truth tables
13204:Venn diagram
12987:Formal proof
12859:Georg Cantor
12854:Paul Bernays
12785:Morse–Kelley
12767:
12760:
12693:
12692:Subset
12639:hereditarily
12601:Venn diagram
12559:ordered pair
12474:Intersection
12418:Axiom schema
12169:(1): 25–32,
12166:
12162:
12117:
12113:
12066:
12062:
12042:
12033:
12029:
12026:Quine, W. V.
12001:
11985:
11961:
11957:
11924:
11920:
11880:
11876:
11846:
11812:
11806:
11800:(2): 41–243.
11797:
11793:
11780:
11750:
11725:
11721:
11705:
11686:. Retrieved
11682:
11645:
11641:
11575:
11557:. Retrieved
11553:
11543:
11531:. Retrieved
11527:
11517:
11505:
11498:Grishin 1969
11493:
11481:
11469:
11457:. Retrieved
11453:
11443:
11438:, sec. 17.5.
11431:
11419:
11412:Forster 2007
11407:
11382:
11378:
11365:
11358:Specker 1953
11345:, sec. 12.1.
11323:
11294:
11282:
11270:
11258:
11246:
11234:
11222:
11210:
11198:
11171:
11159:
11132:
11120:
11108:
11096:
11084:
11072:
11060:
11048:
11036:
11007:
10995:
10983:
10971:
10959:
10951:
10946:For example
10942:
10930:
10918:
10889:
10806:
10800:without the
10795:
10783:
10757:
10756:showed that
10751:
10722:
10718:
10706:
10703:ordered pair
10696:
10686:
10682:
10678:
10674:
10670:
10666:
10662:
10654:
10650:
10646:
10642:
10638:
10634:
10594:
10592:
10590:(α) in NFU.
10587:
10583:
10579:
10575:
10558:
10554:
10552:automorphism
10549:
10544:
10482:
10451:
10447:
10445:
10184:
10174:
10170:
10164:
10140:
10118:
10071:
10069:
10064:
10060:
9975:
9938:
9882:
9878:
9814:
9790:
9786:
9593:
9563:
9559:
9524:
9516:
9512:
9510:automorphism
9454:
9432:
9212:
9183:
9109:
9107:automorphism
9099:model theory
9096:
9071:
9055:
9003:
8812:
8765:
8707:
8367:
8365:
8340:
8021:
7912:
7907:
7631:
7580:
7578:
7568:
7564:
7484:
7292:
7218:
7127:
6872:
6867:
6706:
6411:
6219:
6209:
6144:is trivial:
6139:
6051:
6031:
6021:well-ordered
5982:
5978:
5954:
5943:
5929:
5928:} exists by
5925:
5921:
5917:
5876:
5861:
5857:
5855:
5845:
5841:
5833:
5829:
5825:
5823:
5817:
5813:
5809:
5805:
5749:is infinite.
5714:
5710:
5708:
5605:
5543:
5541:
5506:
5436:equinumerous
5307:
5171:
5165:would be an
5036:
5032:
5018:
4706:
4704:
4699:
4695:
4687:
4683:
4591:
4577:
4565:
4557:
4546:
4381:
4243:
4134:
4061:
3945:
3937:
3930:
3929:
3873:
3869:
3867:
3689:
3680:
3671:
3276:
3272:
3268:
3264:
3260:
3253:
3223:type indices
3222:
3214:
3210:
3206:
3204:
417:
407:
403:
399:
395:
345:
341:
337:
333:
263:
256:
234:
166:
158:
154:
150:
144:
140:
136:
132:
131:and any set
128:
63:
51:
28:
24:
18:
14693:Type theory
14567:Type theory
14515:undecidable
14447:Truth value
14334:equivalence
14013:non-logical
13626:Enumeration
13616:Isomorphism
13563:cardinality
13547:Von Neumann
13512:Ultrafilter
13477:Uncountable
13411:equivalence
13328:Quantifiers
13318:Fixed-point
13287:First-order
13167:Consistency
13152:Proposition
13129:Traditional
13100:Lindström's
13090:Compactness
13032:Type theory
12977:Cardinality
12884:Thomas Jech
12727:Alternative
12706:Uncountable
12660:Ultrafilter
12519:Cardinality
12423:replacement
12364:Determinacy
12069:(1): 1–17,
11815:(1): 1–19.
11510:Fenton 2015
11474:Rosser 1942
11436:Holmes 1998
11343:Holmes 1998
11328:Holmes 2001
11316:Jensen 1969
11287:Fenton 2015
11263:Fenton 2015
11239:Fenton 2015
11215:Fenton 2015
11203:Holmes 1998
11191:Holmes 1998
11176:Holmes 1998
11164:Holmes 1998
11152:Holmes 1998
11137:Fenton 2015
11113:Holmes 1998
11089:Fenton 2015
11065:Holmes 1998
11053:Fenton 2015
11029:Holmes 1998
11012:Fenton 2015
10988:Holmes 1998
10976:Fenton 2015
10964:Holmes 1998
10923:Holmes 1998
10911:Holmes 1998
10894:Holmes 1998
10729:as well as
10443:with care.
9521:truth value
9058:consistency
9052:Consistency
8368:T operation
7646:isomorphism
7557:restriction
7375:(e.g. when
6290:of any set
6229:cardinality
5977:: the sets
5959:circularity
5934:complements
4715:projections
3630:and is not
3219:many-sorted
2911:, the sets
2025:exactly if
1215:Domain: If
1058:exactly if
14698:Urelements
14682:Categories
14378:elementary
14071:arithmetic
13939:Quantifier
13917:functional
13789:Expression
13507:Transitive
13451:identities
13436:complement
13369:hereditary
13352:Set theory
12879:Kurt Gödel
12864:Paul Cohen
12701:Transitive
12469:Identities
12453:Complement
12440:Operations
12401:Regularity
12369:projective
12332:Adjunction
12291:Set theory
11728:: 97–110.
11634:References
11424:Quine 1987
11139:, ax-sset.
10896:, chpt. 8.
10774:urelements
10770:urelements
10711:Kuratowski
10572:urelements
9319:urelements
7744:such that
6129:set theory
5940:structure.
5883:. Because
5852:Large sets
5723:urelements
4592:type-level
3933:urelements
3114:, the set
1975:, exists;
1525:, the set
1107:, the set
942:, the set
749:, the set
619:, the set
418:NF can be
394:, we have
257:stratified
235:A formula
98:membership
60:Definition
40:set theory
14649:Supertask
14552:Recursion
14510:decidable
14344:saturated
14322:of models
14245:deductive
14240:axiomatic
14160:Hilbert's
14147:Euclidean
14128:canonical
14051:axiomatic
13983:Signature
13912:Predicate
13801:Extension
13723:Ackermann
13648:Operation
13527:Universal
13517:Recursive
13492:Singleton
13487:Inhabited
13472:Countable
13462:Types of
13446:power set
13416:partition
13333:Predicate
13279:Predicate
13194:Syllogism
13184:Soundness
13157:Inference
13147:Tautology
13049:paradoxes
12812:Paradoxes
12732:Axiomatic
12711:Universal
12687:Singleton
12682:Recursive
12625:Countable
12620:Amorphous
12479:Power set
12396:Power set
12347:dependent
12342:countable
11897:207242273
11614:α
11592:α
11486:Wang 1950
11217:, ax-nin.
11055:, ax-cnv.
10752:In 1944,
10713:in 1921.
10697:In 1914,
10659:injection
10637:}, where
10616:α
10593:In fact,
10525:α
10498:α
10467:ω
10463:ℶ
10429:α
10151:α
10127:α
10093:α
10035:ϕ
10031:∣
10026:α
10018:∈
9986:ϕ
9954:α
9916:ϕ
9912:∣
9907:α
9899:∈
9877:in which
9859:ϕ
9833:−
9801:ϕ
9785:in which
9767:ϕ
9730:ψ
9719:α
9703:−
9692:∈
9686:∀
9643:−
9629:ψ
9621:α
9613:∈
9607:∀
9577:−
9540:ϕ
9486:ϕ
9465:ϕ
9441:ϕ
9405:α
9391:∈
9385:∧
9379:∈
9352:≡
9333:∈
9294:α
9261:α
9228:α
9197:α
9169:α
9160:α
9128:α
8989:…
8983:Ω
8961:Ω
8942:Ω
8919:α
8910:α
8901:∣
8898:α
8875:β
8869:α
8846:β
8831:α
8798:Ω
8789:Ω
8752:Ω
8729:α
8689:α
8653:α
8620:α
8581:∣
8543:ι
8515:α
8489:α
8486:∈
8407:α
8384:α
8351:α
8339:would be
8327:β
8233:α
8203:α
8195:∼
8189:∣
8177:β
8121:α
8098:α
8089:≤
8083:∣
8057:α
8032:α
8008:α
7986:α
7961:β
7941:α
7921:α
7894:Ω
7874:α
7854:α
7823:∈
7820:Ω
7732:β
7729:∈
7720:α
7717:∈
7694:β
7691:≤
7688:α
7617:Ω
7597:Ω
7561:singleton
7540:⌈
7525:↦
7485:Cantorian
7192:≪
7105:↦
7093:bijection
6811:. In NF,
6669:↦
6643:→
6548:. In NF,
6521:∉
6515:∣
6509:∈
6414:injection
6332:injection
6260:power set
6184:∣
6125:paradoxes
6073:∣
6000:∼
5987:bijection
5783:×
5592:…
5579:∅
5563:∅
5554:∅
5520:∉
5517:∅
5493:∅
5473:∅
5385:∈
5249:∣
5241:∈
5124:∉
5118:∧
5112:∈
5106:∣
5094:∪
5050:∅
4993:∈
4981:∣
4939:π
4918:ϕ
4895:ϕ
4892:∣
4833:π
4779:π
4752:π
4725:π
4583:functions
4579:Relations
4517:ϕ
4514:↔
4508:∈
4496:∀
4490:∧
4461:∃
4432:ϕ
4400:ϕ
4397:∣
4354:→
4342:∈
4336:↔
4330:∈
4318:∀
4312:∧
4289:∧
4254:∀
4205:→
4199:∈
4184:∀
4111:ϕ
4079:ϕ
4076:∣
4035:∈
4029:↔
4023:∈
4011:∀
4005:↔
3990:→
3981:∈
3960:∀
3946:non-empty
3748:∈
3676:relations
3642:ϕ
3585:ϕ
3582:∣
3496:ϕ
3493:↔
3474:∈
3448:∀
3429:∃
3392:ϕ
3339:ϕ
3336:∣
3287:ϕ
3178:∈
3148:∀
3073:∈
2983:∈
2888:, exists.
2861:↔
2855:∈
2843:∀
2831:∃
2746:∪
2673:∈
2667:∧
2661:∈
2652:¬
2616:, exists.
2436:, exists.
2398:∈
2384:∈
2344:⋃
2295:∈
2228:∈
2172:π
2145:∈
2089:π
1832:∪
1752:, exists.
1689:∈
1675:∈
1652:∪
1598:, exists.
1560:∉
1482:∈
1438:×
1429:∩
1423:⊆
1411:∈
1382:⊆
1347:⊆
1295:∈
1271:∃
1212:, exists.
1174:∈
1118:ι
1038:−
1004:∈
955:−
904:×
878:×
809:∈
795:∈
760:×
627:ι
382:ϕ
320:ϕ
297:∈
274:ϕ
243:ϕ
219:ϕ
193:ϕ
190:∣
108:∈
14634:Logicism
14627:timeline
14603:Concrete
14462:Validity
14432:T-schema
14425:Kripke's
14420:Tarski's
14415:semantic
14405:Strength
14354:submodel
14349:spectrum
14317:function
14165:Tarski's
14154:Elements
14141:geometry
14097:Robinson
14018:variable
14003:function
13976:spectrum
13966:Sentence
13922:variable
13865:Language
13818:Relation
13779:Automata
13769:Alphabet
13753:language
13607:-jection
13585:codomain
13571:Function
13532:Universe
13502:Infinite
13406:Relation
13189:Validity
13179:Argument
13077:theorem,
12816:Problems
12720:Theories
12696:Superset
12672:Infinite
12501:Concepts
12381:Infinity
12298:Overview
12199:42852449
12154:16589362
12108:(1953).
12099:13389728
11949:46960777
11941:20114640
11921:Synthese
11837:39672836
11742:15231169
11688:25 April
11683:Metamath
11670:42174966
11533:21 April
11459:21 April
11241:, ax-1c.
11091:, ax-si.
11014:, ax-xp.
10978:, ax-sn.
10832:See also
10809:Metamath
10747:Hao Wang
10483:Infinity
10452:Infinity
10448:Infinity
10171:Infinity
9817:. Apply
9523:because
9006:standard
8815:monotone
8319:), then
7491:. A set
6190:∉
6155:∉
6108:∉
6079:∉
5971:relation
5945:Cardinal
5858:Infinity
5826:Infinity
5818:Infinity
5810:Infinity
5806:Infinity
5711:Infinity
5606:Infinity
5544:Infinity
5509:for NF:
3931:NF with
332:we have
261:function
74:equality
14576:Related
14373:Diagram
14271: (
14250:Hilbert
14235:Systems
14230:Theorem
14108:of the
14053:systems
13833:Formula
13828:Grammar
13744: (
13688:General
13401:Forcing
13386:Element
13306:Monadic
13081:paradox
13022:Theorem
12958:General
12754:General
12749:Zermelo
12655:subbase
12637: (
12576:Forcing
12554:Element
12526: (
12504:Methods
12391:Pairing
12191:0034733
12183:2268438
12145:1063889
12122:Bibcode
12091:0006327
12083:2267550
12020:0045661
11994:0002508
11978:2300564
11869:1759289
11829:2267307
11769:1166801
11662:2273386
11399:2694912
10693:History
10669:} ) = {
9142:of the
8501:, then
7563:map to
7559:of the
6684:, then
6038:curries
5951:numbers
5949:ordinal
5938:Boolean
5402:. Then
4453:, i.e.
3263:, type
3196:exists.
570:, then
157:, then
31:) is a
14339:finite
14102:Skolem
14055:
14030:Theory
13998:Symbol
13988:String
13971:atomic
13848:ground
13843:closed
13838:atomic
13794:ground
13757:syntax
13653:binary
13580:domain
13497:Finite
13262:finite
13120:Logics
13079:
13027:Theory
12645:Filter
12635:Finite
12571:Family
12514:Almost
12352:global
12337:Choice
12324:Axioms
12218:(2011)
12197:
12189:
12181:
12152:
12142:
12097:
12089:
12081:
12050:
12018:
12008:
11992:
11976:
11947:
11939:
11895:
11867:
11857:
11835:
11827:
11767:
11757:
11740:
11668:
11660:
11397:
10677:} ) |
10657:is an
10175:Choice
10166:Choice
9885:. Now
7644:under
7555:, the
7219:Choice
7128:Choice
6465:since
5913:, the
5862:Choice
5814:Choice
4707:(a, b)
4661:
4649:
4631:
4611:
3874:either
3845:where
3770:where
3091:exist.
96:) and
14329:Model
14077:Peano
13934:Proof
13774:Arity
13703:Naive
13590:image
13522:Fuzzy
13482:Empty
13431:union
13376:Class
13017:Model
13007:Lemma
12965:Axiom
12737:Naive
12667:Fuzzy
12630:Empty
12613:types
12564:tuple
12534:Class
12528:large
12489:Union
12406:Union
12195:S2CID
12179:JSTOR
12095:S2CID
12079:JSTOR
11974:JSTOR
11945:S2CID
11937:JSTOR
11909:(PDF)
11893:S2CID
11851:(PDF)
11833:S2CID
11825:JSTOR
11738:S2CID
11718:(PDF)
11702:(PDF)
11666:S2CID
11658:JSTOR
11559:3 May
11395:JSTOR
11375:(PDF)
10864:Notes
10813:arXiv
10561:is a
10389:into
10329:into
10253:into
9508:with
8247:. If
8165:is a
7636:) as
6893:with
6445:into
6416:from
6363:into
6042:topos
6023:sets.
5963:Frege
5909:is a
5642:is a
4709:as a
163:equal
14452:Type
14255:list
14059:list
14036:list
14025:Term
13959:rank
13853:open
13747:list
13559:Maps
13464:sets
13323:Free
13293:list
13043:list
12970:list
12650:base
12150:PMID
12048:ISBN
12006:ISBN
11855:ISBN
11755:ISBN
11690:2024
11561:2024
11535:2024
11461:2024
10826:Lean
10807:The
10731:sets
10671:Endo
10663:Endo
10655:Endo
10651:Endo
10550:The
9166:<
9114:rank
8967:>
8945:>
8916:<
8872:<
8861:iff
8837:<
8795:<
8617:<
8341:four
8299:and
8095:<
7579:The
7260:and
7167:<
7057:<
6986:<
6832:<
6728:<
6568:and
5981:and
5947:and
5877:The
4824:and
4743:and
4698:and
4686:and
4581:and
4244:sets
3870:each
3781:<
3730:and
3632:free
3001:and
2735:and
2596:and
2163:and
2051:and
1923:and
1732:and
1621:and
847:and
450:and
410:).
402:) =
340:) =
64:The
14139:of
14121:of
14069:of
13601:Sur
13575:Map
13382:Ur-
13364:Set
12611:Set
12214:by
12171:doi
12140:PMC
12130:doi
12071:doi
11966:doi
11929:doi
11885:doi
11817:doi
11798:189
11730:doi
11650:doi
11387:doi
10737:of
10673:( {
10665:( {
10187:ZFC
10119:If
9793:in
9531:in
8766:all
8668:or
8632:is
8022:two
7908:all
7640:of
6127:of
6019:of
5973:of
5926:x=x
5920:= {
5872:):
5866:ZFC
5717:):
5608:is
4382:set
3938:NFU
3634:in
3211:TST
1244:dom
893:or
374:of
312:of
165:to
161:is
50:of
19:In
14684::
14525:NP
14149::
14143::
14073::
13750:),
13605:Bi
13597:In
12224::
12193:,
12187:MR
12185:,
12177:,
12167:15
12165:,
12148:.
12138:.
12128:.
12118:39
12116:.
12112:.
12093:,
12087:MR
12085:,
12077:,
12065:,
12016:MR
12014:,
11990:MR
11972:,
11962:44
11960:,
11943:,
11935:,
11925:19
11923:,
11891:.
11881:88
11879:.
11865:MR
11863:,
11831:.
11823:.
11811:.
11796:.
11792:.
11779:.
11765:MR
11763:,
11736:.
11724:.
11720:.
11704:.
11681:.
11664:.
11656:.
11646:47
11644:.
11552:.
11526:.
11452:.
11393:.
11383:66
11381:.
11377:.
11350:^
11335:^
11306:^
11183:^
11144:^
11019:^
10950:,
10901:^
10872:^
10804:.
10177:.
10173:+
9181:.
9069:.
8810:.
8370:,
8363:.
7571:.
7290:.
7217:;
6409:.
6044:.
5924:|
5860:+
5848:.
5832:+
5828:+
5812:+
5169:.
4628::=
4570:.
4547:NF
3123:TL
2459:,
1943:,
1883:,
1821:,
729:,
490:,
176::
139:,
56:.
35:,
29:NF
23:,
14605:/
14520:P
14275:)
14061:)
14057:(
13954:∀
13949:!
13944:∃
13905:=
13900:↔
13895:→
13890:∧
13885:∨
13880:¬
13603:/
13599:/
13573:/
13384:)
13380:(
13267:∞
13257:3
13045:)
12943:e
12936:t
12929:v
12694:·
12678:)
12674:(
12641:)
12530:)
12283:e
12276:t
12269:v
12173::
12156:.
12132::
12124::
12073::
12067:7
12056:.
12036:.
11968::
11931::
11911:.
11899:.
11887::
11839:.
11819::
11813:9
11783:.
11744:.
11732::
11726:1
11708:.
11692:.
11672:.
11652::
11588:V
11563:.
11537:.
11512:.
11500:.
11488:.
11476:.
11463:.
11426:.
11414:.
11401:.
11389::
11360:.
11330:.
11318:.
11301:.
10913:.
10884:.
10821:λ
10817:λ
10778:3
10687:x
10683:x
10681:∈
10679:y
10675:y
10667:x
10647:x
10645:(
10643:j
10639:x
10635:x
10619:)
10613:(
10610:j
10606:V
10595:j
10588:T
10584:W
10582:(
10580:j
10576:W
10559:W
10555:j
10545:j
10521:V
10494:T
10425:T
10402:1
10398:T
10375:0
10371:T
10348:1
10345:+
10342:i
10338:T
10315:i
10311:T
10290:)
10285:1
10282:+
10279:i
10275:T
10271:(
10266:1
10262:P
10241:)
10236:i
10232:T
10228:(
10225:P
10203:i
10199:T
10141:n
10102:1
10099:+
10096:)
10090:(
10087:j
10083:V
10061:j
10047:)
10044:}
10039:3
10022:V
10015:y
10012:{
10009:(
10006:j
9976:y
9960:1
9957:+
9950:V
9939:j
9925:}
9920:3
9903:V
9896:y
9893:{
9883:j
9879:y
9863:3
9836:N
9830:i
9826:j
9815:i
9791:y
9787:j
9771:2
9742:)
9739:)
9736:x
9733:(
9727:.
9724:)
9715:V
9711:(
9706:i
9700:N
9696:j
9689:x
9683:(
9663:)
9660:)
9657:)
9654:x
9651:(
9646:i
9640:N
9636:j
9632:(
9626:.
9617:V
9610:x
9604:(
9594:j
9580:i
9574:N
9564:i
9560:x
9544:1
9525:j
9517:j
9513:j
9490:1
9455:N
9419:.
9414:1
9411:+
9408:)
9402:(
9399:j
9395:V
9388:y
9382:y
9376:)
9373:x
9370:(
9367:j
9362:f
9359:e
9356:d
9348:y
9343:U
9340:F
9337:N
9329:x
9303:1
9300:+
9297:)
9291:(
9288:j
9284:V
9257:V
9234:1
9231:+
9224:V
9213:j
9193:V
9163:)
9157:(
9154:j
9124:V
9110:j
9036:V
9016:V
8986:)
8980:(
8975:4
8971:T
8964:)
8958:(
8953:2
8949:T
8922:}
8913:)
8907:(
8904:T
8895:{
8849:)
8843:(
8840:T
8834:)
8828:(
8825:T
8792:)
8786:(
8781:2
8777:T
8732:)
8726:(
8721:2
8717:T
8692:)
8686:(
8681:4
8677:T
8656:)
8650:(
8645:2
8641:T
8593:}
8590:y
8587:W
8584:x
8578:)
8575:}
8572:y
8569:{
8566:,
8563:}
8560:x
8557:{
8554:(
8551:{
8548:=
8539:W
8518:)
8512:(
8509:T
8483:W
8463:A
8443:)
8440:A
8437:(
8432:1
8428:P
8387:)
8381:(
8378:T
8307:y
8287:x
8267:)
8264:y
8261:,
8258:x
8255:(
8229:R
8208:}
8199:R
8192:S
8186:S
8183:{
8180:=
8153:)
8150:y
8147:,
8144:x
8141:(
8101:}
8092:y
8086:x
8080:)
8077:y
8074:,
8071:x
8068:(
8065:{
8062:=
8053:R
7982:R
7833:d
7830:r
7827:O
7799:d
7796:r
7793:O
7772:R
7752:S
7726:S
7723:,
7714:R
7663:d
7660:r
7657:O
7565:A
7543:A
7537:)
7534:}
7531:x
7528:{
7522:x
7519:(
7499:A
7470:|
7466:)
7463:A
7460:(
7455:1
7451:P
7446:|
7442:=
7438:|
7434:A
7430:|
7409:A
7389:V
7386:=
7383:A
7363:A
7342:|
7338:)
7335:A
7332:(
7327:1
7323:P
7318:|
7314:=
7310:|
7306:A
7302:|
7277:|
7273:V
7269:|
7247:|
7243:)
7240:V
7237:(
7234:P
7230:|
7204:|
7200:V
7196:|
7188:|
7184:)
7181:V
7178:(
7175:P
7171:|
7163:|
7159:)
7156:V
7153:(
7148:1
7144:P
7139:|
7114:}
7111:x
7108:{
7102:x
7078:|
7074:)
7071:V
7068:(
7065:P
7061:|
7053:|
7049:)
7046:V
7043:(
7038:1
7034:P
7029:|
7007:|
7003:)
7000:A
6997:(
6994:P
6990:|
6982:|
6978:)
6975:A
6972:(
6967:1
6963:P
6958:|
6937:A
6917:)
6914:A
6911:(
6906:1
6902:P
6881:A
6853:|
6849:)
6846:A
6843:(
6840:P
6836:|
6828:|
6824:A
6820:|
6799:A
6779:)
6776:A
6773:(
6770:P
6749:|
6745:)
6742:A
6739:(
6736:P
6732:|
6724:|
6720:A
6716:|
6692:B
6672:x
6666:x
6646:V
6640:)
6637:V
6634:(
6631:P
6628::
6625:f
6605:B
6585:)
6582:x
6579:(
6576:f
6556:x
6536:}
6533:)
6530:x
6527:(
6524:f
6518:x
6512:A
6506:x
6503:{
6500:=
6497:B
6473:V
6453:V
6433:)
6430:V
6427:(
6424:P
6397:V
6394:=
6391:A
6371:A
6351:)
6348:A
6345:(
6342:P
6318:A
6298:A
6278:)
6275:A
6272:(
6269:P
6242:V
6196:}
6193:x
6187:x
6181:x
6178:{
6158:x
6152:x
6111:x
6105:x
6085:}
6082:x
6076:x
6070:x
6067:{
6003:B
5997:A
5983:B
5979:A
5955:n
5922:x
5918:V
5897:x
5894:=
5891:x
5881:V
5846:κ
5842:κ
5792:}
5789:0
5786:{
5780:V
5760:V
5737:V
5693:|
5689:V
5685:|
5663:|
5659:V
5655:|
5629:|
5625:V
5621:|
5589:,
5586:}
5583:}
5575:{
5572:{
5569:,
5566:}
5560:{
5557:,
5528:.
5524:N
5470:=
5467:)
5464:n
5461:(
5458:S
5455:=
5452:1
5449:+
5446:n
5422:}
5419:V
5416:{
5413:=
5410:n
5389:N
5382:n
5379:=
5375:|
5371:V
5367:|
5345:|
5341:V
5337:|
5316:V
5293:)
5290:n
5287:(
5284:P
5264:}
5261:)
5258:n
5255:(
5252:P
5245:N
5238:n
5235:{
5215:)
5212:n
5209:(
5206:P
5181:N
5153:V
5133:.
5130:}
5127:a
5121:x
5115:A
5109:a
5103:}
5100:x
5097:{
5091:a
5088:{
5085:=
5082:)
5079:A
5076:(
5073:S
5053:}
5047:{
5037:n
5033:n
4999:}
4996:V
4990:b
4987:,
4984:a
4978:)
4975:a
4972:,
4969:)
4966:b
4963:,
4960:a
4957:(
4954:(
4951:{
4948:=
4943:1
4898:}
4889:x
4886:{
4866:b
4863:=
4860:)
4857:)
4854:b
4851:,
4848:a
4845:(
4842:(
4837:2
4812:a
4809:=
4806:)
4803:)
4800:b
4797:,
4794:a
4791:(
4788:(
4783:1
4756:2
4729:1
4700:b
4696:a
4688:b
4684:a
4670:}
4667:}
4664:b
4658:,
4655:a
4652:{
4646:,
4643:}
4640:a
4637:{
4634:{
4622:K
4618:)
4614:b
4608:,
4605:a
4602:(
4553:4
4549:3
4532:.
4529:)
4526:)
4523:x
4520:(
4511:A
4505:x
4502:.
4499:x
4493:(
4487:)
4484:A
4481:(
4477:t
4474:e
4471:s
4467:.
4464:A
4441:)
4438:x
4435:(
4412:}
4409:)
4406:x
4403:(
4394:x
4391:{
4366:.
4363:z
4360:=
4357:y
4351:)
4348:)
4345:z
4339:x
4333:y
4327:x
4324:.
4321:x
4315:(
4309:)
4306:z
4303:(
4299:t
4296:e
4293:s
4286:)
4283:y
4280:(
4276:t
4273:e
4270:s
4266:(
4263:.
4260:z
4257:y
4228:.
4225:)
4222:y
4219:(
4215:t
4212:e
4209:s
4202:y
4196:x
4193:.
4190:y
4187:x
4160:)
4157:x
4154:(
4150:t
4147:e
4144:s
4120:)
4117:x
4114:(
4091:}
4088:)
4085:x
4082:(
4073:x
4070:{
4047:)
4044:)
4041:)
4038:y
4032:z
4026:x
4020:z
4017:.
4014:z
4008:(
4002:y
3999:=
3996:x
3993:(
3987:)
3984:x
3978:w
3975:(
3972:.
3969:w
3966:y
3963:x
3936:(
3910:i
3890:1
3887:+
3884:i
3853:s
3833:)
3830:i
3827:(
3824:s
3804:i
3784:n
3778:m
3756:n
3752:y
3743:m
3739:x
3716:n
3712:y
3708:=
3703:n
3699:x
3658:)
3653:n
3649:x
3645:(
3615:1
3612:+
3609:n
3605:}
3601:)
3596:n
3592:x
3588:(
3577:n
3573:x
3569:{
3546:1
3543:+
3540:n
3536:A
3515:]
3512:)
3507:n
3503:x
3499:(
3488:1
3485:+
3482:n
3478:A
3469:n
3465:x
3461:[
3456:n
3452:x
3443:1
3440:+
3437:n
3433:A
3408:)
3403:n
3399:x
3395:(
3369:1
3366:+
3363:n
3359:}
3355:)
3350:n
3346:x
3342:(
3331:n
3327:x
3323:{
3303:)
3298:n
3294:x
3290:(
3277:n
3273:n
3269:n
3265:n
3261:n
3254:n
3238:n
3234:x
3209:(
3184:}
3181:S
3175:)
3172:}
3169:z
3166:{
3163:,
3160:w
3157:(
3154::
3151:w
3145::
3142:z
3139:{
3136:=
3133:)
3130:S
3127:(
3102:S
3079:}
3076:R
3070:)
3067:w
3064:,
3061:z
3058:(
3055::
3052:)
3049:t
3046:,
3043:w
3040:,
3037:z
3034:(
3031:{
3028:=
3025:)
3022:R
3019:(
3014:3
3010:I
2989:}
2986:R
2980:)
2977:t
2974:,
2971:z
2968:(
2965::
2962:)
2959:t
2956:,
2953:w
2950:,
2947:z
2944:(
2941:{
2938:=
2935:)
2932:R
2929:(
2924:2
2920:I
2899:R
2876:}
2873:)
2870:y
2867:=
2864:w
2858:x
2852:w
2849::
2846:w
2840:(
2837::
2834:y
2827:|
2823:x
2820:{
2800:1
2789:.
2775:c
2771:y
2766:|
2760:c
2756:x
2752:=
2749:y
2743:x
2723:x
2719:|
2715:x
2712:=
2707:c
2703:x
2682:}
2679:)
2676:y
2670:z
2664:x
2658:z
2655:(
2649::
2646:z
2643:{
2640:=
2637:y
2633:|
2629:x
2604:S
2584:R
2564:}
2561:y
2558:S
2555:z
2547:z
2544:R
2541:x
2538:,
2535:z
2526:|
2522:)
2519:y
2516:,
2513:x
2510:(
2507:{
2504:=
2501:)
2498:S
2494:|
2490:R
2487:(
2467:S
2447:R
2424:A
2404:}
2401:A
2395:B
2387:B
2381:x
2378:,
2375:B
2366:|
2362:x
2359:{
2356:=
2353:]
2350:A
2347:[
2324:A
2301:}
2298:V
2292:x
2288:|
2284:)
2281:x
2278:,
2275:x
2272:(
2269:{
2266:=
2263:]
2260:=
2257:[
2234:}
2231:V
2225:y
2222:,
2219:x
2215:|
2211:)
2208:y
2205:,
2202:)
2199:y
2196:,
2193:x
2190:(
2187:(
2184:{
2181:=
2176:2
2151:}
2148:V
2142:y
2139:,
2136:x
2132:|
2128:)
2125:x
2122:,
2119:)
2116:y
2113:,
2110:x
2107:(
2104:(
2101:{
2098:=
2093:1
2065:d
2062:=
2059:b
2039:c
2036:=
2033:a
2013:)
2010:d
2007:,
2004:c
2001:(
1998:=
1995:)
1992:b
1989:,
1986:a
1983:(
1963:)
1960:b
1957:,
1954:a
1951:(
1931:b
1911:a
1891:b
1871:a
1860:.
1848:V
1845:=
1840:c
1836:x
1829:x
1809:x
1789:}
1786:x
1783:=
1780:x
1776:|
1772:x
1769:{
1766:=
1763:V
1740:B
1720:A
1700:}
1692:B
1686:x
1678:A
1672:x
1668:|
1664:x
1661:{
1658:=
1655:B
1649:A
1629:B
1609:A
1586:A
1566:}
1563:A
1557:x
1553:|
1549:x
1546:{
1543:=
1538:c
1534:A
1513:A
1500:.
1488:}
1485:y
1479:x
1475:|
1471:)
1468:y
1465:,
1462:}
1459:x
1456:{
1453:(
1450:{
1447:=
1444:)
1441:V
1435:1
1432:(
1426:]
1420:[
1417:=
1414:]
1408:[
1388:}
1385:y
1379:x
1375:|
1371:)
1368:y
1365:,
1362:x
1359:(
1356:{
1353:=
1350:]
1344:[
1321:R
1301:}
1298:R
1292:)
1289:y
1286:,
1283:x
1280:(
1277:.
1274:y
1267:|
1263:x
1260:{
1257:=
1254:)
1251:R
1248:(
1223:R
1200:R
1180:}
1177:R
1171:)
1168:y
1165:,
1162:x
1159:(
1155:|
1151:)
1148:}
1145:y
1142:{
1139:,
1136:}
1133:x
1130:{
1127:(
1124:{
1121:=
1115:R
1095:R
1084:.
1072:x
1069:R
1066:y
1046:y
1041:1
1034:R
1030:x
1010:}
1007:R
1001:)
998:x
995:,
992:y
989:(
985:|
981:)
978:y
975:,
972:x
969:(
966:{
963:=
958:1
951:R
930:R
919:.
907:B
901:V
881:V
875:A
855:B
835:A
815:}
812:B
806:b
798:A
792:a
788:|
784:)
781:b
778:,
775:a
772:(
769:{
766:=
763:B
757:A
737:B
717:A
706:.
694:x
674:}
671:x
668:=
665:y
661:|
657:y
654:{
651:=
648:}
645:x
642:{
639:=
636:)
633:x
630:(
607:x
584:B
581:=
578:A
558:B
538:x
518:A
498:x
478:x
458:B
438:A
408:y
406:(
404:f
400:x
398:(
396:f
362:y
359:=
356:x
346:x
344:(
342:f
338:y
336:(
334:f
300:y
294:x
264:f
231:.
196:}
187:x
184:{
169:.
167:B
159:A
155:B
151:X
145:A
141:X
137:X
133:B
129:A
100:(
84:=
76:(
27:(
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.