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

Развитие этой темы см. в самом конце этой главы, где будет представлена оригинальная решетка импликативных расширений логики (см. [Томова 2010]).

3.5.2.2. Решетка паралогик

В указанной работе [Avron 1991] вводится важное понятие базис­ной логики: это весь позитивный фрагмент классической логики С2, плюс законы де Моргана и аксиомы Впервые аксиоматизация этой логики появилась в [Попов 1989], где она обозначена посредством Par (см. ниже раздел 5.4.4.3). Ес­ли теперь добавить то получим в точности аксиоматизацию PCont, предложенную Батенсом-Розоноэром (см. выше). Если же добавитьто получим аксиоматизацию трехзначной

логики с импликацией →1 (см. выше раздел 3.1.1), которая функ­ционально эквивалентна логике Лукасевича

(3 По предложению эту логику обозначим посредством РСотр, по­скольку эта логика в данной формулировке является дуальной к PCont и по­этому называется параполной, О понятии парагголноты см. в разделе 3.5.4.1.)

Если же добавим одновременно обе эти формулы, продолжает А. Аврон, то получим аксиоматизацию классической логики С2. Из [Попов 2009] следует, что Par является одновременно паранепротиворечивой и параполной логикой. Здесь показано, что Par можно расширить законом Клини Эту логику обозначим посредством PNorm, которая также является одновременно паранепротиво­речивой и параполной.

( В [Попов 2009] эта логика обозначается посредством PContPComp. В диплом­ной работе (2010 г.) показано, что характеристической матри­цей для этой логики является девятизначная матрица, полученная посредством умножения матрицы для PCont на матрицу для Рсотр)

В [Знаменская и Попов 2009] показано, что

Понятно, что если добавить к PNorm то получим PCont, если же добавить то полу-

чим РСотр. Все эти логики, кроме С2, назовем паралогиками. Тогда решетка Попова выглядит следующим образом:

Более того, других логик между Par и С2 нет [Попов 2009] (!)

3.5.3. Логика J3

Еще одна весьма известная паранепротиворечивая логика была предложена в [D'Ottaviano and da Costa 1970] со следующими связ­ками: и обозначена как J3. Как уже известно, логика с та-

кими связками функционально эквивалентна логике Лукасевича т. е. в ней выразима импликация Лукасевича → (см.3.1.2). Но J3, в отличие отберется с двумя выделенными значениями. Подоб­ная логика была нами обозначена как (см. 3.4.1). Поэтому, на­пример, в J3 формула тавтология, а в нет.

J3 совпадает с системой CLuNs (см. [Batens 1989] и с системой LFI1 (см. Carnielly, Marcos and de Amo 2000) и совпадает с системой введенной гораздо ранее в [Schiitte I960].

В дальнейшем в качестве исходной связки к J3 добавляется связка Заметим, что Напомним, что логика со

связками есть К3, логика со связками есть PCont. Та-

ким образом, логика J3 есть расширение PCont посредством добав­ления связки или, по-другому, логика J3 есть расширение PCont посредством добавления константы 1 (или 0). Предикатную фор­мулировку J3 (и теорию моделей) можно найти в [D 'Ottaviano 1985; 1987].

Обратим внимание на работу [D'Ottaviano and Epstein 1988] (см. также [Epstein 1990]), где приводится аксиоматизация J3 как расширение классической логики С2. В качестве исходных свя­зок взяты есть отрицание Гейтинга (см. 3.2). По­скольку то исходная система связок J3

D-эквивалентна связкам изЗаметим, что посредством связок и верифицируется С2. В выразима связка Холдена(см. 3.3.1.1), которую мы обозначили посредством Тогда аксиомати­зация J3 выглядит следующим образом.

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

Заметим, что здесь, как и во всех паранепротиворечивых логи­ках, правило эквивалентной замены (см. выше: если то не имеет места и в силу этого для таких логик нельзя построить алгебру Линденбаума (см. раздел 8.6,3.1). На-пример, в но если р принимает значение 1, а q значение '/2.

3.5.4. Логики Р1 и Р2

Кроме требования Яськовского о неверифицируемости в паране-противоречивой логике закона Дунса Скота существует еще до­полнительное требование да Косты о неверифицируемости закона непротиворечия в виде [da Costa 1974]. Следующие две

логики как раз с таким свойством.

А. Сетте [Sette 1973] строит логическое исчисление Р1, которое получается из классического пропозиционального исчисления С2 в формулировке посредством замены аксиомы (9)

на аксиому

Эта логика оказалась трехзначной с двумя выделенными зна­чениями, а связкиесть не что иное, как (см. выше раздел 3.3.1.1).

Сетте показал, что логические связки выразимы

посредством

где не есть, соответственно, тiп и max.

Впервые истинностные таблицы для таких логических связок появились в [da Costa 1963], где использовались для опровержения некоторых тавтологий С2, которые не имеют места в паранепроти-воречивой логике да Косты С1 (см. ниже раздел 8.6.2). Эти же ис­тинностные таблицы появились в [da Costa and Alves 1981], где со­ответствующая логика была обозначена посредством F; она же независимым образом была обнаружена С. Мортенсеном в 1979 г., который обозначил ее посредством (см. [Mortensen 1989]).

Имеются различные аксиоматизации Р1 с исходными связками Наиболее простой является следующая [Sette and Alves, 1996]:

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

(В [Marcos 2005] приведена аксиоматизация Р1 как расширение аксиоматизации последовательности бесконечнозначных паранепротиворечивых логик да Косты Сп (см. ниже гл. 8.6.1).

Добавим также, что в [Popov 1998] появляется аксиоматизация Р1 под названием I1, которая получается из трехзначной паранепро-тиворечивой логики V1 (см. [Arruda 1977]), если в ней останутся только так называемые "переменные Васильева".

Отметим некоторые свойства Р1:

1) Исчисление Р1 как и PCont является максимальным [Sette 1973];