26 марта 2016г.
32 Исследование выполнено при поддержке РГНФ, грант № 13-03-00088а.
В статье описан метод построения аналитико-табличных аксиоматизаций I-логик васильевского типа. Предлагаемые аксиоматизации удобны в применении и предназначены для организации машинного поиска вывода.
В [1] для произвольных x и y из {0, 1, 2,…ω }введена в рассмотрение логика I . Согласно определению, данному в [2], I-логикой васильевского типа называется любая такая логика I , что x или y не равно 0. Заметим, что I< 0,0> является (см. [1] ) классической пропозициональной логикой. Вызывает интерес, что I-логики васильевского типа были открыты в ходе работы с логическим наследием отечественного логика и философа Николая Александровича Васильева и являются паралогиками, позволяющими эксплицировать некоторые логические идеи последнего. В предлагаемой работе описан метод построения по любым x и y из {0, 1, 2,…ω } аналитико-табличной аксиоматизации логики I. Разумеется, что такого рода метод позволяет построить аналитико-табличную аксиоматизацию для всякой I-логики васильевского типа. Аналитико- табличные исчисления, получаемые согласно этому методу, имеют простые правила и удобны для поиска вывода.
Язык L, являющийся языком всех рассматриваемых здесь логик, есть стандартно определяемый пропозициональный язык, алфавиту которого принадлежат только следующие символы: p1, p2, p3,
…(пропозициональные переменные языка L), &, Ú, É (бинарные логические связки языка L), Ø (унарная
логическая связка языка L), левая и правая круглые скобки. Принимаем обычные соглашения об опускании скобок в L - формулах и используем «формула» как сокращение для « L- формула». Следуя [1], квазиэлементарной формулой называем формулу, в которую не входит ни одна бинарная логическая связка языка
L. Длиной формулы называем, как это принято, число всех вхождений логических связок в эту формулу. Условимся, что α и β являются произвольными фиксированными числами из {0, 1, 2,…ω }. Воспроизведем данное в [1] определение исчисления HI< α,β> . Исчисление HI< α,β> является исчислением гильбертовского типа, язык которого есть L. Правило модус поненс в L – единственное правило этого исчисления. Выводы в этом исчислении (в частности, доказательства в этом исчислении) строятся обычным для гильбертовского типа исчислений образом.
Теорема. Для всякой формулы А верно: формула А доказуема в HI< α,β> тогда и только тогда, когда существует замкнутая аналитическая TI<α,β>-таблица, начальная конфигурация которой есть {{FA}}.
Список литературы
1. Попов В.М. Секвенциальная аксиоматизация логики I // Восьмые смирновские чтения: материалы Международной научной конференции, Москва, 19-21 июня 2013г. М.: Современные тетради, 2013.С. 27- 29.
2. Попов В.М. Секвенциальная аксиоматизация и семантика I-логик васильевского типа // Логические исследования. №22 (в печати).
3. Fitting M. C. Intuitionistic logic model theory and Forcing. Nath-Holl. Publishing company, Ams-London, 1969.
