Конверський А. Є. Логіка (традиційна та сучасна)

Подождите немного. Документ загружается.

Книга друга. СУЧАСНА ЛОГІКА

361

При усуненні конкретного знака формула, якої це сто-

сується, і знак, про який йдеться, можуть використовувати-

ся лише в тому значенні, яке вони отримують при введенні

даного знака.

Наприклад, формула А ⊃ В може бути введена, якщо

наявний висновок В із припущення А, тобто, якщо вірно

А |− В.

Застосовуючи до формули А ⊃ В правило УІ (усунення

імплікації), діємо так, якщо б В було вивідним із дове-

деного А, а це можливо в силу того, що формула А ⊃ В у

засновку застосування правила УІ реєструє існування ви-

сновку В із А.

Систематизація правил введення і усунення пропози-

ційних зв’язок належить відомому німецькому математи-

кові і логіку Герхарду Генцену (1909–1946 рр.). Іноді на-

туральні числення називають «генценівські числення».

Запишемо правила висновку для S

ВІ)

В—АГ

—Ф Г,

(

⊃

УІ)

BAA,

(

⊃

ВК)

ВА

В А,

(

∧

)(УК

ВА

ВA

∧∧

Д)(В

ВА

∨∨

—C|ВАГ,

—С|ГВ—С|АГ,

∨

З)(В

А|

|Г

В|

—|ГА—В|АГ,

−

УПЗ)

А|

(

язапереченн

усуненняслабкеУЗСл

—).(

А|

Е)(В

В~А

АВВ,А

⊃⊃

Е)(У

АА

В~А

ВА

B~А

⊃⊃

Над рискою в кожному правилі записані засновки, а під

рискою – резюме застосування правил. Кожне правило

містить один висновок, в той час як засновків може

бути декілька (однозасновкові, двозасновкові тощо).

Всі «правила введення» уводять відповідну зв’язку у

висновок застосування правила, а конже «правило усунен-

ня» усуває відповідну зв’язку із засновків. Виняток скла-

дає лише правило УД: диз’юнкція А ∨ В скоріше тут «вво-

А. Є. Конверський. ЛОГІКА

362

диться» ніж усувається. Але це правило можна записати у

непарадоксальному вигляді:

А ∨ В Γ, А |− С Γ, В |− С

Γ |− С

Із записів ряду правил введення і усунення пропозицій-

них зв’язок очевидно, що в них використовується знак ви-

відності |−, який вважається вихідним знаком. Слідуючи

Генцену, цього можна уникнути:

,І)В(

ВА

[АА

⊃

[][]

()

УД

ССВА

ВА

<<∨

[][]

()

ВЗ

А|

В|

АА

Квадратні дужки вказують на те, що у них знаходяться

припущення (або гіпотези).

В нашій системі S

будемо вважати знак |− вихідним.

При використанні цього знака в наступних доведен-

нях і дедукціях мають на увазі такі його властивості:

а) А |− А – рефлексивність вивідності;

б) якщо Γ ⊆ ∆ і Γ |− А, то ∆ |− А – (де Γ і ∆ – довільні

послідовності формул, А – формула).

Ця властивість фіксує той факт, що якщо А вивідна

із множини засновків, то вона залишається вивідною,

якщо до Γ додати додаткові засновки. Іншими словами:

якщо А |− В, то С, А |− В;

в) Γ |− А тоді і тільки тоді, коли в Γ існує кінцева

підмножина формул ∆, для якої ∆ |− А;

г) якщо ∆ |− А і Γ |− В для будь-якої формули В із ∆, то

із Γ |− А. Іншими словами: якщо А |− В і В |− С, то А |− С

(транзитивність |−).

Власне, ці властивості знака відповідності |− справедливі

і для S

Тепер розглянемо дефініцію доведення в S

На відміну від правил висновку у S

, які застосовуються

тільки для виведення доказаних виразів із доказаних, у

Книга друга. СУЧАСНА ЛОГІКА

363

натуральному численні правила висновку можуть бути за-

стосовані до будь-якого виразу.

Вираз, який випливає за якимось правилом із доведе-

ного виразу, тим, самим є доведенням. Але вираз, який

випливає із недоведеного виразу, ще не доведений. У цьо-

му випадку необхідно звільнитися якимось чином від ви-

користовуваних припущень. У наведених правилах висно-

вку для S

тільки двом правилам притаманна власти-

вість звільнення від припущень: (ВІ) і (ВЗ), адже тільки

вони усувають формулу А із припущень.

Оскільки в S

немає аксіом, то доведення тут базується

або на правилі введення імплікації, або на правилі введен-

ня заперечення.

Якщо останнім застосовується правило (ВІ), то ви-

сновок буде прямим, а якщо – (ВЗ), то висновок буде

непрямим.

Доведення в S

починають із припущень, а потім за

правилами висновку отримують із них відповідні нас-

лідки, після чого за допомогою правил (ВІ) та (ВЗ) елі-

мінують (усувають) припущення. Тому в S

вихідним є

поняття доведення із припущень (гіпотез), а поняття безу-

мовного доведення – похідним.

Дефініція поняття вивідності із припущень: «Фор-

мула В вивідна із припущень Γ, А, символічно: Γ, А |− В,

якщо і тільки якщо:

1) існує правило висновку, в якому Γ і А є засновками,

а В висновком цього правила; або

2) існує деяка кінцева послідовність застосування

правил висновку А

, ..., А

в якій засновками застосу-

вання кожного правила є або формули із Γ, А, або нас-

лідки попередніх (в даній послідовності) застосувань

правил, і наслідком останнього застосування правила є

формула В. При цьому дозволяється використовувати

властивості знака |−».

Гіпотезу називають усуненою в ході дедукції, якщо в

процесі дедукції до цієї гіпотези (або наслідку із неї) за-

стосовується правило (ВІ) або (ВЗ).

Доведенням формули А називається дедукція із де-

якої кінцевої множини гіпотез, в ході якої кожна із гі-

потез усувається.

А. Є. Конверський. ЛОГІКА

364

Здійснимо доведення деяких теорем пропозиційного чи-

слення за допомогою натурального висновку.

Щоб побудувати доведення теореми в S

, необхідно

виконати такі дії:

1) виписати всі можливі припущення, виходячи із

структури даної формули;

2) застосувати до виписаних припущень відповідні

правила висновку із 14 правил, що входять у дедуктику

;

3) застосувати одне із правил (ВІ) або (ВЗ) для елімі-

нації припущень.

Користуючись цими настановами, перейдемо до дове-

дення конкретних теорем.

Теорема 1. (А ⊃ В) ⊃ ((В ⊃ С) ⊃ (А ⊃ С)).

Доведення.

1. А ⊃ В – припущення 1

2. В ⊃ С – припущення 2

3. А – припущення 3

4. В – УІ до 1,3

5. С – УІ до 2, 4

6. А ⊃ С – ВІ до 3,5

7. (А ⊃ В) ⊃ (В ⊃ С) – ВІ до 1, 2

8. |− (А ⊃ В) ⊃ ((В ⊃ С) ⊃ (А ⊃ С)) – ВІ до 6,7.

Теорема 2. (А ⊃ В) ⊃ ((С ⊃ А) ⊃ (С ⊃ В)).

Доведення.

1. (А ⊃ В) – припущення 1

2. (С ⊃ А) – припущення 2

3. С – припущення 3

4. А – УІ до 2, 3

5. В – УІ до 1, 4

6. (С ⊃ В) – ВІ до 3,5

7. (А ⊃ В) ⊃ (С ⊃ А) – ВІ до 1,2

8. |− (А ⊃ В) ⊃ ((С ⊃ А) ⊃ (С ⊃ В)).

Теорема 3. (А ⊃ В) ⊃ ((С ∧ А) ⊃ (С ∧ В)).

Доведення.

1. (А ⊃ В) – припущення 1

2. (С ∧ А) – припущення 2

Книга друга. СУЧАСНА ЛОГІКА

365

3. С – УК до 2

4. А – УК до 2

5. В – УІ до 1,4

6. С ∧ В – ВК до 3,5

7. (А ⊃ В) ⊃ (С ∧ А) – ВІ до 1,2

8. |− (А ⊃ В) ⊃ ((С ∧ А) ⊃ (С ∧ В)) – ВІ до 6,7.

Теорема 4. (А ⊃ В) ⊃ ((А ∧ С) ⊃ (В ∧ С)).

Доведення.

1. (А ⊃ В) – припущення 1

2. (А ∧ С) – припущення 2

3. А – УК до 2

4. С – УК до 2

5. В – УІ до 1,3

6. В ∧ С – ВК до 4,5

7. (А ⊃ В) ⊃ (А ∧ С) – ВІ до 1,2

8. |− (А ⊃ В) ⊃ ((А ∧ С) ⊃ (В ∧ С)) – ВІ до 6,7.

Теорема 5. (А ⊃ В) ⊃ ((С ∨ А) ⊃ (С ∨ В)).

Доведення.

1. А ⊃ В – припущення 1

2. А – припущення 2

3. В – УІ до 1,2

4. С ∨ В – ВД до 3

5. С – припущення 3

6. А ⊃ В, С ∨ А |− С ∨ В – УД

до (1,2,4) і (1,5,4)

7. (А ⊃ В) ⊃ (С ∨ А) – ВІ до 1,6

8. |− (А ⊃ В) ⊃ ((С ∨ А) ⊃ (С ∨ В)) – ВІ до 7,4.

Таким способом будується доведення будь-якої теоре-

ми в S

Отже, в численнях логіки висловлювань виділяють дві

формально логічні теорії: S

і S

, основна різниця яких

полягає в їх дедуктивній логіці або у дедуктиці.

Маються на увазі послідовності 1) А ⊃ В, А |− С ∨ В

2) А ⊃ В, С |− С ∨ В.

А. Є. Конверський. ЛОГІКА

366

Контрольні питання та вправи

1. Поняття числення в логіці.

2. Структура S

3. Порівняльна характеристика систем S

i S

4. Алфавіт S

5. Правила перетворення в S

6. Аксіоми і теореми в S

7. Правила доведення в S

8. Дефініція доведення.

9. Дефініція доказової формули.

10. Структура доведення в S

11. Хід доведення із аксіом.

12. Розширене поняття доведення в S

13. Поняття «теорема» і «метатеорема».

14. Метатеорема про дедукцію.

15. Варіанти доведення метатеореми про дедукцію.

16. Металогічні принципи в S

17. Принцип розв’язання.

18. Принцип несуперечності.

19. Принцип повноти.

20. Принцип незалежності.

21. Загальна характеристика натурального числення вислов-

лювань S

22. Структура S

23. Правила висновку в S

24. Дефініція доведення в S

25. Прямі і непрямі доведення в S

26. Хід побудови доведення в S

27. Довести вивідність формул:

а) (А ⊃ (В ⊃ С)) ⊃ ((А ⊃ В) ⊃ (А ⊃ С))

б) А ⊃ (А ⊃ В)

в) (А ⊃ В) ⊃ ((С ∨ А) ⊃ (С ∨ В))

г) (А ∨ (В ∧ С)) ⊃ ((А ∨ В) ∧(А ∨ С))

д) А ⊃ (В ⊃ (А ∧ В)

е) А ⊃ (А ⊃ В) ⊃ ((А ⊃ В) ⊃ А)

ж) (А ⊃ В) ⊃ ((С ⊃ Д) ⊃ ((А ∨ С) ⊃ (В ∨ D))).

Книга друга. СУЧАСНА ЛОГІКА

367

Б. ЛОГІКА ПРЕДИКАТІВ

Проаналізована у першій частині класична логіка ви-

словлювань є досить специфічною логічною теорією. Засо-

бами цієї логічної теорії можна виділити досить вузьку

множину тавтологій. В її рамках обгрунтовується прави-

льність досить обмеженої групи дедуктивних міркувань.

Основною причиною такої ситуації є недостатньо вираз-

ні можливості логіки висловлювань. Відомо, що розв’язу-

ючи у рамках логіки висловлювань питання про логічну

істинність висловлювань, правильність чи неправильність

міркувань, відволікаються від внутрішньої структури про-

стих висловлювань, замінюючи їх пропозиційними змін-

ними. Але нерідко виникає ситуація, коли логічну істин-

ність висловлювань, правильність міркувань неможливо

дослідити без урахування внутрішньої структури простих

висловлювань.

Наприклад: «Будь-який підручник є книгою. Отже, де-

які книги є підручниками». Правильність такого міркуван-

ня залежить не тільки від зв’язків між висловлюваннями,

а й від внутрішньої структури самих висловлювань.

Ефективний аналіз висловлювань і міркувань такого

типу потребує використання мов з більш виразними мож-

ливостями. Такою мовою є мова класичної логіки преди-

катів.

А. Є. Конверський. ЛОГІКА

368

РОЗДІЛ І

АЛГЕБРАЇЧНА СИСТЕМА ЛОГІКИ ПРЕДИКАТІВ

Цю частину логіки предикатів, як своєрідну формально-

логічну теорію, позначають символом S

Засобами S

здійснюється типологія формул за синтак-

сичними і семантичними ознаками, систематизуються за-

кони логіки предикатів, визначаються основні види логіч-

них відношень між формулами, описується процедура

розв’язання.

1. Мова алгебраїчної системи логіки предикатів

Знайомство з S

розпочнемо із Sin ML. Синтаксис ме-

тамови алгебраїчної системи логіки предикатів склада-

ється із:

1) списку вихідних символів;

2) правил утворення термінів;

3) правил утворення формул.

Розглянемо по порядку кожен із компонентів.

До вихідних символів відносяться:

а) предметні змінні – х

, х

,..., х

(нескінченна мно-

жина);

б) предметні константи – а

, а

,..., а

(кінечна або

нескінченна множина; є мови, де символи такого рангу не

вводяться);

в) предикатні символи (предикатори різних місткостей,

на які вказують верхні числові індекси):

...,,

...............

...,,

Книга друга. СУЧАСНА ЛОГІКА

369

(для зручності будемо використовувати предикатні симво-

ли P, Q, R, S і при необхідності – верхні індекси для вка-

зівки місткості);

г) знаки предметних функцій (предметні функтори рі-

зних місткостей):

...,,

............…..

...,,

ff ;

д) логічні терміни: ∧

∨

⊃

∾



∀

∃;

е) технічні знаки: /,/; / (; ) / – кома, ліва і права ду-

жки.

Дефініція терму:

1. Будь-яка предметна змінна і предметна констан-

та є термом;

2. Якщо t

, t

, ..., t

є терми і Ф є n-місний функтор,

то Ф (t

, t

, ... t

) також є термом.

3. Ніщо, окрім вказаного в пунктах 1 і 2, не є термом.

Дефініція формули:

1. Якщо t

, t

, ..., t

є терми і

– n-містка предика-

торна змінна, то

, t

, ..., t

) є формулою.

2. Якщо А і В – формули, то A ∧ B, A ∨ В, А ⊃ В, А∾

В,  А – також формули.

3. Якщо х – предметна змінна і А – формула, то

∀х А і ∃х А є формулами.

4. Ніщо, окрім вказаного в пунктах 1–3, не є форму-

лами.

У дефініціях терму і формули використовують сим-

воли t

, t

,..., t

, Ф,

, А, В, х. Це символи метамови, які є

синтаксичними змінними, що мають значеннями вирази

відповідних категорій об’єктної мови. Формули А і В, що

зустрічаються в дефініції формули, називають підформу-

лами відповідних формул.

Вважається, що введені визначення вихідного символу,

терму і формули є ефективними або рекурсивними.

А. Є. Конверський. ЛОГІКА

370

Під рекурсивністю поняття розуміють, що існує чі-

ткий спосіб, за допомогою якого завжди можна встано-

вити, чи є даний символ вихідним, чи термом, чи фор-

мулою.

Введемо поняття «зв’язаної змінної» і «вільної змінної».

Індивідна змінна, яка входить до області дії кванто-

ра по цій змінній, зв’язується цим квантором. Таке

входження називається зв’язаним.

Змінна, яка не входить у дію відповідного квантора,

називається вільною.

Одна і та сама змінна в конкретній формулі може мати

зв’язане і вільне входження.

Наприклад:

∀x (P(x) ⊃ Q(y)) ∨ ∃ z (R(x,z) ∧ Q(y)).

Справжніми змінними є тільки вільні змінні.

Зв’язані змінні називаються фіктивними змінними.

У загальному розумінні змінна – це те, замість чого

можна підставити одне із його значень і отримати осмис-

лене висловлювання. Вільні змінні задовольняють цю умо-

ву, а зв’язані – ні.

Наприклад, якщо а є одним із значень змінної х і Р(х)

має смисл, то Р(а) також матиме смисл. За цих умов і ∀х

Р(х) має смисл, а вираз ∀х Р(а) смислу не має. Цим самим

підкреслюється фіктивний характер входження х до фор-

мули ∀х Р(х) і ∀у Р(у), вони означають одне і те саме: «Всі

х мають властивість Р», їх різниця полягає у фіктивних

змінних. Тобто, вони по-різному виражають одне й те саме

висловлювання. Такі формули називають конгруентними

(подібними).

Виходячи з цього, можна сформулювати правило пере-

йменування зв’язаних змінних:

«Усі зв’язані входження змінної х до формули можна

замінити входженням іншої змінної, при цьому отри-

маємо формулу, конгруентну вихідній».

Наприклад, маємо формулу:

Р(х) ∨ ∃х Р(х).

Замінимо в ній зв’язану індивідну змінну х на індивід-

ну змінну у. Отримаємо формулу, яка буде конгруентна

даній:

Р(х) ∨ ∃у Р(у).