1563:
1199:. However, the proof for this theorem was erroneous, and unrestricted bar induction is not considered to be intuitionistically valid (see Dummett 1977 pp 94–104 for a summary of why this is so). The schema of unrestricted bar induction is given below for completeness.
1132:
1010:
224:
1005:
139:
233:
There are three forms of bar induction currently in the literature, each one places certain restrictions on a pair of predicates and the key differences are highlighted using bold font.
1157:
1416:
1464:
1436:
1374:
1350:
1330:
1307:
1287:
1264:
1240:
1220:
1193:
970:
946:
926:
903:
883:
855:
835:
811:
787:
767:
726:
702:
682:
659:
639:
612:
584:
564:
519:
491:
471:
451:
428:
408:
388:
356:
329:
309:
285:
265:
49:
in intuitionistic terminology), by inductively reducing them to properties of finite lists. Bar induction can also be used to prove properties about all
27:. Bar induction's main use is the intuitionistic derivation of the fan theorem, a key result used in the derivation of the uniform continuity theorem.
1623:
1604:
144:
1127:{\displaystyle {\begin{aligned}BI_{M}&\vdash BI_{D}\\BI_{D}&\vdash BI_{T}\\BI_{T}&\vdash BI_{D}\end{aligned}}}
72:
1486:
1628:
1496:
1491:
521:
holds for the empty sequence (i.e. A holds for all choice sequences starting with the empty sequence).
1597:
31:
1140:
1443:
54:
1517:
The foundations of intuitionistic mathematics: especially in relation to recursive functions
1391:
1633:
359:
8:
1590:
1512:
1385:
980:
529:
1578:
1449:
1421:
1359:
1335:
1315:
1292:
1272:
1249:
1242:
on finite sequences of natural numbers such that all of the following conditions hold:
1225:
1205:
1178:
1160:
955:
931:
911:
888:
868:
840:
820:
796:
789:
on finite sequences of natural numbers such that all of the following conditions hold:
772:
752:
711:
687:
667:
644:
624:
597:
586:
on finite sequences of natural numbers such that all of the following conditions hold:
569:
549:
504:
476:
456:
436:
413:
393:
373:
341:
314:
294:
287:
on finite sequences of natural numbers such that all of the following conditions hold:
270:
250:
58:
1475:
1172:
984:
732:
430:
holds for every choice sequence beginning with the aforementioned finite sequence);
24:
1548:
Constructivism in
Mathematics, Studies in Logic and the Foundations of Mathematics
1539:
1529:
1502:
976:
525:
50:
46:
35:
1574:
1543:
42:
41:
The goal of the principle is to prove properties for all infinite sequences of
1617:
990:
735:
and is (intuitionistically) provably equivalent to decidable bar induction.
1171:
An additional schema of bar induction was originally given as a theorem by
996:
20:
1439:
1246:
every choice sequence contains at least one initial segment satisfying
837:, then every possible extension of that finite sequence also satisfies
793:
every choice sequence contains at least one initial segment satisfying
291:
every choice sequence contains at least one initial segment satisfying
1526:, Journal of Symbolic Logic 56 (1991), no. 2, pp. 715–730.
1562:
1312:
if all extensions of a finite sequence by one element satisfy
908:
if all extensions of a finite sequence by one element satisfy
664:
if all extensions of a finite sequence by one element satisfy
433:
if all extensions of a finite sequence by one element satisfy
1570:
524:
This principle of bar induction is favoured in the works of,
731:
This principle of bar induction is favoured in the works of
1418:) denotes the related principle stating that if a relation
991:
Relationships between these schemata and other information
975:
This principle of bar induction is used in the works of
1452:
1424:
1394:
1362:
1338:
1318:
1295:
1275:
1252:
1228:
1208:
1181:
1143:
1008:
958:
934:
914:
891:
871:
843:
823:
799:
775:
755:
714:
690:
670:
647:
627:
600:
572:
552:
507:
479:
459:
439:
416:
396:
376:
344:
317:
297:
273:
253:
219:{\displaystyle x_{0},x_{1},x_{2},x_{3},\ldots ,x_{i}}
147:
75:
1524:
The role of parameters in bar rule and bar induction
1458:
1430:
1410:
1368:
1344:
1324:
1301:
1281:
1258:
1234:
1214:
1187:
1151:
1126:
995:The following results about these schemata can be
964:
940:
920:
897:
877:
849:
829:
805:
781:
761:
720:
696:
676:
653:
633:
606:
578:
558:
513:
485:
465:
445:
422:
402:
382:
350:
323:
303:
279:
259:
218:
133:
1615:
738:
311:at some point (this is expressed by saying that
236:
134:{\displaystyle x_{0},x_{1},x_{2},x_{3},\ldots }
1598:
1166:
1379:
1175:(1975) containing no "extra" restriction on
1481:, Vol. I, Amsterdam: North-Holland (1975).
1332:, then that finite sequence also satisfies
928:, then that finite sequence also satisfies
684:, then that finite sequence also satisfies
535:
453:, then that finite sequence also satisfies
1605:
1591:
1148:
1144:
1484:
1616:
1557:
13:
473:(this is sometimes referred to as
141:, any finite sequence of elements
14:
1645:
1479:Brouwer, L. E. J. Collected Works
1269:every finite sequence satisfying
865:every finite sequence satisfying
817:once a finite sequence satisfies
621:every finite sequence satisfying
370:every finite sequence satisfying
19:is a reasoning principle used in
1561:
614:at some point (i.e. our bar is
590:every choice sequence contains
1376:holds for the empty sequence.
972:holds for the empty sequence.
728:holds for the empty sequence.
226:of this sequence is called an
1:
1485:Dragalin, Albert G. (2001) ,
1469:
1442:, then we have the schema of
64:
1624:Constructivism (mathematics)
1577:. You can help Knowledge by
30:It is also useful in giving
7:
1492:Encyclopedia of Mathematics
1152:{\displaystyle \,\vdash \,}
739:Monotonic bar induction (BI
594:initial segment satisfying
237:Decidable bar induction (BI
10:
1650:
1556:
1356:then we can conclude that
1167:Unrestricted bar induction
952:then we can conclude that
708:then we can conclude that
501:then we can conclude that
21:intuitionistic mathematics
1536:, Clarendon Press (1977)
1509:, Clarendon Press (1977)
1380:Relations to other fields
230:of this choice sequence.
1507:Elements of intuitionism
1466:for arbitrary formulas.
69:Given a choice sequence
1519:, North-Holland (1965)
1629:Mathematical induction
1573:-related article is a
1460:
1432:
1412:
1411:{\displaystyle BI_{D}}
1370:
1346:
1326:
1303:
1283:
1260:
1236:
1216:
1189:
1153:
1128:
966:
942:
922:
899:
879:
851:
831:
807:
783:
763:
722:
698:
678:
655:
635:
608:
580:
560:
536:Thin bar induction (BI
515:
487:
467:
447:
424:
404:
384:
352:
325:
305:
281:
261:
220:
135:
34:alternatives to other
1461:
1444:transfinite induction
1433:
1413:
1371:
1347:
1327:
1304:
1284:
1261:
1237:
1217:
1202:Given two predicates
1190:
1154:
1129:
967:
943:
923:
900:
880:
852:
832:
808:
784:
764:
749:Given two predicates
723:
699:
679:
656:
636:
609:
581:
561:
546:Given two predicates
532:and Albert Dragalin.
516:
488:
468:
448:
425:
405:
385:
353:
326:
306:
282:
262:
247:Given two predicates
221:
136:
1450:
1422:
1392:
1360:
1336:
1316:
1293:
1273:
1250:
1226:
1206:
1179:
1141:
1006:
956:
932:
912:
889:
869:
841:
821:
797:
773:
753:
712:
688:
668:
645:
625:
598:
570:
550:
505:
477:
457:
437:
414:
394:
374:
342:
315:
295:
271:
251:
145:
73:
1388:, "bar induction" (
1386:reverse mathematics
57:(a special kind of
1515:, R. E. Vesley,
1456:
1428:
1408:
1366:
1342:
1322:
1299:
1279:
1256:
1232:
1212:
1185:
1149:
1124:
1122:
997:intuitionistically
962:
938:
918:
895:
875:
847:
827:
803:
779:
759:
718:
694:
674:
651:
631:
604:
576:
556:
511:
483:
463:
443:
420:
400:
380:
348:
321:
301:
277:
257:
216:
131:
1586:
1585:
1550:, Elsevier (1988)
1522:Michael Rathjen,
1459:{\displaystyle R}
1431:{\displaystyle R}
1369:{\displaystyle A}
1345:{\displaystyle A}
1325:{\displaystyle A}
1302:{\displaystyle A}
1282:{\displaystyle R}
1259:{\displaystyle R}
1235:{\displaystyle A}
1215:{\displaystyle R}
1188:{\displaystyle R}
965:{\displaystyle A}
941:{\displaystyle A}
921:{\displaystyle A}
898:{\displaystyle A}
878:{\displaystyle R}
858:(i.e. our bar is
850:{\displaystyle R}
830:{\displaystyle R}
806:{\displaystyle R}
782:{\displaystyle A}
762:{\displaystyle R}
721:{\displaystyle A}
697:{\displaystyle A}
677:{\displaystyle A}
654:{\displaystyle A}
634:{\displaystyle R}
607:{\displaystyle R}
579:{\displaystyle A}
559:{\displaystyle R}
514:{\displaystyle A}
495:upward hereditary
486:{\displaystyle A}
466:{\displaystyle A}
446:{\displaystyle A}
423:{\displaystyle A}
403:{\displaystyle A}
383:{\displaystyle R}
363:(i.e. our bar is
351:{\displaystyle R}
324:{\displaystyle R}
304:{\displaystyle R}
280:{\displaystyle A}
260:{\displaystyle R}
1641:
1607:
1600:
1593:
1565:
1558:
1534:Choice sequences
1499:
1476:L. E. J. Brouwer
1465:
1463:
1462:
1457:
1437:
1435:
1434:
1429:
1417:
1415:
1414:
1409:
1407:
1406:
1375:
1373:
1372:
1367:
1351:
1349:
1348:
1343:
1331:
1329:
1328:
1323:
1308:
1306:
1305:
1300:
1288:
1286:
1285:
1280:
1265:
1263:
1262:
1257:
1241:
1239:
1238:
1233:
1221:
1219:
1218:
1213:
1194:
1192:
1191:
1186:
1158:
1156:
1155:
1150:
1133:
1131:
1130:
1125:
1123:
1119:
1118:
1099:
1098:
1082:
1081:
1062:
1061:
1045:
1044:
1025:
1024:
985:Joan Moschovakis
971:
969:
968:
963:
947:
945:
944:
939:
927:
925:
924:
919:
904:
902:
901:
896:
884:
882:
881:
876:
856:
854:
853:
848:
836:
834:
833:
828:
812:
810:
809:
804:
788:
786:
785:
780:
768:
766:
765:
760:
733:Joan Moschovakis
727:
725:
724:
719:
703:
701:
700:
695:
683:
681:
680:
675:
660:
658:
657:
652:
640:
638:
637:
632:
613:
611:
610:
605:
585:
583:
582:
577:
565:
563:
562:
557:
520:
518:
517:
512:
492:
490:
489:
484:
472:
470:
469:
464:
452:
450:
449:
444:
429:
427:
426:
421:
409:
407:
406:
401:
389:
387:
386:
381:
357:
355:
354:
349:
330:
328:
327:
322:
310:
308:
307:
302:
286:
284:
283:
278:
266:
264:
263:
258:
225:
223:
222:
217:
215:
214:
196:
195:
183:
182:
170:
169:
157:
156:
140:
138:
137:
132:
124:
123:
111:
110:
98:
97:
85:
84:
51:choice sequences
47:choice sequences
25:L. E. J. Brouwer
23:, introduced by
1649:
1648:
1644:
1643:
1642:
1640:
1639:
1638:
1614:
1613:
1612:
1611:
1554:
1540:A. S. Troelstra
1530:A. S. Troelstra
1503:Michael Dummett
1487:"Bar induction"
1472:
1451:
1448:
1447:
1423:
1420:
1419:
1402:
1398:
1393:
1390:
1389:
1382:
1361:
1358:
1357:
1337:
1334:
1333:
1317:
1314:
1313:
1294:
1291:
1290:
1289:also satisfies
1274:
1271:
1270:
1251:
1248:
1247:
1227:
1224:
1223:
1207:
1204:
1203:
1197:The Bar Theorem
1195:under the name
1180:
1177:
1176:
1169:
1142:
1139:
1138:
1121:
1120:
1114:
1110:
1100:
1094:
1090:
1084:
1083:
1077:
1073:
1063:
1057:
1053:
1047:
1046:
1040:
1036:
1026:
1020:
1016:
1009:
1007:
1004:
1003:
993:
983:, Dragalin and
977:A. S. Troelstra
957:
954:
953:
933:
930:
929:
913:
910:
909:
890:
887:
886:
885:also satisfies
870:
867:
866:
842:
839:
838:
822:
819:
818:
798:
795:
794:
774:
771:
770:
754:
751:
750:
747:
744:
713:
710:
709:
689:
686:
685:
669:
666:
665:
646:
643:
642:
641:also satisfies
626:
623:
622:
599:
596:
595:
571:
568:
567:
551:
548:
547:
544:
541:
526:A. S. Troelstra
506:
503:
502:
478:
475:
474:
458:
455:
454:
438:
435:
434:
415:
412:
411:
395:
392:
391:
390:also satisfies
375:
372:
371:
343:
340:
339:
316:
313:
312:
296:
293:
292:
272:
269:
268:
252:
249:
248:
245:
242:
228:initial segment
210:
206:
191:
187:
178:
174:
165:
161:
152:
148:
146:
143:
142:
119:
115:
106:
102:
93:
89:
80:
76:
74:
71:
70:
67:
43:natural numbers
12:
11:
5:
1647:
1637:
1636:
1631:
1626:
1610:
1609:
1602:
1595:
1587:
1584:
1583:
1566:
1552:
1551:
1544:Dirk van Dalen
1537:
1527:
1520:
1510:
1500:
1482:
1471:
1468:
1455:
1427:
1405:
1401:
1397:
1381:
1378:
1365:
1354:
1353:
1341:
1321:
1310:
1298:
1278:
1267:
1266:at some point;
1255:
1231:
1211:
1184:
1168:
1165:
1147:
1135:
1134:
1117:
1113:
1109:
1106:
1103:
1101:
1097:
1093:
1089:
1086:
1085:
1080:
1076:
1072:
1069:
1066:
1064:
1060:
1056:
1052:
1049:
1048:
1043:
1039:
1035:
1032:
1029:
1027:
1023:
1019:
1015:
1012:
1011:
992:
989:
961:
950:
949:
937:
917:
906:
894:
874:
863:
846:
826:
814:
813:at some point;
802:
778:
758:
746:
740:
737:
717:
706:
705:
693:
673:
662:
650:
630:
619:
603:
575:
555:
543:
537:
534:
510:
499:
498:
482:
462:
442:
431:
419:
399:
379:
368:
347:
336:
320:
300:
276:
256:
244:
238:
235:
213:
209:
205:
202:
199:
194:
190:
186:
181:
177:
173:
168:
164:
160:
155:
151:
130:
127:
122:
118:
114:
109:
105:
101:
96:
92:
88:
83:
79:
66:
63:
9:
6:
4:
3:
2:
1646:
1635:
1632:
1630:
1627:
1625:
1622:
1621:
1619:
1608:
1603:
1601:
1596:
1594:
1589:
1588:
1582:
1580:
1576:
1572:
1567:
1564:
1560:
1559:
1555:
1549:
1545:
1541:
1538:
1535:
1531:
1528:
1525:
1521:
1518:
1514:
1511:
1508:
1504:
1501:
1498:
1494:
1493:
1488:
1483:
1480:
1477:
1474:
1473:
1467:
1453:
1445:
1441:
1425:
1403:
1399:
1395:
1387:
1384:In classical
1377:
1363:
1339:
1319:
1311:
1296:
1276:
1268:
1253:
1245:
1244:
1243:
1229:
1209:
1200:
1198:
1182:
1174:
1164:
1162:
1145:
1137:(The symbol "
1115:
1111:
1107:
1104:
1102:
1095:
1091:
1087:
1078:
1074:
1070:
1067:
1065:
1058:
1054:
1050:
1041:
1037:
1033:
1030:
1028:
1021:
1017:
1013:
1002:
1001:
1000:
998:
988:
986:
982:
978:
973:
959:
935:
915:
907:
892:
872:
864:
861:
857:
844:
824:
815:
800:
792:
791:
790:
776:
756:
743:
736:
734:
729:
715:
691:
671:
663:
648:
628:
620:
617:
601:
593:
589:
588:
587:
573:
553:
540:
533:
531:
527:
522:
508:
496:
480:
460:
440:
432:
417:
397:
377:
369:
366:
362:
361:
345:
337:
334:
318:
298:
290:
289:
288:
274:
254:
241:
234:
231:
229:
211:
207:
203:
200:
197:
192:
188:
184:
179:
175:
171:
166:
162:
158:
153:
149:
128:
125:
120:
116:
112:
107:
103:
99:
94:
90:
86:
81:
77:
62:
60:
56:
52:
48:
44:
39:
37:
33:
28:
26:
22:
18:
17:Bar induction
1579:expanding it
1568:
1553:
1547:
1533:
1523:
1516:
1513:S. C. Kleene
1506:
1490:
1478:
1383:
1355:
1201:
1196:
1170:
1136:
994:
981:S. C. Kleene
974:
951:
859:
816:
748:
741:
730:
707:
615:
591:
545:
538:
530:S. C. Kleene
523:
500:
494:
364:
338:
332:
246:
239:
232:
227:
68:
40:
32:constructive
29:
16:
15:
1634:Logic stubs
1618:Categories
1470:References
1440:well-order
65:Definition
1497:EMS Press
1161:turnstile
1146:⊢
1105:⊢
1068:⊢
1031:⊢
860:monotonic
365:decidable
360:decidable
201:…
129:…
38:results.
36:classical
1159:" is a "
999:proved:
592:a unique
45:(called
1173:Brouwer
493:being
55:spread
1571:logic
1569:This
1446:over
1438:is a
331:is a
53:in a
1575:stub
1542:and
1222:and
1163:".)
769:and
616:thin
566:and
410:(so
267:and
358:is
333:bar
61:).
59:set
1620::
1546:,
1532:,
1505:,
1495:,
1489:,
987:.
979:,
862:);
618:);
528:,
497:);
367:);
335:);
1606:e
1599:t
1592:v
1581:.
1454:R
1426:R
1404:D
1400:I
1396:B
1364:A
1352:;
1340:A
1320:A
1309:;
1297:A
1277:R
1254:R
1230:A
1210:R
1183:R
1116:D
1112:I
1108:B
1096:T
1092:I
1088:B
1079:T
1075:I
1071:B
1059:D
1055:I
1051:B
1042:D
1038:I
1034:B
1022:M
1018:I
1014:B
960:A
948:;
936:A
916:A
905:;
893:A
873:R
845:R
825:R
801:R
777:A
757:R
745:)
742:M
716:A
704:;
692:A
672:A
661:;
649:A
629:R
602:R
574:A
554:R
542:)
539:T
509:A
481:A
461:A
441:A
418:A
398:A
378:R
346:R
319:R
299:R
275:A
255:R
243:)
240:D
212:i
208:x
204:,
198:,
193:3
189:x
185:,
180:2
176:x
172:,
167:1
163:x
159:,
154:0
150:x
126:,
121:3
117:x
113:,
108:2
104:x
100:,
95:1
91:x
87:,
82:0
78:x
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.