Секвенциальный вариант арифметической системы Р. Робинсона, не содержащий правил типа сечения

Строится секвенциальный вариант арифметической системы Р. Робинсона, не содержащий правил типа сечения, в том числе и правил типа сечения, вводящих специфические аксиомы теории (имеется в виду, что аксиомы теории не записываются в антецедент доказываемой формулы). Доказательство равнообъемности построенного исчисления с арифметической системой Р. Робинсона таково, что из него вытекает новое доказательство непротиворечивости системы Робинсона. В качестве промежуточного исчисления строится секвенциальный вариант арифметической системы Р. Робинсона, содержащий лишь одно правило типа сечения (соответствующее специфической аксиоме $\forall x(x=0\vee\exists y(x=y'))$). Доказывается ряд теорем о специализации формы вывода в промежуточном исчислении.
Библ. 8 назв.