Введение

правила вывода в логических системах

В логике правило вывода считается допустимым в формальной системе, если добавление этого правила к существующим правилам системы не изменяет множество теорем системы. Иными словами, любая формула, которая может быть выведена с использованием этого правила, уже выводима и без него, и, следовательно, в определенном смысле является избыточной. Понятие допустимого правила было введено Полом Лоренценом в 1955 году.

Основания допустимых правил

Пусть L – логика. Множество R допустимых правил L называется основой допустимых правил, если каждое допустимое правило Γ/B может быть выведено из R и выводимых правил L, используя подстановку, композицию и ослабление. Иными словами, R является основой тогда и только тогда, когда является наименьшим структурным отношением следствия, включающим и R.

Обратите внимание, что децидируемость допустимых правил децидируемой логики эквивалентна существованию рекурсивных (или рекурсивно перечисляемых) основ: с одной стороны, множество всех допустимых правил является рекурсивной основой, если допустимость децидируема. С другой стороны, множество допустимых правил всегда является ко-рекурсивно перечисляемым, и если у нас есть рекурсивно перечисляемая основа, то множество допустимых правил также является рекурсивно перечисляемым; следовательно, оно децидируемо. (Иными словами, мы можем решить допустимость A/B следующим алгоритмом: мы начинаем параллельно два исчерпывающих поиска, один для подстановки σ, которая унифицирует A, но не B, и один для вывода A/B из R и один из поисков должен в конечном итоге дать ответ.) Помимо децидируемости, явные основы допустимых правил полезны для некоторых приложений, например, в сложности доказательств. Для данной логики мы можем спросить, имеет ли она рекурсивную или конечную основу допустимых правил, и предоставить явную основу. Если логика не имеет конечной основы, она тем не менее может иметь независимую основу: основу R, такую, что никакое собственное подмножество R не является основой. В целом, очень мало можно сказать о существовании основ с желательными свойствами. Например, в то время как табличные логики, как правило, хорошо себя ведут и всегда конечно аксиоматизируемы, существуют табличные модальные логики без конечной или независимой основы правил. Конечные основы относительно редки: даже основные транзитивные логики IPC, K4, S4, GL, Grz не имеют конечной основы допустимых правил, хотя они имеют независимые основы.

Структурная полнота

Хотя общая классификация структурно полных логик – непростая задача, мы хорошо понимаем некоторые частные случаи. Сама интуиционистская логика структурно неполна, но её фрагменты могут вести себя по-разному. В частности, любое правило, не содержащее дизъюнкций, или правило, не содержащее импликаций, допустимое в суперинтуиционистской логике, является доказуемым. С другой стороны, правило Минца допустимо в интуиционистской логике, но не доказуемо и содержит только импликации и дизъюнкции. Мы знаем максимальные структурно неполные транзитивные логики. Логика называется наследственно структурно полной, если любое её расширение структурно полно. Например, классическая логика, а также логики LC и Grz.3, упомянутые выше, являются наследственно структурно полными. Полное описание наследственно структурно полных суперинтуиционистских и транзитивных модальных логик было дано соответственно Циткиным и Рыбаковым. А именно, суперинтуиционистская логика является наследственно структурно полной тогда и только тогда, когда она не является валидной ни в одной из пяти фреймов Крипке, но при этом включена в структурно неполную логику KC.