122:
1704:
747:
1716:
25:
1740:
1728:
2168:
164:" (Kleene 1952, p. 59). An important feature of metamathematics is its emphasis on differentiating between reasoning from inside a system and from outside a system. An informal illustration of this is categorizing the proposition "2+2=4" as belonging to mathematics while categorizing the proposition "'2+2=4' is valid" as belonging to metamathematics.
899:
on 28 May 1936, read on 12 November 1936, and published in series 2, volume 42 (1936-7); it appeared in two sections: in Part 3 (pages 230-240), issued on Nov 30, 1936 and in Part 4 (pages 241-265), issued on Dec 23, 1936; Turing added corrections in volume 43(1937) pp. 544–546. See the footnote at
434:
Frege clearly denies that he reached this aim, and also that his main aim would be constructing an ideal language like
Leibniz's, what Frege declares to be quite hard and idealistic, however, not impossible task). Frege went on to employ his logical calculus in his research on the
879:
Church's paper was presented to the
American Mathematical Society on 19 April 1935 and published on 15 April 1936. Turing, who had made substantial progress in writing up his own results, was disappointed to learn of Church's proof upon its publication (see correspondence between
465:
from which all mathematical truths could in principle be proven. As such, this ambitious project is of great importance in the history of mathematics and philosophy, being one of the foremost products of the belief that such an undertaking may be achievable. However, in 1931,
188:(Richard 1905) concerning certain 'definitions' of real numbers in the English language is an example of the sort of contradictions that can easily occur if one fails to distinguish between mathematics and metamathematics. Something similar can be said around the well-known
567:). For any such system, there will always be statements about the natural numbers that are true, but that are unprovable within the system. The second incompleteness theorem, an extension of the first, shows that such a system cannot demonstrate its own consistency.
470:
proved definitively that PM, and in fact any other attempt, could never achieve this goal; that is, for any set of axioms and inference rules proposed to encapsulate mathematics, there would in fact be some truths of mathematics which could not be deduced from them.
199:, so that the early histories of the two fields, during the late 19th and early 20th centuries, largely overlap. More recently, mathematical logic has often included the study of new pure mathematics, such as
494:', a set of a certain type only allowed to contain sets of strictly lower types. Contemporary mathematics, however, avoids paradoxes such as Russell's in less unwieldy ways, such as the system of
490:
sought to avoid this problem by ruling out the unrestricted creation of arbitrary sets. This was achieved by replacing the notion of a general set with notion of a hierarchy of sets of different '
914:
160:
in the early part of the 20th century. Metamathematics provides "a rigorous mathematical technique for investigating a great variety of foundation problems for mathematics and
335:
consequences for metamathematics. Before its discovery there was just one geometry and mathematics; the idea that another geometry existed was considered improbable.
350:(Latin, "the Prince of Mathematicians"). The "uproar of the Boeotians" came and went, and gave an impetus to metamathematics and great improvements in
719:
published independent papers showing that a general solution to the
Entscheidungsproblem is impossible, assuming that the intuitive notation of "
1164:
888:
708:
can also be viewed as asking for an algorithm to decide whether a given statement is provable from the axioms using the rules of logic.
559:" (e.g., a computer program, but it could be any sort of algorithm) is capable of proving all truths about the relations of the
2192:
89:
855:
1081:
148:
about other mathematical theories. Emphasis on metamathematics (and perhaps the creation of the term itself) owes itself to
61:
1527:
507:
467:
1824:
1013:
984:, 3 vols, Cambridge University Press, 1910, 1912, and 1913. Second edition, 1925 (Vol. 1), 1927 (Vols 2, 3). Abridged as
1953:
1672:
1157:
342:
discovered hyperbolic geometry, it is said that he did not publish anything about it out of fear of the "uproar of the
181:
68:
1076:
699:
2102:
1744:
1121:
108:
2186:
1208:
242:, in which finitary methods are used to study various axiomatized mathematical theorems (Kleene 1952, p. 55).
42:
304:
and metamathematics broadly overlap, and both have been substantially subsumed by mathematical logic in academia.
1778:
1622:
495:
75:
1106:
586:
555:
The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an "
2107:
1720:
46:
694:
beyond the usual axioms of first-order logic) and answers "Yes" or "No" according to whether the statement is
1150:
637:
As expressed in semi-natural language (where 'S' is the name of the sentence abbreviated to S): 'S' is true
57:
1732:
2213:
2182:
1647:
1203:
1131:
549:
2133:
1218:
1126:
1064:
436:
318:
157:
2112:
2037:
1819:
1632:
1604:
1241:
775:
533:
423:
2010:
1677:
1049:
732:
598:
121:
2094:
1562:
1552:
1522:
1456:
1191:
1069:
1006:
322:
35:
816:
1660:
1557:
1537:
1532:
1461:
1186:
1101:
971:
847:
720:
453:
Principia
Mathematica, or "PM" as it is often abbreviated, was an attempt to describe a set of
939:
2148:
1687:
1617:
1494:
1418:
1357:
1342:
1337:
1314:
1196:
980:
885:
448:
427:
355:
126:
82:
702:, a statement is universally valid if and only if it can be deduced from the axioms, so the
2067:
1913:
1667:
1547:
1542:
1466:
1367:
1096:
1091:
1043:
895:). Turing quickly completed his paper and rushed it to publication; it was received by the
653:
590:
537:
483:
235:
189:
185:
177:
8:
2223:
2022:
2005:
1985:
1948:
1897:
1892:
1834:
1771:
1682:
1592:
1514:
1413:
1347:
1304:
1294:
1274:
1037:
946:
631:
627:
556:
351:
328:
145:
1958:
1887:
1844:
1708:
1627:
1567:
1499:
1489:
1428:
1403:
1279:
1236:
1231:
999:
934:
840:
752:
517:
462:
196:
2172:
2143:
2138:
2128:
2062:
1990:
1875:
1703:
1423:
1408:
1352:
1299:
851:
746:
687:
238:), in the early 20th century. In his hands, it meant something akin to contemporary
2077:
1803:
1798:
1637:
1612:
1484:
1332:
1269:
1059:
975:
669:
609:
521:
246:
208:
1865:
1577:
1504:
1433:
1226:
892:
728:
665:
613:
602:
560:
491:
377:
371:
343:
282:
274:
224:
204:
192:(Does the set of all those sets that do not contain themselves contain itself?).
153:
991:
601:. Some authors refer to it as the "Equivalence Schema", a synonym introduced by
2218:
2177:
1870:
1849:
1764:
1655:
1582:
1289:
1116:
724:
638:
582:
536:. The two results are widely, but not universally, interpreted as showing that
458:
266:
250:
2207:
2027:
1968:
1443:
1375:
1327:
760:
712:
673:
594:
479:
390:
386:
286:
278:
270:
258:
231:
219:
149:
529:
422:." Frege's motivation for developing his formal approach to logic resembled
294:
2017:
1839:
1385:
1380:
1284:
780:
770:
239:
212:
1142:
2052:
2047:
2000:
1587:
1251:
1174:
1111:
1054:
716:
617:
545:
262:
173:
137:
234:
was the first to invoke the term "metamathematics" with regularity (see
1995:
1963:
1928:
1572:
1451:
1246:
929:
881:
564:
525:
415:
332:
290:
200:
141:
570:
176:
about mathematics itself were originally differentiated from ordinary
2057:
1918:
1829:
1086:
1022:
765:
683:
301:
254:
24:
1978:
1476:
1395:
1322:
576:
482:
on logic, which
Russell discovered allowed for the construction of
411:
2042:
1973:
1261:
647:
513:
419:
408:
520:
that establish inherent limitations of all but the most trivial
1880:
644:
Example: 'snow is white' is true if and only if snow is white.
630:, where they are applied in several important controversies in
2072:
1787:
817:"Principia Mathematica (Stanford Encyclopedia of Philosophy)"
691:
541:
532:
in 1931, are important both in mathematical logic and in the
454:
382:
359:
339:
161:
958:
Les
Principes des Mathématiques et le Problème des Ensembles
2032:
698:, i.e., valid in every structure satisfying the axioms. By
218:
Serious metamathematical reflection began with the work of
928:, New Series, Vol. 75, No. 299 (Jul., 1966), p. 431.
129:(shortened version), an important work of metamathematics.
626:. T-theories form the basis of much fundamental work in
180:
in the 19th century to focus on what was then called the
1756:
593:
of truth which lies at the heart of any realisation of
312:
140:
itself using mathematical methods. This study produces
819:. Metaphysics Research Lab, CSLI, Stanford University
381:(German for, roughly, "concept-script") is a book on
742:
571:
Tarski's definition of model-theoretic satisfaction
49:. Unsourced material may be challenged and removed.
921:, v. 53, No. 1 (Mar., 1988), pp. 36–50.
839:
1021:
501:
474:One of the main inspirations and motivations for
407:; the full title of the book identifies it as "a
2205:
964:(1905); translated in Heijenoort J. van (ed.),
962:Revue Générale des Sciences Pures et Appliquées
915:Alfred Tarski's Work on General Metamathematics
802:Philosophy of Geometry from Riemann to Poincare
723:" is captured by the functions computable by a
897:Proceedings of the London Mathematical Society
837:
727:(or equivalently, by those expressible in the
648:The undecidability of the Entscheidungsproblem
1772:
1158:
1007:
700:the completeness theorem of first-order logic
439:, carried out over the next quarter century.
245:Other prominent figures in the field include
703:
677:
659:
195:Metamathematics was intimately connected to
1172:
966:Source Book in Mathematical Logic 1879-1931
924:I. J. Good. "A Note on Richard's Paradox".
548:is impossible, giving a negative answer to
1779:
1765:
1165:
1151:
1014:
1000:
953:. North Holland. Aimed at mathematicians.
804:. Dordrecht Holland: Reidel. p. 255.
540:to find a complete and consistent set of
109:Learn how and when to remove this message
831:
799:
512:Gödel's incompleteness theorems are two
442:
120:
731:). This assumption is now known as the
2206:
814:
1760:
1146:
995:
686:that takes as input a statement of a
319:Non-Euclidean geometry § History
1727:
943:. Vintage Books. Aimed at laypeople.
313:The discovery of hyperbolic geometry
47:adding citations to reliable sources
18:
1954:Analytic and synthetic propositions
1825:Formal semantics (natural language)
1739:
988:, Cambridge University Press, 1962.
620:; such a formalisation is called a
608:The T-schema is often expressed in
13:
907:
808:
690:(possibly with a finite number of
365:
346:", which would ruin his status as
323:Hyperbolic geometry § History
182:foundational crisis of mathematics
14:
2235:
968:(Cambridge, Massachusetts, 1964).
2166:
1738:
1726:
1715:
1714:
1702:
815:Irvine, Andrew D. (1 May 2003).
745:
23:
1623:Computational complexity theory
1082:Gödel's incompleteness theorems
951:Introduction to Metamathematics
34:needs additional citations for
873:
864:
793:
612:, but it can be formalized in
508:Gödel's incompleteness theorem
502:Gödel's incompleteness theorem
468:Gödel's incompleteness theorem
1:
919:The Journal of Symbolic Logic
913:W. J. Blok and Don Pigozzi, "
786:
389:, published in 1879, and the
307:
1077:Gödel's completeness theorem
986:Principia Mathematica to *56
7:
846:. Clarendon Press. p.
738:
672:') is a challenge posed by
614:many-sorted predicate logic
528:. The theorems, proven by
496:Zermelo–Fraenkel set theory
16:Study of mathematics itself
10:
2240:
1673:Films about mathematicians
1065:Foundations of mathematics
800:Torretti, Roberto (1978).
651:
585:(not to be confused with '
574:
505:
446:
437:foundations of mathematics
369:
316:
167:
158:foundations of mathematics
2161:
2121:
2093:
2086:
2038:Necessity and sufficiency
1941:
1906:
1858:
1812:
1794:
1786:
1696:
1646:
1603:
1513:
1475:
1442:
1394:
1366:
1313:
1260:
1242:Philosophy of mathematics
1217:
1182:
1033:
776:Philosophy of mathematics
534:philosophy of mathematics
399:is usually translated as
1678:Recreational mathematics
1107:Löwenheim–Skolem theorem
599:semantic theory of truth
550:Hilbert's second problem
478:was the earlier work of
1563:Mathematical statistics
1553:Mathematical psychology
1523:Engineering mathematics
1457:Algebraic number theory
1132:Use–mention distinction
838:Wolfgang KĂĽnne (2003).
348:princeps mathematicorum
1709:Mathematics portal
1558:Mathematical sociology
1538:Mathematical economics
1533:Mathematical chemistry
1462:Analytic number theory
1343:Differential equations
1127:Type–token distinction
972:Alfred North Whitehead
900:the end of Soare:1996.
721:effectively calculable
704:
678:
660:
589:') is used to give an
581:The T-schema or truth
430:(despite that, in his
426:'s motivation for his
393:set out in that book.
130:
125:The title page of the
2173:Philosophy portal
1688:Mathematics education
1618:Theory of computation
1338:Hypercomplex analysis
981:Principia Mathematica
870:Hilbert and Ackermann
449:Principia Mathematica
443:Principia Mathematica
428:calculus ratiocinator
414:, modeled on that of
356:analytical philosophy
228:, published in 1879.
178:mathematical theorems
146:mathematical theories
127:Principia Mathematica
124:
1668:Informal mathematics
1548:Mathematical physics
1543:Mathematical finance
1528:Mathematical biology
1467:Diophantine geometry
1050:Church–Turing thesis
1044:Entscheidungsproblem
886:Alonzo Church papers
842:Conceptions of truth
733:Church–Turing thesis
705:Entscheidungsproblem
679:Entscheidungsproblem
661:Entscheidungsproblem
654:Entscheidungsproblem
591:inductive definition
43:improve this article
1835:Philosophy of logic
1683:Mathematics and art
1593:Operations research
1348:Functional analysis
947:Stephen Cole Kleene
940:Gödel, Escher, Bach
632:analytic philosophy
628:philosophical logic
557:effective procedure
352:mathematical rigour
329:hyperbolic geometry
2214:Mathematical logic
2134:Rules of inference
2103:Mathematical logic
1845:Semantics of logic
1628:Numerical analysis
1237:Mathematical logic
1232:Information theory
935:Douglas Hofstadter
891:2010-06-07 at the
753:Mathematics portal
518:mathematical logic
197:mathematical logic
131:
2201:
2200:
2157:
2156:
1991:Deductive closure
1937:
1936:
1876:Critical thinking
1754:
1753:
1353:Harmonic analysis
1140:
1139:
857:978-0-19-928019-3
696:universally valid
688:first-order logic
538:Hilbert's program
524:capable of doing
522:axiomatic systems
327:The discovery of
236:Hilbert's program
222:, especially his
190:Russell's paradox
186:Richard's paradox
172:Metamathematical
119:
118:
111:
93:
58:"Metamathematics"
2231:
2171:
2170:
2169:
2091:
2090:
1856:
1855:
1820:Computer science
1781:
1774:
1767:
1758:
1757:
1742:
1741:
1730:
1729:
1718:
1717:
1707:
1706:
1638:Computer algebra
1613:Computer science
1333:Complex analysis
1167:
1160:
1153:
1144:
1143:
1060:Effective method
1038:Cantor's theorem
1016:
1009:
1002:
993:
992:
976:Bertrand Russell
901:
877:
871:
868:
862:
861:
845:
835:
829:
828:
826:
824:
812:
806:
805:
797:
755:
750:
749:
707:
681:
670:decision problem
663:
610:natural language
484:paradoxical sets
405:concept notation
247:Bertrand Russell
209:recursion theory
136:is the study of
114:
107:
103:
100:
94:
92:
51:
27:
19:
2239:
2238:
2234:
2233:
2232:
2230:
2229:
2228:
2204:
2203:
2202:
2197:
2167:
2165:
2153:
2117:
2108:Boolean algebra
2082:
1933:
1924:Metamathematics
1902:
1854:
1808:
1790:
1785:
1755:
1750:
1701:
1692:
1642:
1599:
1578:Systems science
1509:
1505:Homotopy theory
1471:
1438:
1390:
1362:
1309:
1256:
1227:Category theory
1213:
1178:
1171:
1141:
1136:
1029:
1027:metamathematics
1020:
956:Jules Richard,
910:
908:Further reading
905:
904:
893:Wayback Machine
878:
874:
869:
865:
858:
836:
832:
822:
820:
813:
809:
798:
794:
789:
751:
744:
741:
729:lambda calculus
656:
650:
603:Michael Dummett
579:
573:
561:natural numbers
510:
504:
459:inference rules
451:
445:
401:concept writing
397:Begriffsschrift
378:Begriffsschrift
374:
372:Begriffsschrift
368:
366:Begriffsschrift
325:
315:
310:
283:Gregory Chaitin
275:Paul Benacerraf
225:Begriffsschrift
205:category theory
170:
134:Metamathematics
115:
104:
98:
95:
52:
50:
40:
28:
17:
12:
11:
5:
2237:
2227:
2226:
2221:
2216:
2199:
2198:
2196:
2195:
2190:
2180:
2175:
2162:
2159:
2158:
2155:
2154:
2152:
2151:
2146:
2141:
2136:
2131:
2125:
2123:
2119:
2118:
2116:
2115:
2110:
2105:
2099:
2097:
2088:
2084:
2083:
2081:
2080:
2075:
2070:
2065:
2060:
2055:
2050:
2045:
2040:
2035:
2030:
2025:
2020:
2015:
2014:
2013:
2003:
1998:
1993:
1988:
1983:
1982:
1981:
1976:
1966:
1961:
1956:
1951:
1945:
1943:
1939:
1938:
1935:
1934:
1932:
1931:
1926:
1921:
1916:
1910:
1908:
1904:
1903:
1901:
1900:
1895:
1890:
1885:
1884:
1883:
1878:
1868:
1862:
1860:
1853:
1852:
1847:
1842:
1837:
1832:
1827:
1822:
1816:
1814:
1810:
1809:
1807:
1806:
1801:
1795:
1792:
1791:
1784:
1783:
1776:
1769:
1761:
1752:
1751:
1749:
1748:
1736:
1724:
1712:
1697:
1694:
1693:
1691:
1690:
1685:
1680:
1675:
1670:
1665:
1664:
1663:
1656:Mathematicians
1652:
1650:
1648:Related topics
1644:
1643:
1641:
1640:
1635:
1630:
1625:
1620:
1615:
1609:
1607:
1601:
1600:
1598:
1597:
1596:
1595:
1590:
1585:
1583:Control theory
1575:
1570:
1565:
1560:
1555:
1550:
1545:
1540:
1535:
1530:
1525:
1519:
1517:
1511:
1510:
1508:
1507:
1502:
1497:
1492:
1487:
1481:
1479:
1473:
1472:
1470:
1469:
1464:
1459:
1454:
1448:
1446:
1440:
1439:
1437:
1436:
1431:
1426:
1421:
1416:
1411:
1406:
1400:
1398:
1392:
1391:
1389:
1388:
1383:
1378:
1372:
1370:
1364:
1363:
1361:
1360:
1358:Measure theory
1355:
1350:
1345:
1340:
1335:
1330:
1325:
1319:
1317:
1311:
1310:
1308:
1307:
1302:
1297:
1292:
1287:
1282:
1277:
1272:
1266:
1264:
1258:
1257:
1255:
1254:
1249:
1244:
1239:
1234:
1229:
1223:
1221:
1215:
1214:
1212:
1211:
1206:
1201:
1200:
1199:
1194:
1183:
1180:
1179:
1170:
1169:
1162:
1155:
1147:
1138:
1137:
1135:
1134:
1129:
1124:
1119:
1117:Satisfiability
1114:
1109:
1104:
1102:Interpretation
1099:
1094:
1089:
1084:
1079:
1074:
1073:
1072:
1062:
1057:
1052:
1047:
1040:
1034:
1031:
1030:
1019:
1018:
1011:
1004:
996:
990:
989:
969:
954:
944:
932:
922:
909:
906:
903:
902:
884:and Church in
872:
863:
856:
830:
807:
791:
790:
788:
785:
784:
783:
778:
773:
768:
763:
757:
756:
740:
737:
725:Turing machine
652:Main article:
649:
646:
639:if and only if
575:Main article:
572:
569:
506:Main article:
503:
500:
463:symbolic logic
447:Main article:
444:
441:
370:Main article:
367:
364:
331:had important
314:
311:
309:
306:
267:Stephen Kleene
251:Thoralf Skolem
169:
166:
156:to secure the
117:
116:
31:
29:
22:
15:
9:
6:
4:
3:
2:
2236:
2225:
2222:
2220:
2217:
2215:
2212:
2211:
2209:
2194:
2191:
2188:
2184:
2181:
2179:
2176:
2174:
2164:
2163:
2160:
2150:
2149:Logic symbols
2147:
2145:
2142:
2140:
2137:
2135:
2132:
2130:
2127:
2126:
2124:
2120:
2114:
2111:
2109:
2106:
2104:
2101:
2100:
2098:
2096:
2092:
2089:
2085:
2079:
2076:
2074:
2071:
2069:
2066:
2064:
2061:
2059:
2056:
2054:
2051:
2049:
2046:
2044:
2041:
2039:
2036:
2034:
2031:
2029:
2028:Logical truth
2026:
2024:
2021:
2019:
2016:
2012:
2009:
2008:
2007:
2004:
2002:
1999:
1997:
1994:
1992:
1989:
1987:
1984:
1980:
1977:
1975:
1972:
1971:
1970:
1969:Contradiction
1967:
1965:
1962:
1960:
1957:
1955:
1952:
1950:
1947:
1946:
1944:
1940:
1930:
1927:
1925:
1922:
1920:
1917:
1915:
1914:Argumentation
1912:
1911:
1909:
1905:
1899:
1898:Philosophical
1896:
1894:
1893:Non-classical
1891:
1889:
1886:
1882:
1879:
1877:
1874:
1873:
1872:
1869:
1867:
1864:
1863:
1861:
1857:
1851:
1848:
1846:
1843:
1841:
1838:
1836:
1833:
1831:
1828:
1826:
1823:
1821:
1818:
1817:
1815:
1811:
1805:
1802:
1800:
1797:
1796:
1793:
1789:
1782:
1777:
1775:
1770:
1768:
1763:
1762:
1759:
1747:
1746:
1737:
1735:
1734:
1725:
1723:
1722:
1713:
1711:
1710:
1705:
1699:
1698:
1695:
1689:
1686:
1684:
1681:
1679:
1676:
1674:
1671:
1669:
1666:
1662:
1659:
1658:
1657:
1654:
1653:
1651:
1649:
1645:
1639:
1636:
1634:
1631:
1629:
1626:
1624:
1621:
1619:
1616:
1614:
1611:
1610:
1608:
1606:
1605:Computational
1602:
1594:
1591:
1589:
1586:
1584:
1581:
1580:
1579:
1576:
1574:
1571:
1569:
1566:
1564:
1561:
1559:
1556:
1554:
1551:
1549:
1546:
1544:
1541:
1539:
1536:
1534:
1531:
1529:
1526:
1524:
1521:
1520:
1518:
1516:
1512:
1506:
1503:
1501:
1498:
1496:
1493:
1491:
1488:
1486:
1483:
1482:
1480:
1478:
1474:
1468:
1465:
1463:
1460:
1458:
1455:
1453:
1450:
1449:
1447:
1445:
1444:Number theory
1441:
1435:
1432:
1430:
1427:
1425:
1422:
1420:
1417:
1415:
1412:
1410:
1407:
1405:
1402:
1401:
1399:
1397:
1393:
1387:
1384:
1382:
1379:
1377:
1376:Combinatorics
1374:
1373:
1371:
1369:
1365:
1359:
1356:
1354:
1351:
1349:
1346:
1344:
1341:
1339:
1336:
1334:
1331:
1329:
1328:Real analysis
1326:
1324:
1321:
1320:
1318:
1316:
1312:
1306:
1303:
1301:
1298:
1296:
1293:
1291:
1288:
1286:
1283:
1281:
1278:
1276:
1273:
1271:
1268:
1267:
1265:
1263:
1259:
1253:
1250:
1248:
1245:
1243:
1240:
1238:
1235:
1233:
1230:
1228:
1225:
1224:
1222:
1220:
1216:
1210:
1207:
1205:
1202:
1198:
1195:
1193:
1190:
1189:
1188:
1185:
1184:
1181:
1176:
1168:
1163:
1161:
1156:
1154:
1149:
1148:
1145:
1133:
1130:
1128:
1125:
1123:
1120:
1118:
1115:
1113:
1110:
1108:
1105:
1103:
1100:
1098:
1095:
1093:
1090:
1088:
1085:
1083:
1080:
1078:
1075:
1071:
1068:
1067:
1066:
1063:
1061:
1058:
1056:
1053:
1051:
1048:
1046:
1045:
1041:
1039:
1036:
1035:
1032:
1028:
1024:
1017:
1012:
1010:
1005:
1003:
998:
997:
994:
987:
983:
982:
977:
973:
970:
967:
963:
959:
955:
952:
948:
945:
942:
941:
936:
933:
931:
927:
923:
920:
916:
912:
911:
898:
894:
890:
887:
883:
876:
867:
859:
853:
849:
844:
843:
834:
818:
811:
803:
796:
792:
782:
779:
777:
774:
772:
769:
767:
764:
762:
759:
758:
754:
748:
743:
736:
734:
730:
726:
722:
718:
714:
713:Alonzo Church
709:
706:
701:
697:
693:
689:
685:
680:
676:in 1928. The
675:
674:David Hilbert
671:
667:
662:
655:
645:
642:
640:
635:
633:
629:
625:
624:
619:
615:
611:
606:
604:
600:
596:
595:Alfred Tarski
592:
588:
584:
578:
568:
566:
562:
558:
553:
551:
547:
543:
539:
535:
531:
527:
523:
519:
515:
509:
499:
497:
493:
489:
485:
481:
480:Gottlob Frege
477:
472:
469:
464:
460:
456:
450:
440:
438:
433:
429:
425:
421:
417:
413:
410:
406:
402:
398:
394:
392:
391:formal system
388:
387:Gottlob Frege
384:
380:
379:
373:
363:
361:
357:
353:
349:
345:
341:
336:
334:
333:philosophical
330:
324:
320:
305:
303:
298:
296:
292:
288:
287:Alfred Tarski
284:
280:
279:Hilary Putnam
276:
272:
271:Willard Quine
268:
264:
260:
259:Alonzo Church
256:
252:
248:
243:
241:
237:
233:
232:David Hilbert
229:
227:
226:
221:
220:Gottlob Frege
216:
214:
210:
206:
202:
198:
193:
191:
187:
183:
179:
175:
165:
163:
159:
155:
151:
150:David Hilbert
147:
143:
139:
135:
128:
123:
113:
110:
102:
99:November 2018
91:
88:
84:
81:
77:
74:
70:
67:
63:
60: –
59:
55:
54:Find sources:
48:
44:
38:
37:
32:This article
30:
26:
21:
20:
2068:Substitution
1923:
1888:Mathematical
1813:Major fields
1743:
1731:
1719:
1700:
1633:Optimization
1495:Differential
1419:Differential
1386:Order theory
1381:Graph theory
1285:Group theory
1122:Independence
1097:Decidability
1092:Completeness
1042:
1026:
985:
979:
965:
961:
957:
950:
938:
925:
918:
896:
875:
866:
841:
833:
821:. Retrieved
810:
801:
795:
781:Proof theory
771:Model theory
710:
695:
682:asks for an
657:
643:
636:
622:
621:
607:
587:Convention T
580:
554:
511:
487:
475:
473:
452:
431:
404:
400:
396:
395:
376:
375:
347:
337:
326:
299:
244:
240:proof theory
230:
223:
217:
213:model theory
194:
174:metatheorems
171:
144:, which are
142:metatheories
133:
132:
105:
96:
86:
79:
72:
65:
53:
41:Please help
36:verification
33:
2183:WikiProject
2053:Proposition
2048:Probability
2001:Description
1942:Foundations
1745:WikiProject
1588:Game theory
1568:Probability
1305:Homological
1295:Multilinear
1275:Commutative
1252:Type theory
1219:Foundations
1175:mathematics
1112:Metatheorem
1070:of geometry
1055:Consistency
717:Alan Turing
618:modal logic
546:mathematics
263:Alan Turing
138:mathematics
2224:Metatheory
2208:Categories
2113:Set theory
2011:Linguistic
2006:Entailment
1996:Definition
1964:Consequent
1959:Antecedent
1573:Statistics
1452:Arithmetic
1414:Arithmetic
1280:Elementary
1247:Set theory
882:Max Newman
787:References
565:arithmetic
530:Kurt Gödel
526:arithmetic
418:, of pure
416:arithmetic
317:See also:
308:Milestones
295:Kurt Gödel
291:Paul Cohen
201:set theory
69:newspapers
2144:Fallacies
2139:Paradoxes
2129:Logicians
2063:Statement
2058:Reference
2023:Induction
1986:Deduction
1949:Abduction
1919:Metalogic
1866:Classical
1830:Inference
1500:Geometric
1490:Algebraic
1429:Euclidean
1404:Algebraic
1300:Universal
1087:Soundness
1023:Metalogic
766:Metalogic
711:In 1936,
684:algorithm
344:Boeotians
302:metalogic
255:Emil Post
211:and pure
2178:Category
2078:Validity
1979:Antinomy
1907:Theories
1871:Informal
1721:Category
1477:Topology
1424:Discrete
1409:Analytic
1396:Geometry
1368:Discrete
1323:Calculus
1315:Analysis
1270:Abstract
1209:Glossary
1192:Timeline
949:, 1952.
937:, 1980.
889:Archived
823:5 August
739:See also
623:T-theory
577:T-schema
544:for all
514:theorems
432:Foreword
412:language
2193:changes
2185: (
2043:Premise
1974:Paradox
1804:History
1799:Outline
1733:Commons
1515:Applied
1485:General
1262:Algebra
1187:History
424:Leibniz
420:thought
409:formula
300:Today,
168:History
154:attempt
83:scholar
2095:topics
1881:Reason
1859:Logics
1850:Syntax
1434:Finite
1290:Linear
1197:Future
1173:Major
974:, and
854:
692:axioms
666:German
583:schema
542:axioms
455:axioms
321:, and
85:
78:
71:
64:
56:
2219:Logic
2122:other
2087:Lists
2073:Truth
1840:Proof
1788:Logic
1661:lists
1204:Lists
1177:areas
930:JStor
668:for '
492:types
383:logic
360:logic
340:Gauss
338:When
162:logic
90:JSTOR
76:books
2187:talk
2033:Name
2018:Form
1025:and
926:Mind
852:ISBN
825:2009
761:Meta
715:and
658:The
457:and
358:and
293:and
62:news
1929:Set
978:.
917:",
616:or
597:'s
516:of
461:in
403:or
385:by
152:'s
45:by
2210::
960:,
850:.
848:18
735:.
641:S
634:.
605:.
552:.
498:.
488:PM
486:.
476:PM
362:.
354:,
297:.
289:,
285:,
281:,
277:,
273:,
269:,
265:,
261:,
257:,
253:,
249:,
215:.
207:,
203:,
184:.
2189:)
1780:e
1773:t
1766:v
1166:e
1159:t
1152:v
1015:e
1008:t
1001:v
860:.
827:.
664:(
563:(
112:)
106:(
101:)
97:(
87:·
80:·
73:·
66:·
39:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
