Разработал мощные методы доказательства разрешимости и неразрешимости элементарных теорий, доказал разрешимость элементарной теории поля p-адических чисел и элементарной теории дистрибутивных структур с относительными дополнениями и теории фильтров, неразрешимость теории класса конечных симметрических групп и других теорий. 

Является создателем общей теории нумераций, являющейся методологической базой для исследования алгоритмических проблем математики, имеющей непосредственную связь с методологическими и теоретическими вопросами программирования. 

Получил основополагающие результаты по теории конструктивных структур. 

Его работы по теории рекурсии на допустимых множествах явились основой для разработки новой концепции программирования — концепции семантического программирования. 

Является одним из авторов нового подхода к обоснованию математики, развивающего и модифицирующего программу Гильберта.