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