Primitive recursive function: Difference between revisions

Revision as of 20:04, 4 January 2025

Revision as of 21:03, 4 January 2025

Line 188:

=== Some common primitive recursive functions ===

The following examples and definitions are from {{harvtxt|Kleene (|1952) |pp. =223–231}}. Many appear with proofs. Most also appear with similar names, either as proofs or as examples, in {{harvtxt|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 number]]s.