How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Primitive recursive functions by initial functions and schemes
Definition
For each arity , primitive recursive functions are total maps given by finite derivation trees from the following rules. The empty tuple is the unique element of .
The initial functions are zero (in every arity), successor , and projections for . Composition forms from an -ary and -ary ; gives the constant value of . Primitive recursion forms the -ary function from a -ary and a -ary . In particular is allowed. This finite-tree definition is the least arity-indexed class closed under the rules: every closed class contains the value of each tree, by induction on the tree's finite depth.
A predicate is primitive recursive when its characteristic function, with true represented by and false by , is primitive recursive. This is a definition by the displayed schemes, not by computability or unbounded search.
Facts & Assumptions
Given: Initial functions and the two schemes above, on the naturals of The natural numbers (von Neumann). No choice axiom is assumed.
Recursion on naturals with an initial point in a set and a total successor operation has a unique total solution (The recursion theorem).
Verification
For total , fix . On set and . Recursion produces a unique sequence . Its first coordinate is : it is zero initially and increments at each step. Its second coordinate therefore satisfies exactly the two equations defining .
If another function satisfied those equations, its pairs would be the same unique recursion solution. Thus each parameter tuple and each have exactly one value. Define the parameterized graph by that unique-solution property inside ; this is not a choice of solutions from possibly many witnesses. Composition of total functions is total, and the initial functions are total. Applying these observations successively at the finitely many nodes of a derivation tree proves totality of its denoted function. Empty parameter tuples and nullary constants obey the same construction.
Depends on
Used by
Dependency tree · two levels
8 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Gallier §1.7–§1.8 (recovery edition); local parameter-recursion construction (standard reference, not scraped)