33:
490:
939:
In the setting of arithmetic, the numerical existence property implies the disjunction property. The proof uses the fact that a disjunction can be rewritten as an existential formula quantifying over natural numbers:
655:
1264:
1157:
1467: (1932) stated without proof that intuitionistic propositional logic (with no additional axioms) has the disjunction property; this result was proven and extended to intuitionistic predicate logic by
278:
588:
353:
1033:
838:
eliminated in favor of the axiom of collection has the disjunction property, the numerical existence property, and the existence property. Michael
Rathjen (2005) proved that
320:
910:
888:
774:
752:
722:
1296:
382:
62:
1388:
1066:
686:
521:
1342:
1408:
1362:
1316:
1181:
1086:
402:
412:
420:
826:
While the earliest results were for constructive theories of arithmetic, many results are also known for constructive set theories (Rathjen 2005).
1475: (1945) proved that Heyting arithmetic has the disjunction property and the existence property. Kleene's method introduced the technique of
1424:, the disjunction property implies the numerical existence property. The proof uses self-referential sentences in way similar to the proof of
1656:
1425:
603:
1633:
1189:
1091:
84:
728:
These properties can only be directly expressed for theories that have the ability to quantify over natural numbers and, for CR
234:
1479:, which is now one of the main methods in the study of constructive theories (Kohlenbach 2008; Troelstra 1973).
131:
45:
890:, is not the join of two proper subobjects. Together with the existence property it translates to the assertion that
530:
55:
49:
41:
1417:
806:
1452:). The bounded formula may then be written as a finite disjunction A(1)∨A(2)∨...∨A(n). Finally,
1421:
814:
797:
while having independent statements does not have the disjunction property. So all classical theories expressing
325:
66:
946:
106:
215:
Rathjen (2005) lists five properties that a theory may possess. These include the disjunction property (
1488:
1453:
114:
1508:
1498:
810:
777:
287:
1651:
1587:, 1973, "Some properties of Intuitionistic Zermelo-Fraenkel set theory", in A. Mathias and H. Rogers,
835:
1472:
798:
893:
871:
757:
735:
691:
1493:
1437:
820:
110:
98:
1272:
861:
358:
1605:
1574:
913:
189:
1367:
1045:
802:
1624:
664:
499:
1628:
1547:
1537:
1527:
1468:
1413:
865:
857:
849:
823:
is well known for having the disjunction property and the (numerical) existence property.
794:
1321:
1393:
1347:
1301:
1166:
1071:
845:
387:
809:
in turn do not validate the existence property either, e.g. because they validate the
1645:
1557:
1503:
1476:
1464:
1567:
Stephen Cole Kleene, 1945, "On the interpretation of intuitionistic number theory,"
1596:
The
Disjunction and Related Properties for Constructive Zermelo-Fraenkel Set Theory
485:{\displaystyle (\forall x\in \mathbb {N} )(\exists y\in \mathbb {N} )\varphi (x,y)}
17:
1584:
921:
827:
1428:. The key step is to find a bound on the existential quantifier in a formula (∃
848:
and
Scedrov (1990) observed that the disjunction property holds in free
936:
There are several relationship between the five properties discussed above.
925:
776:. In practice, one may say that a theory has one of these properties if a
1610:
Metamathematical investigation of intuitionistic arithmetic and analysis
1595:
1591:, Lectures Notes in Mathematics v. 337, pp. 206–231, Springer.
917:
817:, do have a weaker form of the existence property (Rathjen 2005).
142:
650:{\displaystyle (\exists f\colon \mathbb {N} \to \mathbb {N} )\psi (f)}
1163:
Thus, assuming the numerical existence property, there exists some
842:
has the disjunction property and the numerical existence property.
813:
existence claim. But some classical theories, such as ZFC plus the
853:
1532:
The disjunction property implies the numerical existence property
1259:{\displaystyle ({\bar {s}}=0\to A)\wedge ({\bar {s}}\neq 0\to B)}
780:
of the theory has the property stated above (Rathjen 2005).
1152:{\displaystyle \exists n\colon (n=0\to A)\wedge (n\neq 0\to B)}
839:
831:
26:
1456:
may be used to show that one of the disjuncts is provable.
1550:, 1935, "Untersuchungen über das logische Schließen. II",
1540:, 1934, "Untersuchungen über das logische Schließen. I",
273:{\displaystyle (\exists x\in \mathbb {N} )\varphi (x)}
1396:
1370:
1350:
1324:
1304:
1275:
1192:
1169:
1094:
1074:
1048:
949:
920:
it represents (the global-section functor) preserves
896:
874:
760:
738:
694:
667:
606:
533:
502:
423:
390:
361:
328:
290:
237:
1562:
Anzeiger der
Akademie der Wissenschaftischen in Wien
1298:
is a numeral, one may concretely check the value of
284:
has no other free variables, then the theory proves
1402:
1382:
1356:
1336:
1310:
1290:
1258:
1175:
1151:
1080:
1060:
1027:
904:
882:
768:
746:
716:
680:
649:
582:
515:
484:
396:
376:
347:
314:
272:
188:) has no other free variables, then there is some
1560:, 1932, "Zum intuitionistischen Aussagenkalkül",
801:do not have it. Most classical theories, such as
164:is satisfied by a theory if, whenever a sentence
54:but its sources remain unclear because it lacks
583:{\displaystyle (\forall x)\varphi (x,f_{e}(x))}
1589:Cambridge Summer School in Mathematical Logic
8:
793:Almost by definition, a theory that accepts
1602:, v. 70 n. 4, pp. 1233–1254.
348:{\displaystyle n\in \mathbb {N} {\text{.}}}
1534:, State University of New York at Buffalo.
1395:
1369:
1349:
1323:
1303:
1277:
1276:
1274:
1230:
1229:
1197:
1196:
1191:
1168:
1093:
1073:
1047:
1028:{\displaystyle A\vee B\equiv (\exists n)}
948:
897:
895:
875:
873:
762:
761:
759:
740:
739:
737:
705:
693:
672:
666:
628:
627:
620:
619:
605:
562:
532:
507:
501:
457:
456:
437:
436:
422:
389:
363:
362:
360:
340:
336:
335:
327:
298:
297:
289:
251:
250:
236:
85:Learn how and when to remove this message
1520:Peter J. Freyd and Andre Scedrov, 1990,
864:, that corresponds to the fact that the
130:is satisfied by a theory if, whenever a
1554:v. 39 n. 3, pp. 405–431.
1544:v. 39 n. 2, pp. 176–210.
1623:Moschovakis, Joan (16 December 2022).
523:be the computable function with index
7:
315:{\displaystyle \varphi ({\bar {n}})}
223:), and three additional properties:
103:disjunction and existence properties
1634:Stanford Encyclopedia of Philosophy
600:, states that if the theory proves
1095:
965:
610:
537:
447:
427:
241:
229:numerical existence property (NEP)
25:
417:states that if the theory proves
231:states that if the theory proves
898:
876:
31:
1571:, v. 10, pp. 109–124.
1426:Gödel's incompleteness theorems
932:Relationship between properties
732:, quantify over functions from
657:then there is a natural number
492:then there is a natural number
1282:
1253:
1247:
1235:
1226:
1220:
1214:
1202:
1193:
1146:
1140:
1128:
1122:
1116:
1104:
1022:
1019:
1013:
1001:
995:
989:
977:
974:
971:
962:
711:
698:
644:
638:
632:
624:
607:
577:
574:
568:
549:
543:
534:
479:
467:
461:
444:
441:
424:
368:
309:
303:
294:
267:
261:
255:
238:
1:
1564:, v. 69, pp. 65–66.
1657:Constructivism (mathematics)
905:{\displaystyle \mathbf {1} }
883:{\displaystyle \mathbf {1} }
769:{\displaystyle \mathbb {N} }
747:{\displaystyle \mathbb {N} }
717:{\displaystyle \psi (f_{e})}
661:such that the theory proves
593:A variant of Church's rule,
195:such that the theory proves
1438:bounded existential formula
219:), the existence property (
1673:
1416:(1974) proved that in any
1291:{\displaystyle {\bar {s}}}
377:{\displaystyle {\bar {n}}}
1600:Journal of Symbolic Logic
1569:Journal of Symbolic Logic
1552:Mathematische Zeitschrift
1542:Mathematische Zeitschrift
1422:intuitionistic arithmetic
830: (1973) showed that
815:axiom of constructibility
789:Non-examples and examples
115:constructive set theories
1594:Michael Rathjen, 2005, "
404:representing the number
40:This article includes a
1489:Constructive set theory
1454:disjunction elimination
1383:{\displaystyle s\neq 0}
1061:{\displaystyle A\vee B}
105:are the "hallmarks" of
69:more precise citations.
1625:"Intuitionistic Logic"
1522:Categories, Allegories
1509:Existential quantifier
1499:Law of excluded middle
1418:recursively enumerable
1404:
1384:
1358:
1338:
1312:
1292:
1260:
1177:
1153:
1082:
1062:
1029:
906:
884:
811:least number principle
778:definitional extension
770:
748:
718:
682:
651:
584:
517:
486:
398:
378:
349:
316:
274:
117:(Rathjen 2005).
1405:
1385:
1359:
1339:
1313:
1293:
1261:
1178:
1154:
1083:
1063:
1030:
912:is an indecomposable
907:
885:
771:
749:
719:
683:
681:{\displaystyle f_{e}}
652:
585:
518:
516:{\displaystyle f_{e}}
487:
399:
379:
350:
317:
275:
1579:Applied proof theory
1471: (1934, 1935).
1394:
1368:
1364:is a theorem and if
1348:
1322:
1302:
1273:
1269:is a theorem. Since
1190:
1167:
1092:
1072:
1046:
947:
894:
872:
836:axiom of replacement
758:
736:
692:
688:is total and proves
665:
604:
531:
527:, the theory proves
500:
421:
388:
359:
326:
288:
235:
180:is a theorem, where
128:disjunction property
1473:Stephen Cole Kleene
1337:{\displaystyle s=0}
799:Robinson arithmetic
496:such that, letting
1494:Heyting arithmetic
1400:
1380:
1354:
1334:
1308:
1288:
1256:
1173:
1149:
1078:
1058:
1025:
902:
880:
821:Heyting arithmetic
766:
744:
714:
678:
647:
580:
513:
482:
394:
374:
345:
312:
270:
211:Related properties
158:existence property
111:Heyting arithmetic
99:mathematical logic
42:list of references
18:Existence property
1606:Anne S. Troelstra
1575:Ulrich Kohlenbach
1403:{\displaystyle B}
1357:{\displaystyle A}
1311:{\displaystyle s}
1285:
1238:
1205:
1176:{\displaystyle s}
1081:{\displaystyle T}
914:projective object
858:categorical terms
397:{\displaystyle T}
371:
343:
306:
149:is a theorem, or
109:theories such as
95:
94:
87:
16:(Redirected from
1664:
1638:
1629:Zalta, Edward N.
1524:. North-Holland.
1409:
1407:
1406:
1401:
1389:
1387:
1386:
1381:
1363:
1361:
1360:
1355:
1343:
1341:
1340:
1335:
1317:
1315:
1314:
1309:
1297:
1295:
1294:
1289:
1287:
1286:
1278:
1265:
1263:
1262:
1257:
1240:
1239:
1231:
1207:
1206:
1198:
1182:
1180:
1179:
1174:
1158:
1156:
1155:
1150:
1087:
1085:
1084:
1079:
1068:is a theorem of
1067:
1065:
1064:
1059:
1034:
1032:
1031:
1026:
911:
909:
908:
903:
901:
889:
887:
886:
881:
879:
850:Heyting algebras
803:Peano arithmetic
775:
773:
772:
767:
765:
753:
751:
750:
745:
743:
723:
721:
720:
715:
710:
709:
687:
685:
684:
679:
677:
676:
656:
654:
653:
648:
631:
623:
589:
587:
586:
581:
567:
566:
522:
520:
519:
514:
512:
511:
491:
489:
488:
483:
460:
440:
403:
401:
400:
395:
383:
381:
380:
375:
373:
372:
364:
354:
352:
351:
346:
344:
341:
339:
321:
319:
318:
313:
308:
307:
299:
279:
277:
276:
271:
254:
205:
179:
162:witness property
90:
83:
79:
76:
70:
65:this article by
56:inline citations
35:
34:
27:
21:
1672:
1671:
1667:
1666:
1665:
1663:
1662:
1661:
1642:
1641:
1622:
1619:
1548:Gerhard Gentzen
1538:Gerhard Gentzen
1528:Harvey Friedman
1517:
1485:
1469:Gerhard Gentzen
1462:
1436:), producing a
1414:Harvey Friedman
1392:
1391:
1366:
1365:
1346:
1345:
1320:
1319:
1300:
1299:
1271:
1270:
1188:
1187:
1165:
1164:
1090:
1089:
1070:
1069:
1044:
1043:
1039:Therefore, if
945:
944:
934:
892:
891:
870:
869:
866:terminal object
795:excluded middle
791:
786:
756:
755:
734:
733:
731:
701:
690:
689:
668:
663:
662:
602:
601:
598:
558:
529:
528:
503:
498:
497:
419:
418:
386:
385:
357:
356:
324:
323:
286:
285:
233:
232:
213:
196:
165:
123:
91:
80:
74:
71:
60:
46:related reading
36:
32:
23:
22:
15:
12:
11:
5:
1670:
1668:
1660:
1659:
1654:
1644:
1643:
1640:
1639:
1618:
1617:External links
1615:
1614:
1613:
1608:, ed. (1973),
1603:
1592:
1582:
1572:
1565:
1555:
1545:
1535:
1525:
1516:
1513:
1512:
1511:
1506:
1501:
1496:
1491:
1484:
1481:
1461:
1458:
1410:is a theorem.
1399:
1379:
1376:
1373:
1353:
1333:
1330:
1327:
1307:
1284:
1281:
1267:
1266:
1255:
1252:
1249:
1246:
1243:
1237:
1234:
1228:
1225:
1222:
1219:
1216:
1213:
1210:
1204:
1201:
1195:
1172:
1161:
1160:
1148:
1145:
1142:
1139:
1136:
1133:
1130:
1127:
1124:
1121:
1118:
1115:
1112:
1109:
1106:
1103:
1100:
1097:
1077:
1057:
1054:
1051:
1037:
1036:
1024:
1021:
1018:
1015:
1012:
1009:
1006:
1003:
1000:
997:
994:
991:
988:
985:
982:
979:
976:
973:
970:
967:
964:
961:
958:
955:
952:
933:
930:
900:
878:
790:
787:
785:
782:
764:
742:
729:
726:
725:
713:
708:
704:
700:
697:
675:
671:
646:
643:
640:
637:
634:
630:
626:
622:
618:
615:
612:
609:
596:
591:
579:
576:
573:
570:
565:
561:
557:
554:
551:
548:
545:
542:
539:
536:
510:
506:
481:
478:
475:
472:
469:
466:
463:
459:
455:
452:
449:
446:
443:
439:
435:
432:
429:
426:
409:
393:
370:
367:
338:
334:
331:
311:
305:
302:
296:
293:
269:
266:
263:
260:
257:
253:
249:
246:
243:
240:
212:
209:
208:
207:
154:
145:, then either
122:
119:
93:
92:
50:external links
39:
37:
30:
24:
14:
13:
10:
9:
6:
4:
3:
2:
1669:
1658:
1655:
1653:
1650:
1649:
1647:
1636:
1635:
1630:
1626:
1621:
1620:
1616:
1611:
1607:
1604:
1601:
1597:
1593:
1590:
1586:
1583:
1580:
1576:
1573:
1570:
1566:
1563:
1559:
1556:
1553:
1549:
1546:
1543:
1539:
1536:
1533:
1529:
1526:
1523:
1519:
1518:
1514:
1510:
1507:
1505:
1504:Realizability
1502:
1500:
1497:
1495:
1492:
1490:
1487:
1486:
1482:
1480:
1478:
1477:realizability
1474:
1470:
1466:
1459:
1457:
1455:
1451:
1447:
1443:
1439:
1435:
1431:
1427:
1423:
1420:extension of
1419:
1415:
1411:
1397:
1377:
1374:
1371:
1351:
1331:
1328:
1325:
1305:
1279:
1250:
1244:
1241:
1232:
1223:
1217:
1211:
1208:
1199:
1186:
1185:
1184:
1170:
1143:
1137:
1134:
1131:
1125:
1119:
1113:
1110:
1107:
1101:
1098:
1075:
1055:
1052:
1049:
1042:
1041:
1040:
1016:
1010:
1007:
1004:
998:
992:
986:
983:
980:
968:
959:
956:
953:
950:
943:
942:
941:
937:
931:
929:
927:
923:
919:
915:
867:
863:
859:
855:
851:
847:
843:
841:
837:
833:
829:
824:
822:
818:
816:
812:
808:
804:
800:
796:
788:
783:
781:
779:
706:
702:
695:
673:
669:
660:
641:
635:
616:
613:
599:
592:
571:
563:
559:
555:
552:
546:
540:
526:
508:
504:
495:
476:
473:
470:
464:
453:
450:
433:
430:
416:
414:
413:Church's rule
410:
407:
391:
384:is a term in
365:
332:
329:
300:
291:
283:
264:
258:
247:
244:
230:
226:
225:
224:
222:
218:
210:
203:
199:
194:
191:
187:
183:
177:
173:
169:
163:
159:
155:
153:is a theorem.
152:
148:
144:
140:
136:
133:
129:
125:
124:
120:
118:
116:
112:
108:
104:
100:
89:
86:
78:
68:
64:
58:
57:
51:
47:
43:
38:
29:
28:
19:
1652:Proof theory
1632:
1609:
1599:
1588:
1578:
1568:
1561:
1551:
1541:
1531:
1521:
1463:
1449:
1445:
1441:
1433:
1429:
1412:
1268:
1162:
1038:
938:
935:
922:epimorphisms
844:
825:
819:
792:
727:
658:
594:
524:
493:
411:
405:
281:
228:
220:
216:
214:
201:
197:
192:
185:
181:
175:
171:
167:
161:
157:
150:
146:
138:
134:
127:
107:constructive
102:
96:
81:
72:
61:Please help
53:
1612:, Springer.
1585:John Myhill
1581:, Springer.
1183:such that
916:—the
828:John Myhill
121:Definitions
67:introducing
1646:Categories
1558:Kurt Gödel
1515:References
1465:Kurt Gödel
926:coproducts
862:free topos
1375:≠
1283:¯
1248:→
1242:≠
1236:¯
1224:∧
1215:→
1203:¯
1141:→
1135:≠
1126:∧
1117:→
1102::
1096:∃
1053:∨
1014:→
1008:≠
999:∧
990:→
966:∃
960:≡
954:∨
860:, in the
852:and free
834:with the
696:ψ
636:ψ
625:→
617::
611:∃
547:φ
538:∀
465:φ
454:∈
448:∃
434:∈
428:∀
369:¯
333:∈
322:for some
304:¯
292:φ
259:φ
248:∈
242:∃
75:July 2023
1577:, 2008,
1530:, 1975,
1483:See also
1088:, so is
280:, where
137:∨
132:sentence
1631:(ed.).
1460:History
918:functor
784:Results
143:theorem
63:improve
101:, the
1627:. In
1390:then
1344:then
1318:: if
856:. In
854:topoi
846:Freyd
355:Here
141:is a
48:, or
1444:<
924:and
805:and
415:(CR)
227:The
190:term
156:The
126:The
113:and
1598:",
1448:)A(
1432:)A(
840:CZF
832:IZF
807:ZFC
754:to
160:or
97:In
1648::
1440:(∃
928:.
868:,
595:CR
221:EP
217:DP
166:(∃
52:,
44:,
1637:.
1450:x
1446:n
1442:x
1434:x
1430:x
1398:B
1378:0
1372:s
1352:A
1332:0
1329:=
1326:s
1306:s
1280:s
1254:)
1251:B
1245:0
1233:s
1227:(
1221:)
1218:A
1212:0
1209:=
1200:s
1194:(
1171:s
1159:.
1147:)
1144:B
1138:0
1132:n
1129:(
1123:)
1120:A
1114:0
1111:=
1108:n
1105:(
1099:n
1076:T
1056:B
1050:A
1035:.
1023:]
1020:)
1017:B
1011:0
1005:n
1002:(
996:)
993:A
987:0
984:=
981:n
978:(
975:[
972:)
969:n
963:(
957:B
951:A
899:1
877:1
763:N
741:N
730:1
724:.
712:)
707:e
703:f
699:(
674:e
670:f
659:e
645:)
642:f
639:(
633:)
629:N
621:N
614:f
608:(
597:1
590:.
578:)
575:)
572:x
569:(
564:e
560:f
556:,
553:x
550:(
544:)
541:x
535:(
525:e
509:e
505:f
494:e
480:)
477:y
474:,
471:x
468:(
462:)
458:N
451:y
445:(
442:)
438:N
431:x
425:(
408:.
406:n
392:T
366:n
342:.
337:N
330:n
310:)
301:n
295:(
282:φ
268:)
265:x
262:(
256:)
252:N
245:x
239:(
206:.
204:)
202:t
200:(
198:A
193:t
186:x
184:(
182:A
178:)
176:x
174:(
172:A
170:)
168:x
151:B
147:A
139:B
135:A
88:)
82:(
77:)
73:(
59:.
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.