1978:. If this is not assumed, then one needs an additional axiom, e.g. stating that for any thing x, there is a set {x}, in order to get the existence of at least one set from only the resources of FOL. Since most presentations of set theory want to be free from urelements, it is easiest to take the existence of the empty set as axiom and to formulate Infinity in terms of the empty set. Devlin, Mendelson, Suppes, and others do this. Smullyan and Fitting (Set Theory and the Continuum Problem) are sloppy here, since their Theorem 1.1 and its proof depends on their being a class to begin with, which does not follow from anything they say previously (including what they say about "V"). Stoll (Set theory and Its Logic) is equally sloppy, taking "there is a set" as a "temporary axiom" but never replacing that axiom with anything else that allows one to remove the "temporary" qualification. I haven't looked at other literature, but it would be interesting to do so!
84:
2137:. If we formulate it as it is formulated in various wikipedia entries, then it already depends on the existence of the empty set, which itself cannot follow from Infinity in this case. So one still needs an axiom implying that there is a set, independent of Infinity, unless one takes the above formulation implying the existence of two sets, one of which need not be the empty set. But that is in any case equivalent to asserting the existence of a set A and then using that in the axiom of Infinity.
74:
53:
2373:. Given any set, we can form the empty set using the axiom of separation. This is why the axiom of the empty set is often not included by authors, because it is provable from separation. Neither of the two most common references, Jech and Kunen, include the axiom of the empty set. It's mostly used, in my experience, in pedagogical contexts where not all of the axioms are assumed from the beginning, and in which the students are not familiar with formal logic. βΒ Carl
2403:
an axiom implying the existence of at least one set. In some theories there are urelements and most axioms are stated as (universally quantified) conditionals: if x and y are sets, there is a set whose members are precisely x and y, etc. (Suppes's version of ZFC is like this.) As such, ExT (e.g. TΒ := x=x) does not imply the existence of a set, so one needs an axiom implying the existence of at least one set.
22:
2031:, provable in logic, means "there exists a set" in ZFC, and it is impossible to speak about "things that are not sets" in ZFC. This may not be true for other set theories (e.g., in set theories with urelements where sets are only objects satisfying a special predicate), but thatβs no reason to delete a piece of information applicable to mainstream set theory.β
1937:
I was not aware of any distinction between "free logic" and first order predicate logic until you mentioned it here. I was aware that some people used what I considered to be invalid and sloppy logic. But I had developed my own rigorous version which I use personally. However, it is a kind of natural
1892:
The completeness of this (and other) calculi heavily relies on using formulas which are not sentences (whether they are considered valid standalone propositions or not), in the same way as I used it in the modus ponens example above. I wonder whether you know a calculus for free logic approaching the
1922:
make sense if used as a basis for a theory which genuinely needs empty models, but that is not the case of set theory. All the trouble necessary to modify the usual logic only serves to justify another complication, viz. addition of an axiom. More precisely, it is even worse: it's purpose is so that
184:
implicitly assume that something exists. However, I consider them to be wrong, a hang-over from the days when "For all" was assumed to imply "Some". What about a model whose universe is the empty set? It contains no elements. So your version of logic would disallow it. But I see no reason to exclude
2402:
It depends on how the theory is formulated, and what theory we are talking about. In some theories there are sets and classes and, while one can prove there is a class from FOL alone, one cannot use this to prove there is a set. (I believe
Mendelson's version of NBG is like this.) As such one needs
2169:
ZFC is a particular set of axioms in first-order logic. The language for these axioms has only one type of variable, and thus each interpretation (model) has only one type of object. The jargon for this is that ZFC is a "single sorted" theory. This is what is meant by saying there is only "one type
198:
It's the other way around. The "axiom" of empty set is a hang-over from early 20th century, when the now familiar logic was not yet spelled out formally. Empty models are disallowed for good reasons, their presence instantly breaks too many things to be worth the trouble, such as modus ponens, the
2047:
What does it mean to say that ZFC has only type of object? Do you mean that its intended interpretation includes only one type of object? True, but ZFC does not demand this. The point is this. None of the non-existential axioms of ZFC entail that there exists a set. Moreover, Infinity entails the
2231:
first-order theory with equality, including the empty theory. The other option, "free logic", would not include that existence axiom as a logical principle. But free logic is not commonly used in the literature, because for example free logic does not validate typical deduction rules such as the
1997:": This may be true in principle, but this assumption is built in the most common axiomatic set theories like ZFC. For example, ZFC is a theory in single-sorted first-order logic, and as such it has only one type of objects. These objects are informally called "sets" for clarity. The statement
2146:
If in ZFC-minus-existential-axioms one could already prove the existence of a set from the bare resources of FOL alone, all these brilliant set theorists keen on theoretical economy would not go out of their way to redundantly postulate as axiom the existence of a set.
264:
find erroneous, but what is accepted as standard by the mathematical community. Every single book on set theory I am aware of declares the background logic to be the first-order classical logic with equality. I've never seen any reference formulating set theory in the
2558:
want to call some things βsetsβ in ZFC, you first need to make sure that your βsetsβ are defined by a formula in the above language). Regardless of any interpretation, it is a purely syntactic fact that in first-order predicate calculus in this language, the sentence
1947:
The now very old discussion above is confused. First-order set theory is based on first-order logic which proves the existence of at least one thing. Proof. Let T be a validity. Then by existential generalization (derivable or taken as primitive),
2553:
are any two of a countable list of object variables. Nothing more. It is customary to call the objects for which these variables stand for βsetsβ, but it does not really matter, you can call them any other way you like (but if you do, and if you
1051:
I rewrote the last paragraph of the article in a way which acknowledges the possibility that logic could force the existence of some set. But since some set theories may not have separation as an axiom schema, empty set may still be required.
2727:
I fail to see how what you wrote about the axiom of infinity has to do with anything. The article already explicitly states that the argument may or may not work depending on the exact formulation of the axiom, which is what you appear to be
2708:
1626:
2816:
That sentence should be stronger, or else removed entirely, because it seems to imply that there are some people who find the existence of an empty set controversial, and axiomatisations of set theory that don't include empty sets.
2135:
1239:
716:
355:
is true in the empty model as are all universally quantified sentences. As for your other claims, "... breaks ... modus ponens, ... prenexing rules, and
Bernays substitution.", I would like to see more explanation.
1863:
884:
1923:
we can say "the axiom is redundant, but that's because of the axiom of infinity, not because of logic". I, for one, find such approach pointless, absurd, and confusing. But I am a logician, not a set theorist. --
1722:
441:
353:
2318:
1312:
1813:
1013:
493:
249:
1774:
2610:
1665:
781:
1062:
I regard formulas with free variables as either a short-hand for a sentence (probably with extra universal quantifiers) or as not well-formed. Since you are not saying what the free variable
1127:
140:
1540:
Treating formulas with free variables as not well-formed or incomplete makes sense. However, the point is that classical logic is described by simple and elegant calculi, such as this one:
548:
2752:
I agree, it depends on how the theory is formulated. This much should be made clear when it is said that ZFC implies the existence of at least one set from the resources of FOL alone.
961:
1491:
1425:
616:
2029:
2371:
2225:
1972:
2473:
2450:
1886:
1033:
2499:
2621:
2551:
2525:
1545:
2813:"The axiom of empty set is generally considered uncontroversial, and it or an equivalent appears in just about any alternative axiomatisation of set theory."
2840:
2051:
130:
1132:
2835:
1938:
deduction and it would be too much (and inappropriate) to describe it on this talk page. And putting it in an article would violate the policy on OR.
1527:
Prenexing: no, it is not so hard. But it is counterintuitive, and it is contrary to what a typical mathematician learns about the standard logic.
106:
621:
2329:
So even without the axiom of the empty set or the axiom of infinity, the background first-order logic used to formalize ZFC still proves
1819:
805:
1671:
380:
288:
2429:(e/c) I am not talking about any interpretations. The formulas of ZFC are constructed by means of Boolean connectives and quantifiers
2237:
97:
58:
2714:
The first one is how this article defines the axiom of empty set, and the second one is an instance of the schema of separation.
1244:
1780:
966:
446:
202:
1728:
2564:
33:
377:
Validity is affected by adding universal quantifiers in front, that's another (mis)feature of free logic. The schema
1632:
725:
1073:
498:
890:
fails in the empty model. Most of the other prenexing rules fail as well, but I didn't bother to check them all.
571:
be a unary predicate symbol (binary would do all the same, if you want to stick to the language of ZFC). Then
170:, in which the theory is assumed to be formulated. Then existence of an empty set follows from separation. --
21:
914:
166:(like infinity) to conclude that there exists at least object; it is a theorem of the first-order predicate
1452:
1322:
2783:
As already mentioned, there are versions of ZFC with urelements (Suppes), so it's not completely clear.
39:
574:
83:
1514:
different regardless of what I want, because ZFC proves the existence of a set in one way or another.
2183:
The first-order logic that is usually studied (and which is usually used to formalize ZFC) includes
2788:
2757:
2408:
2152:
2000:
1983:
105:
on
Knowledge. If you would like to participate, please visit the project page, where you can join
1446:
89:
2703:{\displaystyle \forall x\,\exists y\,\forall z\,(z\in y\leftrightarrow z\in x\land \neg (z=z)).}
2332:
2186:
73:
52:
1951:
2455:
2432:
1621:{\displaystyle (\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))}
181:
1871:
1018:
2478:
2732:
2035:
2530:
2504:
722:
formula with at least one free variable holds in the empty model). However, the formula
2784:
2753:
2404:
2148:
1979:
1939:
1494:
1433:
1053:
357:
186:
2829:
2773:
2380:
2130:{\displaystyle \exists X\exists Y(X\in Y\land \forall Z(Z\in Y\to Z\cup \{Z\}\in Y)}
1493:, as for plain quantifiers, then you must include the empty model as a valid model.
1234:{\displaystyle \forall x((P(x)\lor \neg P(x))\to \exists y\,(P(y)\lor \neg P(y)))}
2766:
But that claim is completely clear, because it is only talking about ZFC. βΒ Carl
1432:
And since free variables are invalid, the
Bernays substitution is not a problem.
2818:
102:
2729:
2032:
266:
79:
2821:
2792:
2778:
2761:
2735:
2412:
2385:
2156:
2038:
1987:
1942:
1927:
1497:
1436:
1056:
1039:
360:
273:
189:
174:
2769:
2376:
1319:
Well, you are correct about the prenexing. But is it so hard to just say
1924:
1036:
711:{\displaystyle (P(x)\lor \neg P(x))\to \exists y\,(P(y)\lor \neg P(y))}
270:
171:
1066:
means, then you have an ambiguity which can lead to logical fallacies.
1858:{\displaystyle \varphi \to \psi \vdash \varphi \to \forall x\,\psi ,}
879:{\displaystyle (Q\lor \exists x\,P(x))\equiv \exists x\,(Q\lor P(x))}
1717:{\displaystyle (\neg \varphi \to \neg \psi )\to (\psi \to \varphi )}
1445:
If you want logic to work the same way for relativized quantifiers (
436:{\displaystyle \forall y\,(\forall x\,\varphi (x)\to \varphi (y))}
348:{\displaystyle \forall y((\forall x\,\varphi (x))\to \varphi (y))}
162:
The last paragraph does not make sense. You don't need any fancy
2048:
existence of TWO sets (given
Regularity) if it is formulated as
2313:{\displaystyle \psi \lor (\exists x)\phi (x)\vdash (\exists x)}
1974:
is a theorem. This does not imply the existence of a set/class
1906:
Let's look at the general picture. I am not saying that it is
15:
1241:
are indeed valid. However, from them you can only conclude
1307:{\displaystyle \forall x(\exists y\,(P(y)\lor \neg P(y)))}
1510:
The logic of relativized and unrelativized quantifiers
1808:{\displaystyle \varphi ,\varphi \to \psi \vdash \psi }
2624:
2567:
2533:
2507:
2481:
2458:
2435:
2335:
2240:
2189:
2054:
2003:
1993:
Re "This does not imply the existence of a set/class
1954:
1874:
1822:
1783:
1731:
1674:
1635:
1548:
1455:
1325:
1247:
1135:
1076:
1021:
1008:{\displaystyle \forall x\,\varphi (x)\to \varphi (y)}
969:
917:
808:
728:
624:
577:
501:
488:{\displaystyle \forall x\,\varphi (x)\to \varphi (y)}
449:
383:
291:
244:{\displaystyle \forall x\,\varphi (x)\to \varphi (y)}
205:
1910:
to develop ZFC on top of free logic. However, it is
1769:{\displaystyle \forall x\,\varphi \to \varphi (t/x)}
101:, a collaborative effort to improve the coverage of
2605:{\displaystyle \exists x\,\forall y\,\neg (y\in x)}
2702:
2604:
2545:
2519:
2493:
2467:
2444:
2365:
2312:
2219:
2129:
2023:
1966:
1880:
1857:
1807:
1768:
1716:
1659:
1620:
1485:
1419:
1306:
1233:
1121:
1027:
1007:
955:
878:
775:
710:
610:
542:
487:
435:
347:
243:
1995:unless it is assumed that only sets/classes exist
1976:unless it is assumed that only sets/classes exist
158:Does logic imply the existence of the empty set?
1660:{\displaystyle \varphi \to (\psi \to \varphi )}
776:{\displaystyle \exists y\,(P(y)\lor \neg P(y))}
1122:{\displaystyle \forall x(P(x)\lor \neg P(x))}
8:
2115:
2109:
1468:
1465:
543:{\displaystyle \varphi (y)=\exists z\,(z=z)}
251:, prenexing rules, and Bernays substitution.
185:it. So that version of logic is erroneous.
19:
260:Bear in mind that it does not matter what
47:
2623:
2566:
2532:
2506:
2480:
2457:
2434:
2334:
2239:
2227:as a logical axiom - this is provable in
2188:
2053:
2002:
1953:
1873:
1821:
1782:
1755:
1730:
1673:
1634:
1547:
1454:
1324:
1246:
1134:
1075:
1020:
968:
916:
807:
727:
623:
576:
500:
448:
382:
290:
204:
800:Prenexing: for example, the equivalence
2647:
2639:
2631:
2582:
2574:
2010:
1847:
1738:
1388:
1362:
1263:
1190:
976:
956:{\displaystyle \forall x\,P(x)\to P(y)}
924:
850:
824:
735:
718:are valid in all models (empty or not;
670:
523:
456:
401:
390:
310:
212:
49:
1486:{\displaystyle \forall x\in \{\}P(x)}
550:for instance. Now the other examples.
7:
1420:{\displaystyle \exists w(\top )\to }
95:This article is within the scope of
38:It is of interest to the following
2676:
2641:
2633:
2625:
2584:
2576:
2568:
2459:
2436:
2339:
2277:
2250:
2193:
2082:
2061:
2055:
2004:
1955:
1841:
1732:
1687:
1678:
1456:
1382:
1356:
1335:
1326:
1283:
1257:
1248:
1210:
1184:
1163:
1136:
1101:
1077:
970:
918:
844:
818:
755:
729:
690:
664:
643:
611:{\displaystyle P(x)\lor \neg P(x)}
593:
517:
450:
395:
384:
304:
292:
206:
14:
2841:Low-priority mathematics articles
783:does not hold in the empty model.
115:Knowledge:WikiProject Mathematics
2836:Start-Class mathematics articles
443:is indeed valid, but the schema
118:Template:WikiProject Mathematics
82:
72:
51:
20:
2616:is derivable from the sentence
1035:is not, as explained above. --
135:This article has been rated as
2822:19:34, 25 September 2017 (UTC)
2694:
2691:
2679:
2661:
2649:
2599:
2587:
2360:
2348:
2345:
2336:
2307:
2304:
2298:
2286:
2283:
2274:
2268:
2262:
2256:
2247:
2214:
2202:
2199:
2190:
2124:
2100:
2088:
2067:
2024:{\displaystyle \exists x\,x=x}
1928:18:23, 21 September 2006 (UTC)
1838:
1826:
1793:
1763:
1749:
1743:
1711:
1705:
1699:
1696:
1693:
1684:
1675:
1654:
1648:
1642:
1639:
1615:
1612:
1606:
1600:
1597:
1594:
1588:
1582:
1579:
1576:
1573:
1570:
1564:
1558:
1555:
1549:
1498:09:09, 20 September 2006 (UTC)
1480:
1474:
1437:06:16, 19 September 2006 (UTC)
1414:
1411:
1408:
1402:
1390:
1376:
1373:
1367:
1347:
1344:
1341:
1338:
1332:
1301:
1298:
1295:
1289:
1277:
1271:
1265:
1254:
1228:
1225:
1222:
1216:
1204:
1198:
1192:
1181:
1178:
1175:
1169:
1157:
1151:
1145:
1142:
1116:
1113:
1107:
1095:
1089:
1083:
1057:06:16, 19 September 2006 (UTC)
1040:17:24, 18 September 2006 (UTC)
1002:
996:
990:
987:
981:
950:
944:
938:
935:
929:
873:
870:
864:
852:
838:
835:
829:
809:
770:
767:
761:
749:
743:
737:
705:
702:
696:
684:
678:
672:
661:
658:
655:
649:
637:
631:
625:
605:
599:
587:
581:
537:
525:
511:
505:
482:
476:
470:
467:
461:
430:
427:
421:
415:
412:
406:
392:
361:02:57, 18 September 2006 (UTC)
342:
339:
333:
327:
324:
321:
315:
301:
298:
274:16:12, 16 September 2006 (UTC)
238:
232:
226:
223:
217:
190:04:17, 16 September 2006 (UTC)
1:
963:is valid, whereas the schema
109:and see a list of open tasks.
2793:16:16, 25 October 2012 (UTC)
2779:14:56, 25 October 2012 (UTC)
2762:14:34, 25 October 2012 (UTC)
2736:13:52, 25 October 2012 (UTC)
2413:14:18, 25 October 2012 (UTC)
2386:13:34, 25 October 2012 (UTC)
2157:12:54, 25 October 2012 (UTC)
2039:11:49, 25 October 2012 (UTC)
1988:09:24, 25 October 2012 (UTC)
2366:{\displaystyle (\exists x)}
2220:{\displaystyle (\exists x)}
1943:09:12, 1 October 2006 (UTC)
911:is a unary predicate, then
269:, as you would want it. --
175:21:51, 17 August 2005 (UTC)
2857:
1967:{\displaystyle \exists xT}
2468:{\displaystyle \forall x}
2445:{\displaystyle \exists x}
907:Bernays substitution: if
134:
67:
46:
1881:{\displaystyle \varphi }
1028:{\displaystyle \varphi }
141:project's priority scale
1916:gratuitous complication
1893:simplicity of this one.
1015:for arbitrary formulas
495:generally is not. Take
98:WikiProject Mathematics
2704:
2606:
2547:
2521:
2495:
2494:{\displaystyle x\in y}
2469:
2446:
2367:
2314:
2221:
2131:
2025:
1968:
1882:
1859:
1809:
1770:
1718:
1661:
1622:
1487:
1421:
1308:
1235:
1123:
1029:
1009:
957:
880:
777:
712:
612:
544:
489:
437:
349:
245:
28:This article is rated
2705:
2607:
2548:
2522:
2496:
2475:from atomic formulas
2470:
2447:
2368:
2315:
2222:
2132:
2026:
1969:
1883:
1860:
1810:
1771:
1719:
1662:
1623:
1488:
1422:
1309:
1236:
1124:
1030:
1010:
958:
881:
778:
713:
613:
545:
490:
438:
350:
246:
2622:
2565:
2531:
2505:
2479:
2456:
2433:
2333:
2238:
2187:
2052:
2001:
1952:
1872:
1820:
1781:
1729:
1672:
1633:
1546:
1453:
1323:
1245:
1133:
1074:
1019:
967:
915:
806:
726:
622:
575:
499:
447:
381:
289:
203:
121:mathematics articles
2546:{\displaystyle x,y}
2520:{\displaystyle x=y}
1447:bounded quantifiers
2700:
2648:
2640:
2632:
2602:
2583:
2575:
2543:
2517:
2491:
2465:
2442:
2363:
2310:
2217:
2170:of object" in ZFC.
2127:
2021:
2011:
1964:
1878:
1855:
1848:
1805:
1766:
1739:
1714:
1657:
1618:
1483:
1417:
1389:
1363:
1304:
1264:
1231:
1191:
1119:
1025:
1005:
977:
953:
925:
876:
851:
825:
773:
736:
708:
671:
608:
567:Modus ponens: let
540:
524:
485:
457:
433:
402:
391:
345:
311:
241:
213:
90:Mathematics portal
34:content assessment
2777:
2384:
182:First-order logic
180:Some versions of
155:
154:
151:
150:
147:
146:
2848:
2809:Uncontroversial?
2767:
2709:
2707:
2706:
2701:
2611:
2609:
2608:
2603:
2552:
2550:
2549:
2544:
2526:
2524:
2523:
2518:
2500:
2498:
2497:
2492:
2474:
2472:
2471:
2466:
2451:
2449:
2448:
2443:
2374:
2372:
2370:
2369:
2364:
2324:is not free in Ο
2319:
2317:
2316:
2311:
2226:
2224:
2223:
2218:
2136:
2134:
2133:
2128:
2030:
2028:
2027:
2022:
1973:
1971:
1970:
1965:
1887:
1885:
1884:
1879:
1864:
1862:
1861:
1856:
1814:
1812:
1811:
1806:
1775:
1773:
1772:
1767:
1759:
1723:
1721:
1720:
1715:
1666:
1664:
1663:
1658:
1627:
1625:
1624:
1619:
1492:
1490:
1489:
1484:
1426:
1424:
1423:
1418:
1313:
1311:
1310:
1305:
1240:
1238:
1237:
1232:
1128:
1126:
1125:
1120:
1034:
1032:
1031:
1026:
1014:
1012:
1011:
1006:
962:
960:
959:
954:
885:
883:
882:
877:
782:
780:
779:
774:
717:
715:
714:
709:
617:
615:
614:
609:
549:
547:
546:
541:
494:
492:
491:
486:
442:
440:
439:
434:
354:
352:
351:
346:
250:
248:
247:
242:
199:intuitive axiom
123:
122:
119:
116:
113:
92:
87:
86:
76:
69:
68:
63:
55:
48:
31:
25:
24:
16:
2856:
2855:
2851:
2850:
2849:
2847:
2846:
2845:
2826:
2825:
2811:
2620:
2619:
2563:
2562:
2529:
2528:
2503:
2502:
2477:
2476:
2454:
2453:
2431:
2430:
2331:
2330:
2236:
2235:
2185:
2184:
2050:
2049:
1999:
1998:
1950:
1949:
1870:
1869:
1818:
1817:
1779:
1778:
1727:
1726:
1670:
1669:
1631:
1630:
1544:
1543:
1451:
1450:
1321:
1320:
1243:
1242:
1131:
1130:
1072:
1071:
1017:
1016:
965:
964:
913:
912:
804:
803:
724:
723:
620:
619:
573:
572:
497:
496:
445:
444:
379:
378:
287:
286:
201:
200:
160:
120:
117:
114:
111:
110:
88:
81:
61:
32:on Knowledge's
29:
12:
11:
5:
2854:
2852:
2844:
2843:
2838:
2828:
2827:
2810:
2807:
2806:
2805:
2804:
2803:
2802:
2801:
2800:
2799:
2798:
2797:
2796:
2795:
2743:
2742:
2741:
2740:
2739:
2738:
2720:
2719:
2718:
2717:
2716:
2715:
2712:
2711:
2710:
2699:
2696:
2693:
2690:
2687:
2684:
2681:
2678:
2675:
2672:
2669:
2666:
2663:
2660:
2657:
2654:
2651:
2646:
2643:
2638:
2635:
2630:
2627:
2614:
2613:
2612:
2601:
2598:
2595:
2592:
2589:
2586:
2581:
2578:
2573:
2570:
2542:
2539:
2536:
2516:
2513:
2510:
2490:
2487:
2484:
2464:
2461:
2441:
2438:
2422:
2421:
2420:
2419:
2418:
2417:
2416:
2415:
2393:
2392:
2391:
2390:
2389:
2388:
2362:
2359:
2356:
2353:
2350:
2347:
2344:
2341:
2338:
2327:
2326:
2325:
2309:
2306:
2303:
2300:
2297:
2294:
2291:
2288:
2285:
2282:
2279:
2276:
2273:
2270:
2267:
2264:
2261:
2258:
2255:
2252:
2249:
2246:
2243:
2216:
2213:
2210:
2207:
2204:
2201:
2198:
2195:
2192:
2176:
2175:
2174:
2173:
2172:
2171:
2162:
2161:
2160:
2159:
2141:
2140:
2139:
2138:
2126:
2123:
2120:
2117:
2114:
2111:
2108:
2105:
2102:
2099:
2096:
2093:
2090:
2087:
2084:
2081:
2078:
2075:
2072:
2069:
2066:
2063:
2060:
2057:
2042:
2041:
2020:
2017:
2014:
2009:
2006:
1963:
1960:
1957:
1935:
1934:
1933:
1932:
1931:
1930:
1914:, and it is a
1899:
1898:
1897:
1896:
1895:
1894:
1890:
1889:
1888:
1877:
1854:
1851:
1846:
1843:
1840:
1837:
1834:
1831:
1828:
1825:
1815:
1804:
1801:
1798:
1795:
1792:
1789:
1786:
1776:
1765:
1762:
1758:
1754:
1751:
1748:
1745:
1742:
1737:
1734:
1724:
1713:
1710:
1707:
1704:
1701:
1698:
1695:
1692:
1689:
1686:
1683:
1680:
1677:
1667:
1656:
1653:
1650:
1647:
1644:
1641:
1638:
1628:
1617:
1614:
1611:
1608:
1605:
1602:
1599:
1596:
1593:
1590:
1587:
1584:
1581:
1578:
1575:
1572:
1569:
1566:
1563:
1560:
1557:
1554:
1551:
1533:
1532:
1531:
1530:
1529:
1528:
1520:
1519:
1518:
1517:
1516:
1515:
1503:
1502:
1501:
1500:
1482:
1479:
1476:
1473:
1470:
1467:
1464:
1461:
1458:
1440:
1439:
1429:
1428:
1416:
1413:
1410:
1407:
1404:
1401:
1398:
1395:
1392:
1387:
1384:
1381:
1378:
1375:
1372:
1369:
1366:
1361:
1358:
1355:
1352:
1349:
1346:
1343:
1340:
1337:
1334:
1331:
1328:
1316:
1315:
1303:
1300:
1297:
1294:
1291:
1288:
1285:
1282:
1279:
1276:
1273:
1270:
1267:
1262:
1259:
1256:
1253:
1250:
1230:
1227:
1224:
1221:
1218:
1215:
1212:
1209:
1206:
1203:
1200:
1197:
1194:
1189:
1186:
1183:
1180:
1177:
1174:
1171:
1168:
1165:
1162:
1159:
1156:
1153:
1150:
1147:
1144:
1141:
1138:
1118:
1115:
1112:
1109:
1106:
1103:
1100:
1097:
1094:
1091:
1088:
1085:
1082:
1079:
1068:
1067:
1049:
1048:
1047:
1046:
1045:
1044:
1043:
1042:
1024:
1004:
1001:
998:
995:
992:
989:
986:
983:
980:
975:
972:
952:
949:
946:
943:
940:
937:
934:
931:
928:
923:
920:
898:
897:
896:
895:
894:
893:
892:
891:
888:
887:
886:
875:
872:
869:
866:
863:
860:
857:
854:
849:
846:
843:
840:
837:
834:
831:
828:
823:
820:
817:
814:
811:
791:
790:
789:
788:
787:
786:
785:
784:
772:
769:
766:
763:
760:
757:
754:
751:
748:
745:
742:
739:
734:
731:
707:
704:
701:
698:
695:
692:
689:
686:
683:
680:
677:
674:
669:
666:
663:
660:
657:
654:
651:
648:
645:
642:
639:
636:
633:
630:
627:
607:
604:
601:
598:
595:
592:
589:
586:
583:
580:
558:
557:
556:
555:
554:
553:
552:
551:
539:
536:
533:
530:
527:
522:
519:
516:
513:
510:
507:
504:
484:
481:
478:
475:
472:
469:
466:
463:
460:
455:
452:
432:
429:
426:
423:
420:
417:
414:
411:
408:
405:
400:
397:
394:
389:
386:
368:
367:
366:
365:
364:
363:
344:
341:
338:
335:
332:
329:
326:
323:
320:
317:
314:
309:
306:
303:
300:
297:
294:
279:
278:
277:
276:
255:
254:
253:
252:
240:
237:
234:
231:
228:
225:
222:
219:
216:
211:
208:
193:
192:
159:
156:
153:
152:
149:
148:
145:
144:
133:
127:
126:
124:
107:the discussion
94:
93:
77:
65:
64:
56:
44:
43:
37:
26:
13:
10:
9:
6:
4:
3:
2:
2853:
2842:
2839:
2837:
2834:
2833:
2831:
2824:
2823:
2820:
2814:
2808:
2794:
2790:
2786:
2782:
2781:
2780:
2775:
2771:
2765:
2764:
2763:
2759:
2755:
2751:
2750:
2749:
2748:
2747:
2746:
2745:
2744:
2737:
2734:
2731:
2726:
2725:
2724:
2723:
2722:
2721:
2713:
2697:
2688:
2685:
2682:
2673:
2670:
2667:
2664:
2658:
2655:
2652:
2644:
2636:
2628:
2618:
2617:
2615:
2596:
2593:
2590:
2579:
2571:
2561:
2560:
2557:
2540:
2537:
2534:
2514:
2511:
2508:
2488:
2485:
2482:
2462:
2439:
2428:
2427:
2426:
2425:
2424:
2423:
2414:
2410:
2406:
2401:
2400:
2399:
2398:
2397:
2396:
2395:
2394:
2387:
2382:
2378:
2357:
2354:
2351:
2342:
2328:
2323:
2301:
2295:
2292:
2289:
2280:
2271:
2265:
2259:
2253:
2244:
2241:
2234:
2233:
2230:
2211:
2208:
2205:
2196:
2182:
2181:
2180:
2179:
2178:
2177:
2168:
2167:
2166:
2165:
2164:
2163:
2158:
2154:
2150:
2145:
2144:
2143:
2142:
2121:
2118:
2112:
2106:
2103:
2097:
2094:
2091:
2085:
2079:
2076:
2073:
2070:
2064:
2058:
2046:
2045:
2044:
2043:
2040:
2037:
2034:
2018:
2015:
2012:
2007:
1996:
1992:
1991:
1990:
1989:
1985:
1981:
1977:
1961:
1958:
1945:
1944:
1941:
1929:
1926:
1921:
1917:
1913:
1909:
1905:
1904:
1903:
1902:
1901:
1900:
1891:
1875:
1867:
1852:
1849:
1844:
1835:
1832:
1829:
1823:
1816:
1802:
1799:
1796:
1790:
1787:
1784:
1777:
1760:
1756:
1752:
1746:
1740:
1735:
1725:
1708:
1702:
1690:
1681:
1668:
1651:
1645:
1636:
1629:
1609:
1603:
1591:
1585:
1567:
1561:
1552:
1542:
1541:
1539:
1538:
1537:
1536:
1535:
1534:
1526:
1525:
1524:
1523:
1522:
1521:
1513:
1509:
1508:
1507:
1506:
1505:
1504:
1499:
1496:
1477:
1471:
1462:
1459:
1448:
1444:
1443:
1442:
1441:
1438:
1435:
1431:
1430:
1405:
1399:
1396:
1393:
1385:
1379:
1370:
1364:
1359:
1353:
1350:
1329:
1318:
1317:
1292:
1286:
1280:
1274:
1268:
1260:
1251:
1219:
1213:
1207:
1201:
1195:
1187:
1172:
1166:
1160:
1154:
1148:
1139:
1110:
1104:
1098:
1092:
1086:
1080:
1070:
1069:
1065:
1061:
1060:
1059:
1058:
1055:
1041:
1038:
1022:
999:
993:
984:
978:
973:
947:
941:
932:
926:
921:
910:
906:
905:
904:
903:
902:
901:
900:
899:
889:
867:
861:
858:
855:
847:
841:
832:
826:
821:
815:
812:
802:
801:
799:
798:
797:
796:
795:
794:
793:
792:
764:
758:
752:
746:
740:
732:
721:
699:
693:
687:
681:
675:
667:
652:
646:
640:
634:
628:
602:
596:
590:
584:
578:
570:
566:
565:
564:
563:
562:
561:
560:
559:
534:
531:
528:
520:
514:
508:
502:
479:
473:
464:
458:
453:
424:
418:
409:
403:
398:
387:
376:
375:
374:
373:
372:
371:
370:
369:
362:
359:
336:
330:
318:
312:
307:
295:
285:
284:
283:
282:
281:
280:
275:
272:
268:
263:
259:
258:
257:
256:
235:
229:
220:
214:
209:
197:
196:
195:
194:
191:
188:
183:
179:
178:
177:
176:
173:
169:
165:
157:
142:
138:
132:
129:
128:
125:
108:
104:
100:
99:
91:
85:
80:
78:
75:
71:
70:
66:
60:
57:
54:
50:
45:
41:
35:
27:
23:
18:
17:
2815:
2812:
2555:
2321:
2228:
1994:
1975:
1946:
1936:
1919:
1915:
1911:
1907:
1868:not free in
1865:
1511:
1063:
1050:
908:
719:
568:
261:
167:
163:
161:
137:Low-priority
136:
96:
62:Lowβpriority
40:WikiProjects
1912:nonstandard
112:Mathematics
103:mathematics
59:Mathematics
30:Start-class
2830:Categories
1908:impossible
267:free logic
2785:Nortexoid
2754:Nortexoid
2405:Nortexoid
2149:Nortexoid
1980:Nortexoid
1940:JRSpriggs
1495:JRSpriggs
1434:JRSpriggs
1054:JRSpriggs
358:JRSpriggs
187:JRSpriggs
2728:saying.β
2527:, where
1449:), e.g.
1427:instead?
139:on the
2819:Zemyla
2232:rule:
36:scale.
2320:when
2229:every
1920:would
1918:. It
720:every
168:logic
164:axiom
2789:talk
2774:talk
2758:talk
2730:Emil
2556:also
2409:talk
2381:talk
2153:talk
2033:Emil
1984:talk
1129:and
618:and
2770:CBM
2377:CBM
262:you
131:Low
2832::
2791:)
2772:Β·
2760:)
2733:J.
2677:Β¬
2674:β§
2668:β
2662:β
2656:β
2642:β
2634:β
2626:β
2594:β
2585:Β¬
2577:β
2569:β
2501:,
2486:β
2460:β
2452:,
2437:β
2411:)
2379:Β·
2340:β
2296:Ο
2293:β¨
2290:Ο
2278:β
2272:β’
2260:Ο
2251:β
2245:β¨
2242:Ο
2194:β
2155:)
2119:β
2107:βͺ
2101:β
2095:β
2083:β
2080:β§
2074:β
2062:β
2056:β
2036:J.
2005:β
1986:)
1956:β
1925:EJ
1876:Ο
1850:Ο
1842:β
1839:β
1836:Ο
1833:β’
1830:Ο
1827:β
1824:Ο
1803:Ο
1800:β’
1797:Ο
1794:β
1791:Ο
1785:Ο
1747:Ο
1744:β
1741:Ο
1733:β
1709:Ο
1706:β
1703:Ο
1697:β
1691:Ο
1688:Β¬
1685:β
1682:Ο
1679:Β¬
1652:Ο
1649:β
1646:Ο
1640:β
1637:Ο
1610:Ο
1607:β
1604:Ο
1598:β
1592:Ο
1589:β
1586:Ο
1577:β
1568:Ο
1565:β
1562:Ο
1556:β
1553:Ο
1512:is
1463:β
1457:β
1397:β¨
1383:β
1380:β‘
1357:β
1354:β¨
1342:β
1336:β€
1327:β
1284:Β¬
1281:β¨
1258:β
1249:β
1211:Β¬
1208:β¨
1185:β
1182:β
1164:Β¬
1161:β¨
1137:β
1102:Β¬
1099:β¨
1078:β
1037:EJ
1023:Ο
994:Ο
991:β
979:Ο
971:β
939:β
919:β
859:β¨
845:β
842:β‘
819:β
816:β¨
756:Β¬
753:β¨
730:β
691:Β¬
688:β¨
665:β
662:β
644:Β¬
641:β¨
594:Β¬
591:β¨
518:β
503:Ο
474:Ο
471:β
459:Ο
451:β
419:Ο
416:β
404:Ο
396:β
385:β
331:Ο
328:β
313:Ο
305:β
293:β
271:EJ
230:Ο
227:β
215:Ο
207:β
172:EJ
2787:(
2776:)
2768:(
2756:(
2698:.
2695:)
2692:)
2689:z
2686:=
2683:z
2680:(
2671:x
2665:z
2659:y
2653:z
2650:(
2645:z
2637:y
2629:x
2600:)
2597:x
2591:y
2588:(
2580:y
2572:x
2541:y
2538:,
2535:x
2515:y
2512:=
2509:x
2489:y
2483:x
2463:x
2440:x
2407:(
2383:)
2375:(
2361:]
2358:x
2355:=
2352:x
2349:[
2346:)
2343:x
2337:(
2322:x
2308:]
2305:)
2302:x
2299:(
2287:[
2284:)
2281:x
2275:(
2269:)
2266:x
2263:(
2257:)
2254:x
2248:(
2215:]
2212:x
2209:=
2206:x
2203:[
2200:)
2197:x
2191:(
2151:(
2125:)
2122:Y
2116:}
2113:Z
2110:{
2104:Z
2098:Y
2092:Z
2089:(
2086:Z
2077:Y
2071:X
2068:(
2065:Y
2059:X
2019:x
2016:=
2013:x
2008:x
1982:(
1962:T
1959:x
1866:x
1853:,
1845:x
1788:,
1764:)
1761:x
1757:/
1753:t
1750:(
1736:x
1712:)
1700:(
1694:)
1676:(
1655:)
1643:(
1616:)
1613:)
1601:(
1595:)
1583:(
1580:(
1574:)
1571:)
1559:(
1550:(
1481:)
1478:x
1475:(
1472:P
1469:}
1466:{
1460:x
1415:]
1412:)
1409:)
1406:x
1403:(
1400:P
1394:Q
1391:(
1386:x
1377:)
1374:)
1371:x
1368:(
1365:P
1360:x
1351:Q
1348:(
1345:[
1339:)
1333:(
1330:w
1314:.
1302:)
1299:)
1296:)
1293:y
1290:(
1287:P
1278:)
1275:y
1272:(
1269:P
1266:(
1261:y
1255:(
1252:x
1229:)
1226:)
1223:)
1220:y
1217:(
1214:P
1205:)
1202:y
1199:(
1196:P
1193:(
1188:y
1179:)
1176:)
1173:x
1170:(
1167:P
1158:)
1155:x
1152:(
1149:P
1146:(
1143:(
1140:x
1117:)
1114:)
1111:x
1108:(
1105:P
1096:)
1093:x
1090:(
1087:P
1084:(
1081:x
1064:x
1003:)
1000:y
997:(
988:)
985:x
982:(
974:x
951:)
948:y
945:(
942:P
936:)
933:x
930:(
927:P
922:x
909:P
874:)
871:)
868:x
865:(
862:P
856:Q
853:(
848:x
839:)
836:)
833:x
830:(
827:P
822:x
813:Q
810:(
771:)
768:)
765:y
762:(
759:P
750:)
747:y
744:(
741:P
738:(
733:y
706:)
703:)
700:y
697:(
694:P
685:)
682:y
679:(
676:P
673:(
668:y
659:)
656:)
653:x
650:(
647:P
638:)
635:x
632:(
629:P
626:(
606:)
603:x
600:(
597:P
588:)
585:x
582:(
579:P
569:P
538:)
535:z
532:=
529:z
526:(
521:z
515:=
512:)
509:y
506:(
483:)
480:y
477:(
468:)
465:x
462:(
454:x
431:)
428:)
425:y
422:(
413:)
410:x
407:(
399:x
393:(
388:y
343:)
340:)
337:y
334:(
325:)
322:)
319:x
316:(
308:x
302:(
299:(
296:y
239:)
236:y
233:(
224:)
221:x
218:(
210:x
143:.
42::
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
