Числення висловлювань

§1 Поняття формальної теорії

Формальна теорія Т вважається визначеною, якщо виконані наступні умови:

1. Задана рахункова множина символів теорії Т (її абетка). Кінцеві послідовності символів називаються виразами теорії Т.

2. Є деяка підмножина виразів-формул теорії Т. (Звичайно існує процедура, яка дозволяє визначити чи є вираз формулою, чи ні).

3. Виділена деяка підмножина формул-аксіом теорії Т. Якщо існує алгоритм розпізнати за формулою є вона аксіомою чи ні, то таку теорію називають аксіоматичною.

4. Є кінцеве число відношень між формулами , які називаються правилами виведеня.

При цьому кожному правилу відповідає ціле додатне число j таке, що для кожних j формул та формули А може бути вирішене питання: чи знаходяться дані j формул в відношенні з формулою А.

Якщо це так, то формула А називається безпосереднім наслідком формул за правилом .

Означення. Виведенням в теорії Т називається послідовність формул така, що формула є або аксіома, або безпосередній наслідок яких-небудь попередніх формул по одному з правил виведення.

df. Формула А називається теоремою теорії Т, якщо існує висновок в теорії Т, в якому останньою формулою є А.

Нехай Г – деяка множина формул теорії Т (множина гіпотез).

df. Висновком з Г в теорії Т називається послідовність формул така, що j або гіпотеза, або аксіома, або безпосередній наслідок деяких попередніх формул по одному з правил виведення.

Говорять, що з Г виведена формула А , якщо існує висновок з Г, в якому останньою формулою є А.

Якщо множина Г кінцева: , то будемо писати .

Якщо Г – пуста множина , то А є теоремою. Замість пишуть звичайно .

Властивості поняття виведення із гіпотез

1. Якщо та , то .

(тобто якщо А виводиться з множини гіпотез Г, то А залишається виведеним, якщо додати до Г нові гіпотези).

2. тоді і тільки тоді, коли в Г існує кінцева підмножина , для якої .

3. Якщо та , то .

Зокрема, якщо , то .

§2 Формальна аксиоматична теорія l для числення висловлювань.

1. Символами теорії L є

а) пропозийні літери з індексами .

б) зв’язки ; (примітивні зв’язки)

в) дужки (, ).

2) Формули.

а) Усяка п.літера є формулою.

б) Якщо А та В – формули, то та - також формули.

в) Вираз є формулою тоді і тільки тоді, коли це випливає з пунктів а) та б).

3) Аксіоми. формул А, В, С теорії L наступні формули є аксіомами:

(А1)

(А2)

(А3) .

4) Єдиним правилом виведення є правило modus ponens: .

Правила зняття дужок залишаються колишніми. Властивості поняття виведення .

Введемо інші зв’язки за допогою наступних означень:

означає

означає

означає

Лема 1. (тобто - це теорема теорії L).

Доведення:

Побудуємо висновок в L.

1. підстановка в схему аксіом (А1)

2. схема аксіом (А2)

3. по m.p. з 1, 2

4. схема аксіом (А1)

5. по m.p. з 3, 4

Теорема дедукції. Нехай Г – деяка множина формул теорії L. А, В – деякі формули теорії L. Якщо , то .

(Зокрема, якщо , то ).

Доведення:

Нехай висновок формули В з Г, А.

Індукцією по i доведемо, що (*) .

1. Перевірка базиса індукції. i=1.

Варіант 1. Нехай вірно a) або b). Маємо наступний висновок з Г:

1. a) або b)

2. (А1)

3. по m.p. з 1, 2

Ми показали, що .

Варіант 2. є А.

За лемою 1 . Значить, . Але, якщо виведена з Г (властивість (d) поняття виведення).

2. Індуктивне припущення: нехай твердження (*) вірне .

3. Індуктивний крок: покажемо, що твердження (*) вірне при .

Варіант 1. доводиться так само, як і для .

Варіант 2. є .

Нехай отримується з деяких формул та по m.p.. Тоді повинна бути влаштована так . Тут k<m, j<m, тому для та твердження (*) вірне.

тобто

тобто

Продовжимо висновок з Г

…

2.

3.

4. по m.p. з 2, 3

5. по m.p. 1, 4

Ми побудували висновок з . Що і треба було.

Наслідок 1.

1. гіпотеза

2. гіпотеза

3. гіпотеза

4. гіпотеза

5. гіпотеза

Показали, що .

Звідси, за теоремою дедукції .

Наслідок 2.

1. гіпотеза

2. гіпотеза

3. гіпотеза

4. по m.p. з 1, 3

5. С по m.p. з 2, 4

За теоремою дедукції .

Теорема дедукції (обернена). Нехай Г – деяка множина формул (гіпотез) теорії L. А, В – деякі формули теорії L. Якщо , то .

Доведення:

, тобто з Г формули , де .

Отримали, що . Що і треба було.

Лема. Для будь-яких формул А, В наступні формули є теоремами теорії L:

а)

Доведення:

(А3)

1. (А3)

2. Лема 1

3. наслідок 2 з 1, 2

4. (А1)

5. наслідок 1 з 3, 4

b)

1.

2. (а)

3. m.p.1, 2

4. (А1)

5. наслідок 1 з 3, 4

c)

1. гіпотеза

2. А гіпотеза

3. (А1)

4. (А1)

5. m.p.1, 3

6. (А3)

7. m.p. 5, 6

8. m.p. 2, 4

9. В m.p. 7, 8

,

За теоремою дедукції

За теоремою дедукції

d)

1. гіпотеза

2. А гіпотеза

3. (А3)

4. (А1)

5. m.p. 1, 3

6. наслідок 1 з 4, 5

7. В m.p. 2, 6

,

За теоремою дедукції

Ще раз застосуємо теорему дедукції

e)

1. гіпотеза

2. (а)

3. наслідок 1 з 1, 2

4. (b)

5. наслідок 1 з 3, 4

6. (d)

7. по m.p. 5, 6

За теоремою дедукції

f)

m.p.

Теорема дедукції

Теорема дедукції

(е)

наслідок 1 з теореми дедукції

(g)

1. гіпотеза

2. гіпотеза

3. (е)

4. m.p. 1, 3

5. (е)

6. m.p. 2, 5

7. (А3)

8. m.p. 6, 7

9. В m.p. 4, 8

Теорема дедукції

Теорема дедукції