一种具有能行性的算术。它构成如下：(1)基础逻辑系统是命题演算。(2)取原始递归函数的定义等式(参看原始递归函数)作非逻辑公理。(3)不引入量词(全称变元用自由变元替代，存在变元用具体的数替代)。(4)数学归纳公理(模式)，其中归纳公式为无量词公式。