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):
ightforward however the set of primitive recursive functions does not include every possible total computable function this can be seen with a variant of cantor s diagonal argument this argument provides a total computable function that is not primitive recursive a sketch of the proof is as follows the primitive recursive functions of one argument i e unary functions can be computably enumerated this enumeration uses the definitions of the primitive recursive functions which are essentially just expressions with the composition and primitive recursion operations as operators and the basic primitive recursive functions as atoms and can be assumed to contain every definition once even though a same function will occur many times on the list since many definitions define the same function indeed simply composing by the identity function generates infinitely many definitions of any one primitive recursive function this means that the n displaystyle n th definition of a primitive recursive function in this enumeration can be effectively determined from n displaystyle n indeed if one uses some gödel numbering to encode definitions as numbers then this n displaystyle n th definition in the list is computed by a primitive recursive function of n displaystyle n let f n displaystyle f_ n denote the unary primitive recursive function given by this definition now define the evaluator function e v displaystyle ev with two arguments by e v i j f i j displaystyle ev i j f_ i j clearly e v displaystyle ev is total and computable since one can effectively determine the definition of f i displaystyle f_ i and being a primitive recursive function f i displaystyle f_ i is itself total and computable so f i j displaystyle f_ i j is always defined and effectively computable however a diagonal argument will show that the function e v displaystyle ev of two arguments is not primitive recursive suppose e v displaystyle ev were primitive recursive then the unary function g displaystyle g defined by g i s e v i i displaystyle g i s ev i i would also be primitive recursive as it is defined by composition from the successor function and e v displaystyle ev but then g displaystyle g occurs in the enumeration so there is some number n displaystyle n such that g f n displaystyle g f_ n but now g n s e v n n s f n n s g n displaystyle g n s ev n n s f_ n n s g n gives a contradiction this argument can be applied to show that the class of total computable functions cannot be enumerated in this way in particular it shows that total turing machines cannot be enumerated note however that the partial computable functions those that need not be defined for all arguments can be explicitly enumerated for instance by enumerating turing machine encodings other examples of total recursive but not primitive recursive functions are known the function that takes m to ackermann m m is a unary total recursive function that is not primitive recursive the paris harrington theorem involves a total recursive function that is not primitive recursive the sudan function the goodstein function variants edit constant functions edit instead of c n k displaystyle c_ n k alternative definitions use just one 0 ary zero function c 0 0 displaystyle c_ 0 0 as a primitive function that always returns zero and build the constant functions from the zero function the successor function and the composition operator citation needed iterative functions edit robinson 10 considered various restrictions of the recursion rule one is the so called iteration rule where the function h does not have access to the parameters x i in this case we may assume without loss of generality that the function g is just the identity as the general case can be obtained by substitution f 0 x x f s y x h y f y x displaystyle begin aligned f 0 x x f s y x h y f y x end aligned he proved that the class of all primitive recursive functions can still be obtained in this way pure recursion edit another restriction considered by robinson 10 is pure recursion where h does not have access to the induction variable y f 0 x 1 x k g x 1 x k f s y x 1 x k h f y x 1 x k x 1 x k displaystyle begin aligned f 0 x_ 1 ldots x_ k g x_ 1 ldots x_ k f s y x_ 1 ldots x_ k h f y x_ 1 ldots x_ k x_ 1 ldots x_ k end aligned gladstone 11 proved that this rule is enough to generate all primitive recursive functions gladstone 12 improved this so that even the combination of these two restrictions i e the pure iteration rule below is enough f 0 x x f s y x h f y x displaystyle begin aligned f 0 x x f s y x h f y x end aligned further improvements are possible severin 13 prove that even the pure iteration rule without parameters namely f 0 0 f s y h f y displaystyle begin aligned f 0 0 f s y h f y end aligned suffices to generate all unary primitive recursive functions if we extend the set of initial functions with truncated subtraction x y we get all primitive recursive functions if we additionally include as an initial function additional primitive recursive forms edit some additional forms of recursion also define functions that are in fact primitive recursive definitions in these forms may be easier to find or more natural for reading or writing course of values recursion defines primitive recursive functions some forms of mutual recursion also define primitive recursive functions the functions that can be programmed in the loop programming language are exactly the primitive recursive functions this gives a different characterization of the power of these functions the main limitation of the loop language compared to a turing complete language is that in the loop language the number of times that each loop will run is specified before the loop begins to run computer language definition edit an example of a primitive recursive programming language is one that contains basic arithmetic operators e g and or add and subtract conditionals and comparison if then equals less than and bounded loops such as the basic for loop where there is a known or calculable upper bound to all loops for i from 1 to n with neither i nor n modifiable by the loop body no control structures of greater generality such as while loops or if then plus goto are admitted in a primitive recursive language the loop language introduced in a 1967 paper by albert r meyer and dennis m ritchie 14 is such a language its computing power coincides with the primitive recursive functions a variant of the loop language is douglas hofstadter s bloop in gödel escher bach adding unbounded loops while goto makes the language general recursive and turing complete as are all real world computer programming languages the definition of primitive recursive functions implies that their computation halts on every input after a finite number of steps on the other hand the halting problem is undecidable for general recursive functions finitism and consistency results edit the primitive recursive functions are closely related to mathematical finitism and are used in several contexts in mathematical logic where a particularly constructive system is desired primitive recursive arithmetic pra a formal axiom system for the natural numbers and the primitive recursive functions on them is often used for this purpose pra is much weaker than peano arithmetic which is not a finitistic system nevertheless many results in number theory and in proof theory can be proved in pra for example gödel s incompleteness theorem can be formalized into pra giving the following theorem if t is a theory of arithmetic satisfying certain hypotheses with gödel sentence g t then pra proves the implication con t g t similarly many of the syntactic results in proof theory can be proved in pra which implies that there are primitive recursive functions that carry out the corresponding syntactic transformations of proofs in proof theory and set theory there is an interest in finitistic consistency proofs that is consistency proofs that themselves are finitistically acceptable such a proof establishes that the consistency of a theory t implies the consistency of a theory s by producing a primitive recursive function that can transform any proof of an inconsistency from s into a proof of an inconsistency from t one sufficient condition for a consistency proof to be finitistic is the ability to formalize it in pra for example many consistency results in set theory that are obtained by forcing can be recast as syntactic proofs that can be formalized in pra history edit recursive definitions had been used more or less formally in mathematics before but the construction of primitive recursion is traced back to richard dedekind s theorem 126 of his was sind und was sollen die zahlen 1888 this work was the first to give a proof that a certain recursive construction defines a unique function 15 16 17 primitive recursive arithmetic was first proposed by thoralf skolem 18 in 1923 the current terminology was coined by rózsa péter 1934 after ackermann had proved in 1928 that the function which today is named after him was not primitive recursive an event which prompted the need to rename what until then were simply called recursive functions 16 17 see also edit grzegorczyk hierarchy recursion computer science primitive recursive functional double recursion primitive recursive set function primitive recursive ordinal function tail call notes edit brainerd landweber 1974 hartmanis 1989 fachini maggiolo schettini 1979 fachini maggiolo schettini 1982 also known as sequence function 3 4 planetmath e g henk barendregt 1990 functional programming and lambda calculus in jan van leeuwen ed formal models and semantics handbook of theoretical computer science vol b elsevier pp 321 364 isbn 0 444 88074 7 here 2 2 6 initial functions def 2 2 7 primitive recursion p 331 332 kleene 1974 pp 226 227 this follows from the facts that the functions of this form are the most quickly growing primitive recursive functions and that a function is primitive recursive if and only if its time complexity is bounded by a primitive recursive function for the former see linz peter 2011 an introduction to formal languages and automata jones bartlett publishers p 332 isbn 9781449615529 for the latter see moore cristopher mertens stephan 2011 the nature of computation oxford university press p 287 isbn 9780191620805 1 2 robinson 1947 gladstone 1967 gladstone 1971 severin 2008 meyer albert r ritchie dennis m 1967 the complexity of loop programs acm 67 proceedings of the 1967 22nd national conference pp 465 469 doi 10 1145 800196 806014 peter smith 2013 an introduction to gödel s theorems 2nd ed cambridge university press pp 98 99 isbn 978 1 107 02284 3 1 2 george tourlakis 2003 lectures in logic and set theory volume 1 mathematical logic cambridge university press p 129 isbn 978 1 139 43942 8 1 2 rod downey ed 2014 turing s legacy developments from turing s ideas in logic cambridge university press p 474 isbn 978 1 107 04348 0 thoralf skolem 1923 the foundations of elementary arithmetic in jean van heijenoort translator and ed 1967 from frege to gödel a source book in mathematical logic 1879 1931 harvard univ press 302 33 references edit boolos george burgess john jeffrey richard c 2002 computability and logic 4th ed cambridge university press isbn 9780521007580 brainerd w s landweber l h 1974 theory of computation wiley isbn 0471095850 fachini emanuela maggiolo schettini andrea 1979 a hierarchy of primitive recursive sequence functions pdf rairo informatique théorique 13 1 49 67 doi 10 1051 ita 1979130100491 fachini emanuela maggiolo schettini andrea 1982 comparing hierarchies of primitive recursive sequence functions zeitschrift für mathematische logik und grundlagen der mathematik 28 27 32 431 445 doi 10 1002 malq 19820282705 gladstone m d 1967 a reduction of the recursion scheme the journal of symbolic logic 32 4 505 508 doi 10 2307 2270177 jstor 2270177 mr 0224460 gladstone m d 1971 simplifications of the recursion scheme the journal of symbolic logic 36 4 653 665 doi 10 2307 2272468 jstor 2272468 mr 0305993 hartmanis juris 1989 overview of computational complexity theory computational complexity theory proceedings of symposia in applied mathematics vol 38 american mathematical society pp 1 17 isbn 978 0 8218 0131 4 mr 1020807 kleene stephen cole 1974 1952 chapter xi general recursive functions 57 introduction to metamathematics 7th reprint 2nd ed north holland publishing company isbn 0444100881 oclc 3757798 planetmath primitive recursive vector valued function retrieved 2025 07 04 rogers hartley jr 1987 1967 theory of recursive functions and effective computability reprint ed mit press isbn 9780262680523 robinson raphael m 1947 primitive recursive functions bulletin of the american mathematical society 53 10 925 942 doi 10 1090 s0002 9904 1947 08911 4 mr 0022536 severin daniel e 2008 unary primitive recursive functions the journal of symbolic logic 73 4 1122 1138 arxiv cs 0603063 doi 10 2178 jsl 1230396909 jstor 275903221 mr 2467207 soare robert i 1987 recursively enumerable sets and degrees springer verlag isbn 0 387 15299 7 soare robert i 1996 computability and recursion the bulletin of symbolic logic 2 3 284 321 doi 10 2307 420992 jstor 420992 mr 1416870 v t e mathematical logic general axiom list cardinality first order logic formal proof formal semantics foundations of mathematics information theory lemma logical consequence model theorem theory type theory theorems list paradoxes gödel s completeness incompleteness theorems tarski s undefinability banach tarski paradox cantor s theorem paradox diagonal argument compactness halting problem lindström s löwenheim skolem russell s paradox logics traditional classical logic logical truth tautology proposition inference logical equivalence consistency equiconsistency argument soundness validity syllogism square of opposition venn diagram propositional boolean algebra boolean functions logical connectives propositional calculus propositional formula truth tables many valued logic 3 finite predicate first order list second order monadic higher order fixed point free quantifiers predicate monadic predicate calculus set theory set hereditary class ur element ordinal number extensionality forcing relation equivalence partition set operations intersection union complement cartesian product power set identities types of sets countable uncountable empty inhabited singleton finite infinite transitive ultrafilter recursive fuzzy universal universe constructible grothendieck von neumann maps cardinality function map domain codomain image in sur bi jection schröder bernstein theorem isomorphism gödel numbering enumeration large cardinal inaccessible aleph number operation binary theories zermelo fraenkel axiom of choice continuum hypothesis general kripke platek morse kelley naive new foundations tarski grothendieck von neumann bernays gödel ackermann constructive formal systems list language syntax alphabet arity automata a...
|
