原始帰納的算術
PRAは形式化において論理記号は不要である - PRAの文は2つの項の間の等号だけであると考えることができる。この設定において項は0またはそれ以上の変数からなる原始帰納的関数である。1941年ハスケル・カリーはそのような体系を与えた。 カリーの体系において帰納法の規則は自然な方法では表現できない。この部分を洗練させたのはグッドスタインである。 グッドスタインの体系において帰納法は次のように表現される:
F ( 0 ) = G ( 0 ) F ( S ( x ) ) = H ( x , F ( x ) ) G ( S ( x ) ) = H ( x , G ( x ) ) F ( x ) = G ( x ) . {\displaystyle {F(0)=G(0)\quad F(S(x))=H(x,F(x))\quad G(S(x))=H(x,G(x)) \over F(x)=G(x)}.}
ここで x は変数、S は後者演算、F, G, H は原始帰納的関数であり、ここに明示した以外の変数を含んでいてもよい。グッドスタインの体系の残る規則は次の代入規則である:
F ( x ) = G ( x ) F ( A ) = G ( A ) A = B F ( A ) = F ( B ) A = B A = C B = C . {\displaystyle {F(x)=G(x) \over F(A)=G(A)}\qquad {A=B \over F(A)=F(B)}\qquad {A=B\quad A=C \over B=C}.}
ここで A, B, C は任意の項(0またはそれ以上の変数からなる原始帰納的関数)である。