Слабая конструктивная арифметика второго порядка с извлечением алгоритмов, вычислимых за полиномиальное время

Строится семейство слабых конструктивных теорий, содержащих арифметику и теорию функций натуральных аргументов с натуральными значениями. Функции, являющиеся значениями функциональных переменных, должны удовлетворять следующим условиям: во-первых, каждая такая функция вычислима за время, ограниченное некоторым полиномом от ее аргументов; во-вторых, каждое значение такой функции ограничено некоторым полиномом от соответствующих значений аргументов. Языки теорий содержат функциональные константы для сложения и умножения натуральных чисел и предикатную константу для равенства натуральных чисел. Допустимо и наличие других функциональных и предикатных констант. Требуется, чтобы функции, обозначаемые этими функциональными константами, удовлетворяли вышеупомянутым условиям полиномиальной ограниченности. Из доказательств рассматриваемых теорий алгоритмически извлекаются реализации доказываемых формул с алгоритмами полиномиальной временной сложности (от значений числовых аргументов этих алгоритмов). Если одним из аргументов реализации должна быть функция, то в реализующем алгоритме эта функция используется как оракул. Библ. – 2 назв.