```Notes on Recursive Analysis by R. L. Goodstein

"
Recursive analysis is a free variable theory of functions in a rational field,
founded on recursive arithmetic.
It involves no logical presuppositions and proceeds from definition to theory
by means of derivation schemata alone.

The elementary formulae of recursive arithmetic are equations between terms,
and the class of formulae is constructed from the elementary formulae by the
operations of propositional calculus.
The terms are the free numeral variables, the sign 0 and the signs for
functions.
The function signs include the sign S(x) for the successor function (so that
S(x) plays the part of x+1 in elementary algebra) and signs for functions
introduced by recursion.
The derivation rules are taken to be sufficient to establish the universally
valid sentences of the propositional calculus, and include a schema permitting
the substitution of terms for variables, the schema of equality

a = b -> {A(a) -> A(b)},

and the induction schema

A(0), A(n) -> A(S(n))
---------------------
A(n)

the schemata for explicit definition of functions for any number of arguments,
and finally schemata for definition by recursion.
The simplest definition schema for recursion, the schema of primitive
recursion, is

f(0, a) = g(a), f(S(n), a) = h(n, a, f(n, a))

Specifically this schema defines f(n, a) by primitive recursion from the
functions g and h.
We take as initial primitive recursive functions the successor function S(x),
the identity function I(x), defined explicitly by the equation I(x)=x, and the
zero function Z(x) defined by Z(x)=0.
A function is said to be primitive recursive if it is an initial function or is
defined from primitive recursion functions by substitution or by primitive
recursion.
" Goodstein Recursive Analysis Chapter 1 Section 1 pg. 1 and 2
```