Meta tags:
Headings (most frequently used words):
functions, primitive, recursive, predicate, definition, to, and, or, equal, operations, on, numbers, function, contents, examples, relationship, limitations, variants, finitism, consistency, results, history, see, also, notes, references, recursiveness, of, vector, valued, addition, doubling, multiplication, predecessor, truncated, subtraction, converting, predicates, numeric, is, zero, less, greater, if, then, else, junctors, equality, other, natural, integers, rational, some, common, constant, iterative, pure, recursion, additional, forms, computer, language,
Text of the page (most frequently used words):
the (255), displaystyle (183), #recursive (140), #primitive (123), operatorname (121), function (108), and (105), functions (90), that (78), def (54), for (53), add (47), are (44), text (43), circ (41), can (38), edit (35), theory (33), pred (33), not (32), this (31), leq (31), aligned (30), rho (30), with (26), then (26), from (23), all (22), definition (22), ldots (22), iszero (22), recursion (21), predicate (21), number (21), ary (21), total (21), set (20), case (20), logic (19), loop (19), which (19), defined (19), such (18), rsub (18), begin (17), end (17), mul (16), computable (15), numbers (15), argument (15), one (15), value (14), proof (14), true (14), example (14), language (14), natural (13), gödel (13), also (13), where (13), every (13), geq (13), isbn (12), some (12), sub (12), operations (11), there (11), turing (10), truth (10), arithmetic (10), logical (10), its (10), obtained (10), returns (10), operator (10), arguments (10), property (10), else (10), was (9), mathematical (9), theorem (9), list (9), first (9), many (9), consistency (9), but (9), definitions (9), may (8), computation (8), general (8), doi (8), unary (8), known (8), less (8), pra (8), define (8), given (8), addition (8), dots (8), wikipedia (7), using (7), mathematics (7), complexity (7), rule (7), formal (7), constant (7), 1967 (7), press (7), only (7), initial (7), called (7), proofs (7), than (7), input (7), loops (7), these (7), subtraction (7), successor (7), examples (7), predicates (7), non (6), computability (6), history (6), enumerable (6), tarski (6), finite (6), order (6), valued (6), recursively (6), gladstone (6), see (6), computer (6), used (6), more (6), following (6), other (6), basic (6), values (6), two (6), composition (6), multiplication (6), mathbin (6), dot (6), calculations (6), languages (5), toggle (5), search (5), page (5), calculus (5), model (5), robinson (5), second (5), variable (5), ackermann (5), 1974 (5), university (5), most (5), bounded (5), programming (5), proved (5), results (5), each (5), will (5), forms (5), fact (5), pure (5), way (5), zero (5), partial (5), otherwise (5), predecessor (5), mathbb (5), stackrel (5), mathrm (5), contents (4), additional (4), use (4), articles (4), machine (4), problem (4), complete (4), prime (4), skolem (4), peano (4), propositional (4), axiom (4), enumeration (4), class (4), fixed (4), jstor (4), symbolic (4), vector (4), kleene (4), 978 (4), fachini (4), maggiolo (4), schettini (4), sequence (4), cambridge (4), form (4), here (4), implies (4), similarly (4), steps (4), equals (4), greater (4), main (4), course (4), does (4), have (4), always (4), show (4), enumerated (4), however (4), those (4), once (4), since (4), computed (4), subset (4), they (4), common (4), similar (4), integers (4), equal (4), equations (4), hide (4), move (4), sidebar (4), view (3), unsourced (3), statements (3), 2025 (3), category (3), sets (3), related (3), type (3), theories (3), semantics (3), elementary (3), standard (3), equivalence (3), atomic (3), ordinal (3), systems (3), axioms (3), boolean (3), substitution (3), functional (3), free (3), bound (3), relation (3), foundations (3), power (3), paradox (3), diagonal (3), theorems (3), 2307 (3), severin (3), journal (3), 1947 (3), introduction (3), computational (3), applied (3), current (3), after (3), had (3), what (3), been (3), before (3), finitistic (3), any (3), into (3), syntactic (3), system (3), finitism (3), their (3), while (3), characterization (3), times (3), truncated (3), get (3), possible (3), even (3), iteration (3), namely (3), parameters (3), just (3), identity (3), variants (3), takes (3), explicitly (3), same (3), effectively (3), itself (3), very (3), create (3), limitations (3), provably (3), well (3), sum (3), has (3), equation (3), cases (3), represent (3), false (3), converting (3), rational (3), implements (3), equality (3), junctors (3), part (3), numeric (3), article (3), quad (3), tools (3), subsection (3), table (2), contact (2), about (2), privacy (2), policy (2), terms (2), categories (2), short (2), description (2), different (2), wikidata (2), retrieved (2), index (2), portal (2), abstract (2), lambda (2), undecidable (2), computably (2), church (2), validity (2), schema (2), kripke (2), diagram (2), spectrum (2), models (2), interpretation (2), reverse (2), hilbert (2), axiomatic (2), inference (2), consequence (2), euclidean (2), real (2), sentence (2), ground (2), formula (2), automata (2), constructive (2), von (2), neumann (2), grothendieck (2), new (2), numbering (2), domain (2), cardinality (2), product (2), forcing (2), monadic (2), halting (2), cantor (2), incompleteness (2), information (2), 321 (2), 420992 (2), bulletin (2), soare (2), robert (2), 1987 (2), 2008 (2), american (2), society (2), reprint (2), planetmath (2), 2nd (2), 1989 (2), proceedings (2), vol (2), hartmanis (2), 1971 (2), scheme (2), 2272468 (2), 2270177 (2), emanuela (2), andrea (2), 1982 (2), und (2), 1979 (2), pdf (2), hierarchy (2), brainerd (2), landweber (2), 2002 (2), jeffrey (2), richard (2), burgess (2), boolos (2), george (2), references (2), 1923 (2), van (2), thoralf (2), 107 (2), legacy (2), peter (2), ritchie (2), dennis (2), meyer (2), albert (2), follows (2), time (2), 2011 (2), 332 (2), science (2), notes (2), terminology (2), need (2), were (2), simply (2), construction (2), certain (2), defines (2), unique (2), interest (2), themselves (2), inconsistency (2), formalized (2), closely (2), particularly (2), them (2), halts (2), hand (2), variant (2), unbounded (2), goto (2), operators (2), upper (2), body (2), generality (2), gives (2), run (2), suffices (2), generate (2), include (2), without (2), enough (2), restrictions (2), below (2), considered (2), access (2), iterative (2), citation (2), needed (2), cannot (2), particular (2), uses (2), assumed (2), indeed (2), means (2), would (2), now (2), contradiction (2), converse (2), thus (2), encoded (2), states (2), result (2), equivalent (2), relationship (2), satisfies (2), shall (2), least (2), denotes (2), exists (2), definable (2), meaning (2), logarithm (2), convention (2), item (2), remainder (2), signum (2), factorial (2), exponentiation (2), mark (2), expressed (2), appear (2), above (2), easy (2), defining (2), identification (2), runs (2), over (2), reversed (2), denoted (2), acts (2), doubling (2), suggests (2), choose (2), obtain (2), right (2), projection (2), recursiveness (2), applying (2), rest (2), conditions (2), immutable (2), perform (2), parameter (2), fed (2), previous (2), appearance (2), upload (2), file (2), changes (2), links (2), read (2), log (2), account (2), donate (2), menu (2), topic, mobile, cookie, statement, statistics, developers, code, conduct, legal, safety, contacts, disclaimers, available, under, apply, site, you, agree, registered, trademark, profit, organization, wikimedia, foundation, inc, creative, commons, attribution, sharealike, license, rendered, parsoid, last, edited, august, 2026, utc, hidden, july, january, mappings, https, org, php, title, primitive_recursive_function, oldid, 1372483162, supertask, philosophy, object, logicism, timeline, concrete, automated, proving, algebraic, kolmogorov, versus, decidable, decision, thesis, encoding, ultraproduct, transfer, principle, semantic, strength, satisfiability, categorical, submodel, saturated, self, verifying, analysis, impossibility, zfc, independence, deductive, sequent, deduction, principia, mathematica, elements, geometry, minimal, canonical, algebras, axiomatization, term, symbol, string, signature, rank, quantifier, connective, metalanguage, open, closed, grammar, formation, conservative, extension, expression, arity, alphabet, syntax, bernays, naive, morse, kelley, platek, continuum, hypothesis, choice, zermelo, fraenkel, binary, operation, aleph, inaccessible, large, cardinal, isomorphism, schröder, bernstein, jection, sur, image, codomain, map, maps, constructible, universe, universal, fuzzy, ultrafilter, transitive, infinite, singleton, inhabited, empty, uncountable, countable, types, identities, cartesian, complement, union, intersection, partition, extensionality, element, hereditary, quantifiers, point, higher, tables, connectives, algebra, venn, square, opposition, syllogism, soundness, equiconsistency, proposition, tautology, classical, traditional, logics, russell, löwenheim, lindström, compactness, banach, undefinability, completeness, paradoxes, lemma, 1996, 1416870, 284, springer, verlag, 387, 15299, degrees, daniel, 1138, 2467207, 275903221, 2178, jsl, 1230396909, 0603063, arxiv, 1122, raphael, 942, 0022536, 1090, s0002, 9904, 08911, 925, rogers, hartley, 9780262680523, mit, effective, 1952, chapter, 7th, 3757798, oclc, 0444100881, north, holland, publishing, company, metamathematics, stephen, cole, overview, symposia, 1020807, 8218, 0131, juris, simplifications, 665, 0305993, 653, reduction, 508, 0224460, 505, comparing, hierarchies, 445, 1002, malq, 19820282705, 431, zeitschrift, für, mathematische, logik, grundlagen, der, mathematik, 1051, ita, 1979130100491, rairo, informatique, théorique, wiley, 0471095850, 4th, 9780521007580, john, translator, harvard, univ, 302, frege, source, book, 1879, 1931, jean, heijenoort, rod, downey, 2014, 474, 04348, developments, ideas, tourlakis, 2003, 129, 139, 43942, lectures, volume, smith, 2013, 02284, programs, 469, 1145, 800196, 806014, 465, acm, 22nd, national, conference, facts, quickly, growing, former, latter, mertens, stephan, oxford, 287, 9780191620805, nature, moore, cristopher, linz, jones, bartlett, publishers, 9781449615529, 226, 227, 331, 1990, handbook, theoretical, elsevier, 364, 444, 88074, jan, leeuwen, henk, barendregt, tail, call, double, grzegorczyk, coined, 1934, 1928, today, named, him, event, prompted, rename, until, rózsa, péter, proposed, formally, traced, back, 126, his, 1888, work, give, sind, sollen, die, zahlen, dedekind, finitistically, acceptable, establishes, producing, transform, sufficient, condition, ability, formalize, recast, carry, out, corresponding, transformations, satisfying, hypotheses, proves, implication, con, much, weaker, nevertheless, giving, several, contexts, desired, often, purpose, introduced, paper, computing, coincides, adding, makes, world, escher, bach, bloop, douglas, hofstadter, contains, subtract, conditionals, comparison, calculable, neither, nor, modifiable, control, structures, plus, admitted, programmed, exactly, limitation, compared, specified, begins, easier, find, reading, writing, mutual, extend, additionally, further, improvements, prove, improved, combination, another, restriction, induction, still, various, assume, loss, instead, alternative, build, goodstein, sudan, involves, paris, harrington, shows, note, instance, enumerating, encodings, machines, essentially, expressions, atoms, contain, though, occur, composing, generates, infinitely, determined, encode, let, denote, suppose, occurs, evaluator, clearly, determine, being, tend, correspond, our, intuition, must, certainly, intuitively, simplicity, straightforward, seen, provides, sketch, enumerate, largest, constructed, iteratively, repeating, ways, creating, leading, diagonalization, inverses, pairing, important, single, enumerates, provable, within, fewer, broader, introducing, fail, encodes, original, mutually, exclusive, clause, applies, minimization, not_q, substituting, respective, variables, constants, abbreviation, subscripts, requires, base, greatest, length, vanishing, exponents, exponent, 1th, presently, especially, computers, amounts, changing, next, leftover, divide, evenly, mod, divides, absolute, difference, maximum, minimum, proper, decrement, usually, thought, respect, extracting, arithmetical, names, either, depending, exact, derivation, 222, 231, extended, operate, objects, including, rationals, represented, field, numberings, when, primality, testing, lead, appropriate, negation, disjunction, based, obtains, both, conjunction, arbitrary, precisely, iff, achieved, settings, consider, take, inputs, tuples, mix, produce, outputs, accomplished, identifying, manner, identify, made, viewed, tells, whether, characteristic, rid, limited, monus, opposite, rules, reproduces, doubles, rephrased, therefore, compute, appropriately, moreover, reasons, authors, adds, left, pairs, respectively, component, scalar, written, during, side, performs, subsequent, performed, mentioned, earlier, altered, ordinary, complex, postulates, nonnegative, integer, importance, lies, studied, generally, showing, size, hence, devise, shown, section, exponential, division, roughly, speaking, whose, iterations, entering, strict, program, encyclopedia, projects, printable, version, download, print, export, switch, parser, shortened, url, cite, permanent, link, actions, english, talk, українська, српски, srpski, português, nederlands, 한국어, 日本語, italiano, עברית, français, español, deutsch, čeština, català, العربية, top, personal, special, pages, recent, community, learn, help, contribute, random, events, navigation, jump, content,
Text of the page (random words):
ore the addition function can be defined as add ρ p 1 1 s p 2 3 displaystyle operatorname add rho p_ 1 1 s circ p_ 2 3 as a computation example add 1 7 ρ p 1 1 s p 2 3 s 0 7 by def add s s p 2 3 0 add 0 7 7 by case ρ g h s s add 0 7 by def p 2 3 s ρ p 1 1 s p 2 3 0 7 by def add s p 1 1 7 by case ρ g h 0 s 7 by def p 1 1 8 by def s displaystyle begin aligned operatorname add 1 7 rho p_ 1 1 s circ p_ 2 3 s 0 7 text by def operatorname add s s circ p_ 2 3 0 operatorname add 0 7 7 text by case rho g h s s operatorname add 0 7 text by def circ p_ 2 3 s rho p_ 1 1 s circ p_ 2 3 0 7 text by def operatorname add s p_ 1 1 7 text by case rho g h 0 s 7 text by def p_ 1 1 8 text by def s end aligned doubling edit given add displaystyle operatorname add the 1 ary function add p 1 1 p 1 1 displaystyle operatorname add circ p_ 1 1 p_ 1 1 doubles its argument add p 1 1 p 1 1 x add x x x x displaystyle operatorname add circ p_ 1 1 p_ 1 1 x operatorname add x x x x multiplication edit in a similar way as addition multiplication can be defined by mul ρ c 0 1 add p 2 3 p 3 3 displaystyle operatorname mul rho c_ 0 1 operatorname add circ p_ 2 3 p_ 3 3 this reproduces the well known multiplication equations mul 0 y ρ c 0 1 add p 2 3 p 3 3 0 y by def mul c 0 1 y by case ρ g h 0 0 by def c 0 1 displaystyle begin aligned operatorname mul 0 y rho c_ 0 1 operatorname add circ p_ 2 3 p_ 3 3 0 y text by def operatorname mul c_ 0 1 y text by case rho g h 0 0 text by def c_ 0 1 end aligned and mul s x y ρ c 0 1 add p 2 3 p 3 3 s x y by def mul add p 2 3 p 3 3 x mul x y y by case ρ g h s add mul x y y by def p 2 3 p 3 3 mul x y y by property of add displaystyle begin aligned operatorname mul s x y rho c_ 0 1 operatorname add circ p_ 2 3 p_ 3 3 s x y text by def operatorname mul operatorname add circ p_ 2 3 p_ 3 3 x operatorname mul x y y text by case rho g h s operatorname add operatorname mul x y y text by def circ p_ 2 3 p_ 3 3 operatorname mul x y y text by property of operatorname add end aligned predecessor edit the predecessor function acts as the opposite of the successor function and is recursively defined by the rules pred 0 0 displaystyle operatorname pred 0 0 and pred s n n displaystyle operatorname pred s n n a primitive recursive definition is pred ρ c 0 0 p 1 2 displaystyle operatorname pred rho c_ 0 0 p_ 1 2 as a computation example pred 8 ρ c 0 0 p 1 2 s 7 by def pred s p 1 2 7 pred 7 by case ρ g h s 7 by def p 1 2 displaystyle begin aligned operatorname pred 8 rho c_ 0 0 p_ 1 2 s 7 text by def operatorname pred s p_ 1 2 7 operatorname pred 7 text by case rho g h s 7 text by def p_ 1 2 end aligned truncated subtraction edit the limited subtraction function also called monus and denoted displaystyle mathbin dot is definable from the predecessor function it satisfies the equations y 0 y y s x pred y x displaystyle begin aligned y mathbin dot 0 y y mathbin dot s x operatorname pred y mathbin dot x end aligned since the recursion runs over the second argument we begin with a primitive recursive definition of the reversed subtraction rsub y x x y displaystyle operatorname rsub y x x mathbin dot y its recursion then runs over the first argument so its primitive recursive definition can be obtained similar to addition as rsub ρ p 1 1 pred p 2 3 displaystyle operatorname rsub rho p_ 1 1 operatorname pred circ p_ 2 3 to get rid of the reversed argument order then define sub rsub p 2 2 p 1 2 displaystyle operatorname sub operatorname rsub circ p_ 2 2 p_ 1 2 as a computation example sub 8 1 rsub p 2 2 p 1 2 8 1 by def sub rsub 1 8 by def p 2 2 p 1 2 ρ p 1 1 pred p 2 3 s 0 8 by def rsub s pred p 2 3 0 rsub 0 8 8 by case ρ g h s pred rsub 0 8 by def p 2 3 pred ρ p 1 1 pred p 2 3 0 8 by def rsub pred p 1 1 8 by case ρ g h 0 pred 8 by def p 1 1 7 by property of pred displaystyle begin aligned operatorname sub 8 1 operatorname rsub circ p_ 2 2 p_ 1 2 8 1 text by def operatorname sub operatorname rsub 1 8 text by def circ p_ 2 2 p_ 1 2 rho p_ 1 1 operatorname pred circ p_ 2 3 s 0 8 text by def operatorname rsub s operatorname pred circ p_ 2 3 0 operatorname rsub 0 8 8 text by case rho g h s operatorname pred operatorname rsub 0 8 text by def circ p_ 2 3 operatorname pred rho p_ 1 1 operatorname pred circ p_ 2 3 0 8 text by def operatorname rsub operatorname pred p_ 1 1 8 text by case rho g h 0 operatorname pred 8 text by def p_ 1 1 7 text by property of operatorname pred end aligned converting predicates to numeric functions edit in some settings it is natural to consider primitive recursive functions that take as inputs tuples that mix numbers with truth values that is t displaystyle t for true and f displaystyle f for false citation needed or that produce truth values as outputs 8 this can be accomplished by identifying the truth values with numbers in any fixed manner for example it is common to identify the truth value t displaystyle t with the number 1 displaystyle 1 and the truth value f displaystyle f with the number 0 displaystyle 0 once this identification has been made the characteristic function of a set a displaystyle a which always returns 1 displaystyle 1 or 0 displaystyle 0 can be viewed as a predicate that tells whether a number is in the set a displaystyle a such an identification of predicates with numeric functions will be assumed for the remainder of this article predicate is zero edit as an example for a primitive recursive predicate the 1 ary function iszero displaystyle operatorname iszero shall be defined such that iszero x 1 displaystyle operatorname iszero x 1 if x 0 displaystyle x 0 and iszero x 0 displaystyle operatorname iszero x 0 otherwise this can be achieved by defining iszero ρ c 1 0 c 0 2 displaystyle operatorname iszero rho c_ 1 0 c_ 0 2 then iszero 0 ρ c 1 0 c 0 2 0 c 1 0 1 displaystyle operatorname iszero 0 rho c_ 1 0 c_ 0 2 0 c_ 1 0 1 and e g iszero 8 ρ c 1 0 c 0 2 s 7 c 0 2 7 iszero 7 0 displaystyle operatorname iszero 8 rho c_ 1 0 c_ 0 2 s 7 c_ 0 2 7 operatorname iszero 7 0 predicate less or equal edit using the property x y x y 0 displaystyle x leq y iff x mathbin dot y 0 the 2 ary function leq displaystyle operatorname leq can be defined by leq iszero sub displaystyle operatorname leq operatorname iszero circ operatorname sub then leq x y 1 displaystyle operatorname leq x y 1 if x y displaystyle x leq y and leq x y 0 displaystyle operatorname leq x y 0 otherwise as a computation example leq 8 3 iszero sub 8 3 by def leq iszero 5 by property of sub 0 by property of iszero displaystyle begin aligned operatorname leq 8 3 operatorname iszero operatorname sub 8 3 text by def operatorname leq operatorname iszero 5 text by property of operatorname sub 0 text by property of operatorname iszero end aligned predicate greater or equal edit once a definition of leq displaystyle operatorname leq is obtained the converse predicate can be defined as geq leq p 2 2 p 1 2 displaystyle operatorname geq operatorname leq circ p_ 2 2 p_ 1 2 then geq x y leq y x displaystyle operatorname geq x y operatorname leq y x is true more precisely has value 1 if and only if x y displaystyle x geq y if then else edit the 3 ary if then else operator known from programming languages can be defined by if ρ p 2 2 p 3 4 displaystyle operatorname if rho p_ 2 2 p_ 3 4 then for arbitrary x displaystyle x if s x y z ρ p 2 2 p 3 4 s x y z by def if p 3 4 x if x y z y z by case ρ s y by def p 3 4 displaystyle begin aligned operatorname if s x y z rho p_ 2 2 p_ 3 4 s x y z text by def operatorname if p_ 3 4 x operatorname if x y z y z text by case rho s y text by def p_ 3 4 end aligned and if 0 y z ρ p 2 2 p 3 4 0 y z by def if p 2 2 y z by case ρ 0 z by def p 2 2 displaystyle begin aligned operatorname if 0 y z rho p_ 2 2 p_ 3 4 0 y z text by def operatorname if p_ 2 2 y z text by case rho 0 z text by def p_ 2 2 end aligned that is if x y z displaystyle operatorname if x y z returns the then part y displaystyle y if the if part x displaystyle x is true and the else part z displaystyle z otherwise junctors edit based on the if displaystyle operatorname if function it is easy to define logical junctors for example defining and if p 1 2 p 2 2 c 0 2 displaystyle operatorname and operatorname if circ p_ 1 2 p_ 2 2 c_ 0 2 one obtains and x y if x y 0 displaystyle operatorname and x y operatorname if x y 0 that is and x y displaystyle operatorname and x y is true if and only if both x displaystyle x and y displaystyle y are true logical conjunction of x displaystyle x and y displaystyle y similarly or if p 1 2 c 1 2 p 2 2 displaystyle operatorname or operatorname if circ p_ 1 2 c_ 1 2 p_ 2 2 and not if p 1 1 c 0 1 c 1 1 displaystyle operatorname not operatorname if circ p_ 1 1 c_ 0 1 c_ 1 1 lead to appropriate definitions of disjunction and negation or x y if x 1 y displaystyle operatorname or x y operatorname if x 1 y and not x if x 0 1 displaystyle operatorname not x operatorname if x 0 1 equality predicate edit using the above functions leq displaystyle operatorname leq geq displaystyle operatorname geq and and displaystyle operatorname and the definition eq and leq geq displaystyle operatorname eq operatorname and circ operatorname leq operatorname geq implements the equality predicate in fact eq x y and leq x y geq x y displaystyle operatorname eq x y operatorname and operatorname leq x y operatorname geq x y is true if and only if x displaystyle x equals y displaystyle y similarly the definition lt not geq displaystyle operatorname lt operatorname not circ operatorname geq implements the predicate less than and gt not leq displaystyle operatorname gt operatorname not circ operatorname leq implements greater than other operations on natural numbers edit exponentiation and primality testing are primitive recursive given primitive recursive functions e displaystyle e f displaystyle f g displaystyle g and h displaystyle h a function that returns the value of g displaystyle g when e f displaystyle e leq f and the value of h displaystyle h otherwise is primitive recursive operations on integers and rational numbers edit by using gödel numberings the primitive recursive functions can be extended to operate on other objects such as integers and rational numbers if integers are encoded by gödel numbers in a standard way the arithmetic operations including addition subtraction and multiplication are all primitive recursive similarly if the rationals are represented by gödel numbers then the field operations are all primitive recursive some common primitive recursive functions edit the following examples and definitions are from kleene 1974 pp 222 231 many appear with proofs most also appear with similar names either as proofs or as examples in boolos burgess jeffrey 2002 pp 63 70 they add the logarithm lo x y or lg x y depending on the exact derivation in the following the mark e g a is the primitive mark meaning the successor of usually thought of as 1 e g a 1 def a the functions 16 20 and g are of particular interest with respect to converting primitive recursive predicates to and extracting them from their arithmetical form expressed as gödel numbers addition a b multiplication a b exponentiation a b factorial a 0 1 a a a pred a predecessor or decrement if a 0 then a 1 else 0 proper subtraction a b if a b then a b else 0 minimum a 1 a n maximum a 1 a n absolute difference a b def a b b a sg a not signum a if a 0 then 1 else 0 sg a signum a if a 0 then 0 else 1 a b a divides b if b k a for some k then 0 else 1 remainder a b the leftover if b does not divide a evenly also called mod a b a b sg a b kleene s convention was to represent true by 0 and false by 1 presently especially in computers the most common convention is the reverse namely to represent true by 1 and false by 0 which amounts to changing sg into sg here and in the next item a b sg a b pr a a is a prime number pr a def a 1 not exists c 1 c a c a p i the i 1th prime number a i exponent of p i in a the unique x such that p i x a not p i x a lh a the length or number of non vanishing exponents in a lo a b logarithm of a to base b if a b 1 then the greatest x such that b x a else 0 in the following the abbreviation x def x 1 x n subscripts may be applied if the meaning requires a a function φ definable explicitly from functions ψ and constants q 1 q n is primitive recursive in ψ b the finite sum σ y z ψ x y and product π y z ψ x y are primitive recursive in ψ c a predicate p obtained by substituting functions χ 1 χ m for the respective variables of a predicate q is primitive recursive in χ 1 χ m q d the following predicates are primitive recursive in q and r not_q x q or r q x v r x q and r q x r x q implies r q x r x q is equivalent to r q x r x e the following predicates are primitive recursive in the predicate r ey y z r x y where ey y z denotes there exists at least one y that is less than z such that y y z r x y where y y z denotes for all y less than z it is true that μy y z r x y the operator μy y z r x y is a bounded form of the so called minimization or mu operator defined as the least value of y less than z such that r x y is true or z if there is no such value f definition by cases the function defined thus where q 1 q m are mutually exclusive predicates or ψ x shall have the value given by the first clause that applies is primitive recursive in φ 1 q 1 q m φ x φ 1 x if q 1 x is true φ m x if q m x is true φ m 1 x otherwise g if φ satisfies the equation φ y x χ y course φ y x 2 x n x 2 x n then φ is primitive recursive in χ the value course φ y x 2 to n of the course of values function encodes the sequence of values φ 0 x 2 to n φ y 1 x 2 to n of the original function relationship to recursive functions edit the broader class of partial recursive functions is defined by introducing an unbounded search operator the use of this operator may result in a partial function that is a relation which has at most one value for each argument but which may fail to have a value at some arguments see domain an equivalent definition states that a partial recursive function is one that can be computed by a turing machine a total recursive function is a partial recursive function that is defined for every input every primitive recursive function is total recursive but not all total recursive functions are primitive recursive the ackermann function a m n is a well known example of a total recursive function in fact provable total that is not primitive recursive there is a characterization of the primitive recursive functions as a subset of the total recursive functions using the ackermann function this characterization states that a function is primitive recursive if and only if there is a natural number m such that the function can be computed by a turing machine that always halts within a m n or fewer steps where n is the sum of the arguments of the primitive recursive function 9 an important property of the primitive recursive functions is that they are a recursively enumerable subset of the set of...
|
