Правило висновування

Правила перетворення
Числення висловлень
Правила висновування
Введення / усунення імплікації (modus ponens) Введення / усунення еквівалентності Введення / усунення кон'юнкції Введення / усунення диз'юнкції Диз'юнктивний / гіпотетичний силогізм Конструктивна / деструктивна дилема Абсорбція / modus tollens / modus ponendo tollens
Правила підстановки
Асоціативність Комутативність Дистрибутивність Подвійне заперечення Правила де Моргана Контрапозиція Матеріальна імплікація Експортація Тавтологія Введення заперечення
Предикатна логіка
Універсальне узагальнення / конкретизація Екзистенційне узагальнення / конкретизація

У логіці пра́вило висно́вування, або пра́вило перетво́рення (англ. rule of inference, inference rule, transformation rule) — це логічна форма, що складається з функції, яка отримує передумови, аналізує їхній синтаксис і повертає висновок (або висновки). Наприклад, правило висновування, що називається modus ponens, отримує дві передумови, одну у формі «Якщо p тоді q», а другу у формі «p», і повертає висновок «q». Це правило є чинним відносно семантики класичної логіки (як і відносно семантик багатьох інших некласичних логік), у тому сенсі, що якщо передумови є істинними (в межах інтерпретації), то істинним є і висновок.

Зазвичай правило висновування зберігає істинність, семантичну властивість. У багатозначній логіці воно зберігає узагальнене значення. Але дія правила висновування є винятково синтаксичною, і не потребує зберігання ніякої семантичної властивості: будь-яка функція з множин формул до формул вважається правилом висновування. Зазвичай важливими є лише рекурсивні правила, тобто такі, що існує ефективна процедура визначення, чи є будь-яка задана формула висновком заданої множини формул відповідно до цього правила. Прикладом правила, що не є ефективним у цьому сенсі, є нескінченномісне ω-правило.

До популярних правил висновування у логіці висловлювань надежать modus ponens, modus tollens та контрапозиція. Предикатна логіка першого порядку використовує правила висновування для обходження з логічними кванторами.

Стандартна форма правил висновування

У формальній логіці (та багатьох пов'язаних галузях), правила висновування зазвичай подають у наступній стандартній формі:

  Передумова#1
  Передумова#2
        ...
  Передумова#n   
  Висновок

Цей вираз стверджує, що кожного разу, коли у ході якогось логічного висновування отримуються дані передумови, то вказаний висновок може також братися до припущення. Точна формальна мова, що використовується для опису як передумов, так і висновків, залежить від фактичного контексту висновувань. У простому випадку можуть використовуватися логічні формули, такі як у

$A\to B$

${\underline {A\quad \quad \quad }}\,\!$

$B\!$

Це є правило modus ponens логіки висловлень. Правила висновування часто формулюються як схеми із застосуванням метазмінних. У наведеному вище правилі (схемі) метазмінним A та B може бути привласнено значення будь-яких об'єктів всесвіту (або, за згодою, обмеженої підмножини, такої як висловлення), щоби сформувати нескінченну множину правил висновування.

Система доведення утворюється набором правил, зчеплених між собою так, щоби формувати докази, що також називаються виведеннями. Будь-яке виведення має лише один остаточний висновок, що є твердженням, яке доводиться або виводиться. Якщо передумови у виведенні залишаються не задовольненими, тоді це виведення є доведенням гіпотетичного висновку: «якщо передумови задовольняються, тоді задовольняється висновок.»

Аксіомні схеми та аксіоми

Правила висновування можуть також передаватися такою формою: (1) нуль або більше передумов, (2) символ турнікету $\vdash$, у сенсі «означає», «доводить» або «випливає» та 3) висновок. Ця форма зазвичай втілює раціональний (у протилежність до функційного) вигляд правила висновування, де турнікет означає відношення вивідності, що виконується між передумовами на висновком.

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

Правила висновування слід відрізняти від аксіом теорії. З точки зору семантики, аксіоми є чинними твердженнями. Аксіоми зазвичай розглядають як відправні точки для застосування правил висновування та породжування набору висновків. Або, менш технічними словами:

Правила є твердженнями про систему, аксіоми є твердженнями у системі. Наприклад:

• Правило, що з $\vdash p$ ми можемо вивести $\vdash {\text{Provable}}(p)$, є твердженням, яке каже, що якщо ви довели $p$, то з цього випливає, що $p$ є довідним. Це правило виконується, наприклад, в арифметиці Пеано.
• Аксіома $p\to {\text{Provable}}(p)$ означатиме, що будь-яке істинне твердження є довідним. Ця аксіома не виконується в арифметиці Пеано.

Правила висновування відіграють життєво важливу роль в описі логічних числень, оскільки їх враховують в теорії доведення, зокрема, в численні секвенцій та природній дедукції.

Приклад: Гільбертові системи для двох логік висловлень

У гільбертовій системі передумови та висновки правил висновування є просто формулами якоїсь мови, зазвичай із застосуванням метазмінних. Задля графічної компактності та для підкреслення різниці між аксіомами та правилами висновування цей розділ використовує послідовний запис (⊢) замість вертикального представлення правил.

Формальну мову класичної логіки висловлень може бути виражено з використанням лише заперечення (¬), імплікації (→) та символів висловлень. Загальновідомою аксіоматизацією, що включає схеми з трьох аксіом та одне правило висновування (modus ponens), є

(CA1) ⊢ A → (B → A)

(CA2) ⊢ (A → (B → C)) → ((A → B) → (A → C))

(CA3) ⊢ (¬A → ¬B) → (B → A)

(MP)  A, A → B ⊢ B

Може здаватися зайвим мати два поняття висновування у цьому випадку, ⊢ та →. У класичній логіці висловлень вони дійсно збігаються; теорема дедукції свідчить, що A ⊢ B тоді й лише тоді, коли ⊢ A → B. Проте навіть у цьому випадку існує варта уваги відмінність: перший запис описує дедукцію, що є діяльністю з переходу від виразів до виразів, тоді як A → B є просто формулою, зробленою із застосуванням логічного сполучника, в даному випадку імплікації. Без правила висновування (як modus ponens у даному випадку) немає дедукції або висновування. Цей момент ілюструється в діалозі Льюїса Керрола «Що Черепаха сказала Ахіллові».

Для деяких некласичних логік теорема дедукції не виконується. Наприклад, тризначну логіку Ł3 Лукашевича може бути аксіоматизовано таким чином:

(CA1) ⊢ A → (B → A)

(LA2) ⊢ (A → B) → ((B → C) → (A → C))

(CA3) ⊢ (¬A → ¬B) → (B → A)

(LA4) ⊢ ((A → ¬A) → A) → A

(MP)  A, A → B ⊢ B

Ця послідовність відрізняється від класичної логіки зміною аксіоми 2 та додаванням аксіоми 4. Класична теорема дедукції для цієї логіки не виконується, проте виконується видозмінена форма, а саме A ⊢ B тоді й лише тоді, коли ⊢ A → (A → B).

Прийнятність та вивідність

Детальніші відомості з цієї теми ви можете знайти в статті Правило прийнятності.

Правило висновування може бути зайвим у наборі правил в тому сенсі, що воно є прийнятним (англ. admissible) або вивідним (англ. derivable). Вивідне правило — це таке правило, чиї висновки може бути виведено з його передумов за допомогою інших правил. Прийнятним є таке правило, чиї висновки виконуються, коли виконуються його передумови. Усі вивідні правила є прийнятними. Щоби оцінити різницю, розгляньмо наступний набір правил для визначення натуральних чисел (судження $n\,\,{\mathsf {nat}}$ стверджує той факт, що $n$ є натуральним числом):

${\begin{matrix}{\frac {}{\mathbf {0} \,\,{\mathsf {nat}}}}&{\frac {n\,\,{\mathsf {nat}}}{\mathbf {s(} n\mathbf {)} \,\,{\mathsf {nat}}}}\\\end{matrix}}$

Перше правило стверджує, що 0 є натуральним числом, а друге стверджує, що s(n) є натуральним числом, якщо ним є n. У цій системі доведення наступне правило, що демонструє, що другий наступник (англ. successor) натурального числа також є натуральним числом, є вивідним:

${\frac {n\,\,{\mathsf {nat}}}{\mathbf {s(s(} n\mathbf {))} \,\,{\mathsf {nat}}}}$

Його виведенням є композиція двох застосувань правила наступника, наведеного вище. Наступне правило для ствердження існування попередника будь-якого ненульового числа є лише прийнятним:

${\frac {\mathbf {s(} n\mathbf {)} \,\,{\mathsf {nat}}}{n\,\,{\mathsf {nat}}}}$

Це є дійсним фактом натуральних чисел, оскільки його може бути доведено індукцією. (Щоби довести, що це правило є прийнятним, розгляньте виведення передумови, і зробіть індуктивний перехід за ним, отримавши виведення $n\,\,{\mathsf {nat}}$.) Але воно не є вивідним, оскільки воно залежить від структури виведення передумови. Через це вивідність зберігається при доповненнях системи доведення, тоді як прийнятність — ні. Щоби побачити різницю, припустімо, що до цієї системи доведення було додано наступне безглузде правило:

${\frac {}{\mathbf {s(-3)} \,\,{\mathsf {nat}}}}$

У цій новій системі правило другого наступника залишається вивідним. Однак правило знаходження попередника більше не є прийнятним, оскільки немає немає способу вивести $\mathbf {-3} \,\,{\mathsf {nat}}$. Крихкість прийнятності походить від способу її доведення: оскільки доведення може робити індуктивний перехід за структурою виведень передумов, розширення системи додають нових випадків до цього доведення, що можуть вже й не задовольнятися.

Прийнятні правила можна розглядати як теореми системи доведення. Наприклад, у численні секвенцій, в якому виконується усунення перетинів, правило перетину є прийнятним.

Див. також

• Безпосереднє висновування
• Спростування висновування
• Закони мислення
• Перелік правил висновування
• Логічна істина
• Структурне правило