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

для произвольных терминов х, у, z. Из исходных комбинаторов по­лучают другие комбинаторы, например В' xyz = x(zy) (= СВ), К' ху = у (= СК), I' ху =ух (= CI). Следующие исходные множества ком­бинаторов {В, С; W, К}, {В', W, К}, и {S, К} являются эквива­лентными и для последнего (а значит и для остальных) доказана комбинаторная полнота, т. е. все другие возможные комбинаторы можно построить из исходных (см. [Сипу and Feys 1958] и [Энгелер 1987]. Оказалось, что между комбинаторами и импликативными формулами существует однозначное соответствие. Главным результатом этого соответствия является следующий важный факт: полное множество исходных комбинаторов опреде­ляет собой импликативный фрагмент интуиционистской пропози­циональной логики

(Уже Гильбертом в 1922 г. была построена логическая система, полу­чившая название «позитивная импликативная логика», которая в каче­стве импликативных формул содержит аксиомы В, С, W, К. Из доказа­тельства М. Вайсберга [Wajsberg 1938] об отделимости импликации в интуи­ционистской логике следует, что система Гильберта есть Для гильбертовского исчисления L отделимость связок имеет место, если для любой доказуе­мой формулы в L существует ее доказательство, которое использует только ак­сиомы для импликации и аксиомы для других логических связок, действитель­но входящих в эту формулу.)

В силу указанного соответствия (оно еще называется изоморфизмом Карри-Ховарда) можно классифициро­вать импликативные логики посредством комбинаторов, и наобо­рот, и, главное, изучать свойств импликативных логик, используя свойства комбинаторов и свойства

λ-исчиления (см. [Bunder 2002]). Однако эта классификация, как и классификация ­нова, не охватывает классической импликативной логики по­скольку нет такого комбинатора, который соответствовал бы зако­ну Пирса и вообще любой неинтуиционистской импликативной формуле. Это объясняет главную цель работы [Gabbay and de Queiroz 1992]: распространить изоморфизм Карри-Ховарда до т. е. сконструировать такой "комбинатор" Р, который соот­ветствовал бы закону Пирса.

Итак, перед нами стоит следующая исходная проблема: найти единое основание для классификации импликативных логик. Пусть есть пропозициональный язык, единственной логической связкой которого является импликация →. Под импликатывной логикой бу­дем понимать множество всех правильно построенных формул, замкнутое относительно правил МР и постановки.

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

Решение проблемы мы видим в построении такой логической кон­струкции, которая позволит из ее элементов конструировать иско­мые импликативные логики. Более того, при применении к самой конструкции простейших операций можно будет получать (порождать) новые логики и даже целые их классы.

В качестве элементарных объектов, из которых будет стро­иться конструкция, возьмем следующие импликативные формулы, которые для удобства будем обозначать посредством соответст­вующих комбинаторов:

Операциями являются два логических правила вывода: modus ponens и подстановка.

Доказуемость формулы А будем обозначать посредством Сами доказательства будем записывать способом, предложенным Я. Лукасевичем в [Lukasiewicz 1929], однако в наших обозначениях. Каждый доказанный тезис будет иметь свой номер и предшест­вующую строку доказательства, которая состоит из двух частей, разделенных звездочкой *. Слева стоит формула (или ее номер), в которую произведена подстановка и которая является большой по­сылкой. Справа указывается малая посылка, которая также может быть получена за счет подстановки. Результат применения МР указывается посредством тире, затем указывается номер новой форму­лы. Например, докажем

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

Теперь самое главное. Основным требованием к элементарным объектам, т. е. к импликативным формулам, будет требование их независимости друг от друга (см, выше раздел 2.3). Легко показать, что формула I не является независимой в приведенном выше ис­ходном множестве объектов, поскольку она доказуема из С, К или W, К. Например,

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

Очевидно, что формулу К нужно как-то ослабить, например, подстановкой в нее других переменных (или их отождествлением). Этим способом можно получить формулу K1:

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

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

Доказательство теоремы состоит из двух частей:

(і) доказательство независимости формул

(іі) доказательство того, чтоесть аксиоматизация

(і). Доказательство независимости производится матрич­ным методом, причем используемые матрицы должны быть нор­мальными в смысле Лукасевича—Тарского (см. выше раздел 4.2), т. е. они должны быть согласованы с правилом МР.

Матрица 1 [Sobocinski 1952]:

Матрица 2 [Anderson andBelnap 1975]:

Матрица 3 [Sobocinski 1952]:

Матрица 4 [Lukasiewicz 1920]:

Матрица 5. [Sobocinski 1952]:

Интересно заметить, что хотя логика является бесконечно-значной [Thomas 1962], тем не менее независимость ее аксиом до­казывается средствами трехзначной логики.

(ii). Надо показать, что Доказательством

является Утверждение 3.[Смирнов 1972].

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

Теперь, в силу доказательства независимости элементов мно­жества мы можем перейти к построению того, что будем называть логической конструкцией. Рассмотрим семейство всех подмножеств этого множества. Как известно, семейство всех подмножеств некоторого конечного множества образует булеву решетку, упорядоченную отношением включения. В нашем случае булева решетка имеет 32 (=25) элементов с единицей Осталь­ные вершины решетки представляют собой подлогики Полу­ченную конечную булеву решетку обозначим посредством и назовем - конструкцией.

Для простоты изображения в качестве нуля решетки возьмем логику IB. В результате имеем следующую 8-элементную решетку импликативных логик:

Система IBCW есть слабая импликация Чёрча R→ [Church 1951]. В силу Утверждений 2 и 3 и того, что K1 есть подстановоч­ный случай Как сообщает А. Прайор [Prior 1962], система IBC (под названием BCI) и ВСК были введены в 1956 г. Более подробно об элементах решетки и вообще об импликативных логиках см. в [Карпенко 1993].

Заметим, что, по-видимому, первая попытка (и не совсем ус­пешная) решеточно упорядочить импликативные логики принад­лежит [More 1964].

Обратим внимание на то, что на данной диаграмме изображена булева решетка подмножеств аксиом относительно включения, но в общем случае не решетка импликативных логик относительно выводимости из аксиом. Например, логика IBC не является пересе­чением множеств теорем, выводимых впоскольку

Но W* является пдстановочным случаем аксиомы W из IBCW. Од­нако W* не выводима из IBC. Последнее следует из свойств матри­цы 6: