Основні проблеми числення висловлень
Числення висловлень і алгебра висловлень. Основні проблеми числення висловлень
Довільну формулу F числення висловлень можна змістовно інтерпретувати як складене висловлення, істинність або хибність якого залежить від істинності елементарних висловлень, що до нього входять. Таким чином, кожній формулі F числення висловлень можна (аналогічно тому, як це було зроблено в алгебрі висловлень) поставити у відповідність функцію істинності f. Виникає питання, як пов'язано таке змістовне «істинносне» тлумачення формул числення висловлень з їхньою формальною вивідністю.
Теорема 1.1
Будь-яка теорема числення висловлень є тотожно істинним висловленням.
Тотожна істинність усіх аксіом легко перевіряється безпосередньо побудовою відповідних таблиць істинності для кожної з них (рекомендуємо це зробити самостійно). Відтак, доведемо, що обидва правила виведення числення висловлень перетворюють тотожно істинні формули у тотожно істинні. Якщо A(p1,p2,…,pn) — тотожно істинна формула, то для довільного набору значень a1,a2,…,an її пропозиційних змінних A(a1,a2,…,an) є істинною. Отже, тотожно істинною буде і будь-яка формула A, що отримується з формули A шляхом підстановки замість пропозиційних змінних p1,p2,…,pn довільних формул B1,B2,…..,Bn, оскільки останні можуть набувати лише значень 0 або 1. Доведемо, що коли формули A і A→B є тотожно істинними, тоді формула B, яку ми дістаємо з них за правилом висновку, також є тотожно істинною. Припустімо супротивне: нехай B не є тотожно істинною формулою, тобто існує набір значень її змінних, на якому вона набуває значення 0. Тоді підставимо цей набір у формулу A→B, оскільки A є тавтологією, то дістанемо вираз 1→0, значенням якого є 0. Останнє суперечить припущенню про тотожну істинність формули A→B. Таким чином, ми переконалися в тому, що всі аксіоми числення висловлень є тотожно істинними формулами алгебри висловлень, а застосування обох правил виведення (підстановки і висновку) до тотожно істинних формул знову приводить до тотожно істинних формул. Отже, всі вивідні формули (теореми) числення висловлень є тотожно істинними формулами алгебри висловлень.
Теорема 2.1
Будь-яка тотожно істинна формула алгебри висловлень є теоремою числення висловлень. Дві останні теореми дозволяють вирішити три важливі проблеми числення висловлень: проблему несуперечності, проблему повноти і проблему розв'язності числення висловлень.
Проблеми
1. Проблема несуперечності.
Для кожної формальної теорії кардинальним є питання несуперечності. Справді, така теорія будується послідовним приєднанням нових теорем, які формально виводять з аксіом за допомогою правил виведення. Отже, немає жодної гарантії, що в цьому процесі ми не дійдемо до суперечності. Інакше кажучи, виникає питання, чи при поступовому нагромадженні теорем формальної теорії не трапиться так, що одна з теорем суперечитиме іншим. Саме так виникає проблема несуперечності числення. Числення є несуперечним, якщо неможливо одночасно вивести з аксіом числення як формулу A, так і її заперечення ¬A.
Наслідок 1.1
Числення висловлень є несуперечною формальною теорією. Справді, якщо формула A вивідна у численні висловлень, то формула ¬A не може бути вивідною, бо за теоремою 1.1 формула A є тотожно істинною в алгебрі висловлень, а формула ¬A — тотожно хибною. Отже, ¬A не може бути теоремою числення висловлень.
2. Проблема повноти.
Інша проблема, що виникає при дослідженні різних числень висловлень: чи будь-яка тотожно істинна формула алгебри висловлень буде вивідною в заданому численні? Це питання й являє собою проблему повноти для числення висловлень. Смисл такої постановки питання полягає в тому, що при побудові числення потрібно знати, чи достатньо аксіом і правил виведення даного числення для того, щоб можна було вивести будь-яку формулу, яка в змістовному розумінні є тотожно істинною.
Наслідок 1.2
Числення висловлень є повним. Справедливість цього твердження безпосередньо випливає з теореми 2.1. У математичній логіці існує й інше поняття повноти системи аксіом, що ґрунтується на неможливості доповнення системи аксіом будь-якою формулою, яку не можна вивести з даних аксіом.
3. Проблема розв'язності.
Розв'язувальним методом для формальної теорії T називають метод, за допомогою якого для довільної формули A з T можна за скінченне число кроків визначити, чи буде A теоремою, чи ні. Числення T називають розв'язним, якщо для T існує розв'язувальний метод, у противному разі — формальна теорія T є нерозв'яною.
Наслідок 1.3
Числення висловлень є розв'язною теорією.
Доведення
Нехай A — довільна формула числення висловлень. Побудуємо для неї таблицю істинності і розглянемо її останній стовпчик. Якщо він містить лише одиниці, то A — тотожно істинна формула і за теоремою 2.1 є теоремою числення висловлень. У противному разі, A — не тавтологія і значить, A не є теоремою. Зрозуміло, що всі ці дії можна зробити за скінченне число кроків.
4.Проблема незалежності.
Нарешті, розглянемо ще одну важливу проблему для формальних теорій. Нехай задано деяку аксіоматичну теорію. Говорять, що деяка аксіома цієї теорії є незалежною, якщо її можна довести методами самої теорії як теорему. Система аксіом аксіоматичниї теорії називається незалежною системою аксіом, якщо всі аксіоми є незалежними.
Наслідок 1.4
Система аксіом числення висловлень є незалежною.
Доведення
Для доведення незалежності деякої аксіоми ЧВ будують таку модель аксіоматичної теорії в якій справджуються всі аксіоми крім даної. Якщо доводиться, то така модель ізоморфна стандартній моделі аксіоматичної теорії, то робиться висновок, що не є незалежною. Якщо такого ізоморфізму немає, то аксіома є незалежною.
Список літератури
- Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947
- Клини С. К. Введение в метаматематику. М., 1957
- Мендельсон Э. Введение в математическую логику. М., 1976
- Enderton, H. B., A Mathematical Introduction to Logic. Harcourt/Academic Press 2002.
- A. G. Hamilton Logic for Mathematicians, Cambridge University Press, Cambridge UK 1978.