Теорема Ербрана

Теорема Ербрана — фундаментальний результат математичної логіки, отриманий Жаком Ербраном в 1930 р. Суть теореми у тому, що вона гарантує формальну виводимість (довідність) формули елементарної (першопорядкової) логіки з аксіом, якщо методом Ербрана можна показати загальзначимість цієї формули в т. зв. ербрановському універсумі, що представляє із себе суто синтаксичну (ефективно породжувану) конструкцію. При цьому в основі методу Ербрана лежать ідея непрямого доказу й ідея зведення формули логіки предикатів у скулемовській нормальній формі (можливо, з функціональними символами) до деякого окремого випадку (до пропозиційної формули в канонічній формі), який дозволив би зробити висновок про загальнозначимість вихідної формули. В результаті такої процедури переходу «від часткового до загального» проблема доказовості (виводимості) в деякій першопорядковій системі аксіом зводиться до проблеми загальнозначимості в логіці висловлювань. Видатне значення роботи Ербрана стало очевидним, по-перше, у світлі пізніших теорем Черча і Шеннона про алгоритмічну нерозв'язність проблеми розвязності (загальнозначимості в будь-якому універсумі) для формул елементарної логіки, а по-друге, у світлі алгоритмічних задач в області штучного інтелекту, які спираються на логіку. Досі метод Ербрана служить основою для більшості сучасних автоматичних алгоритмів пошуку доведень.

Попереджувальна форма

У логіці Ербрана формула є попереджувальною якщо у ній всі квантори існування та загальності знаходяться на початку формули. Кожна формула еквівалентна формулі попередження. Наприклад, формула $(\exists x\;P(x))\to (\exists y\;Q(y))$ еквівалентна формулі $\lnot (\exists x\;P(x))\lor (\exists y\;Q(y))$ , $\forall x\;\lnot P(x)\lor \exists y\;Q(y)$ , і нарешті $\forall x\;\exists y\;\lnot P(x)\lor Q(y)$ (де $\to ,\lnot ,\lor ,\land$ означають імплікацію, заперечення, диз'юнкцію, кон'юнкцію. P та Q одномісні предикати).

Попереджувальна формула є універсальною, якщо вона містить тільки квантори загальності (тобто символ: $\forall$ ). Можна пов'язати будь-яку формулу з еквівалентною, отриману перетворенням Сколема, введенням нових функціональних символів для кожного квантора існування (тобто символ: $\exists$ ). Наприклад сколемівська форма з $\forall x\;\exists y\;(\lnot P(x)\lor Q(y))$ і $\forall x\;\lnot P(x)\lor Q(f(x))$ . Інтуїтивно, якщо для кожного x, існує такий y для якого виконується умова R(x,y) то ми можемо ввести функцію f(x) = y таку, що для всіх x виконується R(x,f(x)). Показано, що початкова формула допускає моделі тоді і тільки тоді, якщо вона допускає сколемівську форму. Іншими словами, вихідна формула здійсненна тоді і тільки тоді коли формула сколемівська.

Теорема Ербрана

Розглянемо універсальну формулу $F$ (або набір формул), наприклад типу $\forall x,\forall y,P(x,y)$ , де $P$ це предикат, а набір змінних $a_{1},a_{2},...,a_{n},...$ . Розглянемо наступні три властивості :

$F$ є послідовною, тобто можна зробити висновок, протиріччя з припущенням $\lnot F$ не доводиться в системі числення предикатів, таких як природного виводу, наприклад ми бачимо: $\not \vdash \lnot F$ .
$F$ є виконуваною, тобто існує модель, в якій $F$ правильною : $\not \vDash \lnot F$ .
Для будь-якого $n$ , існує модель, в якій наступна формула, яку ми позначимо $Q(a_{1},...,a_{n})$ є правильною:

$P(a_{1},a_{1})\land P(a_{1},a_{2})\land P(a_{2},a_{1})\land P(a_{2},a_{2})\land \cdots P(a_{1},a_{n})\land \cdots P(a_{n-1},a_{n})\land P(a_{n},a_{1})\land \cdots P(a_{n},a_{n})$ для усіх $n$ , $\not \vDash \lnot Q(a_{1},...,a_{n})$

Теорема Геделя про повноту заявляє про еквівалентність між 1) і 2). Крім того, 2) результат 3) модель, в якій 2) перевіряється на моделях для отримання перевірки 3). Теорема Ербрана стверджує, що, навпаки, 3) призводить до 2), коли $a_{i}$ описують конкретні області, область Ербрана. Зазначимо, що у формулюванні 3), квантори загальності зникли з формули, і для доведення формули стають просто пропозиціями числення висловів.

Тобто постановка $G=\lnot F$ і $R=\lnot Q$ , отримані з трьох властивостей :

$G$ доказова, тобто це демонстрація $G$ у системі дедукції числення предикатів, де ми бачимо : $\vdash G$ .
$G$ є дійсною, тобто $G$ є істинною в будь-якої моделі, де ми бачимо : $\vDash G$ .
Існує ціле $n$ для яких $R(a_{1},...,a_{n})$ є дійсним : $\vDash R(a_{1},...,a_{n})$

$G$ є теоремою.

Якщо $F$ нездійсненне (що має місце тоді і тільки тоді коли $G=\lnot F$ є теоремою), то доказовість $Q(a_{1},...,a_{n})$ для $n=1$ , або $n=2$ , і так далі, до будь-якого додатнього цілого $n$ як $Q(a_{1},...,a_{n})$ є хибним, і навпаки.

До негативних моментів слід віднести те, що якщо $F$ є виконувана (і тому якщо $G$ не є теоремою), то для усіх $n$ , $Q(a_{1},...,a_{n})$ буде вірною, і процес обчислення не закінчиться, крім особливих випадків, коли змінна $a_{i}$ є кінцевою.

Це ілюструє той факт, що всі формули є нездійсненними, або теореми всіх множин є перелічуваними, але в численні предикатів не розв'язні.

Приклади

Область Ербранових моделей є визначеною принаймні на сталих елементах (крім нульових) і складається з усіх термів, які можуть бути утворені з констант і функцій, розглядаються у формулах. Визначення моделі Ербрана в атрибутах деяких предикатів визначається на цих термах.

Приклад 1 : Розглянемо формулу $F=\forall x,P(x)\land \lnot P(a)$ , де $a$ є константою. Область Ербрана складається з одиничних $\{a\}$ . Потім сформуємо формулу $Q_{1}=P(a)\land \lnot P(a)$ яка є помилковою, так як $F$ нездійсненна.

Приклад 2 : Розглянемо формулу $F=\forall x,(P(x)\lor Q(x))\land \lnot P(a)\land \lnot Q(b)$ . Областю Ербрана є $\{a,b\}$ . Сформуємо потім $Q_{1}=(P(a)\lor Q(a))\land \lnot P(a)\land \lnot Q(b)$ яка є вірно на моделі де ми використовуємо вірне значення $Q(a)$ , і сформуємо $Q_{2}=Q_{1}\land (P(b)\lor Q(b))\land \lnot P(a)\land \lnot Q(b)$ що вірно в моделі, де ми використовуємо справжнє значення $\{Q(a),P(b)\}$ . Перерахувавши область Ербрану, алгоритм закінчується і $F$ здійсненна в заздалегідь заданій моделі.

Приклад 3 : Розглянемо формулу $F=\forall x,\forall y,P(x)\land \lnot P(f(y))$ . Областю Ербрана є $\{a,f(a),f^{2}(a),...,f^{n}(a),...\}$ . Створимо потім $Q_{1}=P(a)\land \lnot P(f(a))$ модель, якої має правильне значення, якщо ми напишемо $P(a)$ але невірне $P(f(a))$ Потім для елементів $a$ та $P(a)$ створимо $Q_{2}=P(a)\land \lnot P(f(a))\land P(a)\land \lnot P(f(f(a)))\land P(f(a))\land \lnot P(f(a))\land P(f(a))\land \lnot P(f(f(a)))$ ка не може мати модель через неправдиві поєднання $P(f(a))\land \lnot P(f(a))$ . Тому $F$ не має моделі.

Приклад 4 : Розглянемо формулу $G=(\exists x,\forall y,P(x,y))\to (\forall y,\exists x,P(x,y))$ яку ми хочемо довести як теорему. Після перейменування змінних x і y другій частині G на інші змінні, отримуємо еквівалентну форму представлення G: :

(\exists x,\forall y,P(x,y))\to (\forall z,\exists t,P(t,z))

\lnot (\exists x,\forall y,P(x,y))\lor (\forall z,\exists t,P(t,z))

(\forall x,\exists y,\lnot P(x,y))\lor (\forall z,\exists t,P(t,z))

\forall x,\exists y,\forall z,\exists t,\lnot P(x,y)\lor P(t,z)

Попереджувальною формою $F$ еквівалентна до $\lnot G$ є:

\exists x,\forall y,\exists z,\forall t,P(x,y)\land \lnot P(t,z)

і сколемівською формою є :

\forall y,\forall t,P(a,y)\land \lnot P(t,f(y))

Будова формули $Q_{1}$ для змінних $(y,t)$ та $(a,a)$ або $Q_{2}$ для змінних $(y,t)=(f(a),a)$ приводить до $P(a,a)\land \lnot P(a,f(a))\land P(a,f(a))\land \lnot P(a,f(f(a)))$ що неправильно в будь-якій моделі. $F$ не є виконуваною $G$ є теоремою.

Приклад 5 : Розглянемо формулу $G=(\forall x,\exists y,P(x,y))\to (\exists y,\forall x,P(x,y))$ . За аналогічний процес як в попередньому прикладі, отримуємо еквівалентну форму попереджання $G$ : $\exists x,\forall y,\exists z,\forall t,\lnot P(x,y)\lor P(t,z)$ . Формула попередження $F$ еквівалентна $\lnot G$ і :

\forall x,\exists y,\forall z,\exists t,P(x,y)\land \lnot P(t,z)

у сколемівській формі :

\forall x,\forall z,P(x,f(x))\land \lnot P(g(x,z),z)

Вона є правильно виконуваною для усіх $P(u,f(u))$ і помилковою на усіх $P(g(u,v),v)$ , де $u$ і $v$ описують область Ербрана $\{a,f(a),g(a,a),f(f(a)),f(g(a,a)),g(a,f(a)),...\}$ , і дає довільні атрибути для інших предикатів. Проте подальші обчислення по відповідних формулах $Q_{1}$ , $Q_{2}$ , … не збігаються. $F$ здійсненна і, отже, $G$ не є теоремою, але попередній підхід не показує розрахунки за кінцеве число кроків.

Висновок в логічних моделях. Метод резолюцій

Докладніше: Метод резолюцій

Висновок у формальній логічній системі є процедурою, яка із заданої групи виразів виводить відмінне від заданих семантично правильний вираз. Ця процедура, представлена у певній формі, і є правилом виводу. Якщо група виразів, що утворює посилку, є істинною, то повинно гарантуватися, що застосування правила виведення забезпечить отримання істинного виразу як висновку.

Найбільш часто використовуються два методи. Перший — метод правил виводу або метод природного (натурального) виведення, названий так тому, що використовуваний тип міркувань в численні предикатів наближається до звичайного людського розуму. Другий — метод резолюцій. У його основі лежить літочислення резольвентів.

У цій статті розглядається другий метод. Метод резолюцій запропонований в 1930 р. в докторській дисертації Ербрана для доведення теорем у формальних системах першого порядку. Метод резолюцій спирається на обчислення резольвентів. Існує теорема, яка стверджує, що питання про доказовість довільної формули в численні предикатів зводиться до питання про доказовість порожнього списку в обчисленні резольвентів. Тому доказ того, що список формул в обчисленні резольвент порожній, еквівалентно доказу хибності формули в численні предикатів.

Ідея методу резолюцій полягає в тому, що доказ істинності чи хибності висунутого припущення, наприклад: ведеться методом від протилежного. Для цього у вихідну множину пропозицій включають аксіоми формальної системи і заперечення гіпотези: Якщо в процесі доведення виникає протиріччя між запереченням гіпотези і аксіомами, що виражається в знаходженні порожнього списку (диз'юнктів), то висунута гіпотеза правильна. Таке доведення може бути отримано на підставі теореми Ербрана, яка гарантує, що існуюче протиріччя може бути завжди досягнуто за кінцеве число кроків, які б не були значення істинності, що даються функціям, присутнім в гіпотезах. У методі резолюцій множина пропозицій зазвичай розглядається як складовий предикат, що містить кілька предикатів, з'єднаних логічними функціями і кванторами існування і спільності. Так як однакові за змістом предикати можуть мати різний вигляд, то пропозиції перетворюються в клаузальну форму — різновид кон'юнктивної нормальної форми (КНФ), в якої вилучені квантори існування, загальності, символи імплікації, рівнозначності та ін. Клаузальну форму називають сколемовскою кон'юнктивною формою. У клаузальній формі вся початкова логічна формула представляється у вигляді безлічі пропозицій (клауз) С, так званою клаузальною множиною S: Будь-яка пропозиція C, з якої утворюється клаузальна множина S, є сукупністю атомарних предикатів або їх заперечень, з'єднаних символом диз'юнкції:

Вивід рішення в логічній моделі на основі методу резолюцій

Дано твердження: «Сократ — людина»;

«Людина — це жива істота»;

«Всі живі істоти смертні».

Потрібно методом резолюцій довести твердження «Сократ смертний».

Рішення: Крок 1. Перетворимо висловлювання на диз'юнктивну форму: Крок 2. Запишемо заперечення цільового виразу (необхідного виводу), тобто «Сократ безсмертний»: Крок 3. Скласти кон'юнкцію всіх диз'юнктів, включивши в неї заперечення цільового виразу: Крок 4. У циклі проведемо операцію пошуку резольвентів над кожною парою диз'юнктів: Отримання порожнього диз'юнкта означає, що висловлювання «Сократ безсмертний» хибне, значить істинно висловлювання «Сократ смертний».

В цілому метод резолюцій цікавий завдяки простоті та системності, але застосуємо тільки для обмеженого числа випадків (доведення не повинно мати велику глибину, а число потенційних резолюцій не повинно бути великим). Крім методу резолюцій і правил виводу існують інші методи отримання висновків в логіці предикатів.

Див. також