Дискретно-непрерывная математика (стр. 114 )

Ими, например, было показано, что

и Х2 доказуема в ВСКХ3.

Поскольку доказать независимость аксиомы I от Х3 не удавалось, то Х3 была заменена на

(Заметим, что только в [Комендантский 2001] с помощью прувера OTTER была доказана выводимость закона тождества I из )

Теорема 4, Множество формул является незави-

симой аксиоматизацией

(і). Независимость доказывается теми же самыми матри­цами, что и для множества аксиом (Теорема 2). (іі).

Утверждение 10.

.

(Доказано вместе с . Впервые Утверждение 10 (в виде было доказано в [Slaney and Bunder 1994] с помощью компьютерной программы. В этой же работе отдельно доказывется Утверждение Как и в первом случае, приведена только довольно-таки непростая схема доказательства. Заметим, что в нашем доказательстве сначала доказывается а затем за один шаг из D и W получаем Р.)

Таким образом, теорема 4 доказана.

Особый интерес представляют подлогики

Утверждение 11. есть

Напомним (см. выше раздел 8.5.3.1), есть [Meyer and Parks 1972]. Матрица 5 с матрицей для инволюции ~ (отрицание Лукасевича) являются характеристическими для импликативно-негативного фрагмента RM [Parks 1972]. Поскольку формула Х4 общезначима здесь, то в силу отделимости импликации в [Meyer and Parks 1972] формула X4 доказуема вТеперь надо показать, что формулы В', I' и Х3 доказуемы в Первая и вторая формулы доказываются Утверждениями 4 и 1 со­ответственно. Х3 получается из Х4 по правилу МР.

Утверждение 12. есть

Поскольку есть а есть(см. вы-

ше), то в [Карпенко и Попов 1997] доказано, что

Таким образом, найдена новая аксиоматизация

(В [Карпенко 2000] с помощью компьютерной программы MaGIC (см. [Slaney and Meglicki 1991]) была доказана также независимость аксиом В, С, К иХ3. )

Теперь представим решетку с аксиомой Х4:

Все логики, указанные на вершинах этой решетки (кроме BCІХ4), являются импликативными логиками, лежащими в основе наиболее фундаментальных логических систем. Из результата А. Аврона [Avron 1984] следует, что является единственным собственным расширением Отсюда следует ответ на вопрос (2) Дж. Слэни и М. Бундера (см. выше) относительно наиболее сильной системы Таковой как раз и является система В силу этого, приведенная решетка была названа макси­мальной [Karpenko 1998]. Обратим внимание на то, что если между нет промежуточных импликативных логик, то между их счетное множество [Komori 1978], а между '. и их континуум [Верхозина 1986].

Имеется также частичный положительный ответ и на первый вопрос. Для этого введем следующие определения. Следуя [Pahi 1971; 1972], пусть α и β обозначают произвольные правильно по­строенные формулы, α называется переменно-подобной {variable-like), если и только если никакая пропозициональная переменная не входит в α больше одного раза. Если β есть результат подстановки в формулутакой, что каждая βі является

переменно-подобной и для не имеют общих пропози-

циональных переменныхтогда формула β называется

ограниченным подстановочным случаем (о. п.с.) формулы α. Напрмер, формула K1 есть о. п.с. формулы К. Из [Pahi 1971] (см. также [Pahi 1972]) следует, что если α* есть любая импликативная фор­мула, которая является о. п.с. α, тогда определяют эквивалентные системы. А это значит, что любое ослабление, кото­рое есть о. п.с. формул X1 — Х4, опять же есть искомая формула X.

Рассмотрим для примера формулу

которя есть о. п.с. формулы Используя Теорему 1,

можно показать, чтоесть В итоге мы име-

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

Обратим внимание на статью [Ernst 2002], где предложено де­вять формул, выполняющих роль нашего X, например, под номе­ром 5 выступает формула

Установлены некоторые взаимоотношения между этими фор­мулами. Также показано (с помощью Компьютерной программы), что

5. Решетка импликативных логик логики

А как быть с импликацией в логике следования Е и с импликацией в льюисовских модальных логиках S4 и S5?

Рассмотрим следующие импликативные формулы:

Правила вывода: МР и подстановка,

Формулы А, В', W представляют собой импликативный фраг­мент Е→ логики следования Е (см. [Anderson and Belnap 1975]). Здесь же показано, что В [Mendez 1988] показано, что есть импликативный фрагментмодальной логики S4. Наконец,есть импликативный фрагмент модальной логики S5. Обычно аксиоматизируется как

где P1 есть ослабленный закон Пирса:

Покажем, что

В [Ulrich 1990] предложена следующая характеристическая матрица для Множеством значений является множество нату­ральных чисел: 1, 2, 3, ... с 0. Единственным выделенным зна­чением является 1. Импликацияопределяется так: если х есть кратное у, ив остальных случаях. Нетрудно вычислить, что Х2 общезначима в этой матрице, т. е. Х2 есть теорема Остается показать, что из выводима формула P1: ,