Поняття виводимості формули з сукупності ла виводимості

Обчислення ВИСКАЗИВАНІЙ.Определеніе формули ІВ.сістема аксіом ІВ.

Обчислення висловлювань - це аксіоматична логічна система, інтерпретацією якої є алгебра висловлювань.

Опис всякого обчислення включає в себе опис символів цього обчислення (алфавіту), формул, які є кінцевими конфігураціями символів, і визначення виведених формул.

2. ¯, , V, → - логічні зв'язки.

Інших символів ІВ не має.

Визначення формули ІВ

1. Будь-яке змінне висловлювання - є формула.

3. Якщо А і В формули ІВ, то А B, A V B, A → B - також формули ІВ.

4. Ніяка інша рядок символів не є формулою ІВ.

Наступним етапом в побудові ІВ є виділення класу доказових формул. Виділення класу доказових формул здійснюється шляхом застосування аксіом ІВ і правил виведення.

Система аксіом числення висловів

Система аксіом ІВ складається з 11 аксіом, які діляться на чотири групи.

I2. (X → (y → z)) → ((x → y) → (x → z));

II3. (Z → x) → ((z → y) → (z → x y));

III1. x → x V y;

III2. y → x y;

III3. (X → z) → ((y → z) → (x V y → z));

Аксіоми ІВ визначають вихідний клас доказових формул. Доказова формула А позначається | --А.

Визначення доказовою формули обчислення висказиваній.Правіло подстановкі.Правіло ув'язнення.

Доказова формула А позначається | --А.

1. Правило підстановки. Нехай А - доказова формула ІВ, x - змінна, В - будь-яка формула ІВ. Тоді формула, яка виходить з формули А шляхом підстановки в неї замість x формули В, доказова. Операція підстановки позначається:

Тоді правило підстановки записується так:

2. Правило висновку. Якщо формули B, B → C - доказові формули ІВ, то формула С - доказова.

Взагалі доказовою формулою називається всяка формула, яка або є аксіомою, або виходить з доказових формул за допомогою правил підстановки і висновку.

3. Похідні правила виведення:

I. - правило одночасної підстановки.

II. - правило силогізму.

III. - правило контрапозиции.

IV. а). б) - правила зняття подвійного заперечення.

V. - правило складного ув'язнення.

Поняття виводимості формули з сукупності формул.Правіла виводимості.

Нехай є кінцева сукупність формул ІВ Н = 1. A2. ..., An>. Кажуть, що формула B виведена з сукупності H (H | - B), якщо:

б) або B - доказова формула ІВ,

в) або B виходить за правилом висновку з формул C і C → B, які виводяться з сукупності H.

Також кажуть, що кінцева сукупність формул B1. B2. ..., Bk є висновок з H. якщо для кожної формули Bi (i = 1, 2, ..., k) цієї сукупності:

б) або Bi доказова,

в) або Bi виходить за правилом висновку з формул C, C → Bi. які знаходяться у висновку, передуючи Bi.

Нехай H і W - дві сукупності формул обчислення висловлювань. Будемо позначати через H, W їх об'єднання, тобто

Зокрема, якщо сукупність W складається з однієї формули C, то будемо записувати об'єднання H у вигляді H, C.

Тоді мають місце правила виводимості:

5. - теорема дедукції.

6. - узагальнена теорема дедукції.

7. - правило введення кон'юнкції.

8. - правило введення диз'юнкції.

9. - правило перестановки посилок.

10. - правило з'єднання посилок.