```Notes on Recursive Number Theory by R. L. Goodstein

I've used an N like language to describe his work here.

Chapter I Definition by Recursion

1. Variables

"
In terms of two operations
1 replacing x by 1+x,
2 replacing x by 0,
we define numerals to be signs constructed from x by the repeated applications
of the operation 1 followed by an application of operation 2.
Starting with the sign x the process of constructing numerals may be regarded
as a process of eliminating x using only the operations 1 and 2.
" RNT Goodstein pg. 13

"
The defining property of a numeral variable x is that it may be replaced by
zero or 1+x .
Any letter may of course serve as a numeral variable, but in this chapter only
the letters x,y, z and w will be used.
By means of variables we can make general statements about numbers, statements
which hold true when any particular numeral is substituted for the variable.
" RNT Goodstein pg. 13

"
the only axioms are explicit and (primitive) recursive function definitions,
and the only inference rules are the substitution schemata

Sb1:
F(x) = G(x)
-----------
F(A) = G(A)

Sb2:
A = B
-----------
F(A) = F(B)

T:
A = B
A = C
-----
B = C

where F(x), G(x) are recursive functions and A,B,C are recursive terms, and the
primitive recursive uniqueness rule

U
F(Sx) = H(x, F(x))
------------------
F(x) = H^x F(0)

where the iterative function H^x t is define by the primitive recursion H^0 t =
t, H^Sx t = H(x, H^x t); in the schema U, F may contain additional parameters
but H is a function of not more than two variables.
In Sb1, the function G(x) may be replaced by a term G independent of x,
provided that G(A) is also replaced by G.

...

the defining equations for these operations to be:

a+0=a , a+Sb=S(a+b);
0-1=0 , Sa-1=a;
a-0=a , a-Sb=(a-b)-1;
a*0=0 , a*Sb=a*b+a
" Goodstein Recursive Number Theory pg. 104 and 106

```