Рекурсивно перечислимые теории, не имеющие алгоритмически разрешимой аксиоматизации

У. Крейг в 1953 г. доказал, что для классической логики рекурсивная перечислимость теории (дедуктивно замкнутого множества формул) равносильна возможности задать эту теорию алгоритмически разрешимым множеством аксиом. Эта теорема Крейга верна также для многих неклассических логик: достаточно, чтобы для каждой формулы существовала эквивалентная ей в данной логике формула сколь угодно большого размера. В докладе будет предъявлен нетривиальный пример логики, для которой теорема Крейга неверна — а именно, исчисление Ламбека с бесконечным множеством переменных. Будет также показано, что теорема Крейга сохраняет силу для фрагментов исчисления Ламбека с конечными множествами переменных, а также для варианта исчисления Ламбека, допускающего пустые левые части секвенций.