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