43:
3606:
173:). The significance of this was that properties of a statement – such as its truth or falsehood – would be equivalent to determining whether its Gödel number had certain properties. The numbers involved might be very large indeed, but this is not a barrier; all that matters is that such numbers can be constructed.
694:
Gödel specifically used this scheme at two levels: first, to encode sequences of symbols representing formulas, and second, to encode sequences of formulas representing proofs. This allowed him to show a correspondence between statements about natural numbers and statements about the provability of
176:
In simple terms, he devised a method by which every formula or statement that can be formulated in the system gets a unique number, in such a way that formulas and Gödel numbers can be mechanically converted back and forth. There are many ways this can be done. A simple example is the way in which
1281:
in which one can make statements about numbers and their arithmetical relationships to each other, one can use a Gödel numbering to indirectly make statements about the theory itself. This technique allowed Gödel to prove results about the consistency and completeness properties of
1655:
678:
1000:
1337:
to encode formulas this is essentially equivalent to the use of Gödel numbers, but somewhat easier to define because the tree structure of formulas can be modeled by the tree structure of sets. Gödel sets can also be used to encode formulas in
714:
In the specific Gödel numbering used by Nagel and Newman, the Gödel number for the symbol "0" is 6 and the Gödel number for the symbol "=" is 5. Thus, in their system, the Gödel number of the formula "0 = 0" is 2 × 3 × 5 = 243,000,000.
1460:
1333:
Gödel sets are sometimes used in set theory to encode formulas, and are similar to Gödel numbers, except that one uses sets rather than numbers to do the encoding. In simple cases when one uses a
1390:
For another, perhaps-more-intuitive example, suppose you have three symbols to encode, and choose bijective base-10 for familiarity (so enumeration starts at 1, 10 is represented by a symbol e.g.
158:
can then represent a sequence of symbols. These sequences of natural numbers can again be represented by single natural numbers, facilitating their manipulation in formal theories of arithmetic.
506:
1099:
1060:
812:
494:
804:
161:
Since the publishing of Gödel's paper in 1931, the term "Gödel numbering" or "Gödel code" has been used to refer to more general assignments of natural numbers to mathematical objects.
1269:
1185:
1985:
1454:
2660:
1727:
1321:
Also, the term Gödel numbering is sometimes used when the assigned "numbers" are actually strings, which is necessary when considering models of computation such as
1678:
1047:
1027:
2743:
1884:
1274:
This is true for the numbering Gödel used, and for any other numbering where the encoded formula can be arithmetically recovered from its Gödel number.
1752:
3057:
3215:
2003:
1366:
132:
3070:
2393:
64:
1855:
2655:
3075:
3065:
2802:
2008:
2553:
1999:
3211:
1650:{\displaystyle (1\times 10^{(3-1)}+2\times 10^{(3-2)}+3\times 10^{(3-3)})=(1\times 10^{2}+2\times 10^{1}+3\times 10^{0})=(100+20+3)}
684:
86:
3308:
3052:
1877:
1361:
703:
409:. He first assigned a unique natural number to each basic symbol in the formal language of arithmetic with which he was dealing.
31:
2613:
2306:
2047:
3640:
727:
basic symbols, an alternative Gödel numbering could be constructed by invertibly mapping this set of symbols (through, say, an
691:, so it is possible to recover the original sequence from its Gödel number (for any given number n of symbols to be encoded).
181:. Since ASCII codes are in the range 0 to 127, it is sufficient to pad them to 3 decimal digits and then to concatenate them:
3635:
3569:
3271:
3034:
3029:
2854:
2275:
1959:
1805:(1959). This book provides a good introduction and summary of the proof, with a large section dedicated to Gödel's numbering.
673:{\displaystyle \mathrm {enc} (x_{1},x_{2},x_{3},\dots ,x_{n})=2^{x_{1}}\cdot 3^{x_{2}}\cdot 5^{x_{3}}\cdots p_{n}^{x_{n}}.}
3564:
3347:
3264:
2977:
2908:
2785:
2027:
2635:
3489:
3315:
3001:
2234:
1087:
2640:
3630:
2972:
2711:
1969:
1870:
1744:
995:{\displaystyle h(s_{1})\times K^{(n-1)}+h(s_{2})\times K^{(n-2)}+\cdots +h(s_{n-1})\times K^{1}+h(s_{n})\times K^{0}.}
3367:
3362:
57:
51:
3296:
2886:
2280:
2248:
1939:
1083:
1077:
415:
2013:
3586:
3535:
3432:
2930:
2891:
2368:
3427:
2042:
749:
68:
3357:
2896:
2748:
2731:
2454:
1934:
412:
To encode an entire formula, which is a sequence of symbols, Gödel used the following system. Given a sequence
1298:, the term "Gödel numbering" is used in settings more general than the one described above. It can refer to:
3259:
3236:
3197:
3083:
3024:
2670:
2590:
2434:
2378:
1991:
1334:
1196:
3549:
3276:
3254:
3221:
3114:
2960:
2945:
2918:
2869:
2753:
2688:
2513:
2479:
2474:
2348:
2179:
2156:
1831:
108:
3479:
3332:
3124:
2842:
2578:
2484:
2343:
2328:
2209:
2184:
1371:
1117:
151:
3605:
1148:
3452:
3414:
3291:
3095:
2935:
2859:
2837:
2665:
2623:
2522:
2489:
2353:
2141:
2052:
1295:
735:
1313:
More generally, an assignment of elements from a countable mathematical object, such as a countable
3581:
3472:
3457:
3437:
3394:
3281:
3231:
3157:
3102:
3039:
2832:
2827:
2775:
2543:
2532:
2204:
2104:
2032:
2023:
2019:
1954:
1949:
1843:
1314:
728:
406:
112:
3610:
3379:
3342:
3327:
3320:
3303:
3089:
2955:
2881:
2864:
2817:
2630:
2539:
2373:
2358:
2318:
2270:
2255:
2243:
2199:
2174:
1944:
1893:
1848:
1836:
1769:
1356:
143:
100:
3107:
1417:
687:, any number (and, in particular, a number obtained in this way) can be uniquely factored into
3545:
3352:
3162:
3152:
3044:
2925:
2760:
2736:
2517:
2501:
2406:
2383:
2260:
2229:
2194:
2089:
1924:
1105:
1694:
3559:
3554:
3447:
3404:
3226:
3187:
3182:
3167:
2993:
2950:
2847:
2645:
2595:
2169:
2131:
1761:
1339:
1278:
169:
Gödel noted that each statement within a system can be represented by a natural number (its
3540:
3530:
3484:
3467:
3422:
3384:
3286:
3206:
3013:
2940:
2913:
2901:
2807:
2721:
2695:
2650:
2618:
2419:
2221:
2164:
2114:
2079:
2037:
1817:
See Gödel 1931, p. 179; Gödel's notation (see p. 176) has been adapted to modern notation.
1802:
1351:
1303:
723:
Infinitely many different Gödel numberings are possible. For example, supposing there are
116:
1663:
3525:
3504:
3462:
3442:
3337:
3192:
2790:
2780:
2770:
2765:
2699:
2573:
2449:
2338:
2333:
2311:
1912:
1322:
1032:
1012:
155:
120:
1745:"Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I"
3624:
3499:
3177:
2684:
2469:
2459:
2429:
2414:
2084:
1773:
1283:
496:
of positive integers, the Gödel encoding of the sequence is the product of the first
128:
1851:. This is a newer book by Hofstadter that includes the history of Gödel's numbering.
3399:
3246:
3147:
3139:
3019:
2967:
2876:
2812:
2795:
2726:
2585:
2444:
2146:
1929:
1798:
688:
1317:, to natural numbers to allow algorithmic manipulation of the mathematical object.
3509:
3389:
2568:
2558:
2505:
2189:
2109:
2094:
1974:
1919:
2439:
2294:
2265:
2071:
3591:
3494:
2547:
2464:
2424:
2388:
2324:
2136:
2126:
2099:
1307:
17:
1777:
1306:
to natural numbers in such a way that the numbers can be manipulated by an
3576:
3374:
2822:
2527:
2121:
1108:
of the theory can be expressed as a function on the natural numbers. If
1055:
each formula may serve just as the very numeral of its own Gödel number.
3172:
1964:
1859:
by Jason Hemann and Eric Holk. Uses Gödel numbering to encode programs.
1765:
1862:
147:
702:
There are more sophisticated (and more concise) ways to construct a
695:
theorems about natural numbers, the key observation of the proof. (
2716:
2062:
1907:
178:
1104:
Once a Gödel numbering for a formal theory is established, each
1866:
177:
English is stored as a sequence of numbers in computers using
36:
1082:
One may use Gödel numbering to show how functions defined by
500:
primes raised to their corresponding values in the sequence:
1839:. This book defines and uses an alternative Gödel numbering.
1310:
to simulate manipulation of elements of the formal language.
30:
For numberings of the set of computable functions, see
1394:
and place-value carries at 11 rather than 10: decimal
1697:
1666:
1463:
1420:
1199:
1151:
1100:
Proof sketch for Gödel's first incompleteness theorem
1035:
1015:
815:
752:
509:
418:
3518:
3413:
3245:
3138:
2990:
2683:
2606:
2500:
2404:
2293:
2220:
2155:
2070:
2061:
1983:
1900:
209:
1721:
1672:
1649:
1448:
1263:
1179:
1041:
1021:
994:
798:
672:
488:
1009:basic symbols in some fixed order, such that the
1116:is an inference rule, then there should be some
1325:that manipulate strings rather than numbers.
1878:
489:{\displaystyle (x_{1},x_{2},x_{3},...,x_{n})}
8:
1832:Gödel, Escher, Bach: an Eternal Golden Braid
1094:Expressing statements and proofs by numbers
142:A Gödel numbering can be interpreted as an
2704:
2299:
2067:
1885:
1871:
1863:
799:{\displaystyle s_{1}s_{2}s_{3}\dots s_{n}}
1696:
1665:
1614:
1595:
1576:
1539:
1508:
1477:
1462:
1431:
1419:
1204:
1198:
1165:
1150:
1034:
1014:
983:
967:
948:
926:
889:
873:
842:
826:
814:
790:
777:
767:
757:
751:
659:
654:
649:
634:
629:
614:
609:
594:
589:
573:
554:
541:
528:
510:
508:
477:
452:
439:
426:
417:
87:Learn how and when to remove this message
1126:of natural numbers such that if formula
252:
50:This article includes a list of general
1810:
1383:
1029:-th symbol corresponds uniquely to the
1264:{\displaystyle g_{r}(f(A),f(B))=f(C).}
1005:In other words, by placing the set of
742:. A formula consisting of a string of
146:in which a number is assigned to each
1753:Monatshefte für Mathematik und Physik
1059:For example, the numbering described
696:
136:
7:
1302:Any assignment of the elements of a
806:would then be mapped to the number
517:
514:
511:
56:it lacks sufficient corresponding
25:
1681:as our numbering—a neat feature.
1277:Thus, in a formal theory such as
685:fundamental theorem of arithmetic
3604:
1691:(or, in bijective base-10 form:
1372:Chaitin's incompleteness theorem
1180:{\displaystyle A,B\vdash _{r}C,}
1067:Application to formal arithmetic
111:that assigns to each symbol and
41:
32:Numbering (computability theory)
1367:Gödel's incompleteness theorems
127:. The concept was developed by
1644:
1626:
1620:
1563:
1557:
1552:
1540:
1521:
1509:
1490:
1478:
1464:
1437:
1424:
1255:
1249:
1240:
1237:
1231:
1222:
1216:
1210:
1049:-th digit of a bijective base-
973:
960:
938:
919:
902:
890:
879:
866:
855:
843:
832:
819:
579:
521:
483:
419:
27:Function in mathematical logic
1:
3565:History of mathematical logic
1856:Visualizing the Turing Tarpit
1362:Gödel numbering for sequences
1088:primitive recursive functions
704:Gödel numbering for sequences
405:Gödel used a system based on
3490:Primitive recursive function
734:) to the set of digits of a
154:, after which a sequence of
3657:
2554:Schröder–Bernstein theorem
2281:Monadic predicate calculus
1940:Foundations of mathematics
1449:{\displaystyle h(s_{n})=n}
1138:through an inference rule
1097:
1084:course-of-values recursion
1078:Course-of-values recursion
1075:
401:Gödel's original encoding
29:
3600:
3587:Philosophy of mathematics
3536:Automated theorem proving
2707:
2661:Von Neumann–Bernays–Gödel
2302:
1130:is derived from formulas
1112:is the Gödel mapping and
260:
257:
255:
248:
3237:Self-verifying theories
3058:Tarski's axiomatization
2009:Tarski's undefinability
2004:incompleteness theorems
1722:{\displaystyle 9A+1A+3}
1456:and the formula above:
1335:hereditarily finite set
133:incompleteness theorems
71:more precise citations.
3611:Mathematics portal
3222:Proof of impossibility
2870:propositional variable
2180:Propositional calculus
1723:
1674:
1651:
1450:
1265:
1181:
1043:
1023:
996:
800:
674:
490:
3636:Theory of computation
3480:Kolmogorov complexity
3433:Computably enumerable
3333:Model complete theory
3125:Principia Mathematica
2185:Propositional formula
2014:Banach–Tarski paradox
1724:
1675:
1652:
1451:
1266:
1182:
1118:arithmetical function
1044:
1024:
997:
801:
675:
491:
152:mathematical notation
131:for the proof of his
3428:Church–Turing thesis
3415:Computability theory
2624:continuum hypothesis
2142:Square of opposition
2000:Gödel's completeness
1743:Gödel, Kurt (1931),
1695:
1664:
1461:
1418:
1340:infinitary languages
1296:computability theory
1197:
1149:
1033:
1013:
813:
750:
507:
416:
207:The logical formula
3641:Works by Kurt Gödel
3582:Mathematical object
3473:P versus NP problem
3438:Computable function
3232:Reverse mathematics
3158:Logical consequence
3035:primitive recursive
3030:elementary function
2803:Free/bound variable
2656:Tarski–Grothendieck
2175:Logical connectives
2105:Logical equivalence
1955:Logical consequence
1844:I Am a Strange Loop
1673:{\displaystyle 123}
729:invertible function
666:
407:prime factorization
402:
261:property variables
165:Simplified overview
113:well-formed formula
3631:Mathematical logic
3380:Transfer principle
3343:Semantics of logic
3328:Categorical theory
3304:Non-standard model
2818:Logical connective
1945:Information theory
1894:Mathematical logic
1849:Douglas Hofstadter
1837:Douglas Hofstadter
1766:10.1007/BF01700692
1719:
1670:
1647:
1446:
1357:Description number
1261:
1177:
1039:
1019:
992:
796:
719:Lack of uniqueness
670:
645:
486:
400:
213:is represented by
191:is represented by
101:mathematical logic
3618:
3617:
3550:Abstract category
3353:Theories of truth
3163:Rule of inference
3153:Natural deduction
3134:
3133:
2679:
2678:
2384:Cartesian product
2289:
2288:
2195:Many-valued logic
2170:Boolean functions
2053:Russell's paradox
2028:diagonal argument
1925:First-order logic
1042:{\displaystyle i}
1022:{\displaystyle i}
683:According to the
403:
399:
258:number variables
97:
96:
89:
16:(Redirected from
3648:
3609:
3608:
3560:History of logic
3555:Category of sets
3448:Decision problem
3227:Ordinal analysis
3168:Sequent calculus
3066:Boolean algebras
3006:
3005:
2980:
2951:logical/constant
2705:
2691:
2614:Zermelo–Fraenkel
2365:Set operations:
2300:
2237:
2068:
2048:Löwenheim–Skolem
1935:Formal semantics
1887:
1880:
1873:
1864:
1818:
1815:
1790:
1789:
1788:
1782:
1776:, archived from
1749:
1730:
1728:
1726:
1725:
1720:
1689:
1683:
1679:
1677:
1676:
1671:
1659:...we arrive at
1656:
1654:
1653:
1648:
1619:
1618:
1600:
1599:
1581:
1580:
1556:
1555:
1525:
1524:
1494:
1493:
1455:
1453:
1452:
1447:
1436:
1435:
1388:
1279:Peano arithmetic
1270:
1268:
1267:
1262:
1209:
1208:
1186:
1184:
1183:
1178:
1170:
1169:
1053:numeral system,
1048:
1046:
1045:
1040:
1028:
1026:
1025:
1020:
1001:
999:
998:
993:
988:
987:
972:
971:
953:
952:
937:
936:
906:
905:
878:
877:
859:
858:
831:
830:
805:
803:
802:
797:
795:
794:
782:
781:
772:
771:
762:
761:
679:
677:
676:
671:
665:
664:
663:
653:
641:
640:
639:
638:
621:
620:
619:
618:
601:
600:
599:
598:
578:
577:
559:
558:
546:
545:
533:
532:
520:
495:
493:
492:
487:
482:
481:
457:
456:
444:
443:
431:
430:
253:
249:Gödel's encoding
243:
242:
239:
236:
233:
230:
227:
224:
221:
218:
211:
203:
202:
199:
196:
189:
92:
85:
81:
78:
72:
67:this article by
58:inline citations
45:
44:
37:
21:
3656:
3655:
3651:
3650:
3649:
3647:
3646:
3645:
3621:
3620:
3619:
3614:
3603:
3596:
3541:Category theory
3531:Algebraic logic
3514:
3485:Lambda calculus
3423:Church encoding
3409:
3385:Truth predicate
3241:
3207:Complete theory
3130:
2999:
2995:
2991:
2986:
2978:
2698: and
2694:
2689:
2675:
2651:New Foundations
2619:axiom of choice
2602:
2564:Gödel numbering
2504: and
2496:
2400:
2285:
2235:
2216:
2165:Boolean algebra
2151:
2115:Equiconsistency
2080:Classical logic
2057:
2038:Halting problem
2026: and
2002: and
1990: and
1989:
1984:Theorems (
1979:
1896:
1891:
1827:
1825:Further reading
1822:
1821:
1816:
1812:
1803:James R. Newman
1786:
1784:
1780:
1747:
1742:
1739:
1734:
1733:
1693:
1692:
1690:
1686:
1662:
1661:
1610:
1591:
1572:
1535:
1504:
1473:
1459:
1458:
1427:
1416:
1415:
1389:
1385:
1380:
1352:Church encoding
1348:
1331:
1323:Turing machines
1304:formal language
1292:
1290:Generalizations
1200:
1195:
1194:
1161:
1147:
1146:
1124:
1102:
1096:
1080:
1074:
1069:
1031:
1030:
1011:
1010:
979:
963:
944:
922:
885:
869:
838:
822:
811:
810:
786:
773:
763:
753:
748:
747:
736:bijective base-
721:
712:
655:
630:
625:
610:
605:
590:
585:
569:
550:
537:
524:
505:
504:
473:
448:
435:
422:
414:
413:
343:
335:
327:
316:
308:
300:
251:
240:
237:
234:
231:
228:
225:
222:
219:
216:
214:
200:
197:
194:
192:
187:
167:
156:natural numbers
117:formal language
105:Gödel numbering
93:
82:
76:
73:
63:Please help to
62:
46:
42:
35:
28:
23:
22:
15:
12:
11:
5:
3654:
3652:
3644:
3643:
3638:
3633:
3623:
3622:
3616:
3615:
3601:
3598:
3597:
3595:
3594:
3589:
3584:
3579:
3574:
3573:
3572:
3562:
3557:
3552:
3543:
3538:
3533:
3528:
3526:Abstract logic
3522:
3520:
3516:
3515:
3513:
3512:
3507:
3505:Turing machine
3502:
3497:
3492:
3487:
3482:
3477:
3476:
3475:
3470:
3465:
3460:
3455:
3445:
3443:Computable set
3440:
3435:
3430:
3425:
3419:
3417:
3411:
3410:
3408:
3407:
3402:
3397:
3392:
3387:
3382:
3377:
3372:
3371:
3370:
3365:
3360:
3350:
3345:
3340:
3338:Satisfiability
3335:
3330:
3325:
3324:
3323:
3313:
3312:
3311:
3301:
3300:
3299:
3294:
3289:
3284:
3279:
3269:
3268:
3267:
3262:
3255:Interpretation
3251:
3249:
3243:
3242:
3240:
3239:
3234:
3229:
3224:
3219:
3209:
3204:
3203:
3202:
3201:
3200:
3190:
3185:
3175:
3170:
3165:
3160:
3155:
3150:
3144:
3142:
3136:
3135:
3132:
3131:
3129:
3128:
3120:
3119:
3118:
3117:
3112:
3111:
3110:
3105:
3100:
3080:
3079:
3078:
3076:minimal axioms
3073:
3062:
3061:
3060:
3049:
3048:
3047:
3042:
3037:
3032:
3027:
3022:
3009:
3007:
2988:
2987:
2985:
2984:
2983:
2982:
2970:
2965:
2964:
2963:
2958:
2953:
2948:
2938:
2933:
2928:
2923:
2922:
2921:
2916:
2906:
2905:
2904:
2899:
2894:
2889:
2879:
2874:
2873:
2872:
2867:
2862:
2852:
2851:
2850:
2845:
2840:
2835:
2830:
2825:
2815:
2810:
2805:
2800:
2799:
2798:
2793:
2788:
2783:
2773:
2768:
2766:Formation rule
2763:
2758:
2757:
2756:
2751:
2741:
2740:
2739:
2729:
2724:
2719:
2714:
2708:
2702:
2685:Formal systems
2681:
2680:
2677:
2676:
2674:
2673:
2668:
2663:
2658:
2653:
2648:
2643:
2638:
2633:
2628:
2627:
2626:
2621:
2610:
2608:
2604:
2603:
2601:
2600:
2599:
2598:
2588:
2583:
2582:
2581:
2574:Large cardinal
2571:
2566:
2561:
2556:
2551:
2537:
2536:
2535:
2530:
2525:
2510:
2508:
2498:
2497:
2495:
2494:
2493:
2492:
2487:
2482:
2472:
2467:
2462:
2457:
2452:
2447:
2442:
2437:
2432:
2427:
2422:
2417:
2411:
2409:
2402:
2401:
2399:
2398:
2397:
2396:
2391:
2386:
2381:
2376:
2371:
2363:
2362:
2361:
2356:
2346:
2341:
2339:Extensionality
2336:
2334:Ordinal number
2331:
2321:
2316:
2315:
2314:
2303:
2297:
2291:
2290:
2287:
2286:
2284:
2283:
2278:
2273:
2268:
2263:
2258:
2253:
2252:
2251:
2241:
2240:
2239:
2226:
2224:
2218:
2217:
2215:
2214:
2213:
2212:
2207:
2202:
2192:
2187:
2182:
2177:
2172:
2167:
2161:
2159:
2153:
2152:
2150:
2149:
2144:
2139:
2134:
2129:
2124:
2119:
2118:
2117:
2107:
2102:
2097:
2092:
2087:
2082:
2076:
2074:
2065:
2059:
2058:
2056:
2055:
2050:
2045:
2040:
2035:
2030:
2018:Cantor's
2016:
2011:
2006:
1996:
1994:
1981:
1980:
1978:
1977:
1972:
1967:
1962:
1957:
1952:
1947:
1942:
1937:
1932:
1927:
1922:
1917:
1916:
1915:
1904:
1902:
1898:
1897:
1892:
1890:
1889:
1882:
1875:
1867:
1861:
1860:
1852:
1840:
1826:
1823:
1820:
1819:
1809:
1808:
1807:
1806:
1792:
1738:
1735:
1732:
1731:
1718:
1715:
1712:
1709:
1706:
1703:
1700:
1684:
1669:
1646:
1643:
1640:
1637:
1634:
1631:
1628:
1625:
1622:
1617:
1613:
1609:
1606:
1603:
1598:
1594:
1590:
1587:
1584:
1579:
1575:
1571:
1568:
1565:
1562:
1559:
1554:
1551:
1548:
1545:
1542:
1538:
1534:
1531:
1528:
1523:
1520:
1517:
1514:
1511:
1507:
1503:
1500:
1497:
1492:
1489:
1486:
1483:
1480:
1476:
1472:
1469:
1466:
1445:
1442:
1439:
1434:
1430:
1426:
1423:
1398:will still be
1382:
1381:
1379:
1376:
1375:
1374:
1369:
1364:
1359:
1354:
1347:
1344:
1330:
1327:
1319:
1318:
1311:
1291:
1288:
1284:formal systems
1272:
1271:
1260:
1257:
1254:
1251:
1248:
1245:
1242:
1239:
1236:
1233:
1230:
1227:
1224:
1221:
1218:
1215:
1212:
1207:
1203:
1188:
1187:
1176:
1173:
1168:
1164:
1160:
1157:
1154:
1122:
1106:inference rule
1098:Main article:
1095:
1092:
1076:Main article:
1073:
1070:
1068:
1065:
1038:
1018:
1003:
1002:
991:
986:
982:
978:
975:
970:
966:
962:
959:
956:
951:
947:
943:
940:
935:
932:
929:
925:
921:
918:
915:
912:
909:
904:
901:
898:
895:
892:
888:
884:
881:
876:
872:
868:
865:
862:
857:
854:
851:
848:
845:
841:
837:
834:
829:
825:
821:
818:
793:
789:
785:
780:
776:
770:
766:
760:
756:
740:numeral system
720:
717:
711:
708:
681:
680:
669:
662:
658:
652:
648:
644:
637:
633:
628:
624:
617:
613:
608:
604:
597:
593:
588:
584:
581:
576:
572:
568:
565:
562:
557:
553:
549:
544:
540:
536:
531:
527:
523:
519:
516:
513:
485:
480:
476:
472:
469:
466:
463:
460:
455:
451:
447:
442:
438:
434:
429:
425:
421:
398:
397:
394:
391:
388:
385:
382:
379:
376:
373:
370:
367:
364:
361:
358:
355:
352:
348:
347:
344:
341:
336:
333:
328:
325:
320:
317:
314:
309:
306:
301:
298:
293:
290:
287:
284:
281:
278:
273:
270:
266:
265:
262:
259:
256:
250:
247:
246:
245:
205:
166:
163:
121:natural number
95:
94:
49:
47:
40:
26:
24:
14:
13:
10:
9:
6:
4:
3:
2:
3653:
3642:
3639:
3637:
3634:
3632:
3629:
3628:
3626:
3613:
3612:
3607:
3599:
3593:
3590:
3588:
3585:
3583:
3580:
3578:
3575:
3571:
3568:
3567:
3566:
3563:
3561:
3558:
3556:
3553:
3551:
3547:
3544:
3542:
3539:
3537:
3534:
3532:
3529:
3527:
3524:
3523:
3521:
3517:
3511:
3508:
3506:
3503:
3501:
3500:Recursive set
3498:
3496:
3493:
3491:
3488:
3486:
3483:
3481:
3478:
3474:
3471:
3469:
3466:
3464:
3461:
3459:
3456:
3454:
3451:
3450:
3449:
3446:
3444:
3441:
3439:
3436:
3434:
3431:
3429:
3426:
3424:
3421:
3420:
3418:
3416:
3412:
3406:
3403:
3401:
3398:
3396:
3393:
3391:
3388:
3386:
3383:
3381:
3378:
3376:
3373:
3369:
3366:
3364:
3361:
3359:
3356:
3355:
3354:
3351:
3349:
3346:
3344:
3341:
3339:
3336:
3334:
3331:
3329:
3326:
3322:
3319:
3318:
3317:
3314:
3310:
3309:of arithmetic
3307:
3306:
3305:
3302:
3298:
3295:
3293:
3290:
3288:
3285:
3283:
3280:
3278:
3275:
3274:
3273:
3270:
3266:
3263:
3261:
3258:
3257:
3256:
3253:
3252:
3250:
3248:
3244:
3238:
3235:
3233:
3230:
3228:
3225:
3223:
3220:
3217:
3216:from ZFC
3213:
3210:
3208:
3205:
3199:
3196:
3195:
3194:
3191:
3189:
3186:
3184:
3181:
3180:
3179:
3176:
3174:
3171:
3169:
3166:
3164:
3161:
3159:
3156:
3154:
3151:
3149:
3146:
3145:
3143:
3141:
3137:
3127:
3126:
3122:
3121:
3116:
3115:non-Euclidean
3113:
3109:
3106:
3104:
3101:
3099:
3098:
3094:
3093:
3091:
3088:
3087:
3085:
3081:
3077:
3074:
3072:
3069:
3068:
3067:
3063:
3059:
3056:
3055:
3054:
3050:
3046:
3043:
3041:
3038:
3036:
3033:
3031:
3028:
3026:
3023:
3021:
3018:
3017:
3015:
3011:
3010:
3008:
3003:
2997:
2992:Example
2989:
2981:
2976:
2975:
2974:
2971:
2969:
2966:
2962:
2959:
2957:
2954:
2952:
2949:
2947:
2944:
2943:
2942:
2939:
2937:
2934:
2932:
2929:
2927:
2924:
2920:
2917:
2915:
2912:
2911:
2910:
2907:
2903:
2900:
2898:
2895:
2893:
2890:
2888:
2885:
2884:
2883:
2880:
2878:
2875:
2871:
2868:
2866:
2863:
2861:
2858:
2857:
2856:
2853:
2849:
2846:
2844:
2841:
2839:
2836:
2834:
2831:
2829:
2826:
2824:
2821:
2820:
2819:
2816:
2814:
2811:
2809:
2806:
2804:
2801:
2797:
2794:
2792:
2789:
2787:
2784:
2782:
2779:
2778:
2777:
2774:
2772:
2769:
2767:
2764:
2762:
2759:
2755:
2752:
2750:
2749:by definition
2747:
2746:
2745:
2742:
2738:
2735:
2734:
2733:
2730:
2728:
2725:
2723:
2720:
2718:
2715:
2713:
2710:
2709:
2706:
2703:
2701:
2697:
2692:
2686:
2682:
2672:
2669:
2667:
2664:
2662:
2659:
2657:
2654:
2652:
2649:
2647:
2644:
2642:
2639:
2637:
2636:Kripke–Platek
2634:
2632:
2629:
2625:
2622:
2620:
2617:
2616:
2615:
2612:
2611:
2609:
2605:
2597:
2594:
2593:
2592:
2589:
2587:
2584:
2580:
2577:
2576:
2575:
2572:
2570:
2567:
2565:
2562:
2560:
2557:
2555:
2552:
2549:
2545:
2541:
2538:
2534:
2531:
2529:
2526:
2524:
2521:
2520:
2519:
2515:
2512:
2511:
2509:
2507:
2503:
2499:
2491:
2488:
2486:
2483:
2481:
2480:constructible
2478:
2477:
2476:
2473:
2471:
2468:
2466:
2463:
2461:
2458:
2456:
2453:
2451:
2448:
2446:
2443:
2441:
2438:
2436:
2433:
2431:
2428:
2426:
2423:
2421:
2418:
2416:
2413:
2412:
2410:
2408:
2403:
2395:
2392:
2390:
2387:
2385:
2382:
2380:
2377:
2375:
2372:
2370:
2367:
2366:
2364:
2360:
2357:
2355:
2352:
2351:
2350:
2347:
2345:
2342:
2340:
2337:
2335:
2332:
2330:
2326:
2322:
2320:
2317:
2313:
2310:
2309:
2308:
2305:
2304:
2301:
2298:
2296:
2292:
2282:
2279:
2277:
2274:
2272:
2269:
2267:
2264:
2262:
2259:
2257:
2254:
2250:
2247:
2246:
2245:
2242:
2238:
2233:
2232:
2231:
2228:
2227:
2225:
2223:
2219:
2211:
2208:
2206:
2203:
2201:
2198:
2197:
2196:
2193:
2191:
2188:
2186:
2183:
2181:
2178:
2176:
2173:
2171:
2168:
2166:
2163:
2162:
2160:
2158:
2157:Propositional
2154:
2148:
2145:
2143:
2140:
2138:
2135:
2133:
2130:
2128:
2125:
2123:
2120:
2116:
2113:
2112:
2111:
2108:
2106:
2103:
2101:
2098:
2096:
2093:
2091:
2088:
2086:
2085:Logical truth
2083:
2081:
2078:
2077:
2075:
2073:
2069:
2066:
2064:
2060:
2054:
2051:
2049:
2046:
2044:
2041:
2039:
2036:
2034:
2031:
2029:
2025:
2021:
2017:
2015:
2012:
2010:
2007:
2005:
2001:
1998:
1997:
1995:
1993:
1987:
1982:
1976:
1973:
1971:
1968:
1966:
1963:
1961:
1958:
1956:
1953:
1951:
1948:
1946:
1943:
1941:
1938:
1936:
1933:
1931:
1928:
1926:
1923:
1921:
1918:
1914:
1911:
1910:
1909:
1906:
1905:
1903:
1899:
1895:
1888:
1883:
1881:
1876:
1874:
1869:
1868:
1865:
1858:
1857:
1853:
1850:
1846:
1845:
1841:
1838:
1834:
1833:
1829:
1828:
1824:
1814:
1811:
1804:
1800:
1796:
1795:Gödel's Proof
1793:
1783:on 2018-04-11
1779:
1775:
1771:
1767:
1763:
1759:
1755:
1754:
1746:
1741:
1740:
1736:
1716:
1713:
1710:
1707:
1704:
1701:
1698:
1688:
1685:
1682:
1680:
1667:
1657:
1641:
1638:
1635:
1632:
1629:
1623:
1615:
1611:
1607:
1604:
1601:
1596:
1592:
1588:
1585:
1582:
1577:
1573:
1569:
1566:
1560:
1549:
1546:
1543:
1536:
1532:
1529:
1526:
1518:
1515:
1512:
1505:
1501:
1498:
1495:
1487:
1484:
1481:
1474:
1470:
1467:
1443:
1440:
1432:
1428:
1421:
1413:
1409:
1405:
1401:
1397:
1393:
1387:
1384:
1377:
1373:
1370:
1368:
1365:
1363:
1360:
1358:
1355:
1353:
1350:
1349:
1345:
1343:
1341:
1336:
1328:
1326:
1324:
1316:
1312:
1309:
1305:
1301:
1300:
1299:
1297:
1289:
1287:
1285:
1280:
1275:
1258:
1252:
1246:
1243:
1234:
1228:
1225:
1219:
1213:
1205:
1201:
1193:
1192:
1191:
1174:
1171:
1166:
1162:
1158:
1155:
1152:
1145:
1144:
1143:
1141:
1137:
1133:
1129:
1125:
1119:
1115:
1111:
1107:
1101:
1093:
1091:
1089:
1085:
1079:
1071:
1066:
1064:
1062:
1057:
1056:
1052:
1036:
1016:
1008:
989:
984:
980:
976:
968:
964:
957:
954:
949:
945:
941:
933:
930:
927:
923:
916:
913:
910:
907:
899:
896:
893:
886:
882:
874:
870:
863:
860:
852:
849:
846:
839:
835:
827:
823:
816:
809:
808:
807:
791:
787:
783:
778:
774:
768:
764:
758:
754:
745:
741:
739:
733:
730:
726:
718:
716:
709:
707:
705:
700:
698:
692:
690:
689:prime factors
686:
667:
660:
656:
650:
646:
642:
635:
631:
626:
622:
615:
611:
606:
602:
595:
591:
586:
582:
574:
570:
566:
563:
560:
555:
551:
547:
542:
538:
534:
529:
525:
503:
502:
501:
499:
478:
474:
470:
467:
464:
461:
458:
453:
449:
445:
440:
436:
432:
427:
423:
410:
408:
395:
392:
389:
386:
383:
380:
377:
374:
371:
368:
365:
362:
359:
356:
353:
350:
349:
345:
340:
337:
332:
329:
324:
321:
318:
313:
310:
305:
302:
297:
294:
291:
288:
285:
282:
279:
277:
274:
271:
268:
267:
263:
254:
212:
210:x=y => y=x
206:
190:
184:
183:
182:
180:
174:
172:
164:
162:
159:
157:
153:
149:
145:
140:
138:
134:
130:
126:
123:, called its
122:
118:
114:
110:
106:
102:
91:
88:
80:
70:
66:
60:
59:
53:
48:
39:
38:
33:
19:
3602:
3400:Ultraproduct
3247:Model theory
3212:Independence
3148:Formal proof
3140:Proof theory
3123:
3096:
3053:real numbers
3025:second-order
2936:Substitution
2813:Metalanguage
2754:conservative
2727:Axiom schema
2671:Constructive
2641:Morse–Kelley
2607:Set theories
2586:Aleph number
2579:inaccessible
2563:
2485:Grothendieck
2369:intersection
2256:Higher-order
2244:Second-order
2190:Truth tables
2147:Venn diagram
1930:Formal proof
1854:
1842:
1830:
1813:
1799:Ernest Nagel
1794:
1785:, retrieved
1778:the original
1757:
1751:
1687:
1660:
1658:
1457:
1411:
1407:
1406:but decimal
1403:
1402:and so with
1399:
1395:
1391:
1386:
1332:
1320:
1293:
1276:
1273:
1189:
1139:
1135:
1131:
1127:
1120:
1113:
1109:
1103:
1086:are in fact
1081:
1063:has K=1000.
1058:
1054:
1050:
1006:
1004:
743:
737:
731:
724:
722:
713:
701:
693:
682:
497:
411:
404:
338:
330:
322:
311:
303:
295:
275:
208:
186:
175:
171:Gödel number
170:
168:
160:
141:
125:Gödel number
124:
104:
98:
83:
74:
55:
18:Gödel number
3510:Type theory
3458:undecidable
3390:Truth value
3277:equivalence
2956:non-logical
2569:Enumeration
2559:Isomorphism
2506:cardinality
2490:Von Neumann
2455:Ultrafilter
2420:Uncountable
2354:equivalence
2271:Quantifiers
2261:Fixed-point
2230:First-order
2110:Consistency
2095:Proposition
2072:Traditional
2043:Lindström's
2033:Compactness
1975:Type theory
1920:Cardinality
1760:: 173–198,
1329:Gödel sets
69:introducing
3625:Categories
3321:elementary
3014:arithmetic
2882:Quantifier
2860:functional
2732:Expression
2450:Transitive
2394:identities
2379:complement
2312:hereditary
2295:Set theory
1787:2013-12-07
1737:References
697:Gödel 1931
137:Gödel 1931
129:Kurt Gödel
77:April 2021
52:references
3592:Supertask
3495:Recursion
3453:decidable
3287:saturated
3265:of models
3188:deductive
3183:axiomatic
3103:Hilbert's
3090:Euclidean
3071:canonical
2994:axiomatic
2926:Signature
2855:Predicate
2744:Extension
2666:Ackermann
2591:Operation
2470:Universal
2460:Recursive
2435:Singleton
2430:Inhabited
2415:Countable
2405:Types of
2389:power set
2359:partition
2276:Predicate
2222:Predicate
2137:Syllogism
2127:Soundness
2100:Inference
2090:Tautology
1992:paradoxes
1774:197663120
1608:×
1589:×
1570:×
1547:−
1533:×
1516:−
1502:×
1485:−
1471:×
1414:). Using
1308:algorithm
1163:⊢
1072:Recursion
977:×
942:×
931:−
911:⋯
897:−
883:×
850:−
836:×
784:…
643:⋯
623:⋅
603:⋅
564:…
185:The word
119:a unique
3577:Logicism
3570:timeline
3546:Concrete
3405:Validity
3375:T-schema
3368:Kripke's
3363:Tarski's
3358:semantic
3348:Strength
3297:submodel
3292:spectrum
3260:function
3108:Tarski's
3097:Elements
3084:geometry
3040:Robinson
2961:variable
2946:function
2919:spectrum
2909:Sentence
2865:variable
2808:Language
2761:Relation
2722:Automata
2712:Alphabet
2696:language
2550:-jection
2528:codomain
2514:Function
2475:Universe
2445:Infinite
2349:Relation
2132:Validity
2122:Argument
2020:theorem,
1410:will be
1346:See also
746:symbols
144:encoding
115:of some
109:function
3519:Related
3316:Diagram
3214: (
3193:Hilbert
3178:Systems
3173:Theorem
3051:of the
2996:systems
2776:Formula
2771:Grammar
2687: (
2631:General
2344:Forcing
2329:Element
2249:Monadic
2024:paradox
1965:Theorem
1901:General
1142:, i.e.
710:Example
351:Number
269:Symbol
65:improve
3282:finite
3045:Skolem
2998:
2973:Theory
2941:Symbol
2931:String
2914:atomic
2791:ground
2786:closed
2781:atomic
2737:ground
2700:syntax
2596:binary
2523:domain
2440:Finite
2205:finite
2063:Logics
2022:
1970:Theory
1772:
148:symbol
54:, but
3272:Model
3020:Peano
2877:Proof
2717:Arity
2646:Naive
2533:image
2465:Fuzzy
2425:Empty
2374:union
2319:Class
1960:Model
1950:Lemma
1908:Axiom
1835:, by
1781:(PDF)
1770:S2CID
1748:(PDF)
1378:Notes
1315:group
1190:then
179:ASCII
150:of a
107:is a
3395:Type
3198:list
3002:list
2979:list
2968:Term
2902:rank
2796:open
2690:list
2502:Maps
2407:sets
2266:Free
2236:list
1986:list
1913:list
1801:and
1134:and
1061:here
396:...
393:529
390:361
387:289
384:...
346:...
319:...
264:...
188:foxy
103:, a
3082:of
3064:of
3012:of
2544:Sur
2518:Map
2325:Ur-
2307:Set
1847:by
1797:by
1762:doi
1668:123
1630:100
1404:21;
1400:19,
1294:In
381:23
378:19
375:17
372:13
369:11
241:120
238:061
235:121
232:032
229:062
226:061
223:032
220:121
217:061
215:120
201:121
198:120
195:111
193:102
135:. (
99:In
3627::
3468:NP
3092::
3086::
3016::
2693:),
2548:Bi
2540:In
1768:,
1758:38
1756:,
1750:,
1636:20
1612:10
1593:10
1574:10
1537:10
1506:10
1475:10
1412:1A
1408:20
1396:19
1392:A,
1342:.
1286:.
1090:.
706:.
699:)
366:9
363:7
360:5
357:3
354:1
292:)
289:(
286:∀
283:∨
280:¬
272:0
139:)
3548:/
3463:P
3218:)
3004:)
3000:(
2897:∀
2892:!
2887:∃
2848:=
2843:↔
2838:→
2833:∧
2828:∨
2823:¬
2546:/
2542:/
2516:/
2327:)
2323:(
2210:∞
2200:3
1988:)
1886:e
1879:t
1872:v
1791:.
1764::
1729:)
1717:3
1714:+
1711:A
1708:1
1705:+
1702:A
1699:9
1645:)
1642:3
1639:+
1633:+
1627:(
1624:=
1621:)
1616:0
1605:3
1602:+
1597:1
1586:2
1583:+
1578:2
1567:1
1564:(
1561:=
1558:)
1553:)
1550:3
1544:3
1541:(
1530:3
1527:+
1522:)
1519:2
1513:3
1510:(
1499:2
1496:+
1491:)
1488:1
1482:3
1479:(
1468:1
1465:(
1444:n
1441:=
1438:)
1433:n
1429:s
1425:(
1422:h
1259:.
1256:)
1253:C
1250:(
1247:f
1244:=
1241:)
1238:)
1235:B
1232:(
1229:f
1226:,
1223:)
1220:A
1217:(
1214:f
1211:(
1206:r
1202:g
1175:,
1172:C
1167:r
1159:B
1156:,
1153:A
1140:r
1136:B
1132:A
1128:C
1123:r
1121:g
1114:r
1110:f
1051:K
1037:i
1017:i
1007:K
990:.
985:0
981:K
974:)
969:n
965:s
961:(
958:h
955:+
950:1
946:K
939:)
934:1
928:n
924:s
920:(
917:h
914:+
908:+
903:)
900:2
894:n
891:(
887:K
880:)
875:2
871:s
867:(
864:h
861:+
856:)
853:1
847:n
844:(
840:K
833:)
828:1
824:s
820:(
817:h
792:n
788:s
779:3
775:s
769:2
765:s
759:1
755:s
744:n
738:K
732:h
725:K
668:.
661:n
657:x
651:n
647:p
636:3
632:x
627:5
616:2
612:x
607:3
596:1
592:x
587:2
583:=
580:)
575:n
571:x
567:,
561:,
556:3
552:x
548:,
543:2
539:x
535:,
530:1
526:x
522:(
518:c
515:n
512:e
498:n
484:)
479:n
475:x
471:,
468:.
465:.
462:.
459:,
454:3
450:x
446:,
441:2
437:x
433:,
428:1
424:x
420:(
342:3
339:P
334:2
331:P
326:1
323:P
315:3
312:x
307:2
304:x
299:1
296:x
276:s
244:.
204:.
90:)
84:(
79:)
75:(
61:.
34:.
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.