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

Чи́слення висло́влень (логіка висловлень, пропозиційна логіка, англ. propositional calculus) — формальна система в математичній логіці, в якій формули, що відповідають висловленням, можуть утворюватись шляхом з'єднання простих висловлень із допомогою логічних операцій, та система правил виводу, які дозволяють визначати певні формули як «теореми» формальної системи.

Формальне визначення

Численням висловлень є формальна система ${\mathcal {L}}={\mathcal {L}}\left(\mathrm {A} ,\ \Omega ,\ \mathrm {Z} ,\ \mathrm {I} \right)$, де:

• Множина $\ \mathrm {A}$ є скінченною множиною символів висловлень (чи елементарних висловлювань, пропозиційних змінних, атомарних формул). Для зображення атомарних формул нижче використовуються малі латинські літери. За потреби можна використовувати і зліченну множину символів.
• Множина $\ \Omega$ — скінченна множина логічних сполучників (логічних операторів). Дану множину можна розбити на підмножини:

$\Omega =\Omega _{0}\cup \Omega _{1}\cup \ldots \cup \Omega _{j}\cup \ldots \cup \Omega _{m}.$

У цьому розбитті $\ \Omega _{j}$ є множина операторів арності $j$ (також позначено $\Omega _{0}=\{0,1\}.\,\!$).

Найчастіше використовуються оператори:

$\Omega _{1}=\{\lnot \},$

$\Omega _{2}\subseteq \{\land ,\lor ,\rightarrow ,\leftrightarrow \}.$

• Множина $\ \mathrm {Z}$ є скінченною множиною правил виводу, що дозволяють одержувати одні формули з інших.

• Множина $\ \mathrm {I}$ є скінченною множиною, елементи якої називаються аксіомами. В окремих прикладах дана множина може бути пустою.

Мовою числення висловлень є множина формул, що визначаються рекурсивно за допомогою наступних правил:

1. всі елементи множини $\ \mathrm {A}$ є формулами;
2. якщо $\ p_{1},p_{2},\ldots ,p_{j}$ є формулами та $f\in \Omega _{j}$, тоді $\left(f(p_{1},p_{2},\ldots ,p_{j})\right)$ теж є формулою.
3. інших формул, ніж побудовані за правилами 1 і 2 немає.

Виведення формул і теорем

Нехай $\Sigma \;$ деяка множина формул ${\mathcal {L}}$, а $A$ — деяка задана формула, то кажуть, що формула $A$ виводиться з множини формул $\Sigma \;$ (позначається $\Sigma \vdash A$), якщо існує така скінченна послідовність формул $A_{1},A_{2}\ldots A_{n}=A,$ де для кожної формули $A_{i}$:

1. $A_{i}$ є аксіомою, або
2. $A_{i}$ належить множині $\Sigma \;$ або
3. $A_{i}$ виводиться з попередніх формул послідовності за допомогою котрогось із правил виводу.

Якщо при цьому множина $\Sigma \;$ — пуста (формула $A$ виводиться лише за допомогою аксіом і правил виводу), то формула $A$ називається теоремою (для цього використовується позначення $\vdash A$).

Приклади аксіоматики

Приклад 1

1. Алфавіт (елементи множини $\mathrm {A}$) числення висловлень складається з елементарних висловлень (пропозиційних змінних): $a,b,c,d,\dots ,x,y,z$ (можливо з індексами), логічними операціями є $\lor ,\land ,\lnot ,\rightarrow$ .
2. Поняття формули визначається аналогічно алгебрі висловлень.
   1. всі пропозиційні змінні та елементарні висловлення є формулами;
   2. якщо A і B — формули, то вирази (слова) $(A\lor B),(A\land B),(\lnot A),(A\rightarrow B)$ також є формулами;
   3. інших формул, ніж побудовані за правилами 2.1 і 2.2 немає.

Аксіоми

В численні висловлень визначають такі схеми аксіом:

1. $A\rightarrow (B\rightarrow A)$
2. $(A\rightarrow B)\rightarrow ((A\rightarrow (B\rightarrow C))\rightarrow (A\rightarrow C))$
3. $(A\land B)\rightarrow A$
4. $(A\land B)\rightarrow B$
5. $(A\rightarrow B)\rightarrow ((A\rightarrow C)\rightarrow (A\rightarrow (B\land C)))$
6. $A\rightarrow (A\lor B)$
7. $B\rightarrow (A\lor B)$
8. $(A\rightarrow C)\rightarrow ((B\rightarrow C)\rightarrow ((A\lor B)\rightarrow C))$
9. $(A\rightarrow \lnot B)\rightarrow (B\rightarrow \lnot A)$
10. $\lnot \lnot A\rightarrow A$

Єдиним правилом виводу є:

${\frac {A\rightarrow B,A}{B}}$ (Modus ponens)

У даних схемах аксіом та правила виводу символи $A,B,C$ можна заміщувати усіма допустимими формулами, після чого і отримуються конкретні аксіоми.

Приклад виведення теореми

Користуючись поданими аксіомами і правилом виведення покажемо, що ($D\rightarrow D$) є теоремою в даній формальній системі для будь-якої формули $D$.

Приклад виводу
Номер	Формула	Спосіб одержання
1	$(D\rightarrow (D\rightarrow D))\rightarrow ((D\rightarrow ((D\rightarrow D)\rightarrow D))\rightarrow (D\rightarrow D))$	Аксіома 2 з заміною $A,B,C\,$ на $D,D\rightarrow D,D$ відповідно
2	$(D\rightarrow (D\rightarrow D))$	аксіома 1(заміна $A,B\,$ на $D\,$)
3	$((D\rightarrow ((D\rightarrow D)\rightarrow D))\rightarrow (D\rightarrow D))$	1, 2 і modus ponens.
4	$((D\rightarrow ((D\rightarrow D)\rightarrow D))$	аксіома 1(заміна $A,B\,$ на $D,D\rightarrow D$ відповідно)
5	$D\rightarrow D$	3, 4 і modus ponens.

Приклад 2 (аксіоми Лукашевича)

1. Алфавіт (елементи множини $\mathrm {A}$) числення висловлень складається з елементарних висловлень (пропозиційних змінних): $a,b,c,d,\dots ,x,y,z$ (можливо з індексами), логічними операціями є $\lnot ,\rightarrow ,$ .
2. Поняття формули визначається аналогічно алгебрі висловлень.
   1. всі пропозиційні змінні та елементарні висловлення є формулами;
   2. якщо A і B — формули, то вирази (слова) $(\lnot A),(A\rightarrow B)$ також є формулами;
   3. інших формул, ніж побудовані за правилами 2.1 і 2.2 немає.

Наступну просту систему аксіом запропонував польський логік Ян Лукашевич:

1. $(A\to (B\to A))$
2. $((A\to (B\to C))\to ((A\to B)\to (A\to C)))$
3. $((\neg A\to \neg B)\to (B\to A))$

Єдиним правилом виводу є:

${\frac {A\rightarrow B,A}{B}}$ (Modus ponens).

Як і у попередньому прикладі дані вирази є схемами аксіом.

Приклад виведення теореми

Користуючись аксіомами Лукасевича і правилом виведення покажемо, що ($D\rightarrow D$) є теоремою в даній формальній системі для будь-якої формули $D$.

Приклад виводу
Номер	Формула	Спосіб одержання
1	$(D\rightarrow ((D\rightarrow D)\rightarrow D))\rightarrow ((D\rightarrow (D\rightarrow D))\rightarrow (D\rightarrow D))$	Аксіома 2 з заміною $A,B,C\,$ на $D,D\rightarrow D,D$ відповідно
2	$D\rightarrow ((D\rightarrow D)\rightarrow D)$	аксіома 1(заміна $A,B\,$ на $D,D\rightarrow D,\,$ відповідно)
3	$(D\rightarrow (D\rightarrow D))\rightarrow (D\rightarrow D)$	1, 2 і modus ponens.
4	$D\rightarrow (D\rightarrow D)$	аксіома 1(заміна $A,B\,$ на $D$ )
5	$D\rightarrow D$	3, 4 і modus ponens.

Семантика

У поданих вище формальних системах атомарні формули і оператори можуть фактично мати довільну природу. Для логіки важливе значення має інтерпретація цих символів.

Інтерпретація визначається заданням істинності тобто наданням кожній атомарній формулі одного із значень 1(«Істина») чи 0(«Хиба»), а також визначенням операторів як булевих функцій від своїх операндів.

Найчастіше вживані оператори задаються за допомогою таблиць істинності:

${\begin{array}{|c||c|}p&\neg p\\\hline 1&0\\0&1\\\hline \end{array}}$

${\begin{array}{|c|c||c|}p&q&p\land q\\\hline 1&1&1\\1&0&0\\0&1&0\\0&0&0\\\hline \end{array}}$

${\begin{array}{|c|c||c|}p&q&p\lor q\\\hline 1&1&1\\1&0&1\\0&1&1\\0&0&0\\\hline \end{array}}$

${\begin{array}{|c|c||c|}p&q&p\to q\\\hline 1&1&1\\1&0&0\\0&1&1\\0&0&1\\\hline \end{array}}$

${\begin{array}{|c|c||c|}p&q&p\land q\\\hline 1&1&1\\1&0&0\\0&1&0\\0&0&1\\\hline \end{array}}$

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

${\begin{array}{|c|c|c||c|c|c|c|}p&q&r&(p\lor q)&\neg (p\lor q)&(p\to r)&\neg (p\lor q)\to (p\to r)\\\hline 1&1&1&1&0&1&1\\1&1&0&1&0&0&1\\1&0&1&1&0&1&1\\1&0&0&1&0&0&1\\0&1&1&1&0&1&1\\0&1&0&1&0&1&1\\0&0&1&0&1&1&1\\0&0&0&0&1&1&1\\\hline \end{array}}$

Якщо для деякого задання істинності $I\;$ формула $A\;$ набуває значення 1, то кажуть, що формула $A\;$ задовольняє задання $I\;$. Формула, що задовольняє усі можливі задання істинності (як формула $\neg (p\lor q)\to (p\to r)$ з прикладу) називається тавтологією. Якщо $\Sigma \;$ — деяка множина формул то кажуть, що дана множина задовольняє задання істинності, якщо це задання задовольняє кожна формула цієї множини. Якщо для деякої формули $A\;$ з того, що множина $\Sigma \;$ задовольняє заданню істинності випливає що $A\;$ задовольняє цьому заданню то формула $A\;$ називається логічним наслідком множини $\Sigma \;$(позначається $\Sigma \vDash A$). У випадку якщо множина $\Sigma \;$ є пустою, формула є тавтологією.

Основні проблеми числення висловлень

Для обґрунтування будь-якої аксіоматичної теорії необхідно розглянути наступні 4 проблеми:

1. Несуперечливості
2. Повноти
3. Незалежності
4. Розв'язності

Проблема несуперечливості

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

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

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

Формальна аксіоматична теорія числення висловлень називається внутрішньо несуперечливою, якщо в цій теорії не можна довести деяку теорему (формулу) разом з її запереченням.

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

Теорема: Формальна аксіоматична теорія числення висловлень є несуперечливою відносно своєї моделі алгебри висловлень.

Наслідок:

1. Числення висловлень – внутрішньо-несуперечлива теорія.
2. Числення висловлень – синтаксично-несуперечлива теорія.

Теорема: Формальна аксіоматична теорія числення висловлень є категоричною.

Проблема повноти

Формальна аксіоматична теорія числення висловлень називається повною у вузькому розумінні, якщо приєднання до системи аксіом цієї теорії хоча б однієї формули, яка не є теоремою веде до того, що теорія стає внутрішньо-суперечливою.

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

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

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

Теорема: Числення висловлень – це формальна аксіоматична теорія, повна у вузькому розумінні.

Проблема незалежності

Означення: Нехай задано деяку формальну аксіоматичну теорію, говорять, що деяка аксіома цієї теорії є незалежною, якщо її не можна довести методами самої теорії, як теорему. Система аксіом формальної аксіоматичної теорії називається незалежною системою аксіом, якщо всі аксіоми є незалежними.

Теорема: Система аксіом числення висловлень є незалежною.

Доведення: Для доведення незалежності деякої аксіоми числення висловлень використовують наступний підхід: будують таку модель формальної аксіоматичної теорії, в якій справджуються всі аксіоми окрім даної. Якщо доводиться, що така модель ізоморфна стандартній моделі формальної аксіоматичної теорії, то робиться висновок, що аксіома не є незалежною, якщо ж такого ізоморфізму немає – незалежна.

Приклад: Як модель формальної аксіоматичної теорії візьмемо

a∧b ≡ b, все інше не змінюємо, покажемо, що ІІ₂ і ІІ₃ справджуються, а ІІ₁ ні.

ІІ₂  a∧b → b

|- b → b

ІІ₃  (a → b) → (( a→ c ) → ( a → b∧c ))

|-  ( a→ b ) → (( a → c ) → ( a → c))

ІІ₁ a∧b → a

b → a

Доведено

Наслідок: Система аксіом числення висловлень є незалежною.

Проблема розв’язності

Полягає в тому щоб довести існування алгоритму, який для будь-якої формули числення висловлень визначає чи можна її довести чи ні.

Теорема: Проблема розв`язності числення висловлень є розв'язною.

Теорема 1: Будь-яка тотожно істинна формула алгебри висловлень є теоремою числення висловлень.

Доведення: Нехай A - довільна формула числення числення висловлень. Побудуємо для неї таблицю істинності і розглянемо її останній стовпчик. Якщо він містить лише одиниці, то A - тотожно істинна формула і за теоремою 1 є теоремою числення висловлень. В іншому випадку (останній стовпчик таблиці істинності містить хоча б один нуль), A - не тавтологія і значить, A не є теоремою.

Див. також

• Математична логіка
• Предикатна логіка
• Булева алгебра
• Логіка першого порядку
• Числення секвенцій
• Кон'юнктивна нормальна форма
• Диз'юнктивна нормальна форма
• Логічний сполучник
• Основні проблеми числення висловлень
• Символічна логіка

Джерела

• Дрозд Ю. А. (2005). Основи математичної логіки (PDF). Київ: ВПЦ "Київський університет". с. 96. (укр.)
• Вітенько І. В. Математична логіка: Курс лекцій. — Ужгород : УжДУ, 1971. — 224 с.(укр.)
• Хромой В. Я. Математична логіка. — Київ : Вища школа, 1983. — 208 с.(укр.)
• Безущак О. О., Ганюшкін О. Г. Математична логіка: Навчальний посібник. — Київ : ВПЦ "Київський університет", 2023. — 143 с.(укр.)
• Прийма С.М. Математична логіка і теорія алгоритмів: Навчальний посібник – Мелітополь: ТОВ „Видавничий будинок ММД”, 2008. - 134 с.
• Гасяк О.С. Формальна логіка : короткий словник-довідник. – Чернівці : Чернівецький нац. ун-т, 2014. – 200 с.
• Логічні числення // Філософський енциклопедичний словник / В. І. Шинкарук (гол. редкол.) та ін ; Інститут філософії імені Григорія Сковороди НАН України. — Київ : Абрис, 2002. — 742 с. — 1000 екз. — ББК 87я2. — ISBN 966-531-128-X.
• Числення висловлювань // ФЕС, с.714
• Матвієнко М.П., Шаповалов С.П. Математична логіка та теорія алгоритмів. Навчальний посібник. – К.: Видавництво Ліра-К, 2015. – 212 с.
• Hilbert D., Ackermann W. Principles of Mathematical Logic. — NY: : Chelsea Pub, 1950. — 172 с.(англ.)
• Stephen C. Kleene. Mathematical logic. — John Wiley & Sons, 1967. — 398 с.(англ.)
• E. Mendelson. Introduction to Mathematical Logic. — London : Chapman & Hall, 1964. — 440 с.(англ.)
• Herbert D. Enderton. A Mathematical Introduction to Logic. — Harcourt/Academic Press, 2002. — 317 с.(англ.)
• A. G. Hamilton Logic for Mathematicians, Cambridge University Press, Cambridge UK 1978 ISBN 0-521-21838-1.

Посилання

• УРЕ