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

2. J1-введение:

3. J1-удаление:

4. -введение:где х не входит свободно в Y.

5. -введение: где х не входит свободно в X.

Определение доказательства стандартное. Теорема дедукции.

Пусть Г — совокупность формул, а X — внешняя замкнутая формула. Тогда влечет

6.3.2.2. Семантика

1.0. Определение - структурой, связанной с языком на­зовем тройкугде —ото­бражение Dk в D, — отображение Dт в V, и тип -структуры

(гдеи — арность операции F1, — арность (п+1)-значного предиката Pj) совпадает с типом языка

1.1. Пусть I- интерпретация языка в L, т. е. I- функция, определенная на(где F — множество пропозициональных букв и Р - множество предикатных букв языка такая, что

Пусть также v* - произвольное отображение из множества X всех предметных переменных языкав множе­ство D.

Определим по индукции оценку v, заданную функцией

(с) пусть— оценка, порожденная функцией такой, что

Положим

1.4. Определение. Формулу А языка назовем истинной

довыполненной) на -структуре L при оценке v, если

1.5. Определение. Формулу А языка назовем истинной

(«выполненной) на -структуре L, если для любой оценки

v в этой структуре.

1.6. Определение. Формулу А языка назовем

-выполнимой, если найдется -структура L, такая, что А истинна

1.7. Определение. Формулу А языка назовем

-общезначимой, если для любой -структуры L формула А истинна на L .

1.8. Теорема о корректности. Все формулы, выводимые в

Являются -общезначимыми.

Доказательство. Достаточно проверить общезначимость аксиом

и то, что правила вывода сохраняют общезначимость.

Далее строится секвенциальное исчисление, эквивалентное

тайному, и доказывается теорема о полноте.

6.3.3. Обобщение и другие вопросы

Изложенный здесь метод может быть применен для более широкого класса логик (см. [Аншаков и Рычков 1984]), а именно для логик с сигнатурой

через которую выразима сигнатура

удовлетворяющая указанным выше условиям (1), (2), (3), и теперь для удобства рассматриваются логики сигнатурыТогда

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

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

Общезначимость определяется как и ранее.

Логику Ln можно аксиоматизировать следующим образом: к группе аксиом связи (А) добавляются следующие схемы аксиом

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

В случае же произвольных конечнозначных логик их язык, т. е. сигнатура δ2, расширяется конечным числом «метасимволов», т. е. вводятся добавочные «внешние» связки, которым соответствуют либо операции на множестве {0, 1}, либо J-операторы, вообще го­воря, не выразимые через исходные логические операции. (Имеют­ся также и внешние кванторы.) Полученные в результате примене­ния данного способа исчисления с такой нестандартной семантикой называются исчислениями квазигильбертовского типа и квазисеквенциальными исчислениями. По своим дедуктивным свойствам они близки к обычным ичислениям гильбертовского типа и секвен­циальным исчислениям. Это позволяет стандартным образом раз­вивать для них теорию моделей и теорию доказательств.

Как отмечают авторы, возможность в общем виде развивать теорию моделей для произвольных конечнозначных логик обу­словлена не только дедуктивными свойствами исчислений, но и в не меньшей степени введением в данной работе общего понятия ультрапроизведения Lп - структур. В указанной работе доказываются аналоги теоремы Лося об ультрапроизведениях и теоремы Мальце­ва о компактности.

В [Anshakov and Rychkov 1994] были рассмотрены алгебраические проблемы, связанные с истинностно-полными С-расширяющими логиками Lп. Показано, что каждой такой логике соответствует некоторый класс алгебр, играющий для Ln ту же роль, что играет класс булевых алгебр для классической логики С2. Доказана теорема представления для Lп - алгебр и предложено новое доказательство полноты для пропозициональных истинностно-полных С-расширяющих логик. В [Ambas 2001] показано, что дан­ные логики алгебраизуемы в смысле [Blok and Pigozzi 1989] и для них доказана строгая теорема полноты.

В [Anshakov, Finn and Skvortsov 1989] рассмотрено обобщение истинностно-полных С-расширяющих логик, названное авторами J-определимыми J-компактными логиками, которые могут и не быть конечнозначными. Именно бесконечнозначные J -опреде­лимые J - компактные логики используются для формализации правдоподобных рассуждений в ДСМ-методе автоматического по­рождения гипотез. В [Атиаков 1998] рассматривается алгебраиче­ская проблематика, связанная с такими логиками. Автор переносит результаты из [Anshakov and Rychkov 1994] на класс подобных ло­гик.

6.4. Некоторые размышления

В итоге мы имеем несколько необычный взгляд на суть п-значных логик: каждая конечнозначная логика (предикатная) есть расширение классической логики. Такую аксиоматизацию на­зовем С-аксиоматизацией. Последнее как раз и позволяет дать еди­ный метод (алгоритм) аксиоматизации конечнозначных логик и до­казать целый ряд известных теоретико-модельных теорем, являющихся аналогами теорем для классической логики предика­тов.

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