N-ary functions

[avekens]

Definition ~df-naryf of n-ary (endo)functions NaryF and related theorems. Additional theorems for nullary and unary functions.

To get a definition which supports arbitrary numbers of arguments, mappings from the half-open range of nonnegative integers to the domain of the arguments is used (to be understood as indexed arguments). Alternatively, elements of Cartesian exponentiations ( U ^^ N ) (see ~ df-finxp ) could have been used to represent multiple arguments. However, this concept is not fully developed yet (it is within a mathbox), and it is currently based on ordinal numbers, e.g., ( U ^^ 2o ), instead of integers, e.g., ( U ^^ 2 ), which is not very practical.

This is a preparation for the definition of primitive recursive functions, which is based on n-ary functions (from nonnegative integers into nonnegative integers).

[savask]

This is a preparation for the definition of primitive recursive functions, which is based on n-ary functions (from nonnegative integers into nonnegative integers).

This is very exciting news! Given your recent pull request, you must be planning to show that Ackermann's function isn't primitive recursive. Of course it would be great to have a more general theory of recursive functions, recursively enumerable sets, Turing degrees etc. In my opinion set.mm is already ripe for that.

I have two small comments. First, in the last section "Primitive recursive functions" there are phrases like

The basic primitive recursive functions are given by ... axioms: More complex primitive recursive functions can be obtained by applying the operations given by ... axioms:

What the ellipsis ... is supposed to mean?

Second comment is more general. I noticed that you often quote wikipedia in set.mm sections. In my opinion, this is not always an ideal choice, since wikipedia is generally a bad source for mathematics and more importantly, it is subject to change (for example, links to specific parts of a wikipedia article can stop working if someone edits the original article). Maybe it is best if we try to reference published books in set.mm sections - for computability theory I suggest Soare's "Recursively enumerable sets and degrees" and references therein.

[avekens]

This is a preparation for the definition of primitive recursive functions, which is based on n-ary functions (from nonnegative integers into nonnegative integers).

This is very exciting news! Given your recent pull request, you must be planning to show that Ackermann's function isn't primitive recursive.

That is exactly my intention.

Of course it would be great to have a more general theory of recursive functions, recursively enumerable sets, Turing degrees etc. In my opinion set.mm is already ripe for that.

I'll see if I can go further in this direction, but others are invited to extend set.mm accordingly.

I have two small comments. First, in the last section "Primitive recursive functions" there are phrases like

The basic primitive recursive functions are given by ... axioms: More complex primitive recursive functions can be obtained by applying the operations given by ... axioms:

What the ellipsis ... is supposed to mean?

The ellipses ... are omissons of the text from Wikipedia, which I regard as not helpful.

Second comment is more general. I noticed that you often quote wikipedia in set.mm sections. In my opinion, this is not always an ideal choice, since wikipedia is generally a bad source for mathematics and more importantly, it is subject to change (for example, links to specific parts of a wikipedia article can stop working if someone edits the original article). Maybe it is best if we try to reference published books in set.mm sections - for computability theory I suggest Soare's "Recursively enumerable sets and degrees" and references therein.

Maybe it is not scientific enough, but citing Wikipedia has several advantages: it is open to the public, it is immediately available by clicking the link, and it is often more general than contents in correspondig books (depending on the author). I always provide the date when I took the copy, so the citation is always transparent looking into the history of the Wikipedia article. Since I have not enough time (and opportunity - no direct access to a adequate and fully equipped libraries) for a deeper research in literature, I would like to stick with Wikipedia. Others are welcome to add additial references.