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

Легко видеть, что в В3 формулы вида не могут быть дока­зуемы, так как в В3 не может быть получена формула А, которая принимает значение 1/2 при любом приписывании значений вхо­дящих в нее переменных. Только в этом случае А была бы дока­зуема. Но формулы, вида доказуемы в расширенном исчислении предикатов, в основе которого лежит пропозициональное исчисле­ние В3. Именно в получении доказательств формул вида и за­ключается анализ парадоксов, предложенный .

3.3.1.1. Трехзначные изоморфы С2

Оказывается, В3 имеет еще один изоморф С2. Поскольку, как уже говорилось, оператор есть то имеем также оператор, ко­торый определяется стандартным образом:Теперь оп­ределим внешние связки аналогично тому, как определялись внешние связки в т. е; вместо оператора перед каждой пропозициональной переменной ставится оператор В результате имеем:

Обозначим логику, основанную на этих связках, посредством

Пусть выделенными значениями здесь являются 1 и 1/2.

Легко проверить, что является нормальным трехзначным изоморфом С2. Таким образом, трехзначная логика Бочвара В3 име­ет два нормальных изоморфа классической двузначной логики С2, в которых правило modus ponens сохраняет классическое отноше­ние логического следования. Обратим внимание, что изоморфы и отличаются друг от друга соответственно тем, что вис­тинностное значение 1/2 отождествляется с 0, а в с 1. При таком отождествлении свойства связок остаются классическими, что яв­ляется подтверждением того, что верифицируются аксиомы С2.

Такой путь доказательства "эквивалентности" и С2 был предложен Н. Решером [Rescher 1969]. При этом он отмечает, что содержит фрагмент Таким образом, возникает вопрос о фрагментах, изоморфных С2, в других трехзначных логиках. Про­рыв в этой области был совершен в диплом­ной работе [Комендантский 2000], где посредством компьютерной программы было вычислено, что имеет 18 нормальных изоморфов С2, 2 из которых с одним выделенным значением и 16 с двумя выделенными значениями. Более того, в [Девяткин 2004] вычисле­но, что трехзначная функционально полная логика (например, обогащенная функтором Слупецкого Тр) имеет 264 нормальных изоморфа, 8 из которых с одним выделенным значением и 256 с двумя выделенными значениями. Здесь же рассматривается вопрос о необходимых и достаточных условиях существования в трех­значной логике определенного вида изоморфа С2. См, также [Девяткин 2007; 2009].

Имеет смысл обобщить понятие изоморфа, введенного , а именно считать обобщенным изоморфом некото­рый фрагмент трехзначной логики, в котором верифицируются ак­сиомы С2, но не обязательно правило modus ponens сохраняет клас­сическое отношение логического следования. Примерами таких. изоморфов являютсяс двумя выделенными значениями и с одним выделенным значением.

Именно такие истинностные таблицы были представлены в [Malinowski 1997], где констатируется тот факт, что здесь верифицируются все аксиомы С2, но правило modus ponens не сохраняет классическое отношение логического сле­дования. Заметим, что уже таковой является логика Клини К3 с двумя выде­ленными значениями (см. 3.4.1). Изучению подобных изоморфов, но с одним выделенным значением, посвящена работа Щевяткин 2007].

Интересно, что в [Девяткин, Кар­пенко и Попов 2007] доказано, что логические матрицы для этих логик (с одним или двумя выделенными значениями) являются ха­рактеристическими для С2. Метод доказательства предложен .

Естественно возникает более общий вопрос: при каких условиях произвольные (конечные) истинностные таблицы равны, т. е. имеют одно и то же множество тавтологий? Наверное, впервые эта проблема обсуждается в [Los 1949] и неза­висимо от него в [Kalicki 1950; 1952].

Роль изоморфов С2 еще полностью не изучена. По-видимому, самое интересное в том, что некоторая логика L, содержащая нор­мальный изоморф С2, может быть аксиоматизирована как расши­рение С2 (развитие этой темы см. в разделах б. З и 7.5.3).

3.3.2. Аксиоматизация В3

В итоге можно констатировать, что логика В3 есть объединение внутренних и внешних логических связок. Как это выглядит в ак­сиоматической форме, впервые было показано в [Финн 1971] (расширенный вариант этой статьи см. в [Финн 1974]). Для этого при аксиоматизации В3 вводятся переменные двух сортов. Пусть р, q, r, ... — пропозициональные переменные, принимающие значения из множества— сентенциональные переменные, принимающие значения из множества {1, 0}. Посредством А, В, С, ... обозначаются произвольные фор­мулы из В3, посредством же обозначаются внешние формулы из В3. Исходными связками исчисления В3 являются (в наших обозначениях последняя связка есть .

Так как то системы связок функционально эквивалентны.

Правила вывода:

Rl, Modus ponens.

R2. Обычная подстановка: вместо р подставляется форму­ла В.

R3. Ограниченная подстановка: вместо v подставляется В0.

( В этой же работе дается аксиоматизация логики которая есть расширение В3 посредством добавления к последней связки Слупецкого Тр (см. выше 3.1.1). Заметим, что в отличие от не является функционально полной, поскольку в ней не определима импликация Лукасевича )

Исчисление, эквивалентное В3, построено также в [Pirog-Rzepecka 1973] под названием W. Значительно более простая ак­сиоматизация В3, чем приведенная выше, принадлежит [Ишмуратов 1974]. Эта аксиоматизация упрощена в [Ишмуратов 1981], где В3 положена в основу специальной системы временной логики.

Подчеркнем, что в приведенной выше аксиоматизации Вз ве­рифицируются не все законы классической пропозициональной ло­гики С2, например, не имеет места контрапозиция

Однако, имея в виду, что В3 содержит фрагмент, изо­морфный С2, естественно было бы посредством внешних формул задать аксиоматизацию классической логики С2. Тогда аксиомати­зацию самой Вз можно представить как расширение С2, что и было сделано Р. Григолия и в [Finn and Grigolia 1993]. В качестве исходных связок берутся следующие:

где есть есть и есть Аксиоматизация ис-