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