Читайте также:
|
План
1. Числення висловлень
Числення висловлень
У загальному вигляді формальна теорія Т, яка ще називається численням, будують таким чином.
1. Означають набір основних символів - алфавіт теорії.
2. Конструктивно означають множину формул, або правильно побудованих виразів, яка утворює мову теорії.
3. Виокремлюють підмножину формул, які називають аксіомами теорії.
4. Задають правила виведення (виводу) теорії.
Розглянемо один із варіантів числення висловлень, яке називатимемо ЧВ.
Алфавіт ЧВ складається з пропозиційних змінних Х1, Х2,..., Хп, знаків логічних операцій 
і технічних знаків (,) - круглих дужок.
Поняття формули ЧВ означається наступним чином.
1. Кожна пропозиційна змінна є формула.
2. Якщо F1 , F2 - формули, то вирази 
також є формулами.
3. Інших формул, ніж побудованих за правилами 1 і 2 немає.
Аксіоми ЧВ.
(А1): 
;
(А2): 
;
(АЗ): 
де F, G, Н - довільні формули.
Правилом виведення в ЧВ єправило тdиs ропеns, (МР): із формул F і F 
G безпосередньо випливає формула G. Це правило будемо записувати у вигляді: МР(F1, F1® G)=G.
Кожен із виразів (А1), (А2), (АЗ) задає лише форму аксіоми, а тому називається схемою аксіом.
Схема формул - це вираз метамови для позначення нескінченної множини всіх тих формул числення, які отримуються після заміни змінних метамови (метазмінних) цієї схеми певними формулами числення.
Якщо у вивідній формулі F(P), яка містить літеру Р, замінити усі входження Р на довільну формулу Q, то формула F(Q) є також вивідною. Таку заміну далі позначатимемо 
.
Для скороченого запису формул вводяться зв’язки 
, які означаються так:
означає 
;
означає; 
;
означає 
.
Означення 7.1. Виведенням формули F із множини формул Г називається така скінчена послідовність формул В1, В2, …, Вs=F, кожна із якої є або аксіомою, або формулою із Г, або формулою, одержаною із попередніх за допомогою правила виведення. Якщо є вивід формули F із множини формул Г, то говорять що F вивідна із Г, і записують Г ├ F. Елементи із Г називають гіпотезами або посилками виводу. Якщо є вивід формули F із пустої множини гіпотез, тобто формула F виводиться лише із аксіом, то таке виведення називається доведенням даної формули, а саму формулу F називають теоремою. Якщо F - теорема, то це записують так ├ F.
Приклад 7.1. Довести F├ F.
В1: 
В2: 
В3: МР(В2, В1)= 
В4: 
;
В5: МР(В4, В3)= 
Теорема 7.1. (Властивості вивідності).
1. Якщо Г ├ F і Г Í D, то Г ├ F і ├ F.
2. Г ├ F тоді й тільки тоді, коли в Г існує така сканченна підмножина D, що D├ F.
3. Якщо Г ├ G для довільної формули G із множини D і D├ F, то Г ├ F.
Будь-яке доведене в численні висловлень виведення вигляду Г ├ F, де Г множина формул, F - довільна формула, можна розглядати як правило виведення 
, яке можна додати до заданої множини правил. Такі правила називаються похідними правилами. Могутнім засобом одержання ряду важливих похідних правил виведення є теорема дедукції.
Теорема 7.2 (теорема дедукції).
Якщо F1, F2,..., Fm-1, Fm ├ G, то F1, F2,..., Fm-1 ├ Fm ® G. Зокрема, якщо F├ G, то ├ F G.
Наслідок 7.1. F1, F2,..., Fm-1, Fm ├ G, тоді й тільки тоді, коли
F1, F2,..., Fm-1 ├ Fm ® G.
Доведення. Необхідність випливає з теореми дедукції. Доведемо достатність. Якщо F1, F2,..., Fm-1 ├ Fm ® G, то існує відповідний вивід: 
,..., 
, 
.
Доповнимо його двома формулами Fт і G. Одержимо послідовність ,..., , Fm ® G, Fт, G,яка є виводом формули G із гіпотез, оскільки передостння формула цієї послідовності є однією з гіпотез, а остання одержана з двох попередніх ій формул за правилом МР.
Наслідок 7.2. F1, F2,..., Fm-1, Fm ├ G тоді й тільки тоді, коли
├ F1 ® (F2 ®...® (Fm-1 ®(Fm ® G))…).
Даний наслідок одержуємо m -кратним застосуванням попереднього наслідку.
За допомогою теореми про дедукцію спочатку доведемо наступну лему, яка потім разом з теоремою про дедукцію використовуватиметься для доведення теорем ЧВ.
Лема 7.1. Для будь-яких формул F, G, Н справедливінаступні виведення:
а) 
├ F H;
б) 
G ├ F H.
Доведення. а) Покажемо спочатку, що , F ├ H. Для цього побудуємо послідовність, яка є відповідним виводом: 
, F, G,, Н. Перші три формули послідовності суть гіпотези. Четверта формула G одержана з першої й третьої формул послідовності за правилом МР, а п’ята - із другої й четвертої за тим же правилом. Отже , F ├ H. Звідси за теоремою про дедукцію робимо висновок ├ F H.
б) Неважко бачити, що G, F ├ H, звідки за теоремою про дедукцію маємо G ├ F H.
Приклад 7.2. Довести теорему 
.
В1: 
,
В2: (Приклад 7.1) = 
,
В3: 
Лема 7.1(б) = 
,
В4: 
,
В5: 
Лема 7.1(б) = .
Послідовність формул В1, В2, В3, В4, В5 не є виводом формули із аксіом. Це виведення ґрунтується не лемі 7.1, яка в свою чергу спирається на теорему дедукції.
Дата добавления: 2015-04-11; просмотров: 106 | Поможем написать вашу работу | Нарушение авторских прав |