6398:
4050:
2472:
The axioms and definitions in this section are, but for a few inessential details, taken from the
Appendix to Kelley (1955). The explanatory remarks below are not his. The Appendix states 181 theorems and definitions, and warrants careful reading as an abbreviated exposition of axiomatic set theory
2297:(representing second-order objects in set rather than predicate language) as its background logic. The language of second-order ZFC is similar to that of MK (although a set and a class having the same extension can no longer be identified), and their
2146:) may range over all sets.) The NBG axiom schema of Class Comprehension can be replaced with finitely many of its instances; this is not possible in MK. MK is consistent relative to ZFC augmented by an axiom asserting the existence of strongly
1474:
512:
140:
of ZFC. Unlike von
Neumann–Bernays–Gödel set theory, where the axiom schema of Class Comprehension can be replaced with finitely many of its instances, Morse–Kelley set theory cannot be finitely axiomatized.
910:
1820:
1640:
2837:' by the formula obtained from Æ by replacing each occurrence of the variable that replaced α by the variable that replaced β provided that the variable that replaced β does not appear bound in
346:
2138:) may contain quantified variables ranging over classes. The quantified variables in NBG's axiom schema of Class Comprehension are restricted to sets; hence Class Comprehension in NBG must be
1116:
406:
2781:
2305:
of second-order ZFC are quite different from those of MK. For example, if MK is consistent then it has a countable first-order model, while second-order ZFC has no countable models.
3346:
723:
3668:
1208:
1155:
3303:
280:
3764:. However, the summary of ML given in Mendelson (1997), p. 296, is easier to follow. Mendelson's axiom schema ML2 is identical to the above axiom schema of Class Comprehension.
3406:
3444:
2039:
3510:
2554:
3529:
2901:
1884:
305:
136:(ZFC, the canonical set theory) in the sense that a statement in the language of ZFC is provable in NBG if and only if it is provable in ZFC, Morse–Kelley set theory is a
1678:
1254:
636:
3615:
3226:
965:
2249:
2222:
759:
431:
3473:
3118:
3029:
2930:
2691:
2269:
2801:
2743:
2662:
2614:
3070:
235:
191:, appearing in Extensionality, Class Comprehension, and Foundation, denote variables ranging over classes. A lower case letter denotes a variable that cannot be a
2824:
4777:
2473:
by a working mathematician of the first rank. Kelley introduced his axioms gradually, as needed to develop the topics listed after each instance of
5452:
4514:
3836:
3188:
2378:
2161:. Limitation of Size does not appear in Rubin (1967), Monk (1980), or Mendelson (1997). Instead, these authors invoke a usual form of the local
2116:
2091:
2085:
2079:
671:
180:
149:
67:
517:
A set and a class having the same extension are identical. Hence MK is not a two-sorted theory, appearances to the contrary notwithstanding.
5535:
4676:
2301:
resources for practical proof are almost identical (and are identical if MK includes the strong form of
Limitation of Size). But the
2052:
in Power Set and Union are universally, not existentially, quantified, as Class
Comprehension suffices to establish the existence of
3535:. Up to this point, everything that has been proved to exist is a class, and Kelley's discussion of sets was entirely hypothetical.
2130:. In fact, NBG—and hence ZFC—can be proved consistent in MK. MK's strength stems from its axiom schema of Class Comprehension being
5849:
2194:. Such an axiom could be added, of course, and minor perturbations of the above axioms would necessitate this addition. The set
2111:. These authors and Mendelson (1997: 287) submit that MK does what is expected of a set theory while being less cumbersome than
2282:. It cannot be a set (under pain of paradox); hence that class is a proper class, and all proper classes have the same size as
771:
6007:
1702:
1522:
4795:
5862:
5185:
4203:
4016:
79:
2426:
is equivalent to Kelley's, but formulated in an idiosyncratic formal language rather than, as is done here, in standard
310:
5867:
5857:
5594:
5447:
4800:
4531:
4791:
6003:
3828:
664:) may contain parameters that are either sets or proper classes. More consequentially, the quantified variables in φ(
5345:
6100:
5844:
4669:
5405:
5098:
4509:
4103:
3695:
2446:
2364:
2322:
2112:
2075:
133:
4839:
4389:
6422:
6361:
6063:
5826:
5821:
5646:
5067:
4751:
981:
206:
157:
2173:
is also a set. Replacement can prove everything that
Limitation of Size proves, except prove some form of the
361:
6356:
6139:
6056:
5769:
5700:
5577:
4819:
4283:
4162:
2748:
6281:
6107:
5793:
5427:
5026:
4526:
3316:
2318:
195:, because it appears to the left of an ∈. As MK is a one-sorted theory, this notational convention is only
2480:
Notations appearing below and now well-known are not defined. Peculiarities of Kelley's notation include:
681:
183:, inessential details aside. The symbolic versions of the axioms employ the following notational devices:
6159:
6154:
5764:
5503:
4761:
4662:
4157:
4120:
3638:
3184:
2180:
2154:
1480:
1222:
1160:
1128:
3975:(1955) by John L. Kelley in various formats. The appendix contains Kelley's axiomatic development of MK.
3282:
244:
6088:
5678:
5072:
5040:
4731:
3385:
20:
4174:
3705:
If the scope of all quantified variables in the above axioms is restricted to sets, all axioms except
3411:
6378:
6327:
6224:
5722:
5683:
5160:
4805:
4208:
4093:
4081:
4076:
2190:(hence the universe is nonempty) renders provable the sethood of the empty set; hence no need for an
4834:
1892:
6219:
6149:
5688:
5540:
5523:
5246:
4726:
4009:
3492:
2512:
1469:{\displaystyle {\begin{array}{l}\forall C\land \\\qquad \forall x\forall y\forall s)].\end{array}}}
3514:
2880:
1854:
290:
6051:
6028:
5989:
5875:
5816:
5462:
5382:
5226:
5170:
4783:
4628:
4546:
4421:
4373:
4187:
4110:
2984:
2704:
1654:
507:{\displaystyle \forall X\,\forall Y\,(\forall z\,(z\in X\leftrightarrow z\in Y)\rightarrow X=Y).}
420:
3989:
2381:, which excludes global choice, replacing limitation of size by replacement and ordinary choice;
540:
6341:
6068:
6046:
6013:
5906:
5752:
5737:
5710:
5661:
5545:
5480:
5305:
5271:
5266:
5140:
4971:
4948:
4580:
4461:
4273:
4086:
3677:
3585:
3208:
3139:
2350:
2158:
2142:. (Separation with respect to sets is still impredicative in NBG, because the quantifiers in φ(
2123:
1211:
932:
355:
129:
2231:
2204:
735:
6271:
6124:
5916:
5634:
5370:
5276:
5135:
5120:
5001:
4976:
4496:
4466:
4410:
4330:
4310:
4288:
3691:
3449:
3369:
3143:
3091:
3008:
2906:
2667:
2326:
2254:
2147:
1215:
82:
to range over sets alone, Morse–Kelley set theory allows these bound variables to range over
2786:
2728:
2641:
2593:
6244:
6206:
6083:
5887:
5727:
5651:
5629:
5457:
5415:
5314:
5281:
5145:
4933:
4844:
4570:
4560:
4394:
4325:
4278:
4218:
4098:
3984:
3938:
3155:
3147:
3049:
2506:
2166:
1487:. The next section explains how Limitation of Size is stronger than the usual forms of the
1236:
412:
211:
63:
3970:
179:
With the exception of Class
Comprehension, the following axioms are the same as those for
8:
6373:
6264:
6249:
6229:
6186:
6073:
6023:
5949:
5894:
5831:
5624:
5619:
5567:
5335:
5324:
4996:
4896:
4824:
4815:
4811:
4746:
4741:
4565:
4476:
4384:
4379:
4193:
4135:
4066:
4002:
3904:
3151:
2988:
2458:
2275:
2170:
521:
2806:
6402:
6171:
6134:
6119:
6112:
6095:
5899:
5881:
5747:
5673:
5656:
5609:
5422:
5331:
5165:
5150:
5110:
5062:
5047:
5035:
4991:
4966:
4736:
4685:
4488:
4483:
4268:
4223:
4130:
3947:
3926:
3861:
3258:
2294:
2191:
2088:(and ZFC, if quantified variables were restricted to sets): Extensionality, Foundation;
1685:
1495:
1241:
5355:
6397:
6337:
6144:
5954:
5944:
5836:
5717:
5552:
5528:
5309:
5293:
5198:
5175:
5052:
5021:
4986:
4881:
4716:
4345:
4182:
4145:
4115:
4039:
3952:
3857:
3824:
3816:
3254:
2427:
2184:
1826:
165:
60:
6351:
6346:
6239:
6196:
6018:
5979:
5974:
5959:
5785:
5742:
5639:
5437:
5387:
4961:
4923:
4633:
4623:
4608:
4603:
4471:
4125:
3942:
3916:
3876:
2422:, using the axioms given in the next section. The system of Anthony Morse's (1965)
916:
137:
6332:
6322:
6276:
6259:
6214:
6176:
6078:
5998:
5805:
5732:
5705:
5693:
5599:
5513:
5487:
5442:
5410:
5211:
5013:
4956:
4906:
4871:
4829:
4502:
4440:
4258:
4071:
3934:
3699:
3558:
2848:
2442:
2438:
2174:
2162:
2139:
2131:
1488:
203:
173:
91:
6317:
6296:
6254:
6234:
6129:
5984:
5582:
5572:
5562:
5557:
5491:
5365:
5241:
5130:
5125:
5103:
4704:
4638:
4435:
4416:
4320:
4305:
4262:
4198:
4140:
3805:
3785:
3758:
3542:
3365:
1646:
118:
98:
71:
6416:
6291:
5969:
5476:
5261:
5251:
5221:
5206:
4876:
4643:
4445:
4359:
4354:
3889:
2450:
2431:
2199:
653:
531:
102:
4613:
3896:. San Francisco: Holden Day. More thorough than Monk; the ontology includes
3881:
6191:
6038:
5939:
5931:
5811:
5759:
5668:
5604:
5587:
5518:
5377:
5236:
4938:
4721:
4593:
4588:
4406:
4335:
4293:
4152:
4049:
3956:
3726:
3550:
3482:
3270:
3135:
2583:
2415:
2127:
2103:
Monk (1980) and Rubin (1967) are set theory texts built around MK; Rubin's
1231:
1122:
192:
169:
161:
87:
83:
75:
3921:
6301:
6181:
5360:
5350:
5297:
4981:
4901:
4886:
4766:
4711:
4618:
4253:
3795:
3792:. Springer. Earlier ed., Van Nostrand. Appendix, "Elementary Set Theory."
3562:
2435:
1259:
117:. Kelley said the system in his book was a variant of the systems due to
2488:
distinguish variables ranging over classes from those ranging over sets;
5231:
5086:
5057:
4863:
4598:
4369:
4025:
3262:
2279:
6383:
6286:
5339:
5256:
5216:
5180:
5116:
4928:
4918:
4891:
4654:
4401:
4364:
4315:
4213:
3930:
3897:
3266:
2852:
2454:
2391:
2302:
2108:
1836:
285:
6368:
6166:
5614:
5319:
4913:
2104:
1210:. With ordered pairs in hand, Class Comprehension enables defining
196:
153:
114:
1218:
on sets as sets of ordered pairs, making possible the next axiom:
5964:
4756:
3554:
3477:
This axiom, or equivalents thereto, are included in ZFC and NBG.
3907:(1949), "On Zermelo's and von Neumann's axioms for set theory",
2071:
The above axioms are shared with other set theories as follows:
70:(NBG). While von Neumann–Bernays–Gödel set theory restricts the
4426:
4248:
2342:
2298:
1505:
5508:
4854:
4699:
4298:
4058:
3994:
3862:"Some impredicative definitions in the axiomatic set theory"
3835:
The definitive treatment of the closely related set theory
2464:
2313:
ZFC, NBG, and MK each have models describable in terms of
1121:
Pairing licenses the unordered pair in terms of which the
121:
and Morse. Morse's own version appeared later in his book
3192:
2708:
668:) may range over all classes and not just over all sets;
3980:
From
Foundations of Mathematics (FOM) discussion group:
905:{\displaystyle \forall W_{1}...W_{n}\exists Y\forall x.}
2165:, and an "axiom of replacement," asserting that if the
1815:{\displaystyle \forall a\,\forall s\,)\rightarrow Ms].}
1635:{\displaystyle \forall a\,\forall p\,)\rightarrow Mp].}
164:. Classes that are members of other classes are called
3839:, followed by a page on MK. Harder than Monk or Rubin.
3076:
is a set because it is a subclass of the power set of
2502:; this peculiarity has been carefully respected below;
97:
Morse–Kelley set theory is named after mathematicians
3641:
3588:
3517:
3495:
3481:
asserts the unconditional existence of two sets, the
3452:
3414:
3388:
3319:
3285:
3211:
3094:
3052:
3011:
2909:
2883:
2809:
2789:
2751:
2731:
2670:
2644:
2596:
2515:
2271:
would follow from either form of
Limitation of Size.
2257:
2234:
2207:
1895:
1857:
1705:
1657:
1525:
1257:
1163:
1131:
984:
935:
774:
738:
684:
543:
434:
364:
313:
293:
247:
214:
425:
Classes having the same members are the same class.
2293:MK can be confused with second-order ZFC, ZFC with
2060:. Power Set and Union only serve to establish that
358:having all possible sets as members, is defined by
3815:
3717:is provable in ZFC. Hence the Kelley treatment of
3662:
3609:
3523:
3504:
3467:
3438:
3400:
3340:
3297:
3220:
3112:
3064:
3023:
2924:
2895:
2818:
2795:
2775:
2737:
2685:
2656:
2608:
2548:
2263:
2243:
2216:
2033:
1878:
1814:
1672:
1634:
1468:
1202:
1149:
1110:
959:
904:
753:
717:
630:
506:
400:
341:{\displaystyle \forall x(x\not \in \varnothing ).}
340:
299:
274:
229:
6414:
3729:as well as sets, and the Classification schema.
648:) be any formula in the language of MK in which
128:While von Neumann–Bernays–Gödel set theory is a
3846:. Krieger. Easier and less thorough than Rubin.
1479:The formal version of this axiom resembles the
109:and later in an appendix to Kelley's textbook
4670:
4010:
3744:See, e.g., Mendelson (1997), p. 239, axiom R.
3721:makes very clear that all that distinguishes
2942:above. Sketch of the proof of Power Set from
3694:of the axiom of choice. As is the case with
3654:
3648:
3427:
3421:
3107:
3095:
3059:
3053:
2770:
2758:
2540:
2519:
2498:denote the domain and range of the function
1870:
1864:
1426:
1414:
1402:
1390:
1343:
1331:
1197:
1194:
1182:
1176:
1170:
1167:
1144:
1132:
954:
942:
712:
691:
3042:above. Sketch of the proof of Pairing from
4862:
4677:
4663:
4017:
4003:
3531:is a set simply because it is a member of
2126:NBG, the other well-known set theory with
1504:be a class whose members are all possible
74:in the schematic formula appearing in the
3946:
3920:
3880:
3856:
2829:'α' and 'β' are replaced by variables, '
2715:includes proper classes as well as sets.
2453:class comprehension was also proposed in
2122:MK is strictly stronger than ZFC and its
1763:
1741:
1719:
1712:
1583:
1561:
1539:
1532:
1111:{\displaystyle \forall x\,\forall y\,)].}
1083:
1079:
1051:
1032:
998:
991:
458:
448:
441:
144:
113:(1955), a graduate level introduction to
2505:His primitive logical language includes
401:{\displaystyle \forall x(Mx\to x\in V).}
3985:Allen Hazen on set theory with classes.
2776:{\displaystyle \beta \in \{\alpha :A\}}
2377:) is a model of Mendelson's version of
86:as well as sets, as first suggested by
6415:
4684:
2082:: Pairing, Power Set, Union, Infinity;
1157:, may be defined in the usual way, as
4658:
3998:
3341:{\displaystyle x\cap y=\varnothing .}
670:this is the only way MK differs from
237:whose intended reading is "the class
3990:Joseph Shoenfield's doubts about MK.
3903:
3800:Introduction to Axiomatic Set Theory
3725:from ZFC are variables ranging over
2411:
718:{\displaystyle Y=\{x\mid \phi (x)\}}
106:
68:von Neumann–Bernays–Gödel set theory
3663:{\displaystyle V-\{\varnothing \}.}
2430:. The first set theory to include
1203:{\displaystyle \ \{\{x\},\{x,y\}\}}
1150:{\displaystyle \langle x,y\rangle }
13:
3821:Introduction to Mathematical Logic
3298:{\displaystyle x\neq \varnothing }
2414:and popularized in an appendix to
2169:of a class function is a set, its
1968:
1947:
1926:
1896:
1757:
1735:
1713:
1706:
1577:
1555:
1533:
1526:
1483:, and embodies the class function
1378:
1372:
1366:
1310:
1292:
1283:
1271:
1262:
1045:
1026:
992:
985:
813:
807:
775:
586:
565:
544:
534:from at least one of its members.
452:
442:
435:
365:
314:
275:{\displaystyle \exists W(x\in W).}
248:
187:The upper case letters other than
14:
6434:
3964:
3651:
3401:{\displaystyle \varnothing \in y}
3332:
3292:
1914:
559:
329:
168:. A class that is not a set is a
16:System of mathematical set theory
6396:
4048:
3894:Set Theory for the Mathematician
3439:{\displaystyle x\cup \{x\}\in y}
3247:may be combined into one axiom.
725:whose members are exactly those
176:involve membership or equality.
3631:There exists a choice function
2308:
2251:In this case, the existence of
1365:
4024:
3767:
3747:
3738:
3702:requires some form of choice.
3598:
3592:
2953:that is a subclass of the set
2537:
2531:
2034:{\displaystyle \exists y)])].}
2025:
2022:
2019:
2016:
2013:
1989:
1986:
1974:
1953:
1944:
1932:
1902:
1831:There exists an inductive set
1806:
1797:
1794:
1791:
1788:
1764:
1754:
1742:
1723:
1720:
1626:
1617:
1614:
1611:
1608:
1596:
1584:
1574:
1562:
1543:
1540:
1456:
1453:
1450:
1438:
1435:
1387:
1384:
1355:
1352:
1316:
1307:
1298:
1289:
1280:
1268:
1102:
1099:
1096:
1093:
1067:
1064:
1052:
1033:
1023:
1020:
1002:
999:
896:
893:
881:
840:
834:
831:
819:
748:
742:
709:
703:
622:
619:
616:
604:
592:
571:
562:
550:
498:
486:
483:
471:
459:
449:
392:
380:
371:
332:
320:
266:
254:
1:
6357:History of mathematical logic
3909:Proc. Natl. Acad. Sci. U.S.A.
3802:. Routledge & Kegan Paul.
3779:
3505:{\displaystyle \varnothing .}
2869:is a set, there exists a set
2549:{\displaystyle \ \{x:A(x)\},}
2098:
761:comes out true. Formally, if
6282:Primitive recursive function
3773:Kelley (1955), p. 261, fn †.
3524:{\displaystyle \varnothing }
2896:{\displaystyle z\subseteq x}
2719:II. Classification (schema):
2319:von Neumann universe of sets
1879:{\displaystyle x\cup \{x\}.}
1680:be the sum class of the set
300:{\displaystyle \varnothing }
7:
3185:axiom schema of replacement
2983:is not a set. Existence of
2855:and of the universal class
2711:, except that the scope of
2228:could be a set larger than
2198:is not identified with the
2155:axiom of limitation of size
1673:{\displaystyle s=\bigcup a}
1481:axiom schema of replacement
134:Zermelo–Fraenkel set theory
66:that is closely related to
10:
6439:
5346:Schröder–Bernstein theorem
5073:Monadic predicate calculus
4732:Foundations of mathematics
4515:von Neumann–Bernays–Gödel
3844:Introduction to Set Theory
3812:. Oxford: Basil Blackwell.
3757:for ML is the 1951 ed. of
2703:would be identical to the
2405:
2153:The only advantage of the
2068:cannot be proper classes.
967:whose members are exactly
631:{\displaystyle \forall A.}
21:foundations of mathematics
6392:
6379:Philosophy of mathematics
6328:Automated theorem proving
6310:
6205:
6037:
5930:
5782:
5499:
5475:
5453:Von Neumann–Bernays–Gödel
5398:
5292:
5196:
5094:
5085:
5012:
4947:
4853:
4775:
4692:
4579:
4542:
4454:
4344:
4316:One-to-one correspondence
4232:
4173:
4057:
4046:
4032:
3698:, the development of the
3610:{\displaystyle c(x)\in x}
3221:{\displaystyle \bigcup x}
2290:too can be well-ordered.
960:{\displaystyle z=\{x,y\}}
105:and was first set out by
57:system of Quine and Morse
3732:
3080:(by two applications of
2833:' by a formula Æ, and '
2634:if and only if for each
2434:class comprehension was
2410:MK was first set out in
2244:{\displaystyle \omega .}
2217:{\displaystyle \omega ,}
754:{\displaystyle \phi (x)}
6029:Self-verifying theories
5850:Tarski's axiomatization
4801:Tarski's undefinability
4796:incompleteness theorems
3882:10.4064/fm-37-1-111-124
3869:Fundamenta Mathematicae
3842:Monk, J. Donald (1980)
3676:is very similar to the
3468:{\displaystyle x\in y.}
3113:{\displaystyle \{x,y\}}
3024:{\displaystyle x\cup y}
2961:is a member of the set
2925:{\displaystyle z\in y.}
2721:An axiom results if in
2705:axiom of extensionality
2686:{\displaystyle z\in y.}
2556:"the class of all sets
2465:The axioms in Kelley's
2264:{\displaystyle \omega }
2157:is that it implies the
1835:, meaning that (i) the
241:is a set", abbreviates
90:in 1940 for his system
41:Morse–Tarski set theory
33:Kelley–Morse set theory
25:Morse–Kelley set theory
6403:Mathematics portal
6014:Proof of impossibility
5662:propositional variable
4972:Propositional calculus
4274:Constructible universe
4094:Constructibility (V=L)
3823:. Chapman & Hall.
3678:axiom of global choice
3664:
3611:
3525:
3506:
3469:
3440:
3402:
3342:
3299:
3222:
3114:
3066:
3025:
2926:
2897:
2820:
2797:
2796:{\displaystyle \beta }
2777:
2739:
2738:{\displaystyle \beta }
2687:
2658:
2657:{\displaystyle z\in x}
2610:
2609:{\displaystyle x\in y}
2550:
2351:constructible universe
2265:
2245:
2218:
2159:axiom of global choice
2148:inaccessible cardinals
2124:conservative extension
2035:
1880:
1816:
1674:
1636:
1470:
1204:
1151:
1112:
961:
906:
755:
719:
675:. Then there exists a
632:
508:
402:
342:
301:
276:
231:
152:and MK share a common
145:MK axioms and ontology
130:conservative extension
49:Quine–Morse set theory
6423:Systems of set theory
6272:Kolmogorov complexity
6225:Computably enumerable
6125:Model complete theory
5917:Principia Mathematica
4977:Propositional formula
4806:Banach–Tarski paradox
4497:Principia Mathematica
4331:Transfinite induction
4190:(i.e. set difference)
3922:10.1073/pnas.35.3.150
3849:Morse, A. P., (1965)
3665:
3612:
3526:
3507:
3470:
3441:
3403:
3370:transfinite induction
3343:
3300:
3223:
3115:
3067:
3065:{\displaystyle \{x\}}
3026:
2927:
2898:
2821:
2798:
2778:
2740:
2688:
2659:
2611:
2551:
2327:inaccessible cardinal
2266:
2246:
2219:
2094:: Limitation of Size.
2036:
1881:
1817:
1675:
1637:
1471:
1205:
1152:
1113:
962:
929:, there exists a set
907:
756:
720:
633:
509:
403:
343:
302:
277:
232:
230:{\displaystyle \ Mx,}
158:universe of discourse
6220:Church–Turing thesis
6207:Computability theory
5416:continuum hypothesis
4934:Square of opposition
4792:Gödel's completeness
4571:Burali-Forti paradox
4326:Set-builder notation
4279:Continuum hypothesis
4219:Symmetric difference
3639:
3586:
3515:
3493:
3450:
3412:
3386:
3317:
3283:
3209:
3156:function composition
3092:
3050:
3009:
3005:are both sets, then
2907:
2881:
2807:
2787:
2749:
2729:
2668:
2642:
2594:
2513:
2276:von Neumann ordinals
2255:
2232:
2205:
1893:
1855:
1703:
1655:
1523:
1255:
1161:
1129:
982:
933:
772:
736:
682:
642:Class Comprehension:
541:
526:Each nonempty class
432:
413:von Neumann universe
362:
311:
291:
245:
212:
64:axiomatic set theory
6374:Mathematical object
6265:P versus NP problem
6230:Computable function
6024:Reverse mathematics
5950:Logical consequence
5827:primitive recursive
5822:elementary function
5595:Free/bound variable
5448:Tarski–Grothendieck
4967:Logical connectives
4897:Logical equivalence
4747:Logical consequence
4532:Tarski–Grothendieck
3489:, and the null set
3378:There exists a set
3168:is a function and
2873:such that for each
2851:. Existence of the
2664:when and only when
2401:, is a model of MK.
80:Class Comprehension
6172:Transfer principle
6135:Semantics of logic
6120:Categorical theory
6096:Non-standard model
5610:Logical connective
4737:Information theory
4686:Mathematical logic
4121:Limitation of size
3858:Mostowski, Andrzej
3817:Mendelson, Elliott
3762:Mathematical Logic
3682:Limitation of Size
3660:
3607:
3582:is a function and
3521:
3502:
3465:
3436:
3398:
3338:
3305:there is a member
3295:
3218:
3110:
3062:
3021:
2922:
2893:
2819:{\displaystyle B,}
2816:
2793:
2773:
2735:
2683:
2654:
2606:
2546:
2295:second-order logic
2261:
2241:
2214:
2192:axiom of empty set
2181:Limitation of Size
2031:
1876:
1812:
1688:of all members of
1670:
1632:
1466:
1464:
1223:Limitation of Size
1200:
1147:
1108:
957:
902:
765:is not free in φ:
751:
715:
628:
504:
398:
338:
297:
272:
227:
6410:
6409:
6342:Abstract category
6145:Theories of truth
5955:Rule of inference
5945:Natural deduction
5926:
5925:
5471:
5470:
5176:Cartesian product
5081:
5080:
4987:Many-valued logic
4962:Boolean functions
4845:Russell's paradox
4820:diagonal argument
4717:First-order logic
4652:
4651:
4561:Russell's paradox
4510:Zermelo–Fraenkel
4411:Dedekind-infinite
4284:Diagonal argument
4183:Cartesian product
4040:Set (mathematics)
3853:. Academic Press.
3255:Cartesian product
3199:VI. Amalgamation:
2582:(and hence not a
2518:
2428:first-order logic
2329:κ be a member of
2134:, meaning that φ(
1242:mapped one-to-one
1166:
217:
6430:
6401:
6400:
6352:History of logic
6347:Category of sets
6240:Decision problem
6019:Ordinal analysis
5960:Sequent calculus
5858:Boolean algebras
5798:
5797:
5772:
5743:logical/constant
5497:
5496:
5483:
5406:Zermelo–Fraenkel
5157:Set operations:
5092:
5091:
5029:
4860:
4859:
4840:Löwenheim–Skolem
4727:Formal semantics
4679:
4672:
4665:
4656:
4655:
4634:Bertrand Russell
4624:John von Neumann
4609:Abraham Fraenkel
4604:Richard Dedekind
4566:Suslin's problem
4477:Cantor's theorem
4194:De Morgan's laws
4052:
4019:
4012:
4005:
3996:
3995:
3973:General Topology
3959:
3950:
3924:
3885:
3884:
3866:
3851:A Theory of Sets
3834:
3810:Parts of Classes
3790:General Topology
3774:
3771:
3765:
3751:
3745:
3742:
3713:are ZFC axioms.
3700:cardinal numbers
3669:
3667:
3666:
3661:
3635:whose domain is
3617:for each member
3616:
3614:
3613:
3608:
3559:rational numbers
3530:
3528:
3527:
3522:
3511:
3509:
3508:
3503:
3474:
3472:
3471:
3466:
3445:
3443:
3442:
3437:
3407:
3405:
3404:
3399:
3347:
3345:
3344:
3339:
3304:
3302:
3301:
3296:
3277:VII. Regularity:
3227:
3225:
3224:
3219:
3162:V. Substitution:
3134:: Unordered and
3119:
3117:
3116:
3111:
3071:
3069:
3068:
3063:
3046:: the singleton
3030:
3028:
3027:
3022:
2965:whose existence
2931:
2929:
2928:
2923:
2902:
2900:
2899:
2894:
2825:
2823:
2822:
2817:
2802:
2800:
2799:
2794:
2782:
2780:
2779:
2774:
2744:
2742:
2741:
2736:
2692:
2690:
2689:
2684:
2663:
2661:
2660:
2655:
2615:
2613:
2612:
2607:
2555:
2553:
2552:
2547:
2516:
2467:General Topology
2441:, that built on
2424:A Theory of Sets
2420:General Topology
2270:
2268:
2267:
2262:
2250:
2248:
2247:
2242:
2223:
2221:
2220:
2215:
2040:
2038:
2037:
2032:
1885:
1883:
1882:
1877:
1821:
1819:
1818:
1813:
1679:
1677:
1676:
1671:
1641:
1639:
1638:
1633:
1475:
1473:
1472:
1467:
1465:
1209:
1207:
1206:
1201:
1164:
1156:
1154:
1153:
1148:
1117:
1115:
1114:
1109:
966:
964:
963:
958:
911:
909:
908:
903:
880:
879:
858:
857:
806:
805:
787:
786:
760:
758:
757:
752:
724:
722:
721:
716:
637:
635:
634:
629:
513:
511:
510:
505:
407:
405:
404:
399:
347:
345:
344:
339:
306:
304:
303:
298:
281:
279:
278:
273:
236:
234:
233:
228:
215:
174:atomic sentences
172:. The primitive
138:proper extension
123:A Theory of Sets
111:General Topology
6438:
6437:
6433:
6432:
6431:
6429:
6428:
6427:
6413:
6412:
6411:
6406:
6395:
6388:
6333:Category theory
6323:Algebraic logic
6306:
6277:Lambda calculus
6215:Church encoding
6201:
6177:Truth predicate
6033:
5999:Complete theory
5922:
5791:
5787:
5783:
5778:
5770:
5490: and
5486:
5481:
5467:
5443:New Foundations
5411:axiom of choice
5394:
5356:Gödel numbering
5296: and
5288:
5192:
5077:
5027:
5008:
4957:Boolean algebra
4943:
4907:Equiconsistency
4872:Classical logic
4849:
4830:Halting problem
4818: and
4794: and
4782: and
4781:
4776:Theorems (
4771:
4688:
4683:
4653:
4648:
4575:
4554:
4538:
4503:New Foundations
4450:
4340:
4259:Cardinal number
4242:
4228:
4169:
4053:
4044:
4028:
4023:
3967:
3864:
3831:
3782:
3777:
3772:
3768:
3752:
3748:
3743:
3739:
3735:
3709:and the schema
3680:derivable from
3640:
3637:
3636:
3587:
3584:
3583:
3576:choice function
3543:Natural numbers
3516:
3513:
3512:
3494:
3491:
3490:
3451:
3448:
3447:
3413:
3410:
3409:
3387:
3384:
3383:
3376:VIII. Infinity:
3366:Ordinal numbers
3318:
3315:
3314:
3284:
3281:
3280:
3210:
3207:
3206:
3205:is a set, then
3183:is that of the
3172:is a set, then
3093:
3090:
3089:
3051:
3048:
3047:
3010:
3007:
3006:
2969:asserts. Hence
2908:
2905:
2904:
2882:
2879:
2878:
2849:algebra of sets
2808:
2805:
2804:
2788:
2785:
2784:
2783:if and only if
2750:
2747:
2746:
2730:
2727:
2726:
2669:
2666:
2665:
2643:
2640:
2639:
2595:
2592:
2591:
2586:) if, for some
2514:
2511:
2510:
2507:class abstracts
2470:
2445:rather than on
2443:New Foundations
2408:
2400:
2389:
2376:
2362:
2340:
2333:. Also let Def(
2311:
2256:
2253:
2252:
2233:
2230:
2229:
2206:
2203:
2202:
2175:axiom of choice
2163:axiom of choice
2101:
1894:
1891:
1890:
1856:
1853:
1852:
1847:is a member of
1839:is a member of
1704:
1701:
1700:
1656:
1653:
1652:
1524:
1521:
1520:
1489:axiom of choice
1463:
1462:
1362:
1361:
1258:
1256:
1253:
1252:
1234:if and only if
1162:
1159:
1158:
1130:
1127:
1126:
983:
980:
979:
934:
931:
930:
875:
871:
853:
849:
801:
797:
782:
778:
773:
770:
769:
737:
734:
733:
683:
680:
679:
660:is not free. φ(
542:
539:
538:
433:
430:
429:
363:
360:
359:
356:universal class
312:
309:
308:
292:
289:
288:
246:
243:
242:
213:
210:
209:
147:
72:bound variables
17:
12:
11:
5:
6436:
6426:
6425:
6408:
6407:
6393:
6390:
6389:
6387:
6386:
6381:
6376:
6371:
6366:
6365:
6364:
6354:
6349:
6344:
6335:
6330:
6325:
6320:
6318:Abstract logic
6314:
6312:
6308:
6307:
6305:
6304:
6299:
6297:Turing machine
6294:
6289:
6284:
6279:
6274:
6269:
6268:
6267:
6262:
6257:
6252:
6247:
6237:
6235:Computable set
6232:
6227:
6222:
6217:
6211:
6209:
6203:
6202:
6200:
6199:
6194:
6189:
6184:
6179:
6174:
6169:
6164:
6163:
6162:
6157:
6152:
6142:
6137:
6132:
6130:Satisfiability
6127:
6122:
6117:
6116:
6115:
6105:
6104:
6103:
6093:
6092:
6091:
6086:
6081:
6076:
6071:
6061:
6060:
6059:
6054:
6047:Interpretation
6043:
6041:
6035:
6034:
6032:
6031:
6026:
6021:
6016:
6011:
6001:
5996:
5995:
5994:
5993:
5992:
5982:
5977:
5967:
5962:
5957:
5952:
5947:
5942:
5936:
5934:
5928:
5927:
5924:
5923:
5921:
5920:
5912:
5911:
5910:
5909:
5904:
5903:
5902:
5897:
5892:
5872:
5871:
5870:
5868:minimal axioms
5865:
5854:
5853:
5852:
5841:
5840:
5839:
5834:
5829:
5824:
5819:
5814:
5801:
5799:
5780:
5779:
5777:
5776:
5775:
5774:
5762:
5757:
5756:
5755:
5750:
5745:
5740:
5730:
5725:
5720:
5715:
5714:
5713:
5708:
5698:
5697:
5696:
5691:
5686:
5681:
5671:
5666:
5665:
5664:
5659:
5654:
5644:
5643:
5642:
5637:
5632:
5627:
5622:
5617:
5607:
5602:
5597:
5592:
5591:
5590:
5585:
5580:
5575:
5565:
5560:
5558:Formation rule
5555:
5550:
5549:
5548:
5543:
5533:
5532:
5531:
5521:
5516:
5511:
5506:
5500:
5494:
5477:Formal systems
5473:
5472:
5469:
5468:
5466:
5465:
5460:
5455:
5450:
5445:
5440:
5435:
5430:
5425:
5420:
5419:
5418:
5413:
5402:
5400:
5396:
5395:
5393:
5392:
5391:
5390:
5380:
5375:
5374:
5373:
5366:Large cardinal
5363:
5358:
5353:
5348:
5343:
5329:
5328:
5327:
5322:
5317:
5302:
5300:
5290:
5289:
5287:
5286:
5285:
5284:
5279:
5274:
5264:
5259:
5254:
5249:
5244:
5239:
5234:
5229:
5224:
5219:
5214:
5209:
5203:
5201:
5194:
5193:
5191:
5190:
5189:
5188:
5183:
5178:
5173:
5168:
5163:
5155:
5154:
5153:
5148:
5138:
5133:
5131:Extensionality
5128:
5126:Ordinal number
5123:
5113:
5108:
5107:
5106:
5095:
5089:
5083:
5082:
5079:
5078:
5076:
5075:
5070:
5065:
5060:
5055:
5050:
5045:
5044:
5043:
5033:
5032:
5031:
5018:
5016:
5010:
5009:
5007:
5006:
5005:
5004:
4999:
4994:
4984:
4979:
4974:
4969:
4964:
4959:
4953:
4951:
4945:
4944:
4942:
4941:
4936:
4931:
4926:
4921:
4916:
4911:
4910:
4909:
4899:
4894:
4889:
4884:
4879:
4874:
4868:
4866:
4857:
4851:
4850:
4848:
4847:
4842:
4837:
4832:
4827:
4822:
4810:Cantor's
4808:
4803:
4798:
4788:
4786:
4773:
4772:
4770:
4769:
4764:
4759:
4754:
4749:
4744:
4739:
4734:
4729:
4724:
4719:
4714:
4709:
4708:
4707:
4696:
4694:
4690:
4689:
4682:
4681:
4674:
4667:
4659:
4650:
4649:
4647:
4646:
4641:
4639:Thoralf Skolem
4636:
4631:
4626:
4621:
4616:
4611:
4606:
4601:
4596:
4591:
4585:
4583:
4577:
4576:
4574:
4573:
4568:
4563:
4557:
4555:
4553:
4552:
4549:
4543:
4540:
4539:
4537:
4536:
4535:
4534:
4529:
4524:
4523:
4522:
4507:
4506:
4505:
4493:
4492:
4491:
4480:
4479:
4474:
4469:
4464:
4458:
4456:
4452:
4451:
4449:
4448:
4443:
4438:
4433:
4424:
4419:
4414:
4404:
4399:
4398:
4397:
4392:
4387:
4377:
4367:
4362:
4357:
4351:
4349:
4342:
4341:
4339:
4338:
4333:
4328:
4323:
4321:Ordinal number
4318:
4313:
4308:
4303:
4302:
4301:
4296:
4286:
4281:
4276:
4271:
4266:
4256:
4251:
4245:
4243:
4241:
4240:
4237:
4233:
4230:
4229:
4227:
4226:
4221:
4216:
4211:
4206:
4201:
4199:Disjoint union
4196:
4191:
4185:
4179:
4177:
4171:
4170:
4168:
4167:
4166:
4165:
4160:
4149:
4148:
4146:Martin's axiom
4143:
4138:
4133:
4128:
4123:
4118:
4113:
4111:Extensionality
4108:
4107:
4106:
4096:
4091:
4090:
4089:
4084:
4079:
4069:
4063:
4061:
4055:
4054:
4047:
4045:
4043:
4042:
4036:
4034:
4030:
4029:
4022:
4021:
4014:
4007:
3999:
3993:
3992:
3987:
3978:
3977:
3966:
3965:External links
3963:
3962:
3961:
3915:(3): 150–155,
3901:
3890:Rubin, Jean E.
3887:
3854:
3847:
3840:
3829:
3813:
3806:David K. Lewis
3803:
3793:
3786:John L. Kelley
3781:
3778:
3776:
3775:
3766:
3755:locus citandum
3746:
3736:
3734:
3731:
3727:proper classes
3659:
3656:
3653:
3650:
3647:
3644:
3606:
3603:
3600:
3597:
3594:
3591:
3520:
3501:
3498:
3485:inductive set
3464:
3461:
3458:
3455:
3435:
3432:
3429:
3426:
3423:
3420:
3417:
3397:
3394:
3391:
3350:The import of
3337:
3334:
3331:
3328:
3325:
3322:
3294:
3291:
3288:
3231:The import of
3217:
3214:
3179:The import of
3109:
3106:
3103:
3100:
3097:
3061:
3058:
3055:
3034:The import of
3020:
3017:
3014:
2934:The import of
2921:
2918:
2915:
2912:
2892:
2889:
2886:
2827:
2826:
2815:
2812:
2792:
2772:
2769:
2766:
2763:
2760:
2757:
2754:
2734:
2697:Extensionality
2682:
2679:
2676:
2673:
2653:
2650:
2647:
2605:
2602:
2599:
2570:
2569:
2545:
2542:
2539:
2536:
2533:
2530:
2527:
2524:
2521:
2503:
2489:
2469:
2463:
2407:
2404:
2403:
2402:
2398:
2387:
2382:
2374:
2368:
2360:
2338:
2337:) denote the Δ
2310:
2307:
2260:
2240:
2237:
2213:
2210:
2128:proper classes
2100:
2097:
2096:
2095:
2089:
2083:
2042:
2041:
2030:
2027:
2024:
2021:
2018:
2015:
2012:
2009:
2006:
2003:
2000:
1997:
1994:
1991:
1988:
1985:
1982:
1979:
1976:
1973:
1970:
1967:
1964:
1961:
1958:
1955:
1952:
1949:
1946:
1943:
1940:
1937:
1934:
1931:
1928:
1925:
1922:
1919:
1916:
1913:
1910:
1907:
1904:
1901:
1898:
1875:
1872:
1869:
1866:
1863:
1860:
1823:
1822:
1811:
1808:
1805:
1802:
1799:
1796:
1793:
1790:
1787:
1784:
1781:
1778:
1775:
1772:
1769:
1766:
1762:
1759:
1756:
1753:
1750:
1747:
1744:
1740:
1737:
1734:
1731:
1728:
1725:
1722:
1718:
1715:
1711:
1708:
1669:
1666:
1663:
1660:
1643:
1642:
1631:
1628:
1625:
1622:
1619:
1616:
1613:
1610:
1607:
1604:
1601:
1598:
1595:
1592:
1589:
1586:
1582:
1579:
1576:
1573:
1570:
1567:
1564:
1560:
1557:
1554:
1551:
1548:
1545:
1542:
1538:
1535:
1531:
1528:
1477:
1476:
1461:
1458:
1455:
1452:
1449:
1446:
1443:
1440:
1437:
1434:
1431:
1428:
1425:
1422:
1419:
1416:
1413:
1410:
1407:
1404:
1401:
1398:
1395:
1392:
1389:
1386:
1383:
1380:
1377:
1374:
1371:
1368:
1364:
1363:
1360:
1357:
1354:
1351:
1348:
1345:
1342:
1339:
1336:
1333:
1330:
1327:
1324:
1321:
1318:
1315:
1312:
1309:
1306:
1303:
1300:
1297:
1294:
1291:
1288:
1285:
1282:
1279:
1276:
1273:
1270:
1267:
1264:
1261:
1260:
1199:
1196:
1193:
1190:
1187:
1184:
1181:
1178:
1175:
1172:
1169:
1146:
1143:
1140:
1137:
1134:
1119:
1118:
1107:
1104:
1101:
1098:
1095:
1092:
1089:
1086:
1082:
1078:
1075:
1072:
1069:
1066:
1063:
1060:
1057:
1054:
1050:
1047:
1044:
1041:
1038:
1035:
1031:
1028:
1025:
1022:
1019:
1016:
1013:
1010:
1007:
1004:
1001:
997:
994:
990:
987:
956:
953:
950:
947:
944:
941:
938:
913:
912:
901:
898:
895:
892:
889:
886:
883:
878:
874:
870:
867:
864:
861:
856:
852:
848:
845:
842:
839:
836:
833:
830:
827:
824:
821:
818:
815:
812:
809:
804:
800:
796:
793:
790:
785:
781:
777:
750:
747:
744:
741:
714:
711:
708:
705:
702:
699:
696:
693:
690:
687:
639:
638:
627:
624:
621:
618:
615:
612:
609:
606:
603:
600:
597:
594:
591:
588:
585:
582:
579:
576:
573:
570:
567:
564:
561:
558:
555:
552:
549:
546:
515:
514:
503:
500:
497:
494:
491:
488:
485:
482:
479:
476:
473:
470:
467:
464:
461:
457:
454:
451:
447:
444:
440:
437:
421:Extensionality
417:
416:
397:
394:
391:
388:
385:
382:
379:
376:
373:
370:
367:
348:
337:
334:
331:
328:
325:
322:
319:
316:
307:is defined by
296:
282:
271:
268:
265:
262:
259:
256:
253:
250:
226:
223:
220:
200:
146:
143:
119:Thoralf Skolem
99:John L. Kelley
84:proper classes
15:
9:
6:
4:
3:
2:
6435:
6424:
6421:
6420:
6418:
6405:
6404:
6399:
6391:
6385:
6382:
6380:
6377:
6375:
6372:
6370:
6367:
6363:
6360:
6359:
6358:
6355:
6353:
6350:
6348:
6345:
6343:
6339:
6336:
6334:
6331:
6329:
6326:
6324:
6321:
6319:
6316:
6315:
6313:
6309:
6303:
6300:
6298:
6295:
6293:
6292:Recursive set
6290:
6288:
6285:
6283:
6280:
6278:
6275:
6273:
6270:
6266:
6263:
6261:
6258:
6256:
6253:
6251:
6248:
6246:
6243:
6242:
6241:
6238:
6236:
6233:
6231:
6228:
6226:
6223:
6221:
6218:
6216:
6213:
6212:
6210:
6208:
6204:
6198:
6195:
6193:
6190:
6188:
6185:
6183:
6180:
6178:
6175:
6173:
6170:
6168:
6165:
6161:
6158:
6156:
6153:
6151:
6148:
6147:
6146:
6143:
6141:
6138:
6136:
6133:
6131:
6128:
6126:
6123:
6121:
6118:
6114:
6111:
6110:
6109:
6106:
6102:
6101:of arithmetic
6099:
6098:
6097:
6094:
6090:
6087:
6085:
6082:
6080:
6077:
6075:
6072:
6070:
6067:
6066:
6065:
6062:
6058:
6055:
6053:
6050:
6049:
6048:
6045:
6044:
6042:
6040:
6036:
6030:
6027:
6025:
6022:
6020:
6017:
6015:
6012:
6009:
6008:from ZFC
6005:
6002:
6000:
5997:
5991:
5988:
5987:
5986:
5983:
5981:
5978:
5976:
5973:
5972:
5971:
5968:
5966:
5963:
5961:
5958:
5956:
5953:
5951:
5948:
5946:
5943:
5941:
5938:
5937:
5935:
5933:
5929:
5919:
5918:
5914:
5913:
5908:
5907:non-Euclidean
5905:
5901:
5898:
5896:
5893:
5891:
5890:
5886:
5885:
5883:
5880:
5879:
5877:
5873:
5869:
5866:
5864:
5861:
5860:
5859:
5855:
5851:
5848:
5847:
5846:
5842:
5838:
5835:
5833:
5830:
5828:
5825:
5823:
5820:
5818:
5815:
5813:
5810:
5809:
5807:
5803:
5802:
5800:
5795:
5789:
5784:Example
5781:
5773:
5768:
5767:
5766:
5763:
5761:
5758:
5754:
5751:
5749:
5746:
5744:
5741:
5739:
5736:
5735:
5734:
5731:
5729:
5726:
5724:
5721:
5719:
5716:
5712:
5709:
5707:
5704:
5703:
5702:
5699:
5695:
5692:
5690:
5687:
5685:
5682:
5680:
5677:
5676:
5675:
5672:
5670:
5667:
5663:
5660:
5658:
5655:
5653:
5650:
5649:
5648:
5645:
5641:
5638:
5636:
5633:
5631:
5628:
5626:
5623:
5621:
5618:
5616:
5613:
5612:
5611:
5608:
5606:
5603:
5601:
5598:
5596:
5593:
5589:
5586:
5584:
5581:
5579:
5576:
5574:
5571:
5570:
5569:
5566:
5564:
5561:
5559:
5556:
5554:
5551:
5547:
5544:
5542:
5541:by definition
5539:
5538:
5537:
5534:
5530:
5527:
5526:
5525:
5522:
5520:
5517:
5515:
5512:
5510:
5507:
5505:
5502:
5501:
5498:
5495:
5493:
5489:
5484:
5478:
5474:
5464:
5461:
5459:
5456:
5454:
5451:
5449:
5446:
5444:
5441:
5439:
5436:
5434:
5431:
5429:
5428:Kripke–Platek
5426:
5424:
5421:
5417:
5414:
5412:
5409:
5408:
5407:
5404:
5403:
5401:
5397:
5389:
5386:
5385:
5384:
5381:
5379:
5376:
5372:
5369:
5368:
5367:
5364:
5362:
5359:
5357:
5354:
5352:
5349:
5347:
5344:
5341:
5337:
5333:
5330:
5326:
5323:
5321:
5318:
5316:
5313:
5312:
5311:
5307:
5304:
5303:
5301:
5299:
5295:
5291:
5283:
5280:
5278:
5275:
5273:
5272:constructible
5270:
5269:
5268:
5265:
5263:
5260:
5258:
5255:
5253:
5250:
5248:
5245:
5243:
5240:
5238:
5235:
5233:
5230:
5228:
5225:
5223:
5220:
5218:
5215:
5213:
5210:
5208:
5205:
5204:
5202:
5200:
5195:
5187:
5184:
5182:
5179:
5177:
5174:
5172:
5169:
5167:
5164:
5162:
5159:
5158:
5156:
5152:
5149:
5147:
5144:
5143:
5142:
5139:
5137:
5134:
5132:
5129:
5127:
5124:
5122:
5118:
5114:
5112:
5109:
5105:
5102:
5101:
5100:
5097:
5096:
5093:
5090:
5088:
5084:
5074:
5071:
5069:
5066:
5064:
5061:
5059:
5056:
5054:
5051:
5049:
5046:
5042:
5039:
5038:
5037:
5034:
5030:
5025:
5024:
5023:
5020:
5019:
5017:
5015:
5011:
5003:
5000:
4998:
4995:
4993:
4990:
4989:
4988:
4985:
4983:
4980:
4978:
4975:
4973:
4970:
4968:
4965:
4963:
4960:
4958:
4955:
4954:
4952:
4950:
4949:Propositional
4946:
4940:
4937:
4935:
4932:
4930:
4927:
4925:
4922:
4920:
4917:
4915:
4912:
4908:
4905:
4904:
4903:
4900:
4898:
4895:
4893:
4890:
4888:
4885:
4883:
4880:
4878:
4877:Logical truth
4875:
4873:
4870:
4869:
4867:
4865:
4861:
4858:
4856:
4852:
4846:
4843:
4841:
4838:
4836:
4833:
4831:
4828:
4826:
4823:
4821:
4817:
4813:
4809:
4807:
4804:
4802:
4799:
4797:
4793:
4790:
4789:
4787:
4785:
4779:
4774:
4768:
4765:
4763:
4760:
4758:
4755:
4753:
4750:
4748:
4745:
4743:
4740:
4738:
4735:
4733:
4730:
4728:
4725:
4723:
4720:
4718:
4715:
4713:
4710:
4706:
4703:
4702:
4701:
4698:
4697:
4695:
4691:
4687:
4680:
4675:
4673:
4668:
4666:
4661:
4660:
4657:
4645:
4644:Ernst Zermelo
4642:
4640:
4637:
4635:
4632:
4630:
4629:Willard Quine
4627:
4625:
4622:
4620:
4617:
4615:
4612:
4610:
4607:
4605:
4602:
4600:
4597:
4595:
4592:
4590:
4587:
4586:
4584:
4582:
4581:Set theorists
4578:
4572:
4569:
4567:
4564:
4562:
4559:
4558:
4556:
4550:
4548:
4545:
4544:
4541:
4533:
4530:
4528:
4527:Kripke–Platek
4525:
4521:
4518:
4517:
4516:
4513:
4512:
4511:
4508:
4504:
4501:
4500:
4499:
4498:
4494:
4490:
4487:
4486:
4485:
4482:
4481:
4478:
4475:
4473:
4470:
4468:
4465:
4463:
4460:
4459:
4457:
4453:
4447:
4444:
4442:
4439:
4437:
4434:
4432:
4430:
4425:
4423:
4420:
4418:
4415:
4412:
4408:
4405:
4403:
4400:
4396:
4393:
4391:
4388:
4386:
4383:
4382:
4381:
4378:
4375:
4371:
4368:
4366:
4363:
4361:
4358:
4356:
4353:
4352:
4350:
4347:
4343:
4337:
4334:
4332:
4329:
4327:
4324:
4322:
4319:
4317:
4314:
4312:
4309:
4307:
4304:
4300:
4297:
4295:
4292:
4291:
4290:
4287:
4285:
4282:
4280:
4277:
4275:
4272:
4270:
4267:
4264:
4260:
4257:
4255:
4252:
4250:
4247:
4246:
4244:
4238:
4235:
4234:
4231:
4225:
4222:
4220:
4217:
4215:
4212:
4210:
4207:
4205:
4202:
4200:
4197:
4195:
4192:
4189:
4186:
4184:
4181:
4180:
4178:
4176:
4172:
4164:
4163:specification
4161:
4159:
4156:
4155:
4154:
4151:
4150:
4147:
4144:
4142:
4139:
4137:
4134:
4132:
4129:
4127:
4124:
4122:
4119:
4117:
4114:
4112:
4109:
4105:
4102:
4101:
4100:
4097:
4095:
4092:
4088:
4085:
4083:
4080:
4078:
4075:
4074:
4073:
4070:
4068:
4065:
4064:
4062:
4060:
4056:
4051:
4041:
4038:
4037:
4035:
4031:
4027:
4020:
4015:
4013:
4008:
4006:
4001:
4000:
3997:
3991:
3988:
3986:
3983:
3982:
3981:
3976:
3974:
3969:
3968:
3958:
3954:
3949:
3944:
3940:
3936:
3932:
3928:
3923:
3918:
3914:
3910:
3906:
3902:
3899:
3895:
3891:
3888:
3883:
3878:
3874:
3870:
3863:
3859:
3855:
3852:
3848:
3845:
3841:
3838:
3832:
3830:0-534-06624-0
3826:
3822:
3818:
3814:
3811:
3807:
3804:
3801:
3797:
3796:Lemmon, E. J.
3794:
3791:
3787:
3784:
3783:
3770:
3763:
3760:
3756:
3750:
3741:
3737:
3730:
3728:
3724:
3720:
3716:
3712:
3708:
3703:
3701:
3697:
3693:
3689:
3685:
3683:
3679:
3675:
3671:
3657:
3645:
3642:
3634:
3630:
3626:
3624:
3620:
3604:
3601:
3595:
3589:
3581:
3577:
3573:
3570:
3566:
3564:
3560:
3556:
3552:
3548:
3544:
3540:
3536:
3534:
3518:
3499:
3496:
3488:
3484:
3480:
3475:
3462:
3459:
3456:
3453:
3433:
3430:
3424:
3418:
3415:
3395:
3392:
3389:
3381:
3377:
3373:
3371:
3367:
3363:
3359:
3357:
3353:
3348:
3335:
3329:
3326:
3323:
3320:
3312:
3308:
3289:
3286:
3278:
3274:
3272:
3268:
3264:
3260:
3256:
3252:
3248:
3246:
3242:
3238:
3234:
3229:
3215:
3212:
3204:
3200:
3196:
3194:
3190:
3186:
3182:
3177:
3175:
3171:
3167:
3163:
3159:
3157:
3153:
3149:
3145:
3141:
3137:
3136:ordered pairs
3133:
3129:
3127:
3123:
3104:
3101:
3098:
3088:implies that
3087:
3083:
3079:
3075:
3056:
3045:
3041:
3037:
3032:
3018:
3015:
3012:
3004:
3000:
2996:
2992:
2990:
2986:
2982:
2978:
2974:
2972:
2968:
2964:
2960:
2956:
2952:
2949:
2945:
2941:
2937:
2932:
2919:
2916:
2913:
2910:
2890:
2887:
2884:
2876:
2872:
2868:
2864:
2863:III. Subsets:
2860:
2858:
2854:
2850:
2846:
2842:
2840:
2836:
2832:
2813:
2810:
2803:is a set and
2790:
2767:
2764:
2761:
2755:
2752:
2732:
2724:
2723:
2722:
2720:
2716:
2714:
2710:
2706:
2702:
2698:
2695:Identical to
2693:
2680:
2677:
2674:
2671:
2651:
2648:
2645:
2637:
2633:
2629:
2625:
2621:
2617:
2603:
2600:
2597:
2589:
2585:
2581:
2577:
2574:
2567:
2563:
2559:
2543:
2534:
2528:
2525:
2522:
2508:
2504:
2501:
2497:
2493:
2490:
2487:
2483:
2482:
2481:
2478:
2476:
2468:
2462:
2460:
2456:
2452:
2451:Impredicative
2448:
2444:
2440:
2437:
2433:
2432:impredicative
2429:
2425:
2421:
2417:
2413:
2397:
2393:
2386:
2383:
2380:
2373:
2369:
2366:
2359:
2356:
2355:
2354:
2352:
2348:
2344:
2336:
2332:
2328:
2324:
2320:
2316:
2306:
2304:
2300:
2296:
2291:
2289:
2285:
2281:
2277:
2274:The class of
2272:
2258:
2238:
2235:
2227:
2211:
2208:
2201:
2200:limit ordinal
2197:
2193:
2189:
2187:
2182:
2178:
2176:
2172:
2168:
2164:
2160:
2156:
2151:
2149:
2145:
2141:
2137:
2133:
2132:impredicative
2129:
2125:
2120:
2118:
2114:
2110:
2106:
2093:
2090:
2087:
2084:
2081:
2077:
2074:
2073:
2072:
2069:
2067:
2063:
2059:
2055:
2051:
2047:
2028:
2010:
2007:
2004:
2001:
1998:
1995:
1992:
1983:
1980:
1977:
1971:
1965:
1962:
1959:
1956:
1950:
1941:
1938:
1935:
1929:
1923:
1920:
1917:
1911:
1908:
1905:
1899:
1889:
1888:
1887:
1873:
1867:
1861:
1858:
1851:, then so is
1850:
1846:
1842:
1838:
1834:
1830:
1828:
1809:
1803:
1800:
1785:
1782:
1779:
1776:
1773:
1770:
1767:
1760:
1751:
1748:
1745:
1738:
1732:
1729:
1726:
1716:
1709:
1699:
1698:
1697:
1695:
1691:
1687:
1684:, namely the
1683:
1667:
1664:
1661:
1658:
1650:
1648:
1629:
1623:
1620:
1605:
1602:
1599:
1593:
1590:
1587:
1580:
1571:
1568:
1565:
1558:
1552:
1549:
1546:
1536:
1529:
1519:
1518:
1517:
1515:
1511:
1507:
1503:
1499:
1497:
1492:
1490:
1486:
1482:
1459:
1447:
1444:
1441:
1432:
1429:
1423:
1420:
1417:
1411:
1408:
1405:
1399:
1396:
1393:
1381:
1375:
1369:
1358:
1349:
1346:
1340:
1337:
1334:
1328:
1325:
1322:
1319:
1313:
1304:
1301:
1295:
1286:
1277:
1274:
1265:
1251:
1250:
1249:
1247:
1243:
1239:
1238:
1233:
1229:
1226:
1224:
1219:
1217:
1213:
1191:
1188:
1185:
1179:
1173:
1141:
1138:
1135:
1124:
1105:
1090:
1087:
1084:
1080:
1076:
1073:
1070:
1061:
1058:
1055:
1048:
1042:
1039:
1036:
1029:
1017:
1014:
1011:
1008:
1005:
995:
988:
978:
977:
976:
974:
970:
951:
948:
945:
939:
936:
928:
924:
921:For any sets
920:
918:
899:
890:
887:
884:
876:
872:
868:
865:
862:
859:
854:
850:
846:
843:
837:
828:
825:
822:
816:
810:
802:
798:
794:
791:
788:
783:
779:
768:
767:
766:
764:
745:
739:
731:
728:
706:
700:
697:
694:
688:
685:
678:
674:
673:
667:
663:
659:
655:
654:free variable
651:
647:
643:
625:
613:
610:
607:
601:
598:
595:
589:
583:
580:
577:
574:
568:
556:
553:
547:
537:
536:
535:
533:
529:
525:
523:
518:
501:
495:
492:
489:
480:
477:
474:
468:
465:
462:
455:
445:
438:
428:
427:
426:
424:
422:
414:
410:
395:
389:
386:
383:
377:
374:
368:
357:
353:
349:
335:
326:
323:
317:
294:
287:
283:
269:
263:
260:
257:
251:
240:
224:
221:
218:
208:
205:
201:
198:
194:
190:
186:
185:
184:
182:
177:
175:
171:
167:
163:
159:
155:
151:
142:
139:
135:
131:
126:
124:
120:
116:
112:
108:
104:
103:Anthony Morse
100:
95:
93:
89:
85:
81:
77:
73:
69:
65:
62:
58:
54:
50:
46:
42:
38:
34:
30:
26:
22:
6394:
6192:Ultraproduct
6039:Model theory
6004:Independence
5940:Formal proof
5932:Proof theory
5915:
5888:
5845:real numbers
5817:second-order
5728:Substitution
5605:Metalanguage
5546:conservative
5519:Axiom schema
5463:Constructive
5433:Morse–Kelley
5432:
5399:Set theories
5378:Aleph number
5371:inaccessible
5277:Grothendieck
5161:intersection
5048:Higher-order
5036:Second-order
4982:Truth tables
4939:Venn diagram
4722:Formal proof
4594:Georg Cantor
4589:Paul Bernays
4520:Morse–Kelley
4519:
4495:
4428:
4427:Subset
4374:hereditarily
4336:Venn diagram
4294:ordered pair
4209:Intersection
4153:Axiom schema
3979:
3972:
3912:
3908:
3893:
3872:
3868:
3850:
3843:
3820:
3809:
3799:
3789:
3788:1975 (1955)
3769:
3761:
3754:
3749:
3740:
3722:
3718:
3714:
3710:
3706:
3704:
3687:
3686:
3681:
3673:
3672:
3632:
3628:
3627:
3622:
3618:
3579:
3575:
3571:
3568:
3567:
3563:real numbers
3551:Peano axioms
3546:
3538:
3537:
3532:
3486:
3478:
3476:
3382:, such that
3379:
3375:
3374:
3361:
3360:
3355:
3351:
3349:
3310:
3306:
3276:
3275:
3271:order theory
3250:
3249:
3244:
3240:
3236:
3232:
3230:
3202:
3198:
3197:
3180:
3178:
3173:
3169:
3165:
3161:
3160:
3131:
3130:
3125:
3121:
3120:is a set if
3085:
3081:
3077:
3073:
3043:
3039:
3035:
3033:
3002:
2998:
2994:
2993:
2980:
2976:
2975:
2970:
2966:
2962:
2958:
2957:, the class
2954:
2950:
2947:
2943:
2939:
2935:
2933:
2874:
2870:
2866:
2862:
2861:
2856:
2844:
2843:
2838:
2834:
2830:
2828:
2718:
2717:
2712:
2700:
2696:
2694:
2635:
2631:
2627:
2623:
2619:
2618:
2587:
2584:proper class
2579:
2575:
2572:
2571:
2565:
2561:
2557:
2509:of the form
2499:
2495:
2491:
2485:
2479:
2474:
2471:
2466:
2423:
2419:
2416:J. L. Kelley
2409:
2395:
2384:
2371:
2363:is model of
2357:
2346:
2334:
2330:
2314:
2312:
2309:Model theory
2292:
2287:
2283:
2280:well-ordered
2273:
2225:
2195:
2185:
2179:
2152:
2143:
2135:
2121:
2102:
2070:
2065:
2061:
2057:
2053:
2049:
2045:
2043:
1848:
1844:
1840:
1832:
1825:
1824:
1693:
1689:
1681:
1645:
1644:
1513:
1509:
1501:
1494:
1493:
1484:
1478:
1245:
1235:
1232:proper class
1227:
1221:
1220:
1123:ordered pair
1120:
972:
968:
926:
922:
915:
914:
762:
729:
726:
676:
669:
665:
661:
657:
649:
645:
641:
640:
527:
520:
519:
516:
419:
418:
411:is also the
408:
351:
238:
193:proper class
188:
178:
170:proper class
160:consists of
148:
127:
122:
110:
96:
76:axiom schema
56:
52:
48:
44:
40:
36:
32:
28:
24:
18:
6302:Type theory
6250:undecidable
6182:Truth value
6069:equivalence
5748:non-logical
5361:Enumeration
5351:Isomorphism
5298:cardinality
5282:Von Neumann
5247:Ultrafilter
5212:Uncountable
5146:equivalence
5063:Quantifiers
5053:Fixed-point
5022:First-order
4902:Consistency
4887:Proposition
4864:Traditional
4835:Lindström's
4825:Compactness
4767:Type theory
4712:Cardinality
4619:Thomas Jech
4462:Alternative
4441:Uncountable
4395:Ultrafilter
4254:Cardinality
4158:replacement
4099:Determinacy
3875:: 111–124,
3692:Equivalents
3629:IX. Choice:
3569:Definition:
3354:is that of
3235:is that of
3038:is that of
2938:is that of
2573:Definition:
2560:satisfying
2457:(1951) and
2412:Wang (1949)
2299:syntactical
2188:being a set
2140:predicative
1508:of the set
107:Wang (1949)
61:first-order
6113:elementary
5806:arithmetic
5674:Quantifier
5652:functional
5524:Expression
5242:Transitive
5186:identities
5171:complement
5104:hereditary
5087:Set theory
4614:Kurt Gödel
4599:Paul Cohen
4436:Transitive
4204:Identities
4188:Complement
4175:Operations
4136:Regularity
4104:projective
4067:Adjunction
4026:Set theory
3898:urelements
3780:References
3549:is a set,
3356:Foundation
3313:such that
3263:surjection
3228:is a set.
3176:is a set.
3128:are sets.
3031:is a set.
2995:IV. Union:
2991:provable.
2989:Separation
2985:singletons
2973:is a set.
2946:: for any
2853:null class
2847:: Boolean
2620:I. Extent:
2418:'s (1955)
2341:definable
2325:. Let the
2109:urelements
2099:Discussion
2044:Note that
1843:; (ii) if
1696:is a set.
1516:is a set.
732:such that
522:Foundation
350:The class
6384:Supertask
6287:Recursion
6245:decidable
6079:saturated
6057:of models
5980:deductive
5975:axiomatic
5895:Hilbert's
5882:Euclidean
5863:canonical
5786:axiomatic
5718:Signature
5647:Predicate
5536:Extension
5458:Ackermann
5383:Operation
5262:Universal
5252:Recursive
5227:Singleton
5222:Inhabited
5207:Countable
5197:Types of
5181:power set
5151:partition
5068:Predicate
5014:Predicate
4929:Syllogism
4919:Soundness
4892:Inference
4882:Tautology
4784:paradoxes
4547:Paradoxes
4467:Axiomatic
4446:Universal
4422:Singleton
4417:Recursive
4360:Countable
4355:Amorphous
4214:Power set
4131:Power set
4082:dependent
4077:countable
3971:Download
3905:Wang, Hao
3652:∅
3646:−
3602:∈
3519:∅
3497:∅
3457:∈
3446:whenever
3431:∈
3419:∪
3393:∈
3390:∅
3333:∅
3324:∩
3293:∅
3290:≠
3267:bijection
3259:injection
3213:⋃
3144:functions
3140:relations
3072:of a set
3016:∪
2940:Power Set
2914:∈
2888:⊆
2791:β
2762:α
2756:∈
2753:β
2733:β
2725:For each
2675:∈
2649:∈
2626:and each
2622:For each
2601:∈
2455:Mostowski
2392:power set
2353:). Then:
2303:semantics
2259:ω
2236:ω
2209:ω
2107:includes
2008:∈
2002:∨
1987:↔
1981:∈
1969:∀
1966:∧
1960:∈
1948:∃
1945:→
1939:∈
1927:∀
1924:∧
1918:∈
1915:∅
1912:∧
1897:∃
1862:∪
1837:empty set
1798:→
1783:∈
1777:∧
1771:∈
1758:∃
1755:↔
1749:∈
1736:∀
1733:∧
1714:∀
1707:∀
1665:⋃
1618:→
1603:∈
1597:→
1591:∈
1578:∀
1575:↔
1569:∈
1556:∀
1553:∧
1534:∀
1527:∀
1496:Power set
1439:→
1430:∈
1427:⟩
1415:⟨
1412:∧
1406:∈
1403:⟩
1391:⟨
1379:∀
1373:∀
1367:∀
1359:∧
1347:∈
1344:⟩
1332:⟨
1329:∧
1323:∈
1311:∃
1308:→
1293:∀
1284:∃
1281:↔
1272:¬
1263:∀
1216:functions
1212:relations
1145:⟩
1133:⟨
1081:∨
1065:↔
1059:∈
1046:∀
1043:∧
1027:∃
1024:→
1012:∧
993:∀
986:∀
885:∧
838:ϕ
832:↔
826:∈
814:∀
808:∃
776:∀
740:ϕ
701:ϕ
698:∣
605:→
599:∈
587:∀
584:∧
578:∈
566:∃
563:→
560:∅
545:∀
487:→
478:∈
472:↔
466:∈
453:∀
443:∀
436:∀
387:∈
381:→
366:∀
330:∅
315:∀
295:∅
286:empty set
261:∈
249:∃
207:predicate
55:) or the
6417:Category
6369:Logicism
6362:timeline
6338:Concrete
6197:Validity
6167:T-schema
6160:Kripke's
6155:Tarski's
6150:semantic
6140:Strength
6089:submodel
6084:spectrum
6052:function
5900:Tarski's
5889:Elements
5876:geometry
5832:Robinson
5753:variable
5738:function
5711:spectrum
5701:Sentence
5657:variable
5600:Language
5553:Relation
5514:Automata
5504:Alphabet
5488:language
5342:-jection
5320:codomain
5306:Function
5267:Universe
5237:Infinite
5141:Relation
4924:Validity
4914:Argument
4812:theorem,
4551:Problems
4455:Theories
4431:Superset
4407:Infinite
4236:Concepts
4116:Infinity
4033:Overview
3957:16588874
3860:(1950),
3819:(1987).
3623:domain c
3555:integers
3483:infinite
3170:domain f
3084:). Then
2492:domain f
2461:(1991).
2286:. Hence
2105:ontology
1827:Infinity
611:∉
557:≠
532:disjoint
327:∉
197:mnemonic
154:ontology
125:(1965).
115:topology
6311:Related
6108:Diagram
6006: (
5985:Hilbert
5970:Systems
5965:Theorem
5843:of the
5788:systems
5568:Formula
5563:Grammar
5479: (
5423:General
5136:Forcing
5121:Element
5041:Monadic
4816:paradox
4757:Theorem
4693:General
4489:General
4484:Zermelo
4390:subbase
4372: (
4311:Forcing
4289:Element
4261: (
4239:Methods
4126:Pairing
3948:1062986
3939:0029850
3892:(1967)
3808:(1991)
3798:(1986)
3759:Quine's
3688:Develop
3684:above.
3539:Develop
3362:Develop
3358:above.
3251:Develop
3239:above.
3174:range f
3132:Develop
3040:Pairing
2977:Develop
2903:, then
2845:Develop
2699:above.
2496:range f
2484:He did
2477:below.
2475:Develop
2436:Quine's
2406:History
2343:subsets
2278:can be
1692:. Then
1512:. Then
1506:subsets
1240:can be
917:Pairing
204:monadic
162:classes
19:In the
6074:finite
5837:Skolem
5790:
5765:Theory
5733:Symbol
5723:String
5706:atomic
5583:ground
5578:closed
5573:atomic
5529:ground
5492:syntax
5388:binary
5315:domain
5232:Finite
4997:finite
4855:Logics
4814:
4762:Theory
4380:Filter
4370:Finite
4306:Family
4249:Almost
4087:global
4072:Choice
4059:Axioms
3955:
3945:
3937:
3929:
3827:
3148:domain
2517:
2390:, the
2317:, the
2167:domain
1165:
644:Let φ(
354:, the
216:
156:. The
6064:Model
5812:Peano
5669:Proof
5509:Arity
5438:Naive
5325:image
5257:Fuzzy
5217:Empty
5166:union
5111:Class
4752:Model
4742:Lemma
4700:Axiom
4472:Naive
4402:Fuzzy
4365:Empty
4348:types
4299:tuple
4269:Class
4263:large
4224:Union
4141:Union
3931:88430
3927:JSTOR
3865:(PDF)
3733:Notes
3574:is a
3237:Union
3152:range
2948:class
2877:, if
2578:is a
2459:Lewis
2349:(see
2183:plus
2171:range
1686:union
1647:Union
1244:into
1230:is a
677:class
652:is a
88:Quine
59:is a
6187:Type
5990:list
5794:list
5771:list
5760:Term
5694:rank
5588:open
5482:list
5294:Maps
5199:sets
5058:Free
5028:list
4778:list
4705:list
4385:base
3953:PMID
3825:ISBN
3753:The
3479:VIII
3408:and
3243:and
3191:and
3124:and
3001:and
2494:and
2370:Def(
2115:and
2078:and
2064:and
2056:and
2048:and
1651:Let
1500:Let
1214:and
971:and
925:and
727:sets
656:and
284:The
202:The
166:sets
101:and
5874:of
5856:of
5804:of
5336:Sur
5310:Map
5117:Ur-
5099:Set
4346:Set
3943:PMC
3917:doi
3877:doi
3837:NBG
3707:III
3696:ZFC
3621:of
3578:if
3541::
3352:VII
3309:of
3279:If
3201:If
3193:ZFC
3189:NBG
3187:in
3164:If
3082:III
2997:If
2967:III
2944:III
2936:III
2865:If
2709:ZFC
2707:in
2632:x=y
2580:set
2568:)."
2486:not
2447:ZFC
2394:of
2388:κ+1
2379:NBG
2365:ZFC
2345:of
2323:ZFC
2321:in
2224:as
2117:NBG
2113:ZFC
2092:NBG
2086:NBG
2080:NBG
2076:ZFC
672:NBG
530:is
181:NBG
150:NBG
132:of
78:of
47:),
39:),
31:),
6419::
6260:NP
5884::
5878::
5808::
5485:),
5340:Bi
5332:In
3951:,
3941:,
3935:MR
3933:,
3925:,
3913:35
3911:,
3873:37
3871:,
3867:,
3723:MK
3719:MK
3715:IV
3711:IV
3690::
3674:IX
3670:.
3625:.
3565:.
3561:,
3557:,
3553:,
3545:,
3372:.
3368:,
3364::
3273:.
3269:,
3265:,
3261:,
3257:,
3253::
3245:VI
3241:IV
3233:VI
3195:.
3158:.
3154:,
3150:,
3146:,
3142:,
3138:,
3086:IV
3044:IV
3036:IV
2987:.
2979::
2859:.
2841:.
2745:,
2638:,
2630:,
2616:.
2590:,
2449:.
2439:ML
2177:.
2150:.
2119:.
1886:.
1491:.
1248:.
1125:,
975:.
94:.
92:ML
53:QM
45:MT
37:KM
29:MK
23:,
6340:/
6255:P
6010:)
5796:)
5792:(
5689:∀
5684:!
5679:∃
5640:=
5635:↔
5630:→
5625:∧
5620:∨
5615:¬
5338:/
5334:/
5308:/
5119:)
5115:(
5002:∞
4992:3
4780:)
4678:e
4671:t
4664:v
4429:·
4413:)
4409:(
4376:)
4265:)
4018:e
4011:t
4004:v
3960:.
3919::
3900:.
3886:.
3879::
3833:.
3658:.
3655:}
3649:{
3643:V
3633:c
3619:x
3605:x
3599:)
3596:x
3593:(
3590:c
3580:c
3572:c
3547:N
3533:y
3500:.
3487:y
3463:.
3460:y
3454:x
3434:y
3428:}
3425:x
3422:{
3416:x
3396:y
3380:y
3336:.
3330:=
3327:y
3321:x
3311:x
3307:y
3287:x
3216:x
3203:x
3181:V
3166:f
3126:y
3122:x
3108:}
3105:y
3102:,
3099:x
3096:{
3078:x
3074:x
3060:}
3057:x
3054:{
3019:y
3013:x
3003:y
2999:x
2981:V
2971:z
2963:y
2959:z
2955:x
2951:z
2920:.
2917:y
2911:z
2891:x
2885:z
2875:z
2871:y
2867:x
2857:V
2839:A
2835:B
2831:A
2814:,
2811:B
2771:}
2768:A
2765::
2759:{
2713:I
2701:I
2681:.
2678:y
2672:z
2652:x
2646:z
2636:z
2628:y
2624:x
2604:y
2598:x
2588:y
2576:x
2566:x
2564:(
2562:A
2558:x
2544:,
2541:}
2538:)
2535:x
2532:(
2529:A
2526::
2523:x
2520:{
2500:f
2399:κ
2396:V
2385:V
2375:κ
2372:V
2367:;
2361:κ
2358:V
2347:X
2339:0
2335:X
2331:V
2315:V
2288:V
2284:V
2239:.
2226:I
2212:,
2196:I
2186:I
2144:x
2136:x
2066:s
2062:p
2058:s
2054:p
2050:s
2046:p
2029:.
2026:]
2023:)
2020:]
2017:)
2014:]
2011:z
2005:w
1999:z
1996:=
1993:w
1990:[
1984:x
1978:w
1975:(
1972:w
1963:y
1957:x
1954:[
1951:x
1942:y
1936:z
1933:(
1930:z
1921:y
1909:y
1906:M
1903:[
1900:y
1874:.
1871:}
1868:x
1865:{
1859:x
1849:y
1845:x
1841:y
1833:y
1829::
1810:.
1807:]
1804:s
1801:M
1795:)
1792:]
1789:)
1786:a
1780:y
1774:y
1768:x
1765:(
1761:y
1752:s
1746:x
1743:[
1739:x
1730:a
1727:M
1724:(
1721:[
1717:s
1710:a
1694:s
1690:a
1682:a
1668:a
1662:=
1659:s
1649::
1630:.
1627:]
1624:p
1621:M
1615:)
1612:]
1609:)
1606:a
1600:y
1594:x
1588:y
1585:(
1581:y
1572:p
1566:x
1563:[
1559:x
1550:a
1547:M
1544:(
1541:[
1537:p
1530:a
1514:p
1510:a
1502:p
1498::
1485:F
1460:.
1457:]
1454:)
1451:]
1448:y
1445:=
1442:x
1436:)
1433:F
1424:s
1421:,
1418:y
1409:F
1400:s
1397:,
1394:x
1388:(
1385:[
1382:s
1376:y
1370:x
1356:]
1353:)
1350:F
1341:s
1338:,
1335:x
1326:C
1320:s
1317:(
1314:s
1305:x
1302:M
1299:[
1296:x
1290:(
1287:F
1278:C
1275:M
1269:[
1266:C
1246:C
1237:V
1228:C
1225::
1198:}
1195:}
1192:y
1189:,
1186:x
1183:{
1180:,
1177:}
1174:x
1171:{
1168:{
1142:y
1139:,
1136:x
1106:.
1103:]
1100:)
1097:]
1094:)
1091:y
1088:=
1085:s
1077:x
1074:=
1071:s
1068:(
1062:z
1056:s
1053:[
1049:s
1040:z
1037:M
1034:(
1030:z
1021:)
1018:y
1015:M
1009:x
1006:M
1003:(
1000:[
996:y
989:x
973:y
969:x
955:}
952:y
949:,
946:x
943:{
940:=
937:z
927:y
923:x
919::
900:.
897:]
894:)
891:x
888:M
882:)
877:n
873:W
869:.
866:.
863:.
860:,
855:1
851:W
847:,
844:x
841:(
835:(
829:Y
823:x
820:[
817:x
811:Y
803:n
799:W
795:.
792:.
789:.
784:1
780:W
763:Y
749:)
746:x
743:(
730:x
713:}
710:)
707:x
704:(
695:x
692:{
689:=
686:Y
666:x
662:x
658:Y
650:x
646:x
626:.
623:]
620:)
617:)
614:A
608:c
602:b
596:c
593:(
590:c
581:A
575:b
572:(
569:b
554:A
551:[
548:A
528:A
524::
502:.
499:)
496:Y
493:=
490:X
484:)
481:Y
475:z
469:X
463:z
460:(
456:z
450:(
446:Y
439:X
423::
415:.
409:V
396:.
393:)
390:V
384:x
378:x
375:M
372:(
369:x
352:V
336:.
333:)
324:x
321:(
318:x
270:.
267:)
264:W
258:x
255:(
252:W
239:x
225:,
222:x
219:M
199:.
189:M
51:(
43:(
35:(
27:(
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.