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

который сам не содержит отрицания, но для вывода которого су­щественным образом используется аксиома 9, т. е. позитивный фрагмент совпадает с позитивным фрагментом Int, который обозначим посредствомТогда аксиоматизациейявляется

(аксиомы 1-8 в аксиоматизации Клини) и добавляются аксио­мы:

Единственным правилом вывода является МР.

Интересно, что Д. Батено [Batens 1980] формулирует паранепротиворечивую систему PI следующим образом. Берется позитивный фрагмент классической логики, т. е. плюс закон Пирса, и добавляется только одна аксиома с отри­цанием:

Из логикиполучается трехзначная PCont посредством до­бавления к первой закона Пирса, законов Де Моргана, выразимости импликации через другие связки и (см. выше раздел 3.5.2).

Логикане является финитно тривиализируемой, т. е. добав­ление к ней произвольной недоказуемой формулы не влечет выво­димости противоречия, как это доказал Н. да Коста. Заметим, что в не имеет места закон линейности

Интересно принципиальное различие между паранепротиворечивыми логиками J иВ J, хотя закон Дунса Скотта не имеет места, но выводим его следующий аналог:

Заметим также, что для как и для J, имеется семантика Крипке (см. [Baaz 1986]).

8.6.2. Иерархия параиепротиворечивых систем Сп

На самом деле Н. да Коста строит линейно-упорядоченную иерар­хию систем Сп (в том числе и предикатных). Аксиоматизация про­извольной Сп выглядит следующим образом.

Для пусть А0 — сокращение формулы Ап —

сокращениедля А0 , повторенного п раз, а А(п) есть формула

Аксиоматизация каждой Сп получается в результате добавления к схемам аксиом для следующих формул:

А. Арруда показала [Arruda 1975], что ни одно из этих исчис­лений не имеет конечной характеристической матрицы, а в [Fidel 1977] показано, что логики Сп разрешимы.

Также установлено, что каждая Сп строго слабее, чем ее пред­шественник, т. е. пусть Th(S) обозначает множество теорем исчис­ления S. Тогда

В отличие от не является пересечением множества теорем в соответствующей последовательности логик, в данном случае в иерархии Сп. Отыскание такой дедуктивной гра­ницы, т. е. является открытой проблемой по сей день (см. [Carnielli and Marcos 1999]).

Особый интерес представляет логика С1, поскольку ею опреде­ляются все основные свойства логик в иерархии Сп. Именно с нее начинается изложение PL в [Da Costa 1974]. Она аксиоматизирует­ся следующим образом: к аксиомам системы добавляются

Заметим, что в трехзначной паранепротиворечивой логике Сетте Р1 (см. выше раздел 3.5.4) верифицируются все аксиомы для C1.

В [Da Costa and Ginllaume 1965] выяснилось, что в С1 выводим закон Пирса, значит она и все Сп содержат позитивный фрагмент классической логики, и все они конечно-тривиализируемы.

8.6.3. Неистинностно-функциональная семантика для паранепротиворечивых логик

В общем случае интерпретация логики PL есть отображение (оцен­ка) v из множества формул пропозиционального языка PL в мно­жество {0,1}, удовлетворяющее следующим требованиям:

Случай с импликацией зависит от свойств последней и если она классическая, как в С1 и PI, то

Главный пункт построения семантики для PL — это определе­ние условий истинности для отрицания ~, поскольку для того, что­бы не выполнялась выводимость мы могли бы выбрать оценку v такую, которая приписывает р и ~р значение 1 (и их конъюнкции), в то время как q приписывается значение 0. Это можно достигнуть различными способами. Вот некоторые их них:

Условие (1) определяет свойства отрицания в системе Д. Батенса PI, а условия (1) и (2) определяют отрицание в ( Этой системе двойственна логика Ж.-И. Безье (J-Y. Beziau), в которой отрица­ние обладает только свойством

Заметим, что вместе (1) и (1') определяют классическое отрицание.)

Для того чтобы получить подобную семантику для С1 (с которой опять

же начинается статья [Da Costa and Alves 1977], где предложена семантика для систем Сп), надо добавить еще два условия:

Логическая истинность определяется обычным образом: т. т.т., когда для всех оценок

В этом же году была построена семантика и для логики что потребовало некоторого усложнения в силу свойств импликации в этой системе (см. [Loparic 1986]).

Обратим внимание, что свойства отрицания весьма необычны в рассмотренных паранепротиворечивых логиках, поскольку ис­тинностные условия для ~А не определяются истинностными условиями А (если v(A) = 1, то v(~A) может быть 1 или 0). Такой под-ход к отрицанию называется неистинностно-функциональным, и семантика такого рода является неистинностно-функционалъной и получила название семантики оценок. На этой семантике мы оста­новимся более подробно в разделе 10.5, а здесь рассмотрим неко­торые проблемы, связанные с такой семантикой, для PL.

8.6.3.1. Неалгебраизуемость С1

Покажем, что в С1 закон Дунса Скота доказуем из следующих двух рссиом (см., например, [Hunter 1998]):

Эти аксиомы проходят во всех рассмотренных нами системах PL. Если же взять хотя бы ослабленный вариант контрапозиции, который не имеет места в PL, то получим закон Дунса Скота:

Но отсутствие контрапозиции ведет к весьма нежелательным

поледствиям. В общем случае оказывается неприменимым правило эквивалентной замены (см. выше раздел 3.5.3 в связи с трехзначной паранепротиворечивой логикой J3). Например, как отмечается в [Priest 2002], хотя А логически эквивалентно нет гарантии, что отрицания этих формул при данной интерпретации имеют одно и то же истинностное значение. В общем случае, мо­жет случиться так, что но Не­медленным следствием этого является то, что логическая эквива­лентность не является конгруэнцией на алгебре формул, т. е. мы не можем построить алгебру Линденбаума.

Этот результат для системы C1 (и, следовательно, для всех Сп) впервые был получен в [Mortensen 1980], а с появлением аппарата алгебраизуемости логик строго обоснован в [Lewin, Mikenberg and Schwarze 1991].

Долгое время такое свойство PL не давало покоя алгебраистам и вообще ставило под сомнение использование отрицания, т. е. ста­вило вопрос, является ли отрицание отрицанием в PL? Но в самое последнее время появились настолько сильные обобщения метода Блока-Пигоцци (см. выше раздел 4.5), что этот новый аппарат стал применяться к PL и, в частности, к логикам Н, даКосты (см. [Caleiro, Congalves and Martins 2009]).