ключається термін, який в цьому рядку є суб'єктом, і термін, який є запереченням суб'єкта. Ці результати заносяться в третю колонку таблиці. Таким чином, з можливих кандидатів у коректні гіпотези відразу ж виключаються судження типу X В® X і X В®. Перше судження стверджує, що кожне безліч включено в самого себе, що є аксіомою, а друге увазі елементарну колізію парадоксу і тому не є коректним.
У четвертій колонці відтворюються запису третьої колонки, але при цьому з правої частини цих записів виключаються предикати, що утворюють у сукупності з суб'єктом судження, зворотні тим, які містяться в CT-замиканні. Наприклад, у другій рядку із запису B В® (A,,) ми виключили з правої частини термін A, так як його присутність увазі, що нам доведеться перевіряти судження B В® A, хоча в CT-замиканні мається зворотне йому судження A В® B. Як вже відомо, суміщення прямого і зворотного судження в одній E-структурі призводить до появи елементарного циклу між двома літералами.
У результаті виявляється, що належить перевірити 12 елементарних суджень - по два судження в кожному рядку. Розглянемо як приклад перший рядок A В® (,), в якій містяться два елементарних судження A В® і A В®. Спочатку відтворимо діаграму Хассе нашої вихідної системи (рис. 3) і додамо до цієї системи першими перевіряються судження (Рис. 4). Тепер досить подивитися на малюнок, щоб переконатися, що нова система містить колізію парадоксу A В®, оскільки з A є шлях в. Той же результат ми отримаємо, якщо у вихідну систему додати другу проверяемое судження (рис. 5).
В
Рис. 3 Рис. 4 Рис. 5
При перевірці всіх інших елементарних суджень з четвертої колонки нашої таблиці виявляється, що всі вони ініціюють колізію парадоксу. Таким чином, в вихідну систему неможливо додати яку-небудь посилку, що містить тільки базові терміни, щоб при цьому не виникало ніяких колізій. Системи з такою властивістю ми надалі будемо називати насиченими системами. При цьому "Насиченість" системи не означає, що в неї взагалі не можна нічого додавати. Як було показано раніше, до зазначених систем можна додавати без колізій скільки завгодно екзистенціальних суджень.
Перевірку коректності гіпотези, яка містить тільки базові літерали, можна спростити, якщо скористатися співвідношенням, вираженим наступною теоремою. Але спочатку необхідно визначити ще одну операцію (інверсію), яка часто використовується в E-структурах.
інверсії (Inv (S)) довільного безлічі S літералів є безліч літералів таке, що кожному ЛІТЕРАЛЬ LiГЋS ставиться у відповідність літерал ГЋ Inv (S). p> Іншими словами, для виконання інверсії в безлічі літералів ми замість кожного литерала з цієї множини записуємо його доповнення. Так, якщо S = {A,, C}, то Inv (S) = {, B,}. Інверсія володіє деякими цікавими властивостями. У Зокрема, неважко перевірити, що при дворазовому застосуванні інверсії до певного безлічі літералів буде отримано те ж саме безліч, тобто Inv (Inv (S)) = S. p> Теорема. Нова базова судження A В® B є коректною гіпотезою в коректній E-структурі G, якщо спільно дотримуються дві рівності:
AÑÇBD = Æ;
AÑÇInv (BD) = Æ.
Доказ. Припустимо, що AÑÇBD В№ Г†. Це означає, що існує деякий літерал W, який одночасно належить і AГ‘, і BD. Звідси випливає, що W є попередником литерала A і нащадком литерала B. Тому, коли літерали A і B з'єднуються дугою A В® B (тобто ми додаємо гіпотезу в структуру), то виходить, що через літерали A і B існує шлях з W в W, що означає колізію циклу. Таким чином, необхідність умови (i) доведена. Припустимо, що AÑÇInv (BD) В№ Г†. Це означає, що існує літерал W, такий, що W є попередником A, а - нащадком литерала B. Тоді при додаванні гіпотези A В® B в структуру з'являється шлях з W в, що означає колізію парадоксу. Таким чином, необхідність умови (ii) доведена. Кінець докази. p> З доведення теореми ясно, що в структурі є колізія циклу в тому випадку, коли не дотримується умова (i), а колізія парадоксу, - коли дотримується умова (ii). p> Розглянемо, як можна використовувати теорему 5 для вирішення попередньої задачі. Припустимо, нам треба перевірити коректність гіпотези B В®. Будуємо для цих літералів відповідні конуси:
BГ‘ = {A, B}; D = {,,}; Inv (D) = {A, B, C}.
Перевіряємо умови теореми 5: BÑÇD = Г†; BÑÇ Inv (D) = {A, B}.
Звідси випливає, що при додаванні гіпотези B В® в структуру колізії циклу не утворюється, зате з'являється колізія парадоксу.
Перевірка насиченості навіть простої системи є досить трудомістким заняттям і тут доцільно скористатися обчислювальними можливостями комп'ютера. Однак маються класи E-структур, насиченість яких легко розпізнається без нудного перебору. До цього класу належать, зокрема, всі E-структури, у яких діаграма Хассе містить дві не перетинаються один з одним максимальні ланцюга, тобто шляху, початком яких є мінімальні елементи структури. Наприклад,...
