Неарифметичность предикатной логики примитивно рекурсивной реализуемости

Понятие примитивно рекурсивной реализуемости было введено С. Салехи как своего рода семантика для языка базисной арифметики с использованием примитивно рекурсивных функций. Представляет интерес изучение соответствующей логики предикатов. Д. А. Витер доказал, что предикатная логика примитивно рекурсивной реализуемости Салехи не является арифметической. Технически сложное доказательство сочетает в себе методы, использованные автором настоящей статьи при изучении предикатных логик конструктивных арифметических теорий, и результаты М. Ардешира по переводу интуиционистской логики предикатов в базисную логику предикатов. Цель этой статьи — представить другое доказательство результата Витера путем прямого переноса методов, использованных ранее в доказательстве неарифметичности предикатной логики рекурсивной реализуемости.
Библиография: 19 наименований.