84:
74:
53:
1228:
metamathematics of Q. For example, ST is essentially undecidable because Q is, and every consistent theory whose theorems include the ST axioms is also essentially undecidable. This includes GST and every axiomatic set theory worth thinking about, assuming these are consistent. In fact, the undecidability of ST implies the undecidability of first-order logic with a single binary predicate letter.
22:
1233:
going to be about the surprising power of ST, rather than that of GST. And of course there needs to be some justification, or at least mention, of the fact that anything that can be done with ST can still be done if you replace empty set with the axiom schema of separation, not just left for people to guess.
247:
When nonempty domain is not a pre-assumption, Separation alone cannot assert the existence of the empty set directly. The articles "Axiom of empty set" and "Zermelo–Fraenkel set theory" give detailed account on this aspect. I prefer to spell it out as a non-logical axiom as I cannot verify that it is
659:
Carl, what you call an axiom of logic strikes me as an assertion that the domain is nonempty. No problem in this corner, as the logic of empty domains ("free" logic) has always struck me as vacuous, pedantic, and uninteresting. Your assumption is part of the bare minimum needed to get mathematics up
162:
Maybe it's just me, but i think the axiom of separation assures the existence of the empty set *if a set already exists*. None of these axioms assures the existence of any set, since their first quantifier is universal, so they suppose a set already exists. It must be just me anyway, because i can't
1232:
There is no mention of ST anywhere before this in the article. Maybe ST is
Burgess's equivalent of Tarski's S', mentioned later in the article as "GST with Empty Set replacing the axiom schema of specification"? But if so, it needs to be mentioned earlier. Especially if so much of this article is
921:
And even if they could be counted, what one would probably be interested in is the depth of quantifier alternation, not the mere number of quantifiers. I have a vague sense that counting existential quantifiers in this way is a Boolos-ism. I have seen other articles where editors, not aware that
1227:
The most remarkable fact about ST (and hence GST), is that these tiny fragments of set theory give rise to such rich metamathematics. While ST is a small fragment of the well-known canonical set theories ZFC and NBG, ST interprets
Robinson arithmetic (Q), so that ST inherits the nontrivial
633:
section). Thus set existence is asserted! Additional existential axiom is not needed with such a pre-assumption. One way to formalize such a pre-assumption is by choosing a suitable proof system, e.g., sequent calculus chosen by Emil
502:
624:
677:
The article said that there were only two existential quantifiers in the three axioms. This is incorrect. The property φ may contain some existential quantifiers. Furthermore, the axiom of extensionality
626:. If the empty domain is under consideration, it is better not to use a calculus with such a pre-assumption. Back to the question by Spiritofhere, I would like to summarize my understanding as follow:
761:
907:
It's patently absurd to count quantifiers when neither theory can be finitely axiomatized. Both GST and ZF use and require infinitely many quantifiers, not two, three, seven, or what have you. —
1205:
140:
888:
1236:
Because I'm only _guessing_ that this is what ST refers to, I don't want to edit the article in a possibly incorrect way; someone who actually knows what's intended needs to fix it. --
1010:
411:
322:
284:
209:
236:) be always false. Starting from the empty set, Adjunction assures the existence, by elementary recursion, of the sets needed for von Neumann's ordinals and Peano arithmetic.
1156:
540:
1089:
1059:
570:
Thanks again Emil J. Your explanation makes me clear about a subtle but important property of many proof cacluli. Many of them pre-assume a non-empty domain, i.e.,
348:
1030:
163:
imagine that GST would be mentinned if it really had the flaw of reasoning on entities while being unable to prove their existence... i'm still puzzled, though.
442:
1264:
130:
286:
as an axiom. Quite the contrary, a number of proof systems, e.g., Hilbert-style, Tait-style and sequent calculi, take the universal counterpart, i.e.,
1259:
106:
1237:
1209:
573:
97:
58:
684:
33:
1204:
GST does not seem to include any induction- or foundation-like axiom (scheme), how does it interpret Peano
Arithmetic?
232:
Separation assures the existence of an empty set in GST in the same way that existence is assured in ZF. Just let φ(
772:
922:
Boolos was writing in a abbreviated way, misinterpreted what he was saying. Maybe that is the case here. — Carl
1241:
350:
as an axiom (of equality). Taking non-empty domain assumption as done in this article is also acceptable to me.
421:
in usual formalisms of first-order logic. (I'm sure that's what Carl meant.) For example, in sequent calculus:
21:
1187:
1108:
644:
355:
39:
164:
83:
968:
948:
897:
378:
289:
251:
176:
105:
on
Knowledge. If you would like to participate, please visit the project page, where you can join
661:
630:
89:
1129:
73:
52:
525:
1183:
1174:
1104:
1068:
911:
640:
546:
351:
1035:
327:
944:
893:
1015:
497:{\displaystyle {\frac {\longrightarrow x=x\qquad }{\longrightarrow \exists x\,(x=x)}}}
1253:
929:
218:
102:
1171:
908:
543:
79:
1118:
You apparently misunderstand the adjunction axiom. It says that for any sets
1245:
1213:
1191:
1177:
1112:
952:
934:
914:
901:
664:
648:
549:
359:
223:
167:
925:
766:
contains an existential quantifier because it is logically equivalent to
214:
629:
In this article, non-empty domain is preassumed (and stated in the
1012:. However, I didn't understand why "Adjunction implies that if
619:{\displaystyle \forall x\varphi (x)\vdash \exists x\varphi (x)}
522:
The first line is an axiom of equality, the second line is an
173:
I am not familiar with Boolos' work, but it is common to take
15:
943:
To EmilJ: Thank you for fixing many errors in this article.
211:
as an axiom of logic. Perhaps that is the case here. — Carl
1132:
1071:
1038:
1018:
971:
775:
687:
576:
528:
445:
381:
330:
292:
254:
179:
756:{\displaystyle \forall x\forall y\rightarrow x=y]\,}
101:, a collaborative effort to improve the coverage of
1103:. None of the 3 axioms does that. What did I miss?
1150:
1083:
1053:
1024:
1004:
882:
755:
618:
534:
496:
405:
342:
316:
278:
203:
965:The article discusses the successor function
248:common to take the existential sentence take
8:
1145:
1139:
1078:
1072:
999:
993:
883:{\displaystyle \forall x\forall y\lor )]\,.}
19:
47:
1131:
1070:
1037:
1017:
970:
774:
686:
575:
527:
446:
444:
380:
329:
291:
253:
178:
875:
751:
474:
324:or the related quantifier-free formula
49:
1182:Thanks. Indeed, I misread the Axiom. —
1206:2003:C5:8F16:A154:4970:6F4A:E249:2A4E
7:
413:is usually not taken directly as an
95:This article is within the scope of
1099:assert that. In GST, we don't have
961:Problem with the successor function
38:It is of interest to the following
803:
782:
776:
703:
694:
688:
598:
577:
529:
468:
382:
293:
255:
180:
14:
1265:Low-priority mathematics articles
1223:In the Peano Arithmetic section:
115:Knowledge:WikiProject Mathematics
1260:Start-Class mathematics articles
1005:{\displaystyle S(x)=x\cup \{x\}}
118:Template:WikiProject Mathematics
82:
72:
51:
20:
1158:is also a set. Specialize with
135:This article has been rated as
1048:
1042:
981:
975:
872:
869:
866:
842:
836:
812:
809:
800:
788:
748:
736:
733:
721:
709:
700:
665:06:53, 15 September 2007 (UTC)
613:
607:
592:
586:
488:
476:
465:
449:
406:{\displaystyle \exists x(x=x)}
400:
388:
317:{\displaystyle \forall x(x=x)}
311:
299:
279:{\displaystyle \exists x(x=x)}
273:
261:
204:{\displaystyle \exists x(x=x)}
198:
186:
1:
1246:03:32, 22 December 2020 (UTC)
1214:18:32, 9 September 2020 (UTC)
1192:04:06, 15 November 2010 (UTC)
1178:11:28, 13 November 2010 (UTC)
1113:15:46, 12 November 2010 (UTC)
649:06:36, 15 November 2010 (UTC)
550:15:35, 12 November 2010 (UTC)
461:
360:15:20, 12 November 2010 (UTC)
109:and see a list of open tasks.
673:Third existential quantifier
1151:{\displaystyle x\cup \{y\}}
224:13:00, 10 August 2007 (UTC)
168:09:54, 10 August 2007 (UTC)
1281:
1065:, we need to assert that
134:
67:
46:
1166:to get the successor of
953:08:58, 5 June 2009 (UTC)
935:11:44, 4 June 2009 (UTC)
915:10:27, 4 June 2009 (UTC)
902:02:08, 4 June 2009 (UTC)
535:{\displaystyle \exists }
141:project's priority scale
98:WikiProject Mathematics
1152:
1085:
1055:
1026:
1006:
884:
757:
620:
536:
498:
417:, but it is certainly
407:
344:
318:
280:
205:
28:This article is rated
1153:
1086:
1084:{\displaystyle \{x\}}
1056:
1027:
1007:
885:
758:
621:
537:
499:
408:
345:
319:
281:
206:
1130:
1069:
1054:{\displaystyle S(x)}
1036:
1016:
969:
773:
685:
574:
526:
443:
379:
328:
290:
252:
177:
121:mathematics articles
343:{\displaystyle x=x}
1148:
1091:is a set. In ZFC,
1081:
1051:
1022:
1002:
880:
876:
753:
752:
616:
542:-right inference.—
532:
494:
475:
462:
403:
340:
314:
276:
201:
158:existential axioms
90:Mathematics portal
34:content assessment
1025:{\displaystyle x}
933:
492:
222:
155:
154:
151:
150:
147:
146:
1272:
1200:Peano arithmetic
1157:
1155:
1154:
1149:
1090:
1088:
1087:
1082:
1060:
1058:
1057:
1052:
1032:is a set, so is
1031:
1029:
1028:
1023:
1011:
1009:
1008:
1003:
923:
889:
887:
886:
881:
762:
760:
759:
754:
625:
623:
622:
617:
541:
539:
538:
533:
503:
501:
500:
495:
493:
491:
463:
447:
412:
410:
409:
404:
349:
347:
346:
341:
323:
321:
320:
315:
285:
283:
282:
277:
212:
210:
208:
207:
202:
123:
122:
119:
116:
113:
92:
87:
86:
76:
69:
68:
63:
55:
48:
31:
25:
24:
16:
1280:
1279:
1275:
1274:
1273:
1271:
1270:
1269:
1250:
1249:
1238:157.131.154.133
1221:
1202:
1128:
1127:
1067:
1066:
1034:
1033:
1014:
1013:
967:
966:
963:
771:
770:
683:
682:
675:
572:
571:
524:
523:
464:
448:
441:
440:
377:
376:
326:
325:
288:
287:
250:
249:
175:
174:
160:
120:
117:
114:
111:
110:
88:
81:
61:
32:on Knowledge's
29:
12:
11:
5:
1278:
1276:
1268:
1267:
1262:
1252:
1251:
1230:
1229:
1220:
1217:
1201:
1198:
1197:
1196:
1195:
1194:
1147:
1144:
1141:
1138:
1135:
1080:
1077:
1074:
1050:
1047:
1044:
1041:
1021:
1001:
998:
995:
992:
989:
986:
983:
980:
977:
974:
962:
959:
958:
957:
956:
955:
938:
937:
918:
917:
891:
890:
879:
874:
871:
868:
865:
862:
859:
856:
853:
850:
847:
844:
841:
838:
835:
832:
829:
826:
823:
820:
817:
814:
811:
808:
805:
802:
799:
796:
793:
790:
787:
784:
781:
778:
764:
763:
750:
747:
744:
741:
738:
735:
732:
729:
726:
723:
720:
717:
714:
711:
708:
705:
702:
699:
696:
693:
690:
674:
671:
670:
669:
668:
667:
657:
656:
655:
654:
653:
652:
651:
637:
636:
635:
615:
612:
609:
606:
603:
600:
597:
594:
591:
588:
585:
582:
579:
559:
558:
557:
556:
555:
554:
553:
552:
531:
513:
512:
511:
510:
509:
508:
507:
506:
505:
504:
490:
487:
484:
481:
478:
473:
470:
467:
460:
457:
454:
451:
429:
428:
427:
426:
425:
424:
423:
422:
402:
399:
396:
393:
390:
387:
384:
367:
366:
365:
364:
363:
362:
339:
336:
333:
313:
310:
307:
304:
301:
298:
295:
275:
272:
269:
266:
263:
260:
257:
240:
239:
238:
237:
227:
226:
200:
197:
194:
191:
188:
185:
182:
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:
1277:
1266:
1263:
1261:
1258:
1257:
1255:
1248:
1247:
1243:
1239:
1234:
1226:
1225:
1224:
1218:
1216:
1215:
1211:
1207:
1199:
1193:
1189:
1185:
1181:
1180:
1179:
1176:
1173:
1169:
1165:
1161:
1142:
1136:
1133:
1125:
1121:
1117:
1116:
1115:
1114:
1110:
1106:
1102:
1098:
1094:
1075:
1064:
1061:...". To use
1045:
1039:
1019:
996:
990:
987:
984:
978:
972:
960:
954:
950:
946:
942:
941:
940:
939:
936:
931:
927:
920:
919:
916:
913:
910:
906:
905:
904:
903:
899:
895:
877:
863:
860:
857:
854:
851:
848:
845:
839:
833:
830:
827:
824:
821:
818:
815:
806:
797:
794:
791:
785:
779:
769:
768:
767:
745:
742:
739:
730:
727:
724:
718:
715:
712:
706:
697:
691:
681:
680:
679:
672:
666:
663:
662:202.36.179.65
658:
650:
646:
642:
638:
632:
628:
627:
610:
604:
601:
595:
589:
583:
580:
569:
568:
567:
566:
565:
564:
563:
562:
561:
560:
551:
548:
545:
521:
520:
519:
518:
517:
516:
515:
514:
485:
482:
479:
471:
458:
455:
452:
439:
438:
437:
436:
435:
434:
433:
432:
431:
430:
420:
416:
397:
394:
391:
385:
375:
374:
373:
372:
371:
370:
369:
368:
361:
357:
353:
337:
334:
331:
308:
305:
302:
296:
270:
267:
264:
258:
246:
245:
244:
243:
242:
241:
235:
231:
230:
229:
228:
225:
220:
216:
195:
192:
189:
183:
172:
171:
170:
169:
166:
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:
1235:
1231:
1222:
1203:
1167:
1163:
1159:
1123:
1119:
1100:
1096:
1092:
1062:
964:
892:
765:
676:
660:and running.
418:
414:
233:
165:Spiritofhere
161:
137:Low-priority
136:
96:
62:Low‑priority
40:WikiProjects
112:Mathematics
103:mathematics
59:Mathematics
30:Start-class
1254:Categories
1184:Tomlee2060
1105:Tomlee2060
1097:Separation
1063:Adjunction
641:Tomlee2060
631:discussion
352:Tomlee2060
945:JRSpriggs
894:JRSpriggs
419:provable
1101:Pairing
1093:Pairing
139:on the
36:scale.
415:axiom
1242:talk
1210:talk
1188:talk
1172:Emil
1122:and
1109:talk
1095:and
949:talk
930:talk
909:Emil
898:talk
645:talk
544:Emil
356:talk
219:talk
926:CBM
215:CBM
131:Low
1256::
1244:)
1219:ST
1212:)
1190:)
1175:J.
1170:.—
1162:=
1137:∪
1126:,
1111:)
991:∪
951:)
928:·
912:J.
900:)
861:∈
855:∧
849:∉
840:∨
831:∉
825:∧
819:∈
804:∃
801:→
795:≠
783:∀
777:∀
737:→
728:∈
722:↔
716:∈
704:∀
695:∀
689:∀
647:)
634:J.
605:φ
599:∃
596:⊢
584:φ
578:∀
547:J.
530:∃
469:∃
466:⟶
450:⟶
383:∃
358:)
294:∀
256:∃
217:·
181:∃
1240:(
1208:(
1186:(
1168:x
1164:y
1160:x
1146:}
1143:y
1140:{
1134:x
1124:y
1120:x
1107:(
1079:}
1076:x
1073:{
1049:)
1046:x
1043:(
1040:S
1020:x
1000:}
997:x
994:{
988:x
985:=
982:)
979:x
976:(
973:S
947:(
932:)
924:(
896:(
878:.
873:]
870:)
867:]
864:y
858:z
852:x
846:z
843:[
837:]
834:y
828:z
822:x
816:z
813:[
810:(
807:z
798:y
792:x
789:[
786:y
780:x
749:]
746:y
743:=
740:x
734:]
731:y
725:z
719:x
713:z
710:[
707:z
701:[
698:y
692:x
643:(
639:—
614:)
611:x
608:(
602:x
593:)
590:x
587:(
581:x
489:)
486:x
483:=
480:x
477:(
472:x
459:x
456:=
453:x
401:)
398:x
395:=
392:x
389:(
386:x
354:(
338:x
335:=
332:x
312:)
309:x
306:=
303:x
300:(
297:x
274:)
271:x
268:=
265:x
262:(
259:x
234:x
221:)
213:(
199:)
196:x
193:=
190:x
187:(
184:x
143:.
42::
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
