В мире логики есть мост. Он перекинут через пропасть, разделяющую допустимость правила и его выводимость из аксиом. Пока правила обходятся конечным числом посылок, мост крепок — для классической логики всё, что не нарушает истинность, уже содержится в синтаксисе. Но стоит добавить бесконечные посылки, и опоры начинают дрожать. Мост, увы, не всесилен.
Структурная полнота — это свойство логической системы, при котором любое допустимое правило (не добавляющее новых теорем) можно вывести из аксиом. В 1971 году В. Погоржельски ввёл это понятие, и с тех пор оно служит пробным камнем для многих неклассических логик. Интуиционистская логика, например, не структурно полна: существуют правила, сохраняющие истинность на всех моделях Гейтинга, но невыводимые из аксиом. Однако для некоторых её фрагментов — логик Дамметта (LC) и Медведева (ML) — мост удерживает конечный трафик.
Беда приходит, когда разрешают бесконечные множества посылок. Свойство, называемое κ-структурной полнотой (где κ — кардинал, ограничивающий число посылок и переменных), оказывается чрезвычайно хрупким. В новой работе доказано: если конгруэнц-дистрибутивное многообразие конечного типа порождено конечными алгебрами, то для любого κ > ω κ-структурная полнота равносильна табулярности — порождению одной конечной алгеброй. Иными словами, мост выдерживает только тогда, когда вся вселенная помещается в конечную таблицу. Логики LC и ML, чьи классы моделей содержат бесконечные неразложимые алгебры, проваливают этот тест. Допустимое бесконечное правило — например, ограничивающее ω-квазиуравнение — нельзя вывести из конечного базиса.
Техника построения таких контрпримеров изящна: для каждой пары неравных элементов алгебры вводится условие, связывающее их с выделенной парой из монолита. Если алгебра конечна, все условия выполняются, и заключение вынуждено. Для бесконечных же алгебр находится опровергающая оценка. Этот приём обобщает классический метод Янкова и опирается на характеристические κ-квазиуравнения для неразложимых алгебр, играющих роль атомов в структуре многообразия.
Мост логики, как выясняется, — сооружение для конечных миров. Бесконечность, вторгаясь в правила, обрушивает его в пропасть между синтаксисом и семантикой. Открытие это не просто курьёз: оно связывает структурную полноту с глубокими вопросами конечной аксиоматизируемости и разрешимости. В перспективе — аксиоматизация сильно полных фрагментов интуиционистской логики, поиск оптимальных базисов и прояснение той тонкой грани, где финитарные следствия переходят в нефинитарные. Мост уцелеет, только если мы останемся на берегу конечного.
Алгебра Гейтинга порядка ω+2 выглядит как счётная цепь с двумя дополнительными элементами наверху. Этого микроскопического отличия достаточно, чтобы бесконечное правило стало невыводимым.