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

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

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

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

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

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

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

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

${\displaystyle A\to B}$

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

${\displaystyle B\!}$

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

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

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

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

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

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

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

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

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

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

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

Формальну мову класичної логіки висловлень може бути виражено з використанням лише заперечення (¬), імплікації (→) та символів висловлень. Загальновідомою аксіоматизацією, що включає схеми з трьох аксіом та одне правило висновування (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).

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

Детальніші відомості з цієї теми ви можете знайти в статті ^[en].

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

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

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

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

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

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

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

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

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

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

Див. також

• ^[en]
• ^[en]
• ^[en]
• ^[en]
• Логічна істина
• ^[en]

Примітки

1. Boolos, George; Burgess, John; Jeffrey, Richard C. (2007). Computability and logic. Cambridge: Cambridge University Press. с. 364. ISBN . (англ.)
2. John C. Reynolds (2009) [1998]. Theories of Programming Languages. Cambridge University Press. с. 12. ISBN . (англ.)
3. Kosta Dosen (1996). Logical consequence: a turn in style. У Maria Luisa Dalla Chiara; Kees Doets; Daniele Mundici; Johan van Benthem (ред.). Logic and Scientific Methods: Volume One of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence, August 1995. Springer. с. 290. ISBN . препринт (з іншою нумерацією сторінок) [ 2014-02-01 у Wayback Machine.] (англ.)
4. Bergmann, Merrie (2008). An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems. Cambridge University Press. с. 100. ISBN . (англ.)
5. Bergmann, Merrie (2008). An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems. Cambridge University Press. с. 114. ISBN . (англ.)