On first order logic of proofs

Логика доказательств LP решила давно стоявшую проблему Гёделя, касающуюся его доказуемостного исчисления (см. [1]). Она также открыла новые направления исследования в теории доказательств, модальной логике, языках программирования с типами, в представлении знаний и т.п. Пропозициональная логика доказательств разрешима и аксиоматизируема. В данной работе мы показываем, что логика доказательств первого порядка не является рекурсивно аксиоматизируемой.