Читайте также:
|
План
1. Властивості числення висловлень.
2. Проблема повноти.
3. Несуперечність числення висловлень.
4. Проблема розв’язності.
5. Незалежність системи аксіом числення висловлень.
1. Властивості числення висловлень
В основі формалізованого числення висловлень лежать поняття, котрі відносяться до так званої області синтаксису, тобто поняття, котрі є деякими абстрагованими від змісту символами й формальні дії з ними: алфавіт, формула, аксіома, правило виведення, доведення, теорема. Ці поняття прийнято називати синтаксичними.
У той же час в алгебрі висловлень за кожною пропозиційною змінною стоїть конкретне висловлення, кожна формула може перетворюватися в конкретне складне висловлення, котре може бути істинним або хибним. У цій сфері, яка є областю семантики, кожне поняття наповнене певним змістом. Поняття істини, хиби, тотожно істинної й тотожно хибної формул, рівносильності й логічного наслідку формул є поняттями семантики.
Проблема повноти
Проблема повноти полягає у з’ясуванні питання, чи достатньо аксіом і правил виведення даного числення для того, щоб можна було вивести будь-яку формулу, яка в змістовному розумінні є тотожно істинною.
Дещо інше поняття повноти системи аксіом ґрунтується на неможливості доповнення системи аксіом будь-якою формулою, яку не можна вивести з даних аксіом.
Система аксіом називається семантично повною, якщо із неї можна отримати всі тотожно-істинні формули, записані засобами цього числення. Це означає, що в даній системі є достатньо аксіом, щоб вивести довільну формулу, котра є істинною прибудь-якому наборі змінних.
Система аксіом називається синтаксично повною, якщо приєднання до неї невивідної у цій системі формули робить систему суперечливою.
Теорема 8.1. Будь яка теорема ЧВ є тавтологією, тобто ├ F Þ ╞ F.
Доведення. Тотожна істинність усіх аксіом перевіряється безпосередньою побудовою таблиць істинності для кожної із них. Отже усі аксіоми - тавтології.
Покажемо тепер, що правило виведення МР перетворює тотожно істинні формули в тотожно істинні формули, тобто покажемо, що коли F і F®G тотожно істинні, формули то й G тотожно істинна. Припустимо супротивне. Нехай G не є тотожно істинною формулою, тобто існує набір значень її змінних, на якому вона набуває значення 0. Тоді підставимо цей набір у формулу F®G. Оскільки F є тавтологією, то дістанемо вираз 1®0, значення якого є 0. Останнє суперечить припущенню про тотожну істинність формули F®G. Отже всі вивідні формули числення висловлень є тотожно істинними формулами тобто тавтологіями.
Має місце й обернена теорема, яку ми наведемо без доведення.
Теорема 8.2. Будь-яка тотожно істинна формула алгебри висловлень є теоремою ЧВ.
Об’єднавши розглянуті теореми одержимо теорему про повноту (теорема тавтології) ЧВ.
Теорема 8.2 (про повноту). Множина теорем числення висловлень збігається з множиною тавтологій алгебри висловлень, тобто ├ F Û ╞ F.
З теореми про повноту випливає її узагальнення - теорема адекватності.
Теорема 8.3 (адекватності). Формула вивідна в ЧВ із скінченної множини гіпотез Г тоді й тільки тоді, коли вона є логічним наслідком усіх формул цієї множини, тобто F1, F2,..., Fm ├ G Û F1, F2,..., Fm ╞ G.
Доведення. Нехай F1, F2,..., Fm ├ G. Тоді за наслідком 7.2 теореми про дедукцію маємо: ├ F1 ® (F2 ®...® (Fm-1 ®(Fm ® G))…).
Звідси за теоремою про повноту одержуємо:
╞ F1 ® (F2 ®...® (Fm-1 ®(Fm ® G))…).
Остання формула рівносильна формулі (F1 Ù F2 Ù... Ù Fm) ® G. Тоді
із тотожної істинності однієї із формул і їх рівносильності випливає, що і друга формула є тавтологією, тобто ╞ (F1 Ù F2 Ù... Ù Fm) ® G.
2. Несуперечність числення висловлень
Аксіоматична теорія називається несуперечною, Якщо для жодного із тверджень А, сформульованого в термінах цієї теорії, само твердження А і його заперечення Ø А не можуть одночасно бути теоремами цієї теорії.
Теорема 8.4 (про несуперечність ЧВ). ЧВ є несуперечною аксіоматичною теорією.
Доведення. Припустимо, що ЧВ суперечлива теорія. Тоді в ЧВ є така формула F, що F і Ø F є теоремами ЧВ. За теоремою про повноту F і Ø F є тавтологіями алгебри висловлень, що неможливо. Отже, ЧВ несуперечна аксіоматична теорія.
3. Проблема розв’язності
Аксіоматична теорія називається розв’язною, якщо існує алгоритм, який дозволяє для будь-якого твердження, сформульованого в термінах цієї теорії, відповісти на запитання, буде чи ні це твердження теоремою даної теорії.
Теорема 8.5 (про несуперечність ЧВ). ЧВ є розв’язною аксіоматичною теорією.
Доведення. Згідно теореми про повноту довідність формули в ЧВ еквівалентна тотожній істинності цієї формули. Останнє можна установити за допомогою побудови таблиці істинності.
4. Незалежність системи аксіом ЧВ
Система аксіом S називається незалежною якщо жодна з аксіом А цієї системи не може бути виведена з інших аксіом системи, тобто з системи S\{ A }.
Щоб довести незалежність певної аксіоми А від інших аксіом системи потрібно побудувати модель у якій би виконувалися всі аксіоми системи S\{ A } і не виконувалася б аксіома А. Це означає, що кожному первісному поняттю й відношенням між поняттями потрібно надати конкретний зміст через деякі конкретні предмети й відношення між ними. Причому це потрібно робити так, щоб вибрані конкретні предмети й відношення між ними мали властивості, сформульовані в аксіомах системи S\{ A }, й не мали б властивості A. Така сукупність конкретних предметів і відношень між ними називається моделлю системи аксіом S\{ A }. ЇЇ наявність доводить незалежність аксіоми A від аксіом S\{ A }. Дійсно, якщо A можна було б вивести із S\{ A }, то в будь-якій моделі, в якій виконувалися б усі аксіоми зі системи S\{ A }, виконувалася б і аксіома A.
Покажемо, наприклад, що аксіома А 1 ЧВ не залежить від аксіом А 2 та А 3. Для цього побудуємо трьохелементну множину М = {1, 2, 3} і введемо в ній дві операції. Перша операція - унарна, вона ставить у відповідність кожному елементу АÎМ елемент із М, який позначається Ø А, а друга операція бінарна, вона ставить у відповідність будь-яким двом елементам А,ВÎМ елемент із М, який позначається А®В. Причому відповідність про яку йде мова визначається наступними таблицями:
| А | А | |
| А | В | 
| |
Якщо тепер усім змінним, що входять в довільну формулу ЧВ надати деякого значення із М, то згідно введеним правилам сама формула прийме деяке значення із М. Формулу Яка завжди приймає значення 0, називатимемо в иділеною.
Покажемо, що будь яка формула, що одержується за схемою аксіома А 2, є виділеною. Для цього складемо таблицю значень формули А 2 (передостанній стовпчик є формулою 
).
| F | G | H | 
| 
| 
| 
| K | (A2) | |
Аналогічно можна показати, що будь яка формула, яка одержується за схемою аксіома А 3, є виділеною.
Далі покажемо, що правило виводу МР зберігає властивість виділення, тобто, якщо формули F i F®G є виділеними, то й формула G є виділеною.
Дійсно, в таблиці, яка визначає операцію ® над елементами множини М = {1, 2, 3}, бачимо, що формули F i F®G приймають одночасно значення 0 лише в першому рядку. Але в цьому рядку й формула G також приймає значення 0.
Із викладеного випливає: будь-яка формула, яка виводиться із аксіом А 2 і А 3 за допомогою правила МР, є виділеною.
Щоб показати, що аксіому А 1 не можна одержати із аксіом А 2 і А 3 за допомогою правила МР, потрібно впевнитися, що А 1 не є виділеною. Це легко зробити використовуючи наведені вище таблиці відповідності.
Аналогічно можна установити незалежність аксіом А 2 і А 3.
Звідси випливає наступна теорема.
Теорема 8.6. Система аксіом А 1, А 2, А 3 ЧВ незалежна.
Існують й інші числення висловлень, тобто числення з іншими системами аксіом і правилами виведення.
Як приклад, розглянемо гільбертовське числення висловлень, викладене у спільній з Аккерманом праці в 1938 році. Воно містить дві пропозиційні зв’язки Ú, Ø. Запис А É В уживається для скорочення запису ØАÚВ. Аксіоми числення наступні:
1. А Ú А É А – принцип тавтології;
2. А É А Ú В – принцип приєднання;
3. А Ú В É В Ú А – принцип переставлення;
4. (А É В) É (С Ú А É С Ú В) – принцип сумування.
Правилом виведення є правило modys ponens:
Наведемо ще один приклад приклад.
Розглянемо гільбертовську аксіоматизацію числення висловлень, яку будемо позначати ЧВ 1.
Аксіоми ЧВ 1 одержуються із наступних 10 схем підстановкою конкретних формул ЧВ 1 замість змінних Ф, Ψ, Х.
1. Ф ® (Ψ ® Ф),
2. (Ф ® Ψ) ® ((Φ ® (Ψ ® Х)) ® (Φ ® Х)),
3. (Ф Ù Ψ) ® Φ,
4. (Ф Ù Ψ) ® Ψ,
5. (Φ ® Ψ) ® ((Φ ® Х) ® (Φ ® (Ψ Ù Х))),
6. Ф ® (Ф Ú Ψ),
7. Ф ® (Ψ Ú Φ),
8. (Ф ® Х) ® ((Ψ ® Х) ® ((Φ Ú Ψ) ® Х)),
9. (Φ ® Ψ) ® ((Φ ® Ø Ψ) ® Ø Φ)
10. Ø Ø Ф ® Ф.
Правило виведення в ЧВ 1 modus ponens.
Приклад виведення формули Ф ® Ф.
1. Ф ® (Ф ® Ф) – аксіома,
2. Ф ® ((Ф ® Ф) ® Ф) – аксіома,
3. (Ф ® (Ф ® Ф)) ® ((Ф ® ((Ф ® Ф) ® Ф)) ® (Ф ® Ф)) – аксіома,
4. (Ф ® ((Ф ® Ф) ® Ф)) ® (Ф ® Ф) – правило виведення до 1 і 3,
5. Ф ® Ф – правило виведення до 2 і 4.
Широко застосовуються також системи С. Кліні, Дж. Россера, Г. Фреге, секвенціальні числення Генцена та інші.
Дата добавления: 2015-04-11; просмотров: 39 | Поможем написать вашу работу | Нарушение авторских прав |