1389:
There is a close connection of ω-logic to ω-consistency. A theory consistent in ω-logic is also ω-consistent (and arithmetically sound). The converse is false, as consistency in ω-logic is a much stronger notion than ω-consistency. However, the following characterization holds: a theory is
411:
of a proof in PA that 0=1". Now, the consistency of PA implies the consistency of PA + ¬Con(PA). Indeed, if PA + ¬Con(PA) was inconsistent, then PA alone would prove ¬Con(PA)→0=1, and a reductio ad absurdum in PA would produce a proof of Con(PA). By
1709:
1298:
collectively for all natural numbers at once via the evident finite universally quantified counterpart of the infinitely many antecedents of the rule. For a theory of arithmetic, meaning one with intended domain the natural numbers such as
1877:
This formulation uses 0=1 instead of a direct contradiction; that gives the same result, because PA certainly proves ¬0=1, so if it proved 0=1 as well we would have a contradiction, and on the other hand, if PA proves a contradiction,
1101:
intended to hold just of the natural numbers, as well as specified names 0, 1, 2, ..., one for each (standard) natural number (which may be separate constants, or constant terms such as 0, 1, 1+1, 1+1+1, ..., etc.). Note that
1501:
1972:
1560:
1276:
1219:
957:
1599:
1615:
1772:
1345:
524:
745:
885:
1732:
1362:
are standardly interpreted, respectively as those numbers and the predicate having just those numbers as its domain (whence there are no nonstandard numbers). If
1411:
1424:
1046:
Let ω-Con(PA) be the arithmetical sentence formalizing the statement "PA is ω-consistent". Then the theory PA + ¬ω-Con(PA) is unsound (Σ
350:), then a sound system is one whose model can be thought of as the set ω, the usual set of mathematical natural numbers. The case of general
403:, and Con(PA) for the statement of arithmetic that formalizes the claim "PA is consistent". Con(PA) could be of the form "No natural number
413:
59:
1510:
1919:
66:), but also avoids proving certain infinite combinations of sentences that are intuitively contradictory. The name is due to
1852:
1378:
need not even be countable, for example.) These requirements make the ω-rule sound in every ω-model. As a corollary to the
71:
334:
is true in the standard model. When Γ is the set of all arithmetical formulas, Γ-soundness is called just (arithmetical)
1129:
The system of ω-logic includes all axioms and rules of the usual first-order predicate logic, together with, for each
17:
1050:-unsound, to be precise), but ω-consistent. The argument is similar to the first example: a suitable version of the
214:
1967:
Kurt Gödel (1931). 'Über formal unentscheidbare Sätze der
Principia Mathematica und verwandter Systeme I'. In
1224:
1930:
55:
1159:
923:
1704:{\displaystyle \forall x\,(\mathrm {Prov} _{T}(\ulcorner \varphi ({\dot {x}})\urcorner )\to \varphi (x))}
1370:
is required to be that of the model, i.e. the model contains only the natural numbers. (Other models of
419:
Therefore, assuming that PA is consistent, PA + ¬Con(PA) is consistent too. However, it would
51:
1569:
545:-sound ω-inconsistent theories using only the language of arithmetic can be constructed as follows. Let
1085:
The concept of theories of arithmetic whose integers are the true mathematical integers is captured by
1909:
1745:
1314:
496:
610:
760:
1879:
1865:
1407:
1379:
993:
431:
is not the Gödel number of a proof that 0=1. However, PA + ¬Con(PA) proves that, for
367:-soundness has the following computational interpretation: if the theory proves that a program
309:
1717:
1988:
1126:
interprets as natural numbers, not all of which need be named by one of the specified names.
279:
1307:
is redundant and may be omitted from the language, with the consequent of the rule for each
446:
the Gödel number of such a proof (this is just a direct restatement of the claim ¬Con(PA)).
1602:
1014:
8:
960:
274:(i.e., the structure of the usual natural numbers with addition and multiplication). If
1947:
94:
of arithmetic if there is a translation of formulas of arithmetic into the language of
31:
489:
is arithmetically sound (as any nonstandard model of PA can be expanded to a model of
1915:
1939:
1300:
1146:
87:
1973:
On
Formally Undecidable Propositions of Principia Mathematica and Related Systems
91:
408:
1816:
Vol. I, Wolters-Noordhoff, North-Holland 0-7204-2103-9, Elsevier 0-444-10088-1.
1789:
1496:{\displaystyle T+\mathrm {RFN} _{T}+\mathrm {Th} _{\Pi _{2}^{0}}(\mathbb {N} )}
1358:
whose domain includes the natural numbers and whose specified names and symbol
379:
291:
103:
1982:
218:
63:
1070:), hence it satisfies an analogue of Gödel's second incompleteness theorem.
1059:
308:
More generally, we can define an analogous concept for higher levels of the
67:
1055:
400:
1891:
1107:
1006:. The argument is more complicated (it relies on the provability of the Σ
1951:
1839:
1734:
with one free variable. In particular, a finitely axiomatizable theory
347:
1840:
A Note on
Wittgenstein's "Notorious Paragraph" about the Gödel Theorem
1079:
1094:
1062:
derivability conditions holds for the "provability predicate" ω-Prov(
335:
1943:
1928:
Boolos, G.; Smorynski, C. (1988). "Self-Reference and Modal Logic".
1366:
is absent from the language then what would have been the domain of
225:(Quine has thus called such theories "numerically insegregative").
1051:
1041:
555:
be the subtheory of PA with the induction schema restricted to Σ
460:
1738:
in the language of arithmetic is ω-consistent if and only if
121:
of natural numbers (defined by a formula in the language of
1410:, ω-consistency has the following characterization, due to
1397:
1386:
has an ω-model if and only if it is consistent in ω-logic.
1106:
itself could be referring to more general objects, such as
602:
is an instance of the induction schema, which has the form
346:
of the language of arithmetic (as opposed to, for example,
141:(2), and so on (that is, for every standard natural number
1566:-sentences valid in the standard model of arithmetic, and
1555:{\displaystyle \mathrm {Th} _{\Pi _{2}^{0}}(\mathbb {N} )}
70:, who introduced the concept in the course of proving the
1374:
may interpret these symbols nonstandardly; the domain of
453:, hence the system PA + ¬Con(PA) is in fact Σ
1814:
A Series of
Monographs on Pure and Applied Mathematics
394:
312:. If Γ is a set of arithmetical sentences (typically Σ
1748:
1720:
1618:
1572:
1513:
1427:
1317:
1227:
1162:
926:
763:
613:
499:
427:, PA, and hence PA + ¬Con(PA), proves that
423:
be ω-consistent. This is because, for any particular
908:(actually, even the pure predicate calculus) proves
286:-soundness is equivalent to demanding that whenever
278:
is strong enough to formalize a reasonable model of
242:
There is a weaker but closely related property of Σ
1766:
1726:
1703:
1593:
1554:
1495:
1339:
1294:given by its specified name, then it also asserts
1270:
1213:
1042:Arithmetically unsound, ω-consistent theories
951:
879:
739:
518:
461:Arithmetically sound, ω-inconsistent theories
1864:The definition of this symbolism can be found at
1980:
1097:language that includes a unary predicate symbol
1927:
177:. This may not generate a contradiction within
1390:ω-consistent if and only if its closure under
485:is a new constant added to the language. Then
301:actually halts. Every ω-consistent theory is Σ
161:also proves that there is some natural number
1282:That is, if the theory asserts (i.e. proves)
580:be its single axiom, and consider the theory
270:is true in the standard model of arithmetic
1855:" (2023), p.14. Accessed 12 September 2023.
1825:Smorynski, "The incompleteness theorems",
1804:
1802:
1394:applications of the ω-rule is consistent.
1907:
1625:
1545:
1486:
1324:
1271:{\displaystyle \forall x\,(N(x)\to P(x))}
1234:
933:
801:
770:
712:
651:
620:
506:
102:is able to prove the basic axioms of the
1812:(1971), p.207. Bibliotheca Mathematica:
1398:Relation to other consistency principles
449:In this example, the axiom ¬Con(PA) is Σ
395:Consistent, ω-inconsistent theories
1799:
14:
1981:
1382:, the converse also holds: the theory
1214:{\displaystyle P(0),P(1),P(2),\ldots }
1290:) separately for each natural number
1066:) = ¬ω-Con(PA + ¬
414:Gödel's second incompleteness theorem
1783:
1421:is ω-consistent if and only if
952:{\displaystyle \exists x\,\neg P(x)}
576:is finitely axiomatizable, let thus
493:), but ω-inconsistent (as it proves
262:, in another terminology) if every Σ
457:-unsound, not just ω-inconsistent.
58:) that is not only (syntactically)
24:
1853:Adventures in Gödel Incompleteness
1750:
1640:
1637:
1634:
1631:
1619:
1594:{\displaystyle \mathrm {RFN} _{T}}
1581:
1578:
1575:
1525:
1519:
1516:
1466:
1460:
1457:
1442:
1439:
1436:
1318:
1228:
996:over the (obviously sound) theory
934:
927:
795:
764:
706:
645:
614:
500:
25:
2000:
1898:, North-Holland, Amsterdam, 1977.
1141:) with a specified free variable
900:), then for every natural number
185:may not be able to prove for any
330:if every Γ-sentence provable in
1961:
1810:Introduction to Metamathematics
1767:{\displaystyle \Sigma _{2}^{0}}
1609:, which consists of the axioms
1340:{\displaystyle \forall x\,P(x)}
469:be PA together with the axioms
1971:. Translated into English as
1911:Self-reference and modal logic
1901:
1896:Handbook of Mathematical Logic
1885:
1871:
1858:
1845:
1832:
1827:Handbook of Mathematical Logic
1819:
1698:
1695:
1689:
1683:
1680:
1674:
1659:
1650:
1626:
1549:
1541:
1490:
1482:
1334:
1328:
1265:
1262:
1256:
1250:
1247:
1241:
1235:
1202:
1196:
1187:
1181:
1172:
1166:
946:
940:
874:
871:
859:
853:
850:
847:
829:
823:
820:
808:
802:
789:
777:
771:
731:
728:
716:
703:
700:
697:
679:
673:
670:
658:
652:
639:
627:
621:
565: > 0. The theory
519:{\displaystyle \exists x\,c=x}
113:that interprets arithmetic is
13:
1:
1931:The Journal of Symbolic Logic
77:
1603:uniform reflection principle
1110:or sets; thus in a model of
974:It is possible to show that
740:{\displaystyle \forall w\,.}
416:, PA would be inconsistent.
355:
305:-sound, but not vice versa.
7:
880:{\displaystyle \forall w\,}
389:
62:(that is, does not prove a
10:
2005:
1969:Monatshefte für Mathematik
1077:
1073:
1908:Smoryński, Craig (1985).
1408:recursively axiomatizable
752:If we denote the formula
201:) fails, only that there
1794:Set Theory and Its Logic
1777:
1727:{\displaystyle \varphi }
1078:Not to be confused with
985:-sound. In fact, it is Π
477:for each natural number
399:Write PA for the theory
106:under this translation.
1880:then it proves anything
1114:the objects satisfying
44:numerically segregative
1866:arithmetical hierarchy
1768:
1728:
1705:
1595:
1556:
1497:
1380:omitting types theorem
1341:
1272:
1215:
953:
916:). On the other hand,
881:
741:
520:
310:arithmetical hierarchy
266:-sentence provable in
209:. In particular, such
117:if, for some property
72:incompleteness theorem
1769:
1729:
1706:
1596:
1557:
1498:
1342:
1273:
1216:
954:
882:
742:
598:. We can assume that
521:
338:. If the language of
246:-soundness. A theory
1914:. Berlin: Springer.
1829:, 1977, p. 851.
1746:
1718:
1616:
1570:
1511:
1425:
1315:
1225:
1160:
1015:reflection principle
961:logically equivalent
924:
761:
611:
497:
1763:
1742: + PA is
1562:is the set of all Π
1538:
1479:
971:is ω-inconsistent.
920:proves the formula
561:-formulas, for any
215:nonstandard integer
27:Mathematical theory
1764:
1749:
1724:
1714:for every formula
1701:
1591:
1552:
1524:
1493:
1465:
1337:
1268:
1211:
949:
877:
737:
516:
354:is different, see
32:mathematical logic
1921:978-0-387-96209-2
1671:
1122:) are those that
1093:be a theory in a
534:for every number
213:is necessarily a
18:Omega-consistency
16:(Redirected from
1996:
1956:
1955:
1925:
1905:
1899:
1889:
1883:
1882:, including 0=1.
1875:
1869:
1862:
1856:
1849:
1843:
1836:
1830:
1823:
1817:
1806:
1797:
1787:
1773:
1771:
1770:
1765:
1762:
1757:
1733:
1731:
1730:
1725:
1710:
1708:
1707:
1702:
1673:
1672:
1664:
1649:
1648:
1643:
1600:
1598:
1597:
1592:
1590:
1589:
1584:
1561:
1559:
1558:
1553:
1548:
1540:
1539:
1537:
1532:
1522:
1502:
1500:
1499:
1494:
1489:
1481:
1480:
1478:
1473:
1463:
1451:
1450:
1445:
1346:
1344:
1343:
1338:
1303:, the predicate
1301:Peano arithmetic
1277:
1275:
1274:
1269:
1220:
1218:
1217:
1212:
959:, because it is
958:
956:
955:
950:
886:
884:
883:
878:
746:
744:
743:
738:
525:
523:
522:
517:
401:Peano arithmetic
386:actually halts.
239:ω-inconsistent.
40:omega-consistent
21:
2004:
2003:
1999:
1998:
1997:
1995:
1994:
1993:
1979:
1978:
1964:
1959:
1944:10.2307/2274450
1922:
1906:
1902:
1890:
1886:
1876:
1872:
1863:
1859:
1850:
1846:
1838:Floyd, Putnam,
1837:
1833:
1824:
1820:
1807:
1800:
1788:
1784:
1780:
1758:
1753:
1747:
1744:
1743:
1719:
1716:
1715:
1663:
1662:
1644:
1630:
1629:
1617:
1614:
1613:
1585:
1574:
1573:
1571:
1568:
1567:
1565:
1544:
1533:
1528:
1523:
1515:
1514:
1512:
1509:
1508:
1485:
1474:
1469:
1464:
1456:
1455:
1446:
1435:
1434:
1426:
1423:
1422:
1412:Craig Smoryński
1400:
1316:
1313:
1312:
1311:simplifying to
1226:
1223:
1222:
1161:
1158:
1157:
1083:
1076:
1049:
1044:
1037:
1026:
1012:
1005:
991:
984:
925:
922:
921:
762:
759:
758:
612:
609:
608:
593:
575:
560:
554:
544:
498:
495:
494:
463:
456:
452:
435:natural number
397:
392:
377:
366:
317:
304:
285:
265:
255:
245:
104:natural numbers
80:
54:(collection of
28:
23:
22:
15:
12:
11:
5:
2002:
1992:
1991:
1977:
1976:
1963:
1960:
1958:
1957:
1920:
1900:
1884:
1870:
1857:
1851:H. Friedman, "
1844:
1831:
1818:
1808:S. C. Kleene,
1798:
1790:W. V. O. Quine
1781:
1779:
1776:
1761:
1756:
1752:
1723:
1712:
1711:
1700:
1697:
1694:
1691:
1688:
1685:
1682:
1679:
1676:
1670:
1667:
1661:
1658:
1655:
1652:
1647:
1642:
1639:
1636:
1633:
1628:
1624:
1621:
1588:
1583:
1580:
1577:
1563:
1551:
1547:
1543:
1536:
1531:
1527:
1521:
1518:
1505:
1504:
1503:is consistent.
1492:
1488:
1484:
1477:
1472:
1468:
1462:
1459:
1454:
1449:
1444:
1441:
1438:
1433:
1430:
1402:If the theory
1399:
1396:
1354:is a model of
1350:An ω-model of
1336:
1333:
1330:
1327:
1323:
1320:
1280:
1279:
1267:
1264:
1261:
1258:
1255:
1252:
1249:
1246:
1243:
1240:
1237:
1233:
1230:
1210:
1207:
1204:
1201:
1198:
1195:
1192:
1189:
1186:
1183:
1180:
1177:
1174:
1171:
1168:
1165:
1075:
1072:
1047:
1043:
1040:
1036: + 1
1032:
1022:
1011: + 2
1007:
1001:
990: + 3
986:
983: + 3
979:
963:to the axiom ¬
948:
945:
942:
939:
936:
932:
929:
890:
889:
888:
887:
876:
873:
870:
867:
864:
861:
858:
855:
852:
849:
846:
843:
840:
837:
834:
831:
828:
825:
822:
819:
816:
813:
810:
807:
804:
800:
797:
794:
791:
788:
785:
782:
779:
776:
773:
769:
766:
750:
749:
748:
747:
736:
733:
730:
727:
724:
721:
718:
715:
711:
708:
705:
702:
699:
696:
693:
690:
687:
684:
681:
678:
675:
672:
669:
666:
663:
660:
657:
654:
650:
647:
644:
641:
638:
635:
632:
629:
626:
623:
619:
616:
594: + ¬
589:
574: + 1
570:
556:
550:
542:
515:
512:
509:
505:
502:
462:
459:
454:
450:
396:
393:
391:
388:
372:
362:
313:
302:
292:Turing machine
290:proves that a
283:
263:
253:
243:
157:) holds), but
115:ω-inconsistent
79:
76:
42:, also called
26:
9:
6:
4:
3:
2:
2001:
1990:
1987:
1986:
1984:
1974:
1970:
1966:
1965:
1953:
1949:
1945:
1941:
1937:
1933:
1932:
1923:
1917:
1913:
1912:
1904:
1897:
1893:
1888:
1881:
1874:
1867:
1861:
1854:
1848:
1841:
1835:
1828:
1822:
1815:
1811:
1805:
1803:
1795:
1791:
1786:
1782:
1775:
1759:
1754:
1741:
1737:
1721:
1692:
1686:
1677:
1668:
1665:
1656:
1653:
1645:
1622:
1612:
1611:
1610:
1608:
1604:
1586:
1534:
1529:
1475:
1470:
1452:
1447:
1431:
1428:
1420:
1417:
1416:
1415:
1413:
1409:
1405:
1395:
1393:
1387:
1385:
1381:
1377:
1373:
1369:
1365:
1361:
1357:
1353:
1348:
1331:
1325:
1321:
1310:
1306:
1302:
1297:
1293:
1289:
1285:
1259:
1253:
1244:
1238:
1231:
1208:
1205:
1199:
1193:
1190:
1184:
1178:
1175:
1169:
1163:
1155:
1154:
1153:
1152:of the form:
1151:
1148:
1144:
1140:
1136:
1132:
1127:
1125:
1121:
1117:
1113:
1109:
1105:
1100:
1096:
1092:
1088:
1081:
1071:
1069:
1065:
1061:
1057:
1053:
1039:
1035:
1030:
1025:
1020:
1016:
1010:
1004:
999:
995:
989:
982:
977:
972:
970:
967:. Therefore,
966:
962:
943:
937:
930:
919:
915:
911:
907:
904:, the theory
903:
899:
895:
868:
865:
862:
856:
844:
841:
838:
835:
832:
826:
817:
814:
811:
805:
798:
792:
786:
783:
780:
774:
767:
757:
756:
755:
754:
753:
734:
725:
722:
719:
713:
709:
694:
691:
688:
685:
682:
676:
667:
664:
661:
655:
648:
642:
636:
633:
630:
624:
617:
607:
606:
605:
604:
603:
601:
597:
592:
587:
584: =
583:
579:
573:
568:
564:
559:
553:
548:
539:
537:
533:
530: ≠
529:
513:
510:
507:
503:
492:
488:
484:
480:
476:
473: ≠
472:
468:
458:
447:
445:
442:
438:
434:
430:
426:
422:
417:
415:
410:
406:
402:
387:
385:
381:
375:
370:
365:
359:
357:
353:
349:
345:
341:
337:
333:
329:
325:
321:
316:
311:
306:
300:
296:
293:
289:
281:
277:
273:
269:
261:
257:
249:
240:
238:
234:
230:
226:
224:
220:
216:
212:
208:
204:
200:
196:
192:
188:
184:
180:
176:
172:
168:
164:
160:
156:
152:
148:
144:
140:
136:
132:
128:
124:
120:
116:
112:
107:
105:
101:
97:
93:
89:
85:
75:
73:
69:
65:
64:contradiction
61:
57:
53:
49:
45:
41:
37:
33:
19:
1989:Proof theory
1968:
1962:Bibliography
1935:
1929:
1926:Reviewed in
1910:
1903:
1895:
1887:
1873:
1860:
1847:
1834:
1826:
1821:
1813:
1809:
1793:
1785:
1739:
1735:
1713:
1606:
1506:
1418:
1403:
1401:
1391:
1388:
1383:
1375:
1371:
1367:
1363:
1359:
1355:
1351:
1349:
1308:
1304:
1295:
1291:
1287:
1283:
1281:
1149:
1142:
1138:
1134:
1130:
1128:
1123:
1119:
1115:
1111:
1108:real numbers
1103:
1098:
1090:
1086:
1084:
1067:
1063:
1045:
1033:
1028:
1023:
1018:
1008:
1002:
997:
994:conservative
987:
980:
975:
973:
968:
964:
917:
913:
909:
905:
901:
897:
893:
891:
751:
599:
595:
590:
585:
581:
577:
571:
566:
562:
557:
551:
546:
540:
535:
531:
527:
490:
486:
482:
478:
474:
470:
466:
464:
448:
443:
440:
436:
432:
428:
424:
420:
418:
409:Gödel number
404:
398:
383:
382:halts, then
373:
368:
363:
360:
351:
343:
339:
331:
327:
323:
322:), a theory
319:
314:
307:
298:
297:halts, then
294:
287:
275:
271:
267:
260:1-consistent
259:
251:
247:
241:
236:
233:ω-consistent
232:
228:
227:
222:
210:
206:
202:
198:
194:
190:
186:
182:
178:
174:
170:
166:
162:
158:
154:
150:
149:proves that
146:
142:
138:
134:
130:
126:
122:
118:
114:
110:
108:
99:
95:
83:
81:
47:
43:
39:
36:ω-consistent
35:
29:
280:computation
86:is said to
1892:J. Barwise
1147:infinitary
348:set theory
165:such that
78:Definition
68:Kurt Gödel
60:consistent
1751:Σ
1722:φ
1687:φ
1684:→
1678:⌝
1669:˙
1657:φ
1654:⌜
1620:∀
1526:Π
1467:Π
1319:∀
1251:→
1229:∀
1209:…
1133:-formula
1095:countable
935:¬
928:∃
854:→
824:→
796:∀
793:∧
765:∀
707:∀
704:→
674:→
646:∀
643:∧
615:∀
501:∃
371:using a Σ
342:consists
336:soundness
318:for some
235:if it is
189:value of
88:interpret
82:A theory
56:sentences
1983:Category
1792:(1971),
1774:-sound.
1392:unnested
481:, where
390:Examples
205:such an
187:specific
181:because
98:so that
92:language
1952:2274450
1938:: 306.
1894:(ed.),
1601:is the
1087:ω-logic
1080:Ω-logic
1074:ω-logic
1056:Bernays
1052:Hilbert
407:is the
358:below.
356:ω-logic
328:Γ-sound
217:in any
129:proves
1950:
1918:
1842:(2000)
1507:Here,
1221:infer
1150:ω-rule
1089:. Let
526:, and
380:oracle
256:-sound
52:theory
48:theory
1948:JSTOR
1778:Notes
1156:From
1145:, an
219:model
193:that
175:fails
137:(1),
133:(0),
50:is a
34:, an
1916:ISBN
1605:for
1017:for
978:is Π
465:Let
433:some
344:only
258:(or
221:for
90:the
38:(or
1940:doi
1406:is
1060:Löb
1038:).
1027:in
892:by
538:).
421:not
326:is
282:, Σ
250:is
237:not
231:is
125:),
30:In
1985::
1946:.
1936:53
1934:.
1801:^
1414::
1347:.
444:is
439:,
376:−1
203:is
173:)
145:,
109:A
74:.
46:)
1975:.
1954:.
1942::
1924:.
1868:.
1796:.
1760:0
1755:2
1740:T
1736:T
1699:)
1696:)
1693:x
1690:(
1681:)
1675:)
1666:x
1660:(
1651:(
1646:T
1641:v
1638:o
1635:r
1632:P
1627:(
1623:x
1607:T
1587:T
1582:N
1579:F
1576:R
1564:2
1550:)
1546:N
1542:(
1535:0
1530:2
1520:h
1517:T
1491:)
1487:N
1483:(
1476:0
1471:2
1461:h
1458:T
1453:+
1448:T
1443:N
1440:F
1437:R
1432:+
1429:T
1419:T
1404:T
1384:T
1376:N
1372:T
1368:N
1364:N
1360:N
1356:T
1352:T
1335:)
1332:x
1329:(
1326:P
1322:x
1309:P
1305:N
1296:P
1292:n
1288:n
1286:(
1284:P
1278:.
1266:)
1263:)
1260:x
1257:(
1254:P
1248:)
1245:x
1242:(
1239:N
1236:(
1232:x
1206:,
1203:)
1200:2
1197:(
1194:P
1191:,
1188:)
1185:1
1182:(
1179:P
1176:,
1173:)
1170:0
1167:(
1164:P
1143:x
1139:x
1137:(
1135:P
1131:T
1124:T
1120:x
1118:(
1116:N
1112:T
1104:T
1099:N
1091:T
1082:.
1068:A
1064:A
1058:–
1054:–
1048:3
1034:n
1031:Σ
1029:I
1024:n
1021:Σ
1019:I
1013:-
1009:n
1003:n
1000:Σ
998:I
992:-
988:n
981:n
976:T
969:T
965:A
947:)
944:x
941:(
938:P
931:x
918:T
914:n
912:(
910:P
906:T
902:n
898:n
896:(
894:P
875:]
872:)
869:w
866:,
863:n
860:(
857:B
851:)
848:)
845:w
842:,
839:1
836:+
833:x
830:(
827:B
821:)
818:w
815:,
812:x
809:(
806:B
803:(
799:x
790:)
787:w
784:,
781:0
778:(
775:B
772:[
768:w
735:.
732:]
729:)
726:w
723:,
720:x
717:(
714:B
710:x
701:)
698:)
695:w
692:,
689:1
686:+
683:x
680:(
677:B
671:)
668:w
665:,
662:x
659:(
656:B
653:(
649:x
640:)
637:w
634:,
631:0
628:(
625:B
622:[
618:w
600:A
596:A
591:n
588:Σ
586:I
582:T
578:A
572:n
569:Σ
567:I
563:n
558:n
552:n
549:Σ
547:I
543:1
541:Σ
536:n
532:n
528:c
514:x
511:=
508:c
504:x
491:T
487:T
483:c
479:n
475:n
471:c
467:T
455:1
451:1
441:n
437:n
429:n
425:n
405:n
384:C
378:-
374:n
369:C
364:n
361:Σ
352:T
340:T
332:T
324:T
320:n
315:n
303:1
299:C
295:C
288:T
284:1
276:T
272:N
268:T
264:1
254:1
252:Σ
248:T
244:1
229:T
223:T
211:n
207:n
199:n
197:(
195:P
191:n
183:T
179:T
171:n
169:(
167:P
163:n
159:T
155:n
153:(
151:P
147:T
143:n
139:P
135:P
131:P
127:T
123:T
119:P
111:T
100:T
96:T
84:T
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.