1331:
1799:
1697:
620:
1604:
788:
1493:
539:
677:
1394:
1178:
368:
470:
416:
994:
1064:
707:
1141:
1930:
242:
169:
117:
1852:
1703:
841:
1610:
1167:
545:
140:
1499:
939:
713:
1898:
907:
192:
1400:
97:
300:
271:
1097:
476:
1872:
1826:
884:
861:
815:
212:
626:
1326:{\displaystyle \Diamond ({\vec {r}},p,{\vec {s}})\rightarrow \Diamond ({\vec {r}},p\wedge \neg q,{\vec {s}})\vee \Diamond ({\vec {r}},q,{\vec {s}})}
1337:
913:
The completeness of ILM with respect to its arithmetical interpretation was independently proven by
Alessandro Berarducci and Vladimir Shavrukov.
314:
48:
422:
374:
1982:
1949:
944:
999:
683:
1102:
1977:
1903:
1794:{\displaystyle \Diamond ({\vec {r}},\Diamond ({\vec {s}}))\rightarrow \Diamond ({\vec {r}},{\vec {s}})}
221:
1692:{\displaystyle \Diamond (p,\Diamond ({\vec {r}}))\rightarrow \Diamond (p\wedge \Diamond ({\vec {r}}))}
145:
102:
79:
The language of ILM extends that of classical propositional logic by adding the unary modal operator
1831:
820:
615:{\displaystyle (p\triangleright r)\wedge (q\triangleright r)\rightarrow ((p\vee q)\triangleright r)}
1599:{\displaystyle \Diamond ({\vec {r}},p,{\vec {s}})\rightarrow \Diamond ({\vec {r}},p,p,{\vec {s}})}
1146:
941:
which is allowed to take any nonempty sequence of arguments. The arithmetical interpretation of
783:{\displaystyle (p\triangleright q)\rightarrow ((p\wedge \Box r)\triangleright (q\wedge \Box r))}
122:
924:
921:
The language of TOL extends that of classical propositional logic by adding the modal operator
1488:{\displaystyle \Diamond ({\vec {r}},p,{\vec {s}})\rightarrow \Diamond ({\vec {r}},{\vec {s}})}
32:
1880:
889:
534:{\displaystyle (p\triangleright q)\wedge (q\triangleright r)\rightarrow (p\triangleright r)}
174:
82:
44:
276:
247:
8:
1076:
1857:
1811:
869:
846:
800:
197:
40:
1936:
The completeness of TOL with respect to its arithmetical interpretation was proven by
1067:
24:
1937:
215:
63:
59:
28:
672:{\displaystyle (p\triangleright q)\rightarrow (\Diamond p\rightarrow \Diamond q)}
1971:
1953:
1389:{\displaystyle \Diamond (p)\rightarrow \Diamond (p\wedge \neg \Diamond (p))}
55:
363:{\displaystyle \Box (p\rightarrow q)\rightarrow (\Box p\rightarrow \Box q)}
20:
31:
or various related metamathematical properties and relations such as
465:{\displaystyle \Box (p\rightarrow q)\rightarrow (p\triangleright q)}
411:{\displaystyle \Box (\Box p\rightarrow p)\rightarrow \Box p}
54:
Main contributors to the field are
Alessandro Berarducci,
1906:
1883:
1860:
1834:
1814:
1706:
1613:
1502:
1403:
1340:
1181:
1149:
1105:
1079:
1002:
947:
927:
892:
872:
849:
823:
803:
716:
686:
629:
548:
479:
425:
377:
317:
279:
250:
224:
200:
177:
148:
125:
105:
85:
1924:
1892:
1866:
1846:
1820:
1793:
1691:
1598:
1487:
1388:
1325:
1161:
1135:
1091:
1058:
988:
933:
901:
878:
855:
835:
809:
782:
701:
671:
614:
533:
464:
410:
362:
294:
265:
236:
206:
186:
163:
134:
111:
91:
1969:
989:{\displaystyle \Diamond (p_{1},\ldots ,p_{n})}
1964:, S. Buss, ed., Elsevier, 1998, pp. 475-546.
1059:{\displaystyle (PA+p_{1},\ldots ,PA+p_{n})}
702:{\displaystyle \Diamond p\triangleright p}
66:, Albert Visser, and Domenico Zambella.
62:, Franco Montagna, Vladimir Shavrukov,
1970:
171:). The arithmetical interpretation of
1136:{\displaystyle {\vec {r}},{\vec {s}}}
1143:for any sequences of formulas, and
13:
1907:
1884:
1368:
1254:
155:
149:
14:
1994:
1925:{\displaystyle \neg \Diamond (p)}
237:{\displaystyle p\triangleright q}
164:{\displaystyle \neg \Box \neg p}
51:, and arithmetic complexities.
112:{\displaystyle \triangleright }
1919:
1913:
1847:{\displaystyle p\rightarrow q}
1838:
1788:
1782:
1767:
1758:
1752:
1749:
1746:
1740:
1731:
1719:
1710:
1686:
1683:
1677:
1668:
1656:
1650:
1647:
1644:
1638:
1629:
1617:
1593:
1587:
1560:
1551:
1545:
1542:
1536:
1515:
1506:
1482:
1476:
1461:
1452:
1446:
1443:
1437:
1416:
1407:
1383:
1380:
1374:
1359:
1353:
1350:
1344:
1320:
1314:
1293:
1284:
1275:
1269:
1239:
1230:
1224:
1221:
1215:
1194:
1185:
1156:
1153:
1127:
1112:
1053:
1003:
983:
951:
836:{\displaystyle p\rightarrow q}
827:
777:
774:
759:
753:
738:
735:
732:
729:
717:
666:
657:
648:
645:
642:
630:
609:
600:
588:
585:
582:
579:
567:
561:
549:
528:
516:
513:
510:
498:
492:
480:
459:
447:
444:
441:
435:
429:
399:
396:
390:
381:
357:
348:
339:
336:
333:
327:
321:
99:and the binary modal operator
1:
1943:
1099:standing for any formulas,
916:
74:
7:
1983:Interpretation (philosophy)
1162:{\displaystyle \Diamond ()}
69:
10:
1999:
135:{\displaystyle \Diamond p}
1173:All classical tautologies
934:{\displaystyle \Diamond }
309:All classical tautologies
1962:Handbook of Proof Theory
1958:The Logic of Provability
58:, Konstantin Ignatiev,
17:Interpretability logics
1926:
1894:
1893:{\displaystyle \neg p}
1868:
1848:
1822:
1795:
1693:
1600:
1489:
1390:
1327:
1163:
1137:
1093:
1060:
990:
935:
903:
902:{\displaystyle \Box p}
880:
857:
837:
811:
784:
703:
673:
616:
535:
466:
412:
364:
296:
267:
238:
208:
188:
187:{\displaystyle \Box p}
165:
136:
113:
93:
1927:
1895:
1869:
1849:
1823:
1804:Rules of inference:
1796:
1694:
1601:
1490:
1391:
1328:
1169:identified with ⊤):
1164:
1138:
1094:
1061:
991:
936:
904:
881:
858:
838:
812:
793:Rules of inference:
785:
704:
674:
617:
536:
467:
413:
365:
297:
268:
239:
209:
189:
166:
137:
114:
94:
92:{\displaystyle \Box }
33:weak interpretability
19:comprise a family of
1904:
1881:
1858:
1832:
1812:
1704:
1611:
1500:
1401:
1338:
1179:
1147:
1103:
1077:
1000:
945:
925:
890:
870:
847:
821:
801:
714:
684:
627:
546:
477:
423:
375:
315:
295:{\displaystyle PA+p}
277:
273:is interpretable in
266:{\displaystyle PA+q}
248:
222:
198:
175:
146:
123:
103:
83:
1092:{\displaystyle p,q}
1922:
1890:
1864:
1844:
1818:
1791:
1689:
1596:
1485:
1386:
1323:
1159:
1133:
1089:
1056:
986:
931:
899:
876:
853:
833:
807:
780:
699:
669:
612:
531:
462:
408:
360:
292:
263:
244:is understood as “
234:
204:
184:
161:
132:
109:
89:
41:cointerpretability
1978:Provability logic
1867:{\displaystyle q}
1821:{\displaystyle p}
1785:
1770:
1743:
1722:
1680:
1641:
1590:
1563:
1539:
1518:
1479:
1464:
1440:
1419:
1317:
1296:
1272:
1242:
1218:
1197:
1130:
1115:
1068:tolerant sequence
879:{\displaystyle p}
856:{\displaystyle q}
810:{\displaystyle p}
305:Axiom schemata:
207:{\displaystyle p}
39:-conservativity,
25:provability logic
1990:
1950:Giorgi Japaridze
1938:Giorgi Japaridze
1931:
1929:
1928:
1923:
1899:
1897:
1896:
1891:
1873:
1871:
1870:
1865:
1853:
1851:
1850:
1845:
1827:
1825:
1824:
1819:
1800:
1798:
1797:
1792:
1787:
1786:
1778:
1772:
1771:
1763:
1745:
1744:
1736:
1724:
1723:
1715:
1698:
1696:
1695:
1690:
1682:
1681:
1673:
1643:
1642:
1634:
1605:
1603:
1602:
1597:
1592:
1591:
1583:
1565:
1564:
1556:
1541:
1540:
1532:
1520:
1519:
1511:
1494:
1492:
1491:
1486:
1481:
1480:
1472:
1466:
1465:
1457:
1442:
1441:
1433:
1421:
1420:
1412:
1395:
1393:
1392:
1387:
1332:
1330:
1329:
1324:
1319:
1318:
1310:
1298:
1297:
1289:
1274:
1273:
1265:
1244:
1243:
1235:
1220:
1219:
1211:
1199:
1198:
1190:
1168:
1166:
1165:
1160:
1142:
1140:
1139:
1134:
1132:
1131:
1123:
1117:
1116:
1108:
1098:
1096:
1095:
1090:
1065:
1063:
1062:
1057:
1052:
1051:
1024:
1023:
995:
993:
992:
987:
982:
981:
963:
962:
940:
938:
937:
932:
908:
906:
905:
900:
885:
883:
882:
877:
862:
860:
859:
854:
842:
840:
839:
834:
816:
814:
813:
808:
789:
787:
786:
781:
708:
706:
705:
700:
678:
676:
675:
670:
621:
619:
618:
613:
540:
538:
537:
532:
471:
469:
468:
463:
417:
415:
414:
409:
369:
367:
366:
361:
301:
299:
298:
293:
272:
270:
269:
264:
243:
241:
240:
235:
216:Peano arithmetic
213:
211:
210:
205:
193:
191:
190:
185:
170:
168:
167:
162:
141:
139:
138:
133:
118:
116:
115:
110:
98:
96:
95:
90:
64:Rineke Verbrugge
60:Giorgi Japaridze
29:interpretability
1998:
1997:
1993:
1992:
1991:
1989:
1988:
1987:
1968:
1967:
1946:
1905:
1902:
1901:
1882:
1879:
1878:
1859:
1856:
1855:
1833:
1830:
1829:
1813:
1810:
1809:
1777:
1776:
1762:
1761:
1735:
1734:
1714:
1713:
1705:
1702:
1701:
1672:
1671:
1633:
1632:
1612:
1609:
1608:
1582:
1581:
1555:
1554:
1531:
1530:
1510:
1509:
1501:
1498:
1497:
1471:
1470:
1456:
1455:
1432:
1431:
1411:
1410:
1402:
1399:
1398:
1339:
1336:
1335:
1309:
1308:
1288:
1287:
1264:
1263:
1234:
1233:
1210:
1209:
1189:
1188:
1180:
1177:
1176:
1148:
1145:
1144:
1122:
1121:
1107:
1106:
1104:
1101:
1100:
1078:
1075:
1074:
1070:of theories”.
1047:
1043:
1019:
1015:
1001:
998:
997:
977:
973:
958:
954:
946:
943:
942:
926:
923:
922:
919:
891:
888:
887:
871:
868:
867:
848:
845:
844:
822:
819:
818:
802:
799:
798:
715:
712:
711:
685:
682:
681:
628:
625:
624:
547:
544:
543:
478:
475:
474:
424:
421:
420:
376:
373:
372:
316:
313:
312:
278:
275:
274:
249:
246:
245:
223:
220:
219:
214:is provable in
199:
196:
195:
176:
173:
172:
147:
144:
143:
124:
121:
120:
104:
101:
100:
84:
81:
80:
77:
72:
38:
12:
11:
5:
1996:
1986:
1985:
1980:
1966:
1965:
1945:
1942:
1934:
1933:
1921:
1918:
1915:
1912:
1909:
1889:
1886:
1875:
1863:
1843:
1840:
1837:
1817:
1802:
1801:
1790:
1784:
1781:
1775:
1769:
1766:
1760:
1757:
1754:
1751:
1748:
1742:
1739:
1733:
1730:
1727:
1721:
1718:
1712:
1709:
1699:
1688:
1685:
1679:
1676:
1670:
1667:
1664:
1661:
1658:
1655:
1652:
1649:
1646:
1640:
1637:
1631:
1628:
1625:
1622:
1619:
1616:
1606:
1595:
1589:
1586:
1580:
1577:
1574:
1571:
1568:
1562:
1559:
1553:
1550:
1547:
1544:
1538:
1535:
1529:
1526:
1523:
1517:
1514:
1508:
1505:
1495:
1484:
1478:
1475:
1469:
1463:
1460:
1454:
1451:
1448:
1445:
1439:
1436:
1430:
1427:
1424:
1418:
1415:
1409:
1406:
1396:
1385:
1382:
1379:
1376:
1373:
1370:
1367:
1364:
1361:
1358:
1355:
1352:
1349:
1346:
1343:
1333:
1322:
1316:
1313:
1307:
1304:
1301:
1295:
1292:
1286:
1283:
1280:
1277:
1271:
1268:
1262:
1259:
1256:
1253:
1250:
1247:
1241:
1238:
1232:
1229:
1226:
1223:
1217:
1214:
1208:
1205:
1202:
1196:
1193:
1187:
1184:
1174:
1158:
1155:
1152:
1129:
1126:
1120:
1114:
1111:
1088:
1085:
1082:
1055:
1050:
1046:
1042:
1039:
1036:
1033:
1030:
1027:
1022:
1018:
1014:
1011:
1008:
1005:
985:
980:
976:
972:
969:
966:
961:
957:
953:
950:
930:
918:
915:
911:
910:
898:
895:
875:
864:
852:
832:
829:
826:
806:
791:
790:
779:
776:
773:
770:
767:
764:
761:
758:
755:
752:
749:
746:
743:
740:
737:
734:
731:
728:
725:
722:
719:
709:
698:
695:
692:
689:
679:
668:
665:
662:
659:
656:
653:
650:
647:
644:
641:
638:
635:
632:
622:
611:
608:
605:
602:
599:
596:
593:
590:
587:
584:
581:
578:
575:
572:
569:
566:
563:
560:
557:
554:
551:
541:
530:
527:
524:
521:
518:
515:
512:
509:
506:
503:
500:
497:
494:
491:
488:
485:
482:
472:
461:
458:
455:
452:
449:
446:
443:
440:
437:
434:
431:
428:
418:
407:
404:
401:
398:
395:
392:
389:
386:
383:
380:
370:
359:
356:
353:
350:
347:
344:
341:
338:
335:
332:
329:
326:
323:
320:
310:
291:
288:
285:
282:
262:
259:
256:
253:
233:
230:
227:
203:
183:
180:
160:
157:
154:
151:
142:is defined as
131:
128:
108:
88:
76:
73:
71:
68:
36:
9:
6:
4:
3:
2:
1995:
1984:
1981:
1979:
1976:
1975:
1973:
1963:
1959:
1955:
1954:Dick de Jongh
1951:
1948:
1947:
1941:
1939:
1916:
1910:
1887:
1876:
1861:
1841:
1835:
1815:
1807:
1806:
1805:
1779:
1773:
1764:
1755:
1737:
1728:
1725:
1716:
1707:
1700:
1674:
1665:
1662:
1659:
1653:
1635:
1626:
1623:
1620:
1614:
1607:
1584:
1578:
1575:
1572:
1569:
1566:
1557:
1548:
1533:
1527:
1524:
1521:
1512:
1503:
1496:
1473:
1467:
1458:
1449:
1434:
1428:
1425:
1422:
1413:
1404:
1397:
1377:
1371:
1365:
1362:
1356:
1347:
1341:
1334:
1311:
1305:
1302:
1299:
1290:
1281:
1278:
1266:
1260:
1257:
1251:
1248:
1245:
1236:
1227:
1212:
1206:
1203:
1200:
1191:
1182:
1175:
1172:
1171:
1170:
1150:
1124:
1118:
1109:
1086:
1083:
1080:
1073:Axioms (with
1071:
1069:
1048:
1044:
1040:
1037:
1034:
1031:
1028:
1025:
1020:
1016:
1012:
1009:
1006:
978:
974:
970:
967:
964:
959:
955:
948:
928:
914:
896:
893:
873:
865:
850:
830:
824:
804:
796:
795:
794:
771:
768:
765:
762:
756:
750:
747:
744:
741:
726:
723:
720:
710:
696:
693:
690:
687:
680:
663:
660:
654:
651:
639:
636:
633:
623:
606:
603:
597:
594:
591:
576:
573:
570:
564:
558:
555:
552:
542:
525:
522:
519:
507:
504:
501:
495:
489:
486:
483:
473:
456:
453:
450:
438:
432:
426:
419:
405:
402:
393:
387:
384:
378:
371:
354:
351:
345:
342:
330:
324:
318:
311:
308:
307:
306:
303:
289:
286:
283:
280:
260:
257:
254:
251:
231:
228:
225:
217:
201:
181:
178:
158:
152:
129:
126:
106:
86:
67:
65:
61:
57:
52:
50:
46:
42:
34:
30:
26:
23:that extend
22:
18:
1961:
1957:
1935:
1803:
1072:
920:
912:
792:
304:
119:(as always,
78:
53:
27:to describe
21:modal logics
16:
15:
218:(PA)”, and
49:cotolerance
1972:Categories
1944:References
56:Petr Hájek
1911:◊
1908:¬
1900:conclude
1885:¬
1854:conclude
1839:→
1783:→
1768:→
1756:◊
1753:→
1741:→
1729:◊
1720:→
1708:◊
1678:→
1666:◊
1663:∧
1654:◊
1651:→
1639:→
1627:◊
1615:◊
1588:→
1561:→
1549:◊
1546:→
1537:→
1516:→
1504:◊
1477:→
1462:→
1450:◊
1447:→
1438:→
1417:→
1405:◊
1372:◊
1369:¬
1366:∧
1357:◊
1354:→
1342:◊
1315:→
1294:→
1282:◊
1279:∨
1270:→
1255:¬
1252:∧
1240:→
1228:◊
1225:→
1216:→
1195:→
1183:◊
1151:◊
1128:→
1113:→
1029:…
968:…
949:◊
929:◊
917:Logic TOL
894:◻
886:conclude
843:conclude
828:→
769:◻
766:∧
757:▹
748:◻
745:∧
733:→
724:▹
694:▹
688:◊
661:◊
658:→
652:◊
646:→
637:▹
604:▹
595:∨
583:→
574:▹
565:∧
556:▹
523:▹
514:→
505:▹
496:∧
487:▹
454:▹
445:→
436:→
427:◻
403:◻
400:→
391:→
385:◻
379:◻
352:◻
349:→
343:◻
337:→
328:→
319:◻
229:▹
179:◻
156:¬
153:◻
150:¬
127:◊
107:▹
87:◻
75:Logic ILM
45:tolerance
70:Examples
1877:“From
1808:“From
866:“From
797:“From
1960:. In
1066:is a
1952:and
1828:and
996:is “
817:and
302:”.
194:is “
35:, Î
1974::
1956:,
1940:.
1932:”.
909:”.
47:,
43:,
1920:)
1917:p
1914:(
1888:p
1874:”
1862:q
1842:q
1836:p
1816:p
1789:)
1780:s
1774:,
1765:r
1759:(
1750:)
1747:)
1738:s
1732:(
1726:,
1717:r
1711:(
1687:)
1684:)
1675:r
1669:(
1660:p
1657:(
1648:)
1645:)
1636:r
1630:(
1624:,
1621:p
1618:(
1594:)
1585:s
1579:,
1576:p
1573:,
1570:p
1567:,
1558:r
1552:(
1543:)
1534:s
1528:,
1525:p
1522:,
1513:r
1507:(
1483:)
1474:s
1468:,
1459:r
1453:(
1444:)
1435:s
1429:,
1426:p
1423:,
1414:r
1408:(
1384:)
1381:)
1378:p
1375:(
1363:p
1360:(
1351:)
1348:p
1345:(
1321:)
1312:s
1306:,
1303:q
1300:,
1291:r
1285:(
1276:)
1267:s
1261:,
1258:q
1249:p
1246:,
1237:r
1231:(
1222:)
1213:s
1207:,
1204:p
1201:,
1192:r
1186:(
1157:)
1154:(
1125:s
1119:,
1110:r
1087:q
1084:,
1081:p
1054:)
1049:n
1045:p
1041:+
1038:A
1035:P
1032:,
1026:,
1021:1
1017:p
1013:+
1010:A
1007:P
1004:(
984:)
979:n
975:p
971:,
965:,
960:1
956:p
952:(
897:p
874:p
863:”
851:q
831:q
825:p
805:p
778:)
775:)
772:r
763:q
760:(
754:)
751:r
742:p
739:(
736:(
730:)
727:q
721:p
718:(
697:p
691:p
667:)
664:q
655:p
649:(
643:)
640:q
634:p
631:(
610:)
607:r
601:)
598:q
592:p
589:(
586:(
580:)
577:r
571:q
568:(
562:)
559:r
553:p
550:(
529:)
526:r
520:p
517:(
511:)
508:r
502:q
499:(
493:)
490:q
484:p
481:(
460:)
457:q
451:p
448:(
442:)
439:q
433:p
430:(
406:p
397:)
394:p
388:p
382:(
358:)
355:q
346:p
340:(
334:)
331:q
325:p
322:(
290:p
287:+
284:A
281:P
261:q
258:+
255:A
252:P
232:q
226:p
202:p
182:p
159:p
130:p
37:1
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.