4239:
68:, computable functions are exactly the functions that can be calculated using a mechanical (that is, automatic) calculation device given unlimited amounts of time and storage space. More precisely, every model of computation that has ever been imagined can compute only computable functions, and all computable functions can be computed by any of several models of computation that are apparently very different, such as
1625:. In this case, and in the case of the primitive recursive functions, well-ordering is obvious, but some "refers-to" relations are nontrivial to prove as being well-orderings. Any function defined recursively in a well-ordered way is computable: each value can be computed by expanding a tree of recursive calls to the function, and this expansion must terminate after a finite number of calls, because otherwise
555:) telling how to compute the function. The models of computation listed above give different interpretations of what a procedure is and how it is used, but these interpretations share many properties. The fact that these models give equivalent classes of computable functions stems from the fact that each model is capable of reading and mimicking a procedure for any of the other models, much as a
1741:, asked whether there is an effective procedure to determine which mathematical statements (coded as natural numbers) are true. Turing and Church independently showed in the 1930s that this set of natural numbers is not computable. According to the Church–Turing thesis, there is no effective procedure (with an algorithm) which can perform these computations.
569:"There must be exact instructions (i.e. a program), finite in length, for the procedure." Thus every computable function must have a finite program that completely describes how the function is to be computed. It is possible to compute the function by just following the instructions; no guessing or special insight is required.
1802:. As with the concept of a computable function relative computability can be given equivalent definitions in many different models of computation. This is commonly accomplished by supplementing the model of computation with an additional primitive operation which asks whether a given integer is a member of
1641:
proof system, every provably total function is indeed total, but the converse is not true: in every first-order proof system that is strong enough and sound (including Peano arithmetic), one can prove (in another proof system) the existence of total functions that cannot be proven total in the proof
926:
A key property of a formal language is the level of difficulty required to decide whether a given word is in the language. Some coding system must be developed to allow a computable function to take an arbitrary word in the language as input; this is usually considered routine. A language is called
1419:
The Church–Turing thesis is sometimes used in proofs to justify that a particular function is computable by giving a concrete description of a procedure for the computation. This is permitted because it is believed that all such uses of the thesis can be removed by the tedious process of writing a
299:
Although these models use different representations for the functions, their inputs, and their outputs, translations exist between any two models, and so every model describes essentially the same class of functions, giving rise to the opinion that formal computability is both natural and not too
1645:
If the total computable functions are enumerated via the Turing machines that produces them, then the above statement can be shown, if the proof system is sound, by a similar diagonalization argument to that used above, using the enumeration of provably total functions given earlier. One uses a
41:, in the sense that a function is computable if there exists an algorithm that can do the job of the function, i.e. given an input of the function domain it can return the corresponding output. Computable functions are used to discuss computability without referring to any concrete
637:
Although the procedure may use only a finite amount of storage space during a successful computation, there is no bound on the amount of space that is used. It is assumed that additional storage space can be given to the procedure whenever the procedure asks for
99:
computed (i.e. computed within a reasonable amount of time). In fact, for some effectively calculable functions it can be shown that any algorithm that computes them will be very inefficient in the sense that the running time of the algorithm increases
53:. Any definition, however, must make reference to some specific model of computation but all valid definitions yield the same class of functions. Particular models of computability that give rise to the set of computable functions are the
1856:
Although the Church–Turing thesis states that the computable functions include all functions with algorithms, it is possible to consider broader classes of functions that relax the requirements that algorithms must possess. The field of
1694:
Every computable function has a finite procedure giving explicit, unambiguous instructions on how to compute it. Furthermore, this procedure has to be encoded in the finite alphabet used by the computational model, so there are only
1450:: one can enumerate all the provably total functions by enumerating all their corresponding proofs, that prove their computability. This can be done by enumerating all the proofs of the proof system and ignoring irrelevant ones.
623:) is ever found, it must be the correct value. It is not necessary for the computing agent to distinguish correct outcomes from incorrect ones because the procedure is defined as correct if and only if it produces an outcome.
592:)." Intuitively, the procedure proceeds step by step, with a specific rule to cover what to do at each step of the calculation. Only finitely many steps can be carried out before the value of the function is returned.
647:
given an input from its domain, possibly relying on unbounded storage space, it can give the corresponding output by following a procedure (program, algorithm) that is formed by a finite number of exact unambiguous
390:
190:
607:, then the procedure might go on forever, never halting. Or it might get stuck at some point (i.e., one of its instructions cannot be executed), but it must not pretend to produce a value for
1473:
For definitions of this type to avoid circularity or infinite regress, it is necessary that recursive calls to the same function within a definition be to arguments that are smaller in some
1462:, each value is defined by a fixed first-order formula of other, previously defined values of the same function or other functions, which might be simply constants. A subset of these is the
1404:
is a computable function. Because these three properties are not formally stated, the Church–Turing thesis cannot be proved. The following facts are often taken as evidence for the thesis:
300:
narrow. These functions are sometimes referred to as "recursive", to contrast with the informal term "computable", a distinction stemming from a 1934 discussion between Kleene and Gödel.
923:
is a subset of the collection of all words on a fixed alphabet. For example, the collection of all binary strings that contain exactly 3 ones is a language over the binary alphabet.
1201:
973:
if the word is not in the language. Thus a language is computable just in case there is a procedure that is able to correctly tell whether arbitrary words are in the language.
915:
on an alphabet is a finite sequence of symbols from the alphabet; the same symbol may be used more than once. For example, binary strings are exactly the words on the alphabet
634:
The procedure is required to halt after finitely many steps in order to produce an output, but it may take arbitrarily many steps before halting. No time limitation is assumed.
2618:
512:
478:
425:
250:
1615:
319:
and return a single natural number (just as above). They are the smallest class of partial functions that includes the constant, successor, and projection functions, and is
631:
The procedure must theoretically work for arbitrarily large arguments. It is not assumed that the arguments are smaller than the number of atoms in the Earth, for example.
534:
447:
219:
259:
As counterparts to this informal description, there exist multiple formal, mathematical definitions. The class of computable functions can be defined in many equivalent
3293:
1565:
1530:
1680:
enumeration) by invoking the Turing machine that computes it according to the n-th proof. Such a Turing machine is guaranteed to halt if the proof system is sound.
565:
gives the following characteristics of a procedure for computing a computable function; similar characterizations have been given by Turing , Rogers , and others.
1840:
of the empty set. This is equivalent to sets defined by both a universal and existential formula in the language of second order arithmetic and to some models of
1495:
3376:
2517:
2108:
95:. This term has since come to be identified with the computable functions. The effective computability of these functions does not imply that they can be
127:
on the set of computable functions. In computational complexity theory, the problem of determining the complexity of a computable function is known as a
1408:
Many equivalent models of computation are known, and they all give the same definition of computable function (or a weaker version, in some instances).
1322:. Every such function is computable. It is not known whether there are arbitrarily long runs of fives in the decimal expansion of π, so we don't know
145:
Computability of a function is an informal notion. One way to describe it is to say that a function is computable if its value can be obtained by an
900:
3690:
3848:
2636:
3703:
3026:
3288:
3708:
3698:
3435:
2641:
3186:
2632:
3844:
2470:
1964:
1939:
338:
Equivalently, computable functions can be formalized as functions which can be calculated by an idealized computing agent such as a
3941:
3685:
2510:
2101:
1365:. Thus, "Print 0, 1, 4, 6, 13" is a trivial algorithm to compute Σ(0), Σ(1), Σ(2), Σ(3), Σ(4); similarly, for any given value of
3246:
2939:
2680:
352:
152:
660:
124:
113:
4268:
4202:
3904:
3667:
3662:
3487:
2908:
2592:
4263:
4197:
3980:
3897:
3610:
3541:
3418:
2660:
1428:
Given a function (or, similarly, a set), one may be interested not only if it is computable, but also whether this can be
3268:
877:
on the natural numbers can be identified with a corresponding set of finite sequences of natural numbers, the notions of
794:
is in the set. Thus a set is computably enumerable if and only if it is the domain of some computable function. The word
252:. In agreement with this definition, the remainder of this article presumes that computable functions take finitely many
4122:
3948:
3634:
2867:
1689:
1463:
1250:
The following examples illustrate that a function may be computable though it is not known which algorithm computes it.
328:
3273:
3605:
3344:
2602:
2503:
2094:
4000:
3995:
2293:
1714:
functions on the natural numbers is uncountable so most are not computable. Concrete examples of such functions are
627:
Enderton goes on to list several clarifications of these 3 requirements of the procedure for a computable function:
3929:
3519:
2913:
2881:
2572:
2486:
81:
58:
54:
2646:
4219:
4168:
4065:
3563:
3524:
3001:
1905:
4060:
2675:
1391:
65:
3990:
3529:
3381:
3364:
3087:
2567:
2475:
1829:
283:
3892:
3869:
3830:
3716:
3657:
3303:
3223:
3067:
3011:
2624:
1910:
1127:
304:
272:
1178:
4182:
3909:
3887:
3854:
3747:
3593:
3578:
3551:
3502:
3386:
3321:
3146:
3112:
3107:
2981:
2812:
2789:
2429:
1895:
1799:
1755:
1447:
1412:
109:
4112:
3965:
3757:
3475:
3211:
3117:
2976:
2961:
2842:
2817:
2424:
2419:
2011:
1880:
1719:
320:
4238:
1723:
1134:
663:
studies functions with prescribed bounds on the time and/or space allowed in a successful computation.
1699:
many computable functions. For example, functions may be encoded using a string of bits (the alphabet
4085:
4047:
3924:
3728:
3568:
3492:
3470:
3298:
3256:
3155:
3122:
2986:
2774:
2685:
2414:
1734:
1459:
1175:
1028:
486:
452:
399:
324:
260:
224:
140:
42:
1570:
4214:
4105:
4090:
4027:
3914:
3864:
3790:
3735:
3672:
3465:
3460:
3408:
3176:
3165:
2837:
2737:
2665:
2656:
2652:
2587:
2582:
1629:
would lead to an infinite descending sequence of calls, violating the assumption of well-ordering.
1618:
1794:) when it satisfies the definition of a computable function with modifications allowing access to
1626:
517:
430:
202:
4243:
4012:
3975:
3960:
3953:
3936:
3722:
3588:
3514:
3497:
3450:
3263:
3172:
3006:
2991:
2951:
2903:
2888:
2876:
2832:
2807:
2577:
2526:
2028:
1833:
1474:
1467:
559:
is able to read instructions in one computer language and emit instructions in another language.
101:
3740:
3196:
392:
can be calculated if and only if there exists a computer program with the following properties:
1993:
551:
The basic characteristic of a computable function is that there must be a finite procedure (an
4178:
3985:
3795:
3785:
3677:
3558:
3393:
3369:
3150:
3134:
3039:
3016:
2893:
2862:
2827:
2722:
2557:
2434:
2006:
1960:
1935:
1870:
1759:
1707:
1433:
1035:
874:
4192:
4187:
4080:
4037:
3859:
3820:
3815:
3800:
3626:
3583:
3480:
3278:
3228:
2802:
2764:
2398:
2288:
2220:
2210:
2117:
2051:
2020:
1900:
1885:
1875:
1858:
1841:
1535:
1500:
1436:
1400:
states that any function computable from a procedure possessing the three properties listed
562:
347:
343:
308:
293:
146:
128:
73:
50:
34:
2323:
4173:
4163:
4117:
4100:
4055:
4017:
3919:
3839:
3646:
3573:
3546:
3534:
3440:
3354:
3328:
3283:
3251:
3052:
2854:
2797:
2747:
2712:
2670:
2393:
2383:
2340:
2330:
2313:
2303:
2261:
2256:
2251:
2235:
2215:
2193:
2188:
2183:
2171:
2166:
2161:
2156:
1730:
1209:
904:
894:
277:
253:
77:
584:, then after a finite number of discrete steps the procedure must terminate and produce
4158:
4137:
4095:
4075:
3970:
3825:
3423:
3413:
3403:
3398:
3332:
3206:
3082:
2971:
2966:
2944:
2545:
2388:
2276:
2198:
2151:
1763:
1622:
1480:
1349:, there exists an algorithm that computes the finite sequence Σ(0), Σ(1), Σ(2), ..., Σ(
1165:
786:
339:
316:
267:
69:
46:
4257:
4132:
3810:
3317:
3102:
3092:
3062:
3047:
2717:
2032:
1890:
1738:
332:
88:
654:
if given an input which is not in its domain it either never halts or it gets stuck.
17:
4032:
3879:
3780:
3772:
3652:
3600:
3509:
3445:
3428:
3359:
3218:
3077:
2779:
2562:
1696:
1141:
4142:
4022:
3201:
3191:
3138:
2822:
2742:
2727:
2607:
2552:
2266:
2176:
1837:
1715:
1342:
120:
3072:
2927:
2898:
2704:
2378:
2203:
2072:
1706:
The real numbers are uncountable so most real numbers are not computable. See
287:
37:. Computable functions are the formalized analogue of the intuitive notion of
1722:, or any function that outputs the digits of a noncomputable number, such as
192:
is computable if and only if there is an effective procedure that, given any
4224:
4127:
3180:
3097:
3057:
3021:
2957:
2769:
2759:
2732:
2373:
2068:
1638:
1015:
has the same etymology as in computably enumerable sets of natural numbers.
828:
552:
546:
105:
38:
1286:
is either the constant 1 function, which is computable, or else there is a
4209:
4007:
3455:
3160:
2754:
2368:
2363:
2308:
2131:
1711:
1353:) — in contrast to the fact that there is no algorithm that computes the
1076:
556:
1861:
studies models of computation that go beyond normal Turing computation.
1848:
in which any set can be used as an argument to an E-recursive function.
1646:
Turing machine that enumerates the relevant proofs, and for every input
3805:
2597:
2358:
2024:
1729:
Similarly, most subsets of the natural numbers are not computable. The
1230:
2318:
2079:, Series 2, Volume 42 (1937), p.230–265. Reprinted in M. Davis (ed.),
2073:
On
Computable Numbers, With an Application to the Entscheidungsproblem
2495:
2465:
2460:
2335:
2086:
1411:
No stronger model of computation which is generally considered to be
1477:
on the function's domain. For instance, for the
Ackermann function
798:
is used because the following are equivalent for a nonempty subset
256:
as arguments and produce a value which is a single natural number.
3349:
2695:
2540:
2455:
2450:
2271:
1844:. Even more general recursion theories have been studied, such as
312:
197:
2283:
2141:
1983:(Studies in Logic and the Foundation of Mathematics, 2000), p. 4
1420:
formal procedure for the function in some model of computation.
2499:
2090:
651:
it returns such output (halts) in a finite number of steps; and
2298:
2230:
2225:
2146:
2136:
642:
To summarise, based on this view a function is computable if:
514:
is undefined, then the program never terminates on the input
1470:, which is recursively defined but not primitive recursive.
1439:). A function that can be proven to be computable is called
1401:
1377:
or produced by anyone) to compute Σ(0), Σ(1), Σ(2), ..., Σ(
385:{\displaystyle f:\mathbb {N} ^{k}\rightarrow \mathbb {N} }
185:{\displaystyle f:\mathbb {N} ^{k}\rightarrow \mathbb {N} }
1981:
Computable
Structures and the Hyperarithmetical Hierarchy
427:
is defined, then the program will terminate on the input
2063:
Theory of recursive functions and effective computation
303:
For example, one can formalize computable functions as
27:
Mathematical function that can be computed by a program
87:
Before the precise definition of computable function,
1573:
1538:
1503:
1483:
1181:
847:
then the function can be viewed as an enumeration of
520:
489:
455:
433:
402:
355:
227:
205:
155:
1341:
computable sequence of natural numbers (such as the
4151:
4046:
3878:
3771:
3623:
3316:
3239:
3133:
3037:
2926:
2853:
2788:
2703:
2694:
2616:
2533:
2443:
2407:
2351:
2244:
2124:
2009:(1935). "Konstruktion nichtrekursiver Funktionen".
1959:(Second ed.). USA: Elsevier. p. 208,262.
827:is infinite then the function can be assumed to be
1609:
1559:
1524:
1489:
1195:
528:
506:
472:
441:
419:
384:
244:
213:
184:
116:study functions that can be computed efficiently.
1754:The notion of computability of a function can be
1345:Σ) is computable. E.g., for each natural number
821:is the range of a total computable function. If
1934:(Second ed.). USA: Elsevier. p. 209.
1832:studies those sets that can be computed from a
1031:; e.g., any finite sequence of natural numbers.
2077:Proceedings of the London Mathematical Society
1733:was the first such set to be constructed. The
1684:Uncomputable functions and unsolvable problems
1282:) = 0 otherwise, is computable. (The function
1270:consecutive fives in the decimal expansion of
885:can be defined from their analogues for sets.
108:) with the length of the input. The fields of
2511:
2102:
8:
1633:Total functions that are not provably total
689:) if there is a computable, total function
221:of natural numbers, will produce the value
3337:
2932:
2700:
2518:
2504:
2496:
2109:
2095:
2087:
1330:. Nevertheless, we know that the function
1572:
1537:
1502:
1482:
1454:Relation to recursively defined functions
1180:
521:
519:
496:
488:
462:
454:
434:
432:
409:
401:
378:
377:
368:
364:
363:
354:
234:
226:
206:
204:
178:
177:
168:
164:
163:
154:
1023:The following functions are computable:
901:computability theory in computer science
1922:
1446:The set of provably total functions is
813:is the domain of a computable function.
541:Characteristics of computable functions
2058:(North-Holland 1977) pp. 527–566.
1432:in a particular proof system (usually
1196:{\displaystyle \color {Blue}f\circ g}
1182:
7:
1957:A Mathematical Introduction to Logic
1932:A Mathematical Introduction to Logic
988:) if there is a computable function
939:) if there is a computable function
762:) if there is a computable function
2048:. Cambridge University Press, 1980.
1005:is defined if and only if the word
962:if the word is in the language and
750:A set of natural numbers is called
123:can be used to define an abstract
33:are the basic objects of study in
25:
2471:Probabilistically checkable proof
2083:, Raven Press, Hewlett, NY, 1965.
1996:(1995). Accessed 9 November 2022.
695:such that for any natural number
4237:
1266:) = 1 if there is a sequence of
522:
497:
463:
435:
410:
235:
207:
507:{\displaystyle f(\mathbf {x} )}
473:{\displaystyle f(\mathbf {x} )}
420:{\displaystyle f(\mathbf {x} )}
245:{\displaystyle f(\mathbf {x} )}
125:computational complexity theory
2056:Handbook of Mathematical Logic
2054:Elements of recursion theory.
1610:{\displaystyle (p,q)<(x,y)}
1604:
1592:
1586:
1574:
1554:
1542:
1519:
1507:
883:computably enumerable relation
864:will include every element of
603:which is not in the domain of
501:
493:
480:stored in the computer memory.
467:
459:
414:
406:
374:
239:
231:
174:
149:. With more rigor, a function
1:
4198:History of mathematical logic
1497:, whenever the definition of
1464:primitive recursive functions
1373:(even though it may never be
1156:are computable, then so are:
1011:is in the language. The term
677:of natural numbers is called
667:Computable sets and relations
595:"If the procedure is given a
572:"If the procedure is given a
91:often used the informal term
4123:Primitive recursive function
1690:List of undecidable problems
1247:and many more combinations.
1027:Each function with a finite
529:{\displaystyle \mathbf {x} }
442:{\displaystyle \mathbf {x} }
214:{\displaystyle \mathbf {x} }
1994:Computability and Recursion
1745:Extensions of computability
1458:In a function defined by a
1369:, such a trivial algorithm
903:, it is common to consider
841:is the range of a function
82:general recursive functions
59:general recursive functions
55:Turing-computable functions
4285:
3187:Schröder–Bernstein theorem
2914:Monadic predicate calculus
2573:Foundations of mathematics
2487:List of complexity classes
1955:Enderton, Herbert (2002).
1930:Enderton, Herbert (2002).
1836:number of iterates of the
1687:
1389:
1337:Each finite segment of an
892:
768:such that for each number
544:
138:
4233:
4220:Philosophy of mathematics
4169:Automated theorem proving
3340:
3294:Von Neumann–Bernays–Gödel
2935:
2484:
1906:Super-recursive algorithm
1806:. We can also talk about
1466:. Another example is the
2476:Interactive proof system
1830:Hyperarithmetical theory
945:such that for each word
804:of the natural numbers:
661:computational complexity
114:computational complexity
3870:Self-verifying theories
3691:Tarski's axiomatization
2642:Tarski's undefinability
2637:incompleteness theorems
1911:Semicomputable function
1825:Higher recursion theory
1789:computable relative to
1128:greatest common divisor
911:is an arbitrary set. A
615:." Thus if a value for
346:. Formally speaking, a
4244:Mathematics portal
3855:Proof of impossibility
3503:propositional variable
2813:Propositional calculus
2430:Arithmetical hierarchy
1979:C. J. Ash, J. Knight,
1896:Arithmetical hierarchy
1750:Relative computability
1611:
1561:
1560:{\displaystyle A(p,q)}
1526:
1525:{\displaystyle A(x,y)}
1491:
1448:recursively enumerable
1413:effectively calculable
1326:of those functions is
1197:
982:recursively enumerable
756:recursively enumerable
530:
508:
474:
443:
421:
386:
246:
215:
186:
110:feasible computability
93:effectively calculable
4269:Theory of computation
4113:Kolmogorov complexity
4066:Computably enumerable
3966:Model complete theory
3758:Principia Mathematica
2818:Propositional formula
2647:Banach–Tarski paradox
2425:Grzegorczyk hierarchy
2420:Exponential hierarchy
2352:Considered infeasible
2012:Mathematische Annalen
1881:Theory of computation
1720:Kolmogorov complexity
1612:
1562:
1527:
1492:
1198:
978:computably enumerable
752:computably enumerable
531:
509:
475:
444:
422:
387:
305:μ-recursive functions
273:μ-recursive functions
261:models of computation
247:
216:
187:
4264:Computability theory
4061:Church–Turing thesis
4048:Computability theory
3257:continuum hypothesis
2775:Square of opposition
2633:Gödel's completeness
2415:Polynomial hierarchy
2245:Suspected infeasible
1735:Entscheidungsproblem
1571:
1536:
1501:
1481:
1460:recursive definition
1398:Church–Turing thesis
1392:Church–Turing thesis
1386:Church–Turing thesis
1343:Busy Beaver function
1334:must be computable.)
1179:
518:
487:
453:
431:
400:
353:
284:Post–Turing machines
225:
203:
153:
141:Total Turing machine
66:Church–Turing thesis
43:model of computation
35:computability theory
31:Computable functions
18:Computable predicate
4215:Mathematical object
4106:P versus NP problem
4071:Computable function
3865:Reverse mathematics
3791:Logical consequence
3668:primitive recursive
3663:elementary function
3436:Free/bound variable
3289:Tarski–Grothendieck
2808:Logical connectives
2738:Logical equivalence
2588:Logical consequence
2444:Families of classes
2125:Considered feasible
2065:(McGraw–Hill 1967).
1619:lexicographic order
1357:Σ-sequence, i.e. Σ(
951:over the alphabet,
879:computable relation
853:, because the list
329:primitive recursion
147:effective procedure
4013:Transfer principle
3976:Semantics of logic
3961:Categorical theory
3937:Non-standard model
3451:Logical connective
2578:Information theory
2527:Mathematical logic
2118:Complexity classes
2025:10.1007/BF01472200
1846:E-recursion theory
1834:computable ordinal
1724:Chaitin's constant
1607:
1557:
1522:
1487:
1475:well-partial-order
1468:Ackermann function
1415:has been proposed.
1193:
1192:
1135:Bézout coefficient
526:
504:
470:
439:
417:
382:
242:
211:
182:
106:superexponentially
4251:
4250:
4183:Abstract category
3986:Theories of truth
3796:Rule of inference
3786:Natural deduction
3767:
3766:
3312:
3311:
3017:Cartesian product
2922:
2921:
2828:Many-valued logic
2803:Boolean functions
2686:Russell's paradox
2661:diagonal argument
2558:First-order logic
2493:
2492:
2435:Boolean hierarchy
2408:Class hierarchies
1871:Computable number
1852:Hyper-computation
1773:is defined to be
1708:computable number
1490:{\displaystyle A}
1036:constant function
875:finitary relation
580:in the domain of
311:that take finite
309:partial functions
294:Register machines
74:register machines
64:According to the
51:register machines
16:(Redirected from
4276:
4242:
4241:
4193:History of logic
4188:Category of sets
4081:Decision problem
3860:Ordinal analysis
3801:Sequent calculus
3699:Boolean algebras
3639:
3638:
3613:
3584:logical/constant
3338:
3324:
3247:Zermelo–Fraenkel
2998:Set operations:
2933:
2870:
2701:
2681:Löwenheim–Skolem
2568:Formal semantics
2520:
2513:
2506:
2497:
2111:
2104:
2097:
2088:
2044:Cutland, Nigel.
2037:
2036:
2003:
1997:
1990:
1984:
1977:
1971:
1970:
1952:
1946:
1945:
1927:
1901:Hypercomputation
1886:Recursion theory
1876:Effective method
1859:Hypercomputation
1842:Hypercomputation
1821:with its graph.
1758:to an arbitrary
1702:
1676:-th function by
1616:
1614:
1613:
1608:
1566:
1564:
1563:
1558:
1531:
1529:
1528:
1523:
1496:
1494:
1493:
1488:
1437:Peano arithmetic
1273:
1246:
1202:
1200:
1199:
1194:
1010:
1004:
993:
972:
961:
950:
944:
918:
905:formal languages
889:Formal languages
869:
863:
852:
846:
840:
826:
820:
812:
803:
793:
784:
773:
767:
746:
740:
734:
723:
717:
711:
700:
694:
676:
535:
533:
532:
527:
525:
513:
511:
510:
505:
500:
479:
477:
476:
471:
466:
448:
446:
445:
440:
438:
426:
424:
423:
418:
413:
391:
389:
388:
383:
381:
373:
372:
367:
348:partial function
344:register machine
251:
249:
248:
243:
238:
220:
218:
217:
212:
210:
195:
191:
189:
188:
183:
181:
173:
172:
167:
129:function problem
21:
4284:
4283:
4279:
4278:
4277:
4275:
4274:
4273:
4254:
4253:
4252:
4247:
4236:
4229:
4174:Category theory
4164:Algebraic logic
4147:
4118:Lambda calculus
4056:Church encoding
4042:
4018:Truth predicate
3874:
3840:Complete theory
3763:
3632:
3628:
3624:
3619:
3611:
3331: and
3327:
3322:
3308:
3284:New Foundations
3252:axiom of choice
3235:
3197:Gödel numbering
3137: and
3129:
3033:
2918:
2868:
2849:
2798:Boolean algebra
2784:
2748:Equiconsistency
2713:Classical logic
2690:
2671:Halting problem
2659: and
2635: and
2623: and
2622:
2617:Theorems (
2612:
2529:
2524:
2494:
2489:
2480:
2439:
2403:
2347:
2341:PSPACE-complete
2240:
2120:
2115:
2081:The Undecidable
2041:
2040:
2005:
2004:
2000:
1991:
1987:
1978:
1974:
1967:
1954:
1953:
1949:
1942:
1929:
1928:
1924:
1919:
1867:
1854:
1827:
1817:by identifying
1764:natural numbers
1752:
1747:
1731:halting problem
1700:
1692:
1686:
1671:
1658:
1635:
1623:natural numbers
1569:
1568:
1534:
1533:
1499:
1498:
1479:
1478:
1456:
1426:
1394:
1388:
1271:
1229:
1177:
1176:
1123:
1116:
1109:
1100:
1068:
1059:
1021:
1009:
1006:
1002:
995:
989:
970:
963:
959:
952:
949:
946:
940:
916:
897:
895:Formal language
891:
868:
865:
854:
851:
848:
842:
839:
836:
825:
822:
819:
816:
811:
808:
802:
799:
792:
789:
782:
775:
772:
769:
763:
745:
742:
739:
736:
732:
725:
722:
719:
716:
713:
709:
702:
699:
696:
690:
675:
672:
669:
657:
549:
543:
516:
515:
485:
484:
451:
450:
449:with the value
429:
428:
398:
397:
362:
351:
350:
317:natural numbers
282:Post machines (
278:Lambda calculus
268:Turing machines
254:natural numbers
223:
222:
201:
200:
193:
162:
151:
150:
143:
137:
78:lambda calculus
70:Turing machines
47:Turing machines
28:
23:
22:
15:
12:
11:
5:
4282:
4280:
4272:
4271:
4266:
4256:
4255:
4249:
4248:
4234:
4231:
4230:
4228:
4227:
4222:
4217:
4212:
4207:
4206:
4205:
4195:
4190:
4185:
4176:
4171:
4166:
4161:
4159:Abstract logic
4155:
4153:
4149:
4148:
4146:
4145:
4140:
4138:Turing machine
4135:
4130:
4125:
4120:
4115:
4110:
4109:
4108:
4103:
4098:
4093:
4088:
4078:
4076:Computable set
4073:
4068:
4063:
4058:
4052:
4050:
4044:
4043:
4041:
4040:
4035:
4030:
4025:
4020:
4015:
4010:
4005:
4004:
4003:
3998:
3993:
3983:
3978:
3973:
3971:Satisfiability
3968:
3963:
3958:
3957:
3956:
3946:
3945:
3944:
3934:
3933:
3932:
3927:
3922:
3917:
3912:
3902:
3901:
3900:
3895:
3888:Interpretation
3884:
3882:
3876:
3875:
3873:
3872:
3867:
3862:
3857:
3852:
3842:
3837:
3836:
3835:
3834:
3833:
3823:
3818:
3808:
3803:
3798:
3793:
3788:
3783:
3777:
3775:
3769:
3768:
3765:
3764:
3762:
3761:
3753:
3752:
3751:
3750:
3745:
3744:
3743:
3738:
3733:
3713:
3712:
3711:
3709:minimal axioms
3706:
3695:
3694:
3693:
3682:
3681:
3680:
3675:
3670:
3665:
3660:
3655:
3642:
3640:
3621:
3620:
3618:
3617:
3616:
3615:
3603:
3598:
3597:
3596:
3591:
3586:
3581:
3571:
3566:
3561:
3556:
3555:
3554:
3549:
3539:
3538:
3537:
3532:
3527:
3522:
3512:
3507:
3506:
3505:
3500:
3495:
3485:
3484:
3483:
3478:
3473:
3468:
3463:
3458:
3448:
3443:
3438:
3433:
3432:
3431:
3426:
3421:
3416:
3406:
3401:
3399:Formation rule
3396:
3391:
3390:
3389:
3384:
3374:
3373:
3372:
3362:
3357:
3352:
3347:
3341:
3335:
3318:Formal systems
3314:
3313:
3310:
3309:
3307:
3306:
3301:
3296:
3291:
3286:
3281:
3276:
3271:
3266:
3261:
3260:
3259:
3254:
3243:
3241:
3237:
3236:
3234:
3233:
3232:
3231:
3221:
3216:
3215:
3214:
3207:Large cardinal
3204:
3199:
3194:
3189:
3184:
3170:
3169:
3168:
3163:
3158:
3143:
3141:
3131:
3130:
3128:
3127:
3126:
3125:
3120:
3115:
3105:
3100:
3095:
3090:
3085:
3080:
3075:
3070:
3065:
3060:
3055:
3050:
3044:
3042:
3035:
3034:
3032:
3031:
3030:
3029:
3024:
3019:
3014:
3009:
3004:
2996:
2995:
2994:
2989:
2979:
2974:
2972:Extensionality
2969:
2967:Ordinal number
2964:
2954:
2949:
2948:
2947:
2936:
2930:
2924:
2923:
2920:
2919:
2917:
2916:
2911:
2906:
2901:
2896:
2891:
2886:
2885:
2884:
2874:
2873:
2872:
2859:
2857:
2851:
2850:
2848:
2847:
2846:
2845:
2840:
2835:
2825:
2820:
2815:
2810:
2805:
2800:
2794:
2792:
2786:
2785:
2783:
2782:
2777:
2772:
2767:
2762:
2757:
2752:
2751:
2750:
2740:
2735:
2730:
2725:
2720:
2715:
2709:
2707:
2698:
2692:
2691:
2689:
2688:
2683:
2678:
2673:
2668:
2663:
2651:Cantor's
2649:
2644:
2639:
2629:
2627:
2614:
2613:
2611:
2610:
2605:
2600:
2595:
2590:
2585:
2580:
2575:
2570:
2565:
2560:
2555:
2550:
2549:
2548:
2537:
2535:
2531:
2530:
2525:
2523:
2522:
2515:
2508:
2500:
2491:
2490:
2485:
2482:
2481:
2479:
2478:
2473:
2468:
2463:
2458:
2453:
2447:
2445:
2441:
2440:
2438:
2437:
2432:
2427:
2422:
2417:
2411:
2409:
2405:
2404:
2402:
2401:
2396:
2391:
2386:
2381:
2376:
2371:
2366:
2361:
2355:
2353:
2349:
2348:
2346:
2345:
2344:
2343:
2333:
2328:
2327:
2326:
2316:
2311:
2306:
2301:
2296:
2291:
2286:
2281:
2280:
2279:
2277:co-NP-complete
2274:
2269:
2264:
2254:
2248:
2246:
2242:
2241:
2239:
2238:
2233:
2228:
2223:
2218:
2213:
2208:
2207:
2206:
2196:
2191:
2186:
2181:
2180:
2179:
2169:
2164:
2159:
2154:
2149:
2144:
2139:
2134:
2128:
2126:
2122:
2121:
2116:
2114:
2113:
2106:
2099:
2091:
2085:
2084:
2066:
2059:
2052:Enderton, H.B.
2049:
2039:
2038:
1998:
1985:
1972:
1965:
1947:
1940:
1921:
1920:
1918:
1915:
1914:
1913:
1908:
1903:
1898:
1893:
1888:
1883:
1878:
1873:
1866:
1863:
1853:
1850:
1826:
1823:
1812:computable in
1780:(equivalently
1775:computable in
1751:
1748:
1746:
1743:
1737:, proposed by
1701:Σ = {0, 1
1688:Main article:
1685:
1682:
1667:
1654:
1634:
1631:
1606:
1603:
1600:
1597:
1594:
1591:
1588:
1585:
1582:
1579:
1576:
1556:
1553:
1550:
1547:
1544:
1541:
1521:
1518:
1515:
1512:
1509:
1506:
1486:
1455:
1452:
1441:provably total
1425:
1422:
1417:
1416:
1409:
1390:Main article:
1387:
1384:
1383:
1382:
1335:
1191:
1188:
1185:
1146:
1145:
1138:
1137:of two numbers
1131:
1130:of two numbers
1124:
1121:
1114:
1105:
1098:
1074:
1064:
1057:
1032:
1020:
1017:
1007:
1000:
976:A language is
968:
957:
947:
893:Main article:
890:
887:
866:
849:
837:
833:
832:
823:
817:
814:
809:
800:
790:
787:if and only if
780:
770:
743:
737:
730:
720:
714:
707:
697:
673:
668:
665:
656:
655:
652:
649:
644:
640:
639:
635:
632:
625:
624:
593:
570:
545:Main article:
542:
539:
538:
537:
524:
503:
499:
495:
492:
481:
469:
465:
461:
458:
437:
416:
412:
408:
405:
380:
376:
371:
366:
361:
358:
340:Turing machine
297:
296:
291:
280:
275:
270:
241:
237:
233:
230:
209:
180:
176:
171:
166:
161:
158:
136:
133:
89:mathematicians
26:
24:
14:
13:
10:
9:
6:
4:
3:
2:
4281:
4270:
4267:
4265:
4262:
4261:
4259:
4246:
4245:
4240:
4232:
4226:
4223:
4221:
4218:
4216:
4213:
4211:
4208:
4204:
4201:
4200:
4199:
4196:
4194:
4191:
4189:
4186:
4184:
4180:
4177:
4175:
4172:
4170:
4167:
4165:
4162:
4160:
4157:
4156:
4154:
4150:
4144:
4141:
4139:
4136:
4134:
4133:Recursive set
4131:
4129:
4126:
4124:
4121:
4119:
4116:
4114:
4111:
4107:
4104:
4102:
4099:
4097:
4094:
4092:
4089:
4087:
4084:
4083:
4082:
4079:
4077:
4074:
4072:
4069:
4067:
4064:
4062:
4059:
4057:
4054:
4053:
4051:
4049:
4045:
4039:
4036:
4034:
4031:
4029:
4026:
4024:
4021:
4019:
4016:
4014:
4011:
4009:
4006:
4002:
3999:
3997:
3994:
3992:
3989:
3988:
3987:
3984:
3982:
3979:
3977:
3974:
3972:
3969:
3967:
3964:
3962:
3959:
3955:
3952:
3951:
3950:
3947:
3943:
3942:of arithmetic
3940:
3939:
3938:
3935:
3931:
3928:
3926:
3923:
3921:
3918:
3916:
3913:
3911:
3908:
3907:
3906:
3903:
3899:
3896:
3894:
3891:
3890:
3889:
3886:
3885:
3883:
3881:
3877:
3871:
3868:
3866:
3863:
3861:
3858:
3856:
3853:
3850:
3849:from ZFC
3846:
3843:
3841:
3838:
3832:
3829:
3828:
3827:
3824:
3822:
3819:
3817:
3814:
3813:
3812:
3809:
3807:
3804:
3802:
3799:
3797:
3794:
3792:
3789:
3787:
3784:
3782:
3779:
3778:
3776:
3774:
3770:
3760:
3759:
3755:
3754:
3749:
3748:non-Euclidean
3746:
3742:
3739:
3737:
3734:
3732:
3731:
3727:
3726:
3724:
3721:
3720:
3718:
3714:
3710:
3707:
3705:
3702:
3701:
3700:
3696:
3692:
3689:
3688:
3687:
3683:
3679:
3676:
3674:
3671:
3669:
3666:
3664:
3661:
3659:
3656:
3654:
3651:
3650:
3648:
3644:
3643:
3641:
3636:
3630:
3625:Example
3622:
3614:
3609:
3608:
3607:
3604:
3602:
3599:
3595:
3592:
3590:
3587:
3585:
3582:
3580:
3577:
3576:
3575:
3572:
3570:
3567:
3565:
3562:
3560:
3557:
3553:
3550:
3548:
3545:
3544:
3543:
3540:
3536:
3533:
3531:
3528:
3526:
3523:
3521:
3518:
3517:
3516:
3513:
3511:
3508:
3504:
3501:
3499:
3496:
3494:
3491:
3490:
3489:
3486:
3482:
3479:
3477:
3474:
3472:
3469:
3467:
3464:
3462:
3459:
3457:
3454:
3453:
3452:
3449:
3447:
3444:
3442:
3439:
3437:
3434:
3430:
3427:
3425:
3422:
3420:
3417:
3415:
3412:
3411:
3410:
3407:
3405:
3402:
3400:
3397:
3395:
3392:
3388:
3385:
3383:
3382:by definition
3380:
3379:
3378:
3375:
3371:
3368:
3367:
3366:
3363:
3361:
3358:
3356:
3353:
3351:
3348:
3346:
3343:
3342:
3339:
3336:
3334:
3330:
3325:
3319:
3315:
3305:
3302:
3300:
3297:
3295:
3292:
3290:
3287:
3285:
3282:
3280:
3277:
3275:
3272:
3270:
3269:Kripke–Platek
3267:
3265:
3262:
3258:
3255:
3253:
3250:
3249:
3248:
3245:
3244:
3242:
3238:
3230:
3227:
3226:
3225:
3222:
3220:
3217:
3213:
3210:
3209:
3208:
3205:
3203:
3200:
3198:
3195:
3193:
3190:
3188:
3185:
3182:
3178:
3174:
3171:
3167:
3164:
3162:
3159:
3157:
3154:
3153:
3152:
3148:
3145:
3144:
3142:
3140:
3136:
3132:
3124:
3121:
3119:
3116:
3114:
3113:constructible
3111:
3110:
3109:
3106:
3104:
3101:
3099:
3096:
3094:
3091:
3089:
3086:
3084:
3081:
3079:
3076:
3074:
3071:
3069:
3066:
3064:
3061:
3059:
3056:
3054:
3051:
3049:
3046:
3045:
3043:
3041:
3036:
3028:
3025:
3023:
3020:
3018:
3015:
3013:
3010:
3008:
3005:
3003:
3000:
2999:
2997:
2993:
2990:
2988:
2985:
2984:
2983:
2980:
2978:
2975:
2973:
2970:
2968:
2965:
2963:
2959:
2955:
2953:
2950:
2946:
2943:
2942:
2941:
2938:
2937:
2934:
2931:
2929:
2925:
2915:
2912:
2910:
2907:
2905:
2902:
2900:
2897:
2895:
2892:
2890:
2887:
2883:
2880:
2879:
2878:
2875:
2871:
2866:
2865:
2864:
2861:
2860:
2858:
2856:
2852:
2844:
2841:
2839:
2836:
2834:
2831:
2830:
2829:
2826:
2824:
2821:
2819:
2816:
2814:
2811:
2809:
2806:
2804:
2801:
2799:
2796:
2795:
2793:
2791:
2790:Propositional
2787:
2781:
2778:
2776:
2773:
2771:
2768:
2766:
2763:
2761:
2758:
2756:
2753:
2749:
2746:
2745:
2744:
2741:
2739:
2736:
2734:
2731:
2729:
2726:
2724:
2721:
2719:
2718:Logical truth
2716:
2714:
2711:
2710:
2708:
2706:
2702:
2699:
2697:
2693:
2687:
2684:
2682:
2679:
2677:
2674:
2672:
2669:
2667:
2664:
2662:
2658:
2654:
2650:
2648:
2645:
2643:
2640:
2638:
2634:
2631:
2630:
2628:
2626:
2620:
2615:
2609:
2606:
2604:
2601:
2599:
2596:
2594:
2591:
2589:
2586:
2584:
2581:
2579:
2576:
2574:
2571:
2569:
2566:
2564:
2561:
2559:
2556:
2554:
2551:
2547:
2544:
2543:
2542:
2539:
2538:
2536:
2532:
2528:
2521:
2516:
2514:
2509:
2507:
2502:
2501:
2498:
2488:
2483:
2477:
2474:
2472:
2469:
2467:
2464:
2462:
2459:
2457:
2454:
2452:
2449:
2448:
2446:
2442:
2436:
2433:
2431:
2428:
2426:
2423:
2421:
2418:
2416:
2413:
2412:
2410:
2406:
2400:
2397:
2395:
2392:
2390:
2387:
2385:
2382:
2380:
2377:
2375:
2372:
2370:
2367:
2365:
2362:
2360:
2357:
2356:
2354:
2350:
2342:
2339:
2338:
2337:
2334:
2332:
2329:
2325:
2322:
2321:
2320:
2317:
2315:
2312:
2310:
2307:
2305:
2302:
2300:
2297:
2295:
2292:
2290:
2287:
2285:
2282:
2278:
2275:
2273:
2270:
2268:
2265:
2263:
2260:
2259:
2258:
2255:
2253:
2250:
2249:
2247:
2243:
2237:
2234:
2232:
2229:
2227:
2224:
2222:
2219:
2217:
2214:
2212:
2209:
2205:
2202:
2201:
2200:
2197:
2195:
2192:
2190:
2187:
2185:
2182:
2178:
2175:
2174:
2173:
2170:
2168:
2165:
2163:
2160:
2158:
2155:
2153:
2150:
2148:
2145:
2143:
2140:
2138:
2135:
2133:
2130:
2129:
2127:
2123:
2119:
2112:
2107:
2105:
2100:
2098:
2093:
2092:
2089:
2082:
2078:
2074:
2070:
2067:
2064:
2060:
2057:
2053:
2050:
2047:
2046:Computability
2043:
2042:
2034:
2030:
2026:
2022:
2018:
2014:
2013:
2008:
2002:
1999:
1995:
1989:
1986:
1982:
1976:
1973:
1968:
1966:0-12-238452-0
1962:
1958:
1951:
1948:
1943:
1941:0-12-238452-0
1937:
1933:
1926:
1923:
1916:
1912:
1909:
1907:
1904:
1902:
1899:
1897:
1894:
1892:
1891:Turing degree
1889:
1887:
1884:
1882:
1879:
1877:
1874:
1872:
1869:
1868:
1864:
1862:
1860:
1851:
1849:
1847:
1843:
1839:
1835:
1831:
1824:
1822:
1820:
1816:
1815:
1809:
1805:
1801:
1797:
1793:
1792:
1786:
1784:
1779:
1778:
1772:
1769:. A function
1768:
1765:
1761:
1757:
1749:
1744:
1742:
1740:
1739:David Hilbert
1736:
1732:
1727:
1725:
1721:
1717:
1713:
1710:. The set of
1709:
1704:
1698:
1691:
1683:
1681:
1679:
1675:
1670:
1666:
1662:
1657:
1653:
1649:
1643:
1640:
1632:
1630:
1628:
1627:Kőnig's lemma
1624:
1620:
1601:
1598:
1595:
1589:
1583:
1580:
1577:
1551:
1548:
1545:
1539:
1516:
1513:
1510:
1504:
1484:
1476:
1471:
1469:
1465:
1461:
1453:
1451:
1449:
1444:
1442:
1438:
1435:
1431:
1423:
1421:
1414:
1410:
1407:
1406:
1405:
1403:
1399:
1393:
1385:
1380:
1376:
1372:
1368:
1364:
1360:
1356:
1352:
1348:
1344:
1340:
1336:
1333:
1329:
1325:
1321:
1317:
1313:
1309:
1305:
1301:
1297:
1293:
1289:
1285:
1281:
1277:
1269:
1265:
1261:
1257:
1254:The function
1253:
1252:
1251:
1248:
1244:
1240:
1236:
1232:
1227:
1223:
1219:
1215:
1211:
1207:
1203:
1189:
1186:
1183:
1173:
1172:
1168:
1163:
1159:
1155:
1151:
1143:
1140:The smallest
1139:
1136:
1132:
1129:
1125:
1120:
1113:
1108:
1104:
1097:
1093:
1089:
1085:
1081:
1078:
1075:
1072:
1067:
1063:
1056:
1052:
1048:
1044:
1040:
1037:
1033:
1030:
1026:
1025:
1024:
1018:
1016:
1014:
998:
992:
987:
986:semidecidable
983:
979:
974:
966:
955:
943:
938:
934:
930:
924:
922:
914:
910:
906:
902:
896:
888:
886:
884:
880:
876:
873:Because each
871:
861:
857:
845:
830:
815:
807:
806:
805:
797:
788:
778:
766:
761:
760:semidecidable
757:
753:
748:
728:
705:
693:
688:
684:
680:
666:
664:
662:
659:The field of
653:
650:
648:instructions;
646:
645:
643:
636:
633:
630:
629:
628:
622:
618:
614:
610:
606:
602:
598:
594:
591:
587:
583:
579:
575:
571:
568:
567:
566:
564:
560:
558:
554:
548:
540:
490:
482:
456:
403:
395:
394:
393:
369:
359:
356:
349:
345:
341:
336:
334:
330:
326:
322:
318:
314:
310:
306:
301:
295:
292:
289:
285:
281:
279:
276:
274:
271:
269:
266:
265:
264:
262:
257:
255:
228:
199:
169:
159:
156:
148:
142:
134:
132:
130:
126:
122:
117:
115:
111:
107:
103:
102:exponentially
98:
94:
90:
85:
83:
79:
75:
71:
67:
62:
60:
56:
52:
48:
44:
40:
36:
32:
19:
4235:
4070:
4033:Ultraproduct
3880:Model theory
3845:Independence
3781:Formal proof
3773:Proof theory
3756:
3729:
3686:real numbers
3658:second-order
3569:Substitution
3446:Metalanguage
3387:conservative
3360:Axiom schema
3304:Constructive
3274:Morse–Kelley
3240:Set theories
3219:Aleph number
3212:inaccessible
3118:Grothendieck
3002:intersection
2889:Higher-order
2877:Second-order
2823:Truth tables
2780:Venn diagram
2563:Formal proof
2080:
2076:
2062:
2055:
2045:
2016:
2010:
2007:Péter, Rózsa
2001:
1988:
1980:
1975:
1956:
1950:
1931:
1925:
1855:
1845:
1828:
1818:
1813:
1811:
1807:
1803:
1795:
1790:
1788:
1782:
1781:
1776:
1774:
1770:
1766:
1753:
1728:
1705:
1693:
1677:
1673:
1668:
1664:
1660:
1655:
1651:
1647:
1644:
1636:
1621:on pairs of
1472:
1457:
1445:
1440:
1429:
1427:
1418:
1397:
1395:
1378:
1374:
1370:
1366:
1362:
1358:
1354:
1350:
1346:
1338:
1331:
1327:
1323:
1319:
1315:
1311:
1307:
1303:
1299:
1295:
1291:
1287:
1283:
1279:
1275:
1267:
1263:
1259:
1255:
1249:
1242:
1238:
1234:
1225:
1221:
1217:
1213:
1205:
1170:
1166:
1161:
1157:
1153:
1149:
1147:
1142:prime factor
1118:
1111:
1106:
1102:
1095:
1091:
1087:
1083:
1079:
1070:
1065:
1061:
1054:
1050:
1046:
1042:
1038:
1022:
1012:
996:
990:
985:
981:
977:
975:
964:
953:
941:
936:
932:
928:
925:
920:
912:
908:
898:
882:
878:
872:
859:
855:
843:
834:
795:
776:
764:
759:
755:
751:
749:
726:
703:
691:
686:
682:
678:
670:
658:
641:
626:
620:
616:
612:
608:
604:
600:
596:
589:
585:
581:
577:
573:
561:
550:
337:
307:, which are
302:
298:
288:tag machines
263:, including
258:
144:
118:
96:
92:
86:
63:
30:
29:
4143:Type theory
4091:undecidable
4023:Truth value
3910:equivalence
3589:non-logical
3202:Enumeration
3192:Isomorphism
3139:cardinality
3123:Von Neumann
3088:Ultrafilter
3053:Uncountable
2987:equivalence
2904:Quantifiers
2894:Fixed-point
2863:First-order
2743:Consistency
2728:Proposition
2705:Traditional
2676:Lindström's
2666:Compactness
2608:Type theory
2553:Cardinality
2324:#P-complete
2262:NP-complete
2177:NL-complete
2061:Rogers, H.
1838:Turing jump
1785:-computable
1756:relativized
1716:Busy beaver
1617:w.r.t. the
1434:first order
1424:Provability
1144:of a number
980:(synonyms:
931:(synonyms:
785:is defined
754:(synonyms:
681:(synonyms:
325:composition
121:Blum axioms
97:efficiently
4258:Categories
3954:elementary
3647:arithmetic
3515:Quantifier
3493:functional
3365:Expression
3083:Transitive
3027:identities
3012:complement
2945:hereditary
2928:Set theory
2379:ELEMENTARY
2204:P-complete
2069:Turing, A.
1992:R. Soare,
1917:References
1532:refers to
1361:) for all
1290:such that
1268:at least n
1258:such that
1110:) :=
1069:) :=
1013:enumerable
994:such that
929:computable
796:enumerable
741:is not in
679:computable
333:μ operator
331:, and the
139:See also:
135:Definition
39:algorithms
4225:Supertask
4128:Recursion
4086:decidable
3920:saturated
3898:of models
3821:deductive
3816:axiomatic
3736:Hilbert's
3723:Euclidean
3704:canonical
3627:axiomatic
3559:Signature
3488:Predicate
3377:Extension
3299:Ackermann
3224:Operation
3103:Universal
3093:Recursive
3068:Singleton
3063:Inhabited
3048:Countable
3038:Types of
3022:power set
2992:partition
2909:Predicate
2855:Predicate
2770:Syllogism
2760:Soundness
2733:Inference
2723:Tautology
2625:paradoxes
2374:2-EXPTIME
2033:121107217
2019:: 42–60.
1697:countably
1663:) (where
1314:) = 0 if
1298:) = 1 if
1187:∘
937:decidable
933:recursive
835:If a set
829:injective
687:decidable
683:recursive
553:algorithm
547:Algorithm
375:→
175:→
104:(or even
4210:Logicism
4203:timeline
4179:Concrete
4038:Validity
4008:T-schema
4001:Kripke's
3996:Tarski's
3991:semantic
3981:Strength
3930:submodel
3925:spectrum
3893:function
3741:Tarski's
3730:Elements
3717:geometry
3673:Robinson
3594:variable
3579:function
3552:spectrum
3542:Sentence
3498:variable
3441:Language
3394:Relation
3355:Automata
3345:Alphabet
3329:language
3183:-jection
3161:codomain
3147:Function
3108:Universe
3078:Infinite
2982:Relation
2765:Validity
2755:Argument
2653:theorem,
2369:EXPSPACE
2364:NEXPTIME
2132:DLOGTIME
2071:(1937),
1865:See also
1712:finitary
1642:system.
1082: :
1077:Addition
1041: :
1019:Examples
921:language
909:alphabet
862:(1), ...
563:Enderton
557:compiler
57:and the
45:such as
4152:Related
3949:Diagram
3847: (
3826:Hilbert
3811:Systems
3806:Theorem
3684:of the
3629:systems
3409:Formula
3404:Grammar
3320: (
3264:General
2977:Forcing
2962:Element
2882:Monadic
2657:paradox
2598:Theorem
2534:General
2359:EXPTIME
2267:NP-hard
1567:, then
1231:arg max
1220:), min(
917:{0, 1}
599:-tuple
576:-tuple
3915:finite
3678:Skolem
3631:
3606:Theory
3574:Symbol
3564:String
3547:atomic
3424:ground
3419:closed
3414:atomic
3370:ground
3333:syntax
3229:binary
3156:domain
3073:Finite
2838:finite
2696:Logics
2655:
2603:Theory
2466:NSPACE
2461:DSPACE
2336:PSPACE
2031:
1963:
1938:
1810:being
1800:oracle
1798:as an
1650:calls
1430:proven
1371:exists
1355:entire
1274:, and
1212:, max(
1029:domain
718:is in
671:A set
323:under
321:closed
313:tuples
3905:Model
3653:Peano
3510:Proof
3350:Arity
3279:Naive
3166:image
3098:Fuzzy
3058:Empty
3007:union
2952:Class
2593:Model
2583:Lemma
2541:Axiom
2456:NTIME
2451:DTIME
2272:co-NP
2029:S2CID
1639:sound
1637:In a
1402:above
1375:known
1324:which
1302:<
1210:unary
1034:Each
971:) = 0
960:) = 1
907:. An
858:(0),
733:) = 0
710:) = 1
342:or a
198:tuple
4028:Type
3831:list
3635:list
3612:list
3601:Term
3535:rank
3429:open
3323:list
3135:Maps
3040:sets
2899:Free
2869:list
2619:list
2546:list
2284:TFNP
1961:ISBN
1936:ISBN
1703:}).
1678:this
1590:<
1396:The
1306:and
1152:and
1126:The
1060:,...
919:. A
913:word
881:and
724:and
286:and
119:The
112:and
80:and
3715:of
3697:of
3645:of
3177:Sur
3151:Map
2958:Ur-
2940:Set
2399:ALL
2299:QMA
2289:FNP
2231:APX
2226:BQP
2221:BPP
2211:ZPP
2142:ACC
2021:doi
2017:111
1787:or
1762:of
1760:set
1672:is
1228:),
1208:is
1204:if
1148:If
899:In
735:if
712:if
638:it.
611:at
483:If
396:If
315:of
49:or
4260::
4101:NP
3725::
3719::
3649::
3326:),
3181:Bi
3173:In
2394:RE
2384:PR
2331:IP
2319:#P
2314:PP
2309:⊕P
2304:PH
2294:AM
2257:NP
2252:UP
2236:FP
2216:RP
2194:CC
2189:SC
2184:NC
2172:NL
2167:FL
2162:RL
2157:SL
2147:TC
2137:AC
2075:.
2027:.
2015:.
1726:.
1718:,
1443:.
1381:).
1339:un
1318:≥
1245:)}
1237:≤
1174:,
1169:*
1164:,
1160:+
1133:A
1117:+
1090:,
1086:→
1049:,
1045:→
984:,
935:,
870:.
774:,
758:,
747:.
701:,
685:,
335:.
327:,
290:).
131:.
84:.
76:,
72:,
61:.
4181:/
4096:P
3851:)
3637:)
3633:(
3530:∀
3525:!
3520:∃
3481:=
3476:↔
3471:→
3466:∧
3461:∨
3456:¬
3179:/
3175:/
3149:/
2960:)
2956:(
2843:∞
2833:3
2621:)
2519:e
2512:t
2505:v
2389:R
2199:P
2152:L
2110:e
2103:t
2096:v
2035:.
2023::
1969:.
1944:.
1819:g
1814:g
1808:f
1804:A
1796:A
1791:A
1783:A
1777:A
1771:f
1767:A
1674:n
1669:n
1665:f
1661:n
1659:(
1656:n
1652:f
1648:n
1605:)
1602:y
1599:,
1596:x
1593:(
1587:)
1584:q
1581:,
1578:p
1575:(
1555:)
1552:q
1549:,
1546:p
1543:(
1540:A
1520:)
1517:y
1514:,
1511:x
1508:(
1505:A
1485:A
1379:n
1367:n
1363:n
1359:n
1351:n
1347:n
1332:f
1328:f
1320:k
1316:n
1312:n
1310:(
1308:f
1304:k
1300:n
1296:n
1294:(
1292:f
1288:k
1284:f
1280:n
1278:(
1276:f
1272:π
1264:n
1262:(
1260:f
1256:f
1243:x
1241:(
1239:f
1235:y
1233:{
1226:g
1224:,
1222:f
1218:g
1216:,
1214:f
1206:f
1190:g
1184:f
1171:g
1167:f
1162:g
1158:f
1154:g
1150:f
1122:2
1119:n
1115:1
1112:n
1107:2
1103:n
1101:,
1099:1
1096:n
1094:(
1092:f
1088:N
1084:N
1080:f
1073:.
1071:n
1066:k
1062:n
1058:1
1055:n
1053:(
1051:f
1047:N
1043:N
1039:f
1008:w
1003:)
1001:w
999:(
997:f
991:f
969:w
967:(
965:f
958:w
956:(
954:f
948:w
942:f
867:B
860:f
856:f
850:B
844:f
838:B
831:.
824:B
818:B
810:B
801:B
791:n
783:)
781:n
779:(
777:f
771:n
765:f
744:A
738:n
731:n
729:(
727:f
721:A
715:n
708:n
706:(
704:f
698:n
692:f
674:A
621:x
619:(
617:f
613:x
609:f
605:f
601:x
597:k
590:x
588:(
586:f
582:f
578:x
574:k
536:.
523:x
502:)
498:x
494:(
491:f
468:)
464:x
460:(
457:f
436:x
415:)
411:x
407:(
404:f
379:N
370:k
365:N
360::
357:f
240:)
236:x
232:(
229:f
208:x
196:-
194:k
179:N
170:k
165:N
160::
157:f
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.