66:"When we are engaged in investigating the foundations of a science, we must set up a system of axioms which contains an exact and complete description of the relations subsisting between the elementary ideas of that science. ... But above all I wish to designate the following as the most important among the numerous questions which can be asked with regard to the axioms: To prove that they are not contradictory, that is, that a definite number of logical steps based upon them can never lead to contradictory results. In geometry, the proof of the compatibility of the axioms can be effected by constructing a suitable field of numbers, such that analogous relations between the numbers of this field correspond to the geometrical axioms. ... On the other hand a direct method is needed for the proof of the compatibility of the arithmetical axioms."
128:, a member of the Hilbert school, in 1936, and by others since then. ... But these meta-mathematical proofs cannot be represented within the arithmetical calculus; and, since they are not finitistic, they do not achieve the proclaimed objectives of Hilbert's original program. ... The possibility of constructing a finitistic absolute proof of consistency for arithmetic is not excluded by Gödelâs results. Gödel showed that no such proof is possible that can be represented within arithmetic. His argument does not eliminate the possibility of strictly finitistic proofs that cannot be represented within arithmetic. But no one today appears to have a clear idea of what a finitistic proof would be like that is not capable of formulation within arithmetic."
2644:
89:. These do not provide a resolution to Hilbert's second question, however, because someone who doubts the consistency of Peano arithmetic is unlikely to accept the axioms of set theory (which are much stronger) to prove its consistency. Thus a satisfactory answer to Hilbert's problem must be carried out using principles that would be acceptable to someone who does not already believe PA is consistent. Such principles are often called
124:"This imposing result of Godel's analysis should not be misunderstood: it does not exclude a meta-mathematical proof of the consistency of arithmetic. What it excludes is a proof of consistency that can be mirrored by the formal deductions of arithmetic. Meta-mathematical proofs of the consistency of arithmetic have, in fact, been constructed, notably by
115:
shows that it is not possible for any proof that Peano
Arithmetic is consistent to be carried out within Peano arithmetic itself. This theorem shows that if the only acceptable proof procedures are those that can be formalized within arithmetic then Hilbert's call for a consistency proof cannot be
297:
Actually, the proof assigns a "notation" for an ordinal number to each proof. The notation is a finite string of symbols that intuitively stands for an ordinal number. By representing the ordinal in a finite way, Gentzen's proof does not presuppose strong axioms regarding ordinal
70:
Hilbert's statement is sometimes misunderstood, because by the "arithmetical axioms" he did not mean a system equivalent to Peano arithmetic, but a stronger system with a second-order completeness axiom. The system
Hilbert asked for a completeness proof of is more like
200:
While the theorems of Gödel and
Gentzen are now well understood by the mathematical logic community, no consensus has formed on whether (or in what way) these theorems answer Hilbert's second problem.
54:
proved results that cast new light on the problem. Some feel that Gödel's theorems give a negative solution to the problem, while others consider
Gentzen's proof as a partial positive solution.
143:
In 1936, Gentzen published a proof that Peano
Arithmetic is consistent. Gentzen's result shows that a consistency proof can be obtained in a system that is much weaker than set theory.
1023:
216:
argues that Gödel's theorem does not prevent a consistency proof because its hypotheses might not apply to all the systems in which a consistency proof could be carried out.
349:
Dawson, John W. (2006). "Shaken foundations or groundbreaking realignment? A Centennial
Assessment of Kurt Gödel's Impact on Logic, Mathematics, and Computer Science.".
1698:
752:
220:
calls the belief that Gödel's theorem eliminates the possibility of a persuasive consistency proof "erroneous", citing the consistency proof given by
Gentzen and
565:
1781:
922:
93:
because they are completely constructive and do not presuppose a completed infinity of natural numbers. Gödel's second incompleteness theorem (see
169:
in a stronger logic than first-order logic, but the consistency proof itself can be carried out in ordinary first-order logic using the axioms of
2095:
717:
2253:
1041:
106:
94:
2108:
1431:
745:
1693:
204:
argues that Gödel's incompleteness theorem shows that it is not possible to produce finitistic consistency proofs of strong theories.
2113:
2103:
1840:
1046:
888:
877:
1591:
1037:
2249:
613:
547:
428:
366:
208:
states that although Gödel's results imply that no finitistic syntactic consistency proof can be obtained, semantic (in particular,
882:
872:
557:
2346:
2090:
915:
852:
39:– free of any internal contradictions. Hilbert stated that the axioms he considered for arithmetic were the ones given in
1651:
1344:
1085:
86:
862:
857:
837:
832:
78:
As a nowadays common interpretation, a positive solution to
Hilbert's second question would in particular provide a proof that
2668:
2607:
2309:
2072:
2067:
1892:
1313:
997:
170:
867:
847:
842:
738:
161:
on these ordinals that no proof can conclude in a contradiction. The method used in this proof can also be used to prove a
138:
540:
Mathematical developments arising from
Hilbert problems (Proc. Sympos. Pure Math., Northern Illinois Univ., De Kalb, Ill.,)
192:
of the theories. A theory will be unable to prove the consistency of another theory with a higher proof theoretic ordinal.
2602:
2385:
2302:
2015:
1946:
1823:
1065:
822:
676:(2005). "Gödel's reformulation of Gentzen's first consistency proof of arithmetic: the no-counterexample interpretation".
574:
151:
112:
1673:
2527:
2353:
2039:
1272:
827:
802:
97:) places a severe limit on how weak a finitistic system can be while still proving the consistency of Peano arithmetic.
1678:
2010:
1749:
1007:
908:
2405:
2400:
807:
787:
2334:
1924:
1318:
1286:
977:
817:
812:
797:
792:
782:
772:
1051:
466:
85:
There are many known proofs that Peano arithmetic is consistent that can be carried out in strong systems such as
2624:
2573:
2470:
1968:
1929:
1406:
221:
2465:
1080:
2395:
1934:
1786:
1769:
1492:
972:
416:
2297:
2274:
2235:
2121:
2062:
1708:
1628:
1472:
1416:
1029:
72:
2587:
2314:
2292:
2259:
2152:
1998:
1983:
1956:
1907:
1791:
1726:
1551:
1517:
1512:
1386:
1217:
1194:
635:
2517:
2370:
2162:
1880:
1616:
1522:
1381:
1366:
1247:
1222:
599:
285:
158:
2643:
761:
32:
2490:
2452:
2329:
2133:
1973:
1897:
1875:
1703:
1661:
1560:
1527:
1391:
1179:
1090:
189:
379:(1990). "On an alleged refutation of Hilbert's Program using Gödel's First Incompleteness Theorem".
2619:
2510:
2495:
2475:
2432:
2319:
2269:
2195:
2140:
2077:
1870:
1865:
1813:
1581:
1570:
1242:
1142:
1070:
1061:
1057:
992:
987:
697:
640:
2648:
2417:
2380:
2365:
2358:
2341:
2127:
1993:
1919:
1902:
1855:
1668:
1577:
1411:
1396:
1356:
1308:
1293:
1281:
1237:
1212:
982:
931:
685:
661:
623:
486:
396:
233:
209:
2145:
1601:
2583:
2390:
2200:
2190:
2082:
1963:
1798:
1774:
1555:
1539:
1444:
1421:
1298:
1267:
1232:
1127:
962:
653:
609:
603:
543:
424:
408:
376:
362:
36:
2597:
2592:
2485:
2442:
2264:
2225:
2220:
2205:
2031:
1988:
1885:
1683:
1633:
1207:
1169:
645:
478:
450:
388:
354:
184:
in proof theory. In this program, formal theories of arithmetic or set theory are assigned
181:
166:
79:
2578:
2568:
2522:
2505:
2460:
2422:
2324:
2244:
2051:
1978:
1951:
1939:
1845:
1759:
1733:
1688:
1656:
1457:
1259:
1202:
1152:
1117:
1075:
673:
586:
506:
438:
185:
162:
125:
51:
2563:
2542:
2500:
2480:
2375:
2230:
1828:
1818:
1808:
1803:
1737:
1611:
1487:
1376:
1371:
1349:
950:
535:
467:"Ăber formal unentscheidbare SĂ€tze der Principia Mathematica und verwandter Systeme, I"
147:
2662:
2537:
2215:
1722:
1507:
1497:
1467:
1452:
1122:
502:
490:
462:
47:
28:
722:
400:
2437:
2284:
2185:
2177:
2057:
2005:
1914:
1850:
1833:
1764:
1623:
1482:
1184:
967:
582:
120:
explain, there is still room for a proof that cannot be formalized in arithmetic:
2547:
2427:
1606:
1596:
1543:
1227:
1147:
1132:
1012:
957:
20:
1477:
1332:
1303:
1109:
730:
420:
657:
150:, based on the structure of the proof, with each of these ordinals less than
2629:
2532:
1585:
1502:
1462:
1426:
1362:
1174:
1164:
1137:
146:
Gentzen's proof proceeds by assigning to each proof in Peano arithmetic an
2614:
2412:
1860:
1565:
1159:
358:
90:
2210:
1002:
689:
665:
494:
482:
454:
392:
900:
649:
1754:
1100:
945:
280:
A similar quotation with minor variations in wording appears in
904:
734:
212:) arguments can be used to give convincing consistency proofs.
538:(1976). "What have we learnt from Hilbert's second problem?".
441:(1936). "Die Widerspruchsfreiheit der reinen Zahlentheorie".
252:
351:
2006 21st Annual IEEE Symposium on Logic in
Computer Science
177:
gives a game-theoretic interpretation of Gentzen's method.
522:——— (1901) . "Mathematische Probleme".
413:
Godel's theorem: An Incomplete Guide to its Use and Abuse
255:, translated by M. Newson. For the original version, see
702:
From Frege to Gödel: A Source Book on Mathematical Logic
542:. Providence, R. I.: Amer. Math. Soc. pp. 93â130.
626:(1988). "Partial realizations of Hilbert's Program".
598:———; ——— (2001).
180:
Gentzen's consistency proof initiated the program of
511:
Jahresbericht der Deutschen Mathematiker-Vereinigung
2556:
2451:
2283:
2176:
2028:
1721:
1644:
1538:
1442:
1331:
1258:
1193:
1108:
1099:
1021:
938:
43:, which include a second order completeness axiom.
196:Modern viewpoints on the status of the problem
57:
916:
746:
723:English translation of Hilbert's 1900 address
704:. Harvard University Press. pp. 596â616.
566:Bulletin of the American Mathematical Society
8:
281:
268:
117:
1742:
1337:
1105:
923:
909:
901:
753:
739:
731:
718:Original text of Hilbert's talk, in German
62:In one English translation, Hilbert asks:
35:. It asks for a proof that arithmetic is
639:
319:
213:
58:Hilbert's problem and its interpretation
307:
256:
245:
205:
201:
173:and a transfinite induction principle.
40:
16:Consistency of the axioms of arithmetic
331:
217:
100:
471:Monatshefte fĂŒr Mathematik und Physik
7:
253:American Mathematical Society (1902)
174:
75:than first-order Peano arithmetic.
284:, p. 107–108, as revised by
222:a later one given by Gödel in 1958
14:
132:
2642:
524:Archiv der Mathematik und Physik
107:Gödel's incompleteness theorems
95:Gödel's incompleteness theorems
381:Journal of Philosophical Logic
171:primitive recursive arithmetic
101:Gödel's incompleteness theorem
1:
2603:History of mathematical logic
608:. New York University Press.
575:American Mathematical Society
113:second incompleteness theorem
2528:Primitive recursive function
593:. New York University Press.
449:. Springer: 493–565.
139:Gentzen's consistency proof
133:Gentzen's consistency proof
87:ZermeloâFraenkel set theory
2685:
1592:SchröderâBernstein theorem
1319:Monadic predicate calculus
978:Foundations of mathematics
678:Bulletin of Symbolic Logic
353:. IEEE. pp. 339â341.
136:
104:
2638:
2625:Philosophy of mathematics
2574:Automated theorem proving
1745:
1699:Von NeumannâBernaysâGödel
1340:
768:
628:Journal of Symbolic Logic
282:Nagel & Newman (2001)
269:Nagel & Newman (1958)
118:Nagel & Newman (1958)
387:(4). Springer: 343â377.
25:Hilbert's second problem
2275:Self-verifying theories
2096:Tarski's axiomatization
1047:Tarski's undefinability
1042:incompleteness theorems
558:"Mathematical Problems"
116:answered. However, as
73:second-order arithmetic
2649:Mathematics portal
2260:Proof of impossibility
1908:propositional variable
1218:Propositional calculus
600:Hofstadter, Douglas R.
507:"Ăber den Zahlbegriff"
271:, p. 96–99.
68:
31:in 1900 as one of his
2518:Kolmogorov complexity
2471:Computably enumerable
2371:Model complete theory
2163:Principia Mathematica
1223:Propositional formula
1052:BanachâTarski paradox
443:Mathematische Annalen
286:Douglas R. Hofstadter
159:transfinite induction
64:
2466:ChurchâTuring thesis
2453:Computability theory
1662:continuum hypothesis
1180:Square of opposition
1038:Gödel's completeness
698:van Heijenoort, Jean
530:(1): 44â63, 213â237.
359:10.1109/LICS.2006.47
190:consistency strength
157:. He then proves by
2620:Mathematical object
2511:P versus NP problem
2476:Computable function
2270:Reverse mathematics
2196:Logical consequence
2073:primitive recursive
2068:elementary function
1841:Free/bound variable
1694:TarskiâGrothendieck
1213:Logical connectives
1143:Logical equivalence
993:Logical consequence
624:Simpson, Stephen G.
2669:Hilbert's problems
2418:Transfer principle
2381:Semantics of logic
2366:Categorical theory
2342:Non-standard model
1856:Logical connective
983:Information theory
932:Mathematical logic
762:Hilbert's problems
483:10.1007/BF01700692
455:10.1007/BF01565428
393:10.1007/BF00263316
377:Detlefsen, Michael
234:Takeuti conjecture
2656:
2655:
2588:Abstract category
2391:Theories of truth
2201:Rule of inference
2191:Natural deduction
2172:
2171:
1717:
1716:
1422:Cartesian product
1327:
1326:
1233:Many-valued logic
1208:Boolean functions
1091:Russell's paradox
1066:diagonal argument
963:First-order logic
898:
897:
188:that measure the
2676:
2647:
2646:
2598:History of logic
2593:Category of sets
2486:Decision problem
2265:Ordinal analysis
2206:Sequent calculus
2104:Boolean algebras
2044:
2043:
2018:
1989:logical/constant
1743:
1729:
1652:ZermeloâFraenkel
1403:Set operations:
1338:
1275:
1106:
1086:LöwenheimâSkolem
973:Formal semantics
925:
918:
911:
902:
755:
748:
741:
732:
705:
693:
674:Tait, William W.
669:
643:
619:
594:
587:Newman, James R.
578:
577:: 437â479. 1902.
562:
553:
531:
518:
498:
493:. Archived from
458:
439:Gentzen, Gerhard
434:
404:
372:
335:
329:
323:
320:Detlefsen (1990)
317:
311:
305:
299:
295:
289:
278:
272:
266:
260:
250:
214:Detlefsen (1990)
182:ordinal analysis
167:Peano arithmetic
80:Peano arithmetic
2684:
2683:
2679:
2678:
2677:
2675:
2674:
2673:
2659:
2658:
2657:
2652:
2641:
2634:
2579:Category theory
2569:Algebraic logic
2552:
2523:Lambda calculus
2461:Church encoding
2447:
2423:Truth predicate
2279:
2245:Complete theory
2168:
2037:
2033:
2029:
2024:
2016:
1736: and
1732:
1727:
1713:
1689:New Foundations
1657:axiom of choice
1640:
1602:Gödel numbering
1542: and
1534:
1438:
1323:
1273:
1254:
1203:Boolean algebra
1189:
1153:Equiconsistency
1118:Classical logic
1095:
1076:Halting problem
1064: and
1040: and
1028: and
1027:
1022:Theorems (
1017:
934:
929:
899:
894:
764:
759:
728:
714:
709:
696:
672:
650:10.2307/2274508
622:
616:
597:
581:
560:
556:
550:
536:Kreisel, George
534:
521:
501:
461:
437:
431:
409:Franzen, Torkel
407:
375:
369:
348:
344:
339:
338:
330:
326:
318:
314:
306:
302:
296:
292:
279:
275:
267:
263:
251:
247:
242:
230:
198:
186:ordinal numbers
163:cut elimination
155:
141:
135:
126:Gerhard Gentzen
109:
103:
82:is consistent.
60:
52:Gerhard Gentzen
17:
12:
11:
5:
2682:
2680:
2672:
2671:
2661:
2660:
2654:
2653:
2639:
2636:
2635:
2633:
2632:
2627:
2622:
2617:
2612:
2611:
2610:
2600:
2595:
2590:
2581:
2576:
2571:
2566:
2564:Abstract logic
2560:
2558:
2554:
2553:
2551:
2550:
2545:
2543:Turing machine
2540:
2535:
2530:
2525:
2520:
2515:
2514:
2513:
2508:
2503:
2498:
2493:
2483:
2481:Computable set
2478:
2473:
2468:
2463:
2457:
2455:
2449:
2448:
2446:
2445:
2440:
2435:
2430:
2425:
2420:
2415:
2410:
2409:
2408:
2403:
2398:
2388:
2383:
2378:
2376:Satisfiability
2373:
2368:
2363:
2362:
2361:
2351:
2350:
2349:
2339:
2338:
2337:
2332:
2327:
2322:
2317:
2307:
2306:
2305:
2300:
2293:Interpretation
2289:
2287:
2281:
2280:
2278:
2277:
2272:
2267:
2262:
2257:
2247:
2242:
2241:
2240:
2239:
2238:
2228:
2223:
2213:
2208:
2203:
2198:
2193:
2188:
2182:
2180:
2174:
2173:
2170:
2169:
2167:
2166:
2158:
2157:
2156:
2155:
2150:
2149:
2148:
2143:
2138:
2118:
2117:
2116:
2114:minimal axioms
2111:
2100:
2099:
2098:
2087:
2086:
2085:
2080:
2075:
2070:
2065:
2060:
2047:
2045:
2026:
2025:
2023:
2022:
2021:
2020:
2008:
2003:
2002:
2001:
1996:
1991:
1986:
1976:
1971:
1966:
1961:
1960:
1959:
1954:
1944:
1943:
1942:
1937:
1932:
1927:
1917:
1912:
1911:
1910:
1905:
1900:
1890:
1889:
1888:
1883:
1878:
1873:
1868:
1863:
1853:
1848:
1843:
1838:
1837:
1836:
1831:
1826:
1821:
1811:
1806:
1804:Formation rule
1801:
1796:
1795:
1794:
1789:
1779:
1778:
1777:
1767:
1762:
1757:
1752:
1746:
1740:
1723:Formal systems
1719:
1718:
1715:
1714:
1712:
1711:
1706:
1701:
1696:
1691:
1686:
1681:
1676:
1671:
1666:
1665:
1664:
1659:
1648:
1646:
1642:
1641:
1639:
1638:
1637:
1636:
1626:
1621:
1620:
1619:
1612:Large cardinal
1609:
1604:
1599:
1594:
1589:
1575:
1574:
1573:
1568:
1563:
1548:
1546:
1536:
1535:
1533:
1532:
1531:
1530:
1525:
1520:
1510:
1505:
1500:
1495:
1490:
1485:
1480:
1475:
1470:
1465:
1460:
1455:
1449:
1447:
1440:
1439:
1437:
1436:
1435:
1434:
1429:
1424:
1419:
1414:
1409:
1401:
1400:
1399:
1394:
1384:
1379:
1377:Extensionality
1374:
1372:Ordinal number
1369:
1359:
1354:
1353:
1352:
1341:
1335:
1329:
1328:
1325:
1324:
1322:
1321:
1316:
1311:
1306:
1301:
1296:
1291:
1290:
1289:
1279:
1278:
1277:
1264:
1262:
1256:
1255:
1253:
1252:
1251:
1250:
1245:
1240:
1230:
1225:
1220:
1215:
1210:
1205:
1199:
1197:
1191:
1190:
1188:
1187:
1182:
1177:
1172:
1167:
1162:
1157:
1156:
1155:
1145:
1140:
1135:
1130:
1125:
1120:
1114:
1112:
1103:
1097:
1096:
1094:
1093:
1088:
1083:
1078:
1073:
1068:
1056:Cantor's
1054:
1049:
1044:
1034:
1032:
1019:
1018:
1016:
1015:
1010:
1005:
1000:
995:
990:
985:
980:
975:
970:
965:
960:
955:
954:
953:
942:
940:
936:
935:
930:
928:
927:
920:
913:
905:
896:
895:
893:
892:
885:
880:
875:
870:
865:
860:
855:
850:
845:
840:
835:
830:
825:
820:
815:
810:
805:
800:
795:
790:
785:
780:
775:
769:
766:
765:
760:
758:
757:
750:
743:
735:
726:
725:
720:
713:
712:External links
710:
708:
707:
694:
684:(2): 225â238.
670:
641:10.1.1.79.5808
634:(2): 349â363.
620:
614:
595:
579:
554:
548:
532:
519:
503:Hilbert, David
499:
497:on 2006-07-05.
459:
435:
429:
405:
373:
367:
345:
343:
340:
337:
336:
324:
312:
308:Simpson (1988)
300:
290:
273:
261:
257:Hilbert (1901)
244:
243:
241:
238:
237:
236:
229:
226:
206:Kreisel (1976)
202:Simpson (1988)
197:
194:
153:
148:ordinal number
137:Main article:
134:
131:
130:
129:
105:Main article:
102:
99:
59:
56:
46:In the 1930s,
41:Hilbert (1900)
15:
13:
10:
9:
6:
4:
3:
2:
2681:
2670:
2667:
2666:
2664:
2651:
2650:
2645:
2637:
2631:
2628:
2626:
2623:
2621:
2618:
2616:
2613:
2609:
2606:
2605:
2604:
2601:
2599:
2596:
2594:
2591:
2589:
2585:
2582:
2580:
2577:
2575:
2572:
2570:
2567:
2565:
2562:
2561:
2559:
2555:
2549:
2546:
2544:
2541:
2539:
2538:Recursive set
2536:
2534:
2531:
2529:
2526:
2524:
2521:
2519:
2516:
2512:
2509:
2507:
2504:
2502:
2499:
2497:
2494:
2492:
2489:
2488:
2487:
2484:
2482:
2479:
2477:
2474:
2472:
2469:
2467:
2464:
2462:
2459:
2458:
2456:
2454:
2450:
2444:
2441:
2439:
2436:
2434:
2431:
2429:
2426:
2424:
2421:
2419:
2416:
2414:
2411:
2407:
2404:
2402:
2399:
2397:
2394:
2393:
2392:
2389:
2387:
2384:
2382:
2379:
2377:
2374:
2372:
2369:
2367:
2364:
2360:
2357:
2356:
2355:
2352:
2348:
2347:of arithmetic
2345:
2344:
2343:
2340:
2336:
2333:
2331:
2328:
2326:
2323:
2321:
2318:
2316:
2313:
2312:
2311:
2308:
2304:
2301:
2299:
2296:
2295:
2294:
2291:
2290:
2288:
2286:
2282:
2276:
2273:
2271:
2268:
2266:
2263:
2261:
2258:
2255:
2254:from ZFC
2251:
2248:
2246:
2243:
2237:
2234:
2233:
2232:
2229:
2227:
2224:
2222:
2219:
2218:
2217:
2214:
2212:
2209:
2207:
2204:
2202:
2199:
2197:
2194:
2192:
2189:
2187:
2184:
2183:
2181:
2179:
2175:
2165:
2164:
2160:
2159:
2154:
2153:non-Euclidean
2151:
2147:
2144:
2142:
2139:
2137:
2136:
2132:
2131:
2129:
2126:
2125:
2123:
2119:
2115:
2112:
2110:
2107:
2106:
2105:
2101:
2097:
2094:
2093:
2092:
2088:
2084:
2081:
2079:
2076:
2074:
2071:
2069:
2066:
2064:
2061:
2059:
2056:
2055:
2053:
2049:
2048:
2046:
2041:
2035:
2030:Example
2027:
2019:
2014:
2013:
2012:
2009:
2007:
2004:
2000:
1997:
1995:
1992:
1990:
1987:
1985:
1982:
1981:
1980:
1977:
1975:
1972:
1970:
1967:
1965:
1962:
1958:
1955:
1953:
1950:
1949:
1948:
1945:
1941:
1938:
1936:
1933:
1931:
1928:
1926:
1923:
1922:
1921:
1918:
1916:
1913:
1909:
1906:
1904:
1901:
1899:
1896:
1895:
1894:
1891:
1887:
1884:
1882:
1879:
1877:
1874:
1872:
1869:
1867:
1864:
1862:
1859:
1858:
1857:
1854:
1852:
1849:
1847:
1844:
1842:
1839:
1835:
1832:
1830:
1827:
1825:
1822:
1820:
1817:
1816:
1815:
1812:
1810:
1807:
1805:
1802:
1800:
1797:
1793:
1790:
1788:
1787:by definition
1785:
1784:
1783:
1780:
1776:
1773:
1772:
1771:
1768:
1766:
1763:
1761:
1758:
1756:
1753:
1751:
1748:
1747:
1744:
1741:
1739:
1735:
1730:
1724:
1720:
1710:
1707:
1705:
1702:
1700:
1697:
1695:
1692:
1690:
1687:
1685:
1682:
1680:
1677:
1675:
1674:KripkeâPlatek
1672:
1670:
1667:
1663:
1660:
1658:
1655:
1654:
1653:
1650:
1649:
1647:
1643:
1635:
1632:
1631:
1630:
1627:
1625:
1622:
1618:
1615:
1614:
1613:
1610:
1608:
1605:
1603:
1600:
1598:
1595:
1593:
1590:
1587:
1583:
1579:
1576:
1572:
1569:
1567:
1564:
1562:
1559:
1558:
1557:
1553:
1550:
1549:
1547:
1545:
1541:
1537:
1529:
1526:
1524:
1521:
1519:
1518:constructible
1516:
1515:
1514:
1511:
1509:
1506:
1504:
1501:
1499:
1496:
1494:
1491:
1489:
1486:
1484:
1481:
1479:
1476:
1474:
1471:
1469:
1466:
1464:
1461:
1459:
1456:
1454:
1451:
1450:
1448:
1446:
1441:
1433:
1430:
1428:
1425:
1423:
1420:
1418:
1415:
1413:
1410:
1408:
1405:
1404:
1402:
1398:
1395:
1393:
1390:
1389:
1388:
1385:
1383:
1380:
1378:
1375:
1373:
1370:
1368:
1364:
1360:
1358:
1355:
1351:
1348:
1347:
1346:
1343:
1342:
1339:
1336:
1334:
1330:
1320:
1317:
1315:
1312:
1310:
1307:
1305:
1302:
1300:
1297:
1295:
1292:
1288:
1285:
1284:
1283:
1280:
1276:
1271:
1270:
1269:
1266:
1265:
1263:
1261:
1257:
1249:
1246:
1244:
1241:
1239:
1236:
1235:
1234:
1231:
1229:
1226:
1224:
1221:
1219:
1216:
1214:
1211:
1209:
1206:
1204:
1201:
1200:
1198:
1196:
1195:Propositional
1192:
1186:
1183:
1181:
1178:
1176:
1173:
1171:
1168:
1166:
1163:
1161:
1158:
1154:
1151:
1150:
1149:
1146:
1144:
1141:
1139:
1136:
1134:
1131:
1129:
1126:
1124:
1123:Logical truth
1121:
1119:
1116:
1115:
1113:
1111:
1107:
1104:
1102:
1098:
1092:
1089:
1087:
1084:
1082:
1079:
1077:
1074:
1072:
1069:
1067:
1063:
1059:
1055:
1053:
1050:
1048:
1045:
1043:
1039:
1036:
1035:
1033:
1031:
1025:
1020:
1014:
1011:
1009:
1006:
1004:
1001:
999:
996:
994:
991:
989:
986:
984:
981:
979:
976:
974:
971:
969:
966:
964:
961:
959:
956:
952:
949:
948:
947:
944:
943:
941:
937:
933:
926:
921:
919:
914:
912:
907:
906:
903:
890:
886:
884:
881:
879:
876:
874:
871:
869:
866:
864:
861:
859:
856:
854:
851:
849:
846:
844:
841:
839:
836:
834:
831:
829:
826:
824:
821:
819:
816:
814:
811:
809:
806:
804:
801:
799:
796:
794:
791:
789:
786:
784:
781:
779:
776:
774:
771:
770:
767:
763:
756:
751:
749:
744:
742:
737:
736:
733:
729:
724:
721:
719:
716:
715:
711:
703:
699:
695:
691:
687:
683:
679:
675:
671:
667:
663:
659:
655:
651:
647:
642:
637:
633:
629:
625:
621:
617:
615:9780814758014
611:
607:
606:
605:Godel's Proof
601:
596:
592:
591:Godel's Proof
588:
584:
583:Nagel, Ernest
580:
576:
572:
568:
567:
559:
555:
551:
549:0-8218-1428-1
545:
541:
537:
533:
529:
525:
520:
516:
512:
508:
504:
500:
496:
492:
488:
484:
480:
476:
472:
468:
464:
460:
456:
452:
448:
444:
440:
436:
432:
430:1-56881-238-8
426:
422:
418:
414:
410:
406:
402:
398:
394:
390:
386:
382:
378:
374:
370:
368:0-7695-2631-4
364:
360:
356:
352:
347:
346:
341:
333:
332:Dawson (2006)
328:
325:
322:, p. 65.
321:
316:
313:
309:
304:
301:
294:
291:
287:
283:
277:
274:
270:
265:
262:
258:
254:
249:
246:
239:
235:
232:
231:
227:
225:
223:
219:
218:Dawson (2006)
215:
211:
207:
203:
195:
193:
191:
187:
183:
178:
176:
172:
168:
164:
160:
156:
149:
144:
140:
127:
123:
122:
121:
119:
114:
108:
98:
96:
92:
88:
83:
81:
76:
74:
67:
63:
55:
53:
49:
44:
42:
38:
34:
30:
29:David Hilbert
27:was posed by
26:
22:
2640:
2438:Ultraproduct
2285:Model theory
2250:Independence
2186:Formal proof
2178:Proof theory
2161:
2134:
2091:real numbers
2063:second-order
1974:Substitution
1851:Metalanguage
1792:conservative
1765:Axiom schema
1709:Constructive
1679:MorseâKelley
1645:Set theories
1624:Aleph number
1617:inaccessible
1523:Grothendieck
1407:intersection
1294:Higher-order
1282:Second-order
1228:Truth tables
1185:Venn diagram
968:Formal proof
777:
727:
701:
681:
677:
631:
627:
604:
590:
570:
564:
539:
527:
523:
514:
510:
495:the original
474:
470:
446:
442:
417:Wellesley MA
412:
384:
380:
350:
327:
315:
303:
293:
276:
264:
248:
210:second-order
199:
179:
145:
142:
110:
84:
77:
69:
65:
61:
45:
24:
18:
2548:Type theory
2496:undecidable
2428:Truth value
2315:equivalence
1994:non-logical
1607:Enumeration
1597:Isomorphism
1544:cardinality
1528:Von Neumann
1493:Ultrafilter
1458:Uncountable
1392:equivalence
1309:Quantifiers
1299:Fixed-point
1268:First-order
1148:Consistency
1133:Proposition
1110:Traditional
1081:Lindström's
1071:Compactness
1013:Type theory
958:Cardinality
463:Gödel, Kurt
421:A.K. Peters
175:Tait (2005)
165:result for
33:23 problems
21:mathematics
2359:elementary
2052:arithmetic
1920:Quantifier
1898:functional
1770:Expression
1488:Transitive
1432:identities
1417:complement
1350:hereditary
1333:Set theory
517:: 180â184.
477:: 173â98.
342:References
91:finitistic
48:Kurt Gödel
37:consistent
2630:Supertask
2533:Recursion
2491:decidable
2325:saturated
2303:of models
2226:deductive
2221:axiomatic
2141:Hilbert's
2128:Euclidean
2109:canonical
2032:axiomatic
1964:Signature
1893:Predicate
1782:Extension
1704:Ackermann
1629:Operation
1508:Universal
1498:Recursive
1473:Singleton
1468:Inhabited
1453:Countable
1443:Types of
1427:power set
1397:partition
1314:Predicate
1260:Predicate
1175:Syllogism
1165:Soundness
1138:Inference
1128:Tautology
1030:paradoxes
658:0022-4812
636:CiteSeerX
491:197663120
334:, sec. 2.
310:, sec. 3.
2663:Category
2615:Logicism
2608:timeline
2584:Concrete
2443:Validity
2413:T-schema
2406:Kripke's
2401:Tarski's
2396:semantic
2386:Strength
2335:submodel
2330:spectrum
2298:function
2146:Tarski's
2135:Elements
2122:geometry
2078:Robinson
1999:variable
1984:function
1957:spectrum
1947:Sentence
1903:variable
1846:Language
1799:Relation
1760:Automata
1750:Alphabet
1734:language
1588:-jection
1566:codomain
1552:Function
1513:Universe
1483:Infinite
1387:Relation
1170:Validity
1160:Argument
1058:theorem,
700:(1967).
589:(1958).
505:(1900).
465:(1931).
411:(2005).
401:44736805
298:numbers.
228:See also
111:Gödel's
2557:Related
2354:Diagram
2252: (
2231:Hilbert
2216:Systems
2211:Theorem
2089:of the
2034:systems
1814:Formula
1809:Grammar
1725: (
1669:General
1382:Forcing
1367:Element
1287:Monadic
1062:paradox
1003:Theorem
939:General
690:1556751
666:2274508
602:(ed.).
2320:finite
2083:Skolem
2036:
2011:Theory
1979:Symbol
1969:String
1952:atomic
1829:ground
1824:closed
1819:atomic
1775:ground
1738:syntax
1634:binary
1561:domain
1478:Finite
1243:finite
1101:Logics
1060:
1008:Theory
688:
664:
656:
638:
612:
546:
489:
427:
399:
365:
2310:Model
2058:Peano
1915:Proof
1755:Arity
1684:Naive
1571:image
1503:Fuzzy
1463:Empty
1412:union
1357:Class
998:Model
988:Lemma
946:Axiom
686:JSTOR
662:JSTOR
561:(PDF)
487:S2CID
397:S2CID
240:Notes
2433:Type
2236:list
2040:list
2017:list
2006:Term
1940:rank
1834:open
1728:list
1540:Maps
1445:sets
1304:Free
1274:list
1024:list
951:list
654:ISSN
610:ISBN
544:ISBN
425:ISBN
363:ISBN
50:and
2120:of
2102:of
2050:of
1582:Sur
1556:Map
1363:Ur-
1345:Set
646:doi
479:doi
451:doi
447:112
389:doi
355:doi
19:In
2665::
2506:NP
2130::
2124::
2054::
1731:),
1586:Bi
1578:In
889:24
883:23
878:22
873:21
868:20
863:19
858:18
853:17
848:16
843:15
838:14
833:13
828:12
823:11
818:10
682:11
680:.
660:.
652:.
644:.
632:53
630:.
585:;
573:.
569:.
563:.
526:.
513:.
509:.
485:.
475:38
473:.
469:.
445:.
423:.
419::
415:.
395:.
385:19
383:.
361:.
224:.
23:,
2586:/
2501:P
2256:)
2042:)
2038:(
1935:â
1930:!
1925:â
1886:=
1881:â
1876:â
1871:â§
1866:âš
1861:ÂŹ
1584:/
1580:/
1554:/
1365:)
1361:(
1248:â
1238:3
1026:)
924:e
917:t
910:v
891:)
887:(
813:9
808:8
803:7
798:6
793:5
788:4
783:3
778:2
773:1
754:e
747:t
740:v
706:.
692:.
668:.
648::
618:.
571:8
552:.
528:3
515:8
481::
457:.
453::
433:.
403:.
391::
371:.
357::
288:.
259:.
154:0
152:Δ
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.