Реферат на тему:
Числення висловлень і алгебра висловлень. Основні проблеми числення
висловлень.
Довільну формулу F числення висловлень можна змістовно інтерпретувати
як складене висловлення, істинність або хибність якого залежить від
істинності елементарних висловлень, що до нього входять. Таким чином,
кожній формулі F числення висловлень можна аналогічно тому, як це було
зроблено в алгебрі висловлень, поставити у відповідність функцію
істинності f.
Виникає питання, як пов’язано таке змістовне «істинносне» тлумачення
(інтерпретація) формул числення висловлень з їхньою формальною
вивідністю.
Теорема 5.5. Будь-яка теорема числення висловлень ЧВ є тотожно істинним
висловленням (тавтологією).
Доведення. Тотожна істинність усіх аксіом легко перевіряється
безпосередньо побудовою відповідних таблиць істинності для кожної з них
(рекомендуємо це зробити самостійно).
Відтак, доведемо, що обидва правила виведення числення висловлень
перетворюють тотожно істинні формули у тотожно істинні.
A, що отримується з формули A шляхом підстановки замість пропозиційних
змінних p1,p2,…,pn довільних формул B1,B2,…..,Bn, оскільки останні
можуть набувати лише значень 0 або 1.
Доведемо, що коли формули A і A(B є тотожно істинними, тоді формула B,
яку ми дістаємо з них за правилом висновку, також є тотожно істинною.
Припустімо супротивне: нехай B не є тотожно істинною формулою, тобто
існує набір значень її змінних, на якому вона набуває значення 0. Тоді
підставимо цей набір у формулу A(B, оскільки A є тавтологією, то
дістанемо вираз 1(0, значенням якого є 0. Останнє суперечить припущенню
про тотожну істинність формули A(B.
Таким чином, ми переконалися в тому, що всі аксіоми числення висловлень
ЧВ є тотожно істинними формулами алгебри висловлень, а застосування обох
правил виведення (підстановки і висновку) до тотожно істинних формул
знову приводить до тотожно істинних формул. Отже, всі вивідні формули
(теореми) числення висловлень є тотожно істинними формулами алгебри
висловлень.
Справедливою є й обернена теорема, яку подамо без доведення.
Теорема 5.6. Будь-яка тотожно істинна формула алгебри висловлень є
теоремою числення висловлень ЧВ.
Дві останні теореми дозволяють вирішити три важливі проблеми числення
висловлень: проблему несуперечності, проблему повноти і проблему
розв’язності. Розглянемо їх послідовно.
1. Проблема несуперечності.
Для кожної формальної теорії кардинальним є питання несуперечності.
Справді, така теорія будується послідовним приєднанням нових теорем, які
формально виводять з аксіом за допомогою правил виведення. Отже, немає
жодної гарантії, що в цьому процесі ми не дійдемо до суперечності.
Iнакше кажучи, виникає питання, чи при поступовому нагромадженні теорем
формальної теорії (числення) не трапиться так, що одна з теорем
суперечитиме іншим. Саме так виникає проблема несуперечності числення.
Числення є несуперечним, якщо неможливо одночасно вивести з аксіом
числення як формулу A, так і її заперечення (A.
Наслідок 5.1. Числення висловлень ЧВ є несуперечною формальною теорією.
Справді, якщо формула A вивідна у численні висловлень, то формула (A не
може бути вивідною, бо за теоремою 5.5 формула A є тотожно істинною в
алгебрі висловлень, а формула (A – тотожно хибною. Отже, (A не може бути
теоремою числення висловлень ЧВ.
2. Проблема повноти.
Iнша проблема, що виникає при дослідженні різних числень висловлень: чи
будь-яка тотожно істинна формула алгебри висловлень буде вивідною в
заданому численні? Це питання й являє собою проблему повноти для
числення висловлень.
Смисл такої постановки питання полягає в тому, що при побудові числення
потрібно знати, чи достатньо аксіом і правил виведення даного числення
для того, щоб можна було вивести будь-яку формулу, яка в змістовному
розумінні є тотожно істинною.
Наслідок 5.2. Числення висловлень ЧВ є повним.
Справедливість цього твердження безпосередньо випливає з теореми 5.6.
У математичній логіці існує й інше поняття повноти системи аксіом (або
числення), що грунтується на неможливості доповнення системи аксіом
будь-якою формулою, яку не можна вивести з даних аксіом.
3. Проблема розв’язності.
Розв’язувальним методом для формальної теорії T називають метод, за
допомогою якого для довільної формули A з T можна за скінченне число
кроків визначити, чи буде A теоремою, чи ні.
Числення T називають розв’язним, якщо для T існує розв’язувальний метод,
у противному разі – формальна теорія T є нерозв’яною.
Наслідок 5.3. Числення висловлень ЧВ є розв’язною теорією.
Доведення. Нехай A – довільна формула числення ЧВ. Побудуємо для неї
таблицю істинності і розглянемо її останній стовпчик. Якщо він містить
лише одиниці, то A – тотожно істинна формула і за теоремою 5.6 є
теоремою ЧВ. У противному разі (останній стовпчик таблиці істинності
містить хоча б один нуль), A – не тавтологія і значить, A не є теоремою.
Зрозуміло, що всі ці дії можна зробити за скінченне число кроків.
Нарешті, розглянемо ще одну важливу проблему для формальних теорій.
Система аксіом числення називається незалежною, якщо жодна з аксіом цієї
системи не може бути виведена з інших аксіом системи.
Зрозуміло, що аксіому, яку можна вивести з інших, можна виключити зі
системи аксіом, і при цьому множина теорем теорії залишиться тією ж
самою (тобто отримаємо рівносильне числення). Отже, залежна система
аксіом у певному розумінні менш досконала, ніж незалежна система, бо
вона містить зайві аксіоми.
Можна довести, що системи аксіом числень висловлень ЧВ і ЧВ1 є
незалежними.
Iснують й інші формальні теорії, що означаються і досліджуються у
математичній логіці: числення предикатів, різноманітні числення (теорії)
першого порядку, числення з рівностями, формальна арифметика тощо. У
наступних розділах розглянемо основні ідеї і принципи побудови однієї з
таких теорій – числення предикатів.
Нашли опечатку? Выделите и нажмите CTRL+Enter