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