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

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

Логічні сполучники
NOT ${\displaystyle \neg A,-A,{\overline {A}},\sim A}$ AND ${\displaystyle A\land B,A\cdot B,AB,A\&B,A\&\&B}$ OR ${\displaystyle A\lor B,A+B,A\mid B,A\parallel B}$ XOR ${\displaystyle A{\underline {\lor }}B,A\oplus B}$ еквівалентність ${\displaystyle A\equiv B,A\Leftrightarrow B,A\leftrightarrow B}$ нееквівалентність ${\displaystyle A\not \equiv B,A\not \Leftrightarrow B,A\nleftrightarrow B}$ імплікація ${\displaystyle A\Rightarrow B,A\supset B,A\rightarrow B}$ обернення ${\displaystyle A\Leftarrow B,A\subset B,A\leftarrow B}$ NAND ${\displaystyle A{\overline {\land }}B,A\uparrow B,A\mid B,{\overline {A\cdot B}}}$ NOR ${\displaystyle A{\overline {\lor }}B,A\downarrow B,{\overline {A+B}}}$
Зв'язані поняття
Числення висловлень Предикатна логіка Булева алгебра Таблиця істинності Булева функція Функціональна повнота
Застосування
Логічний вентиль Мова програмування Математична логіка Філософія логіки
Категорія
п о р

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

${\displaystyle {\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}}}$

${\displaystyle {\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}}}$

${\displaystyle {\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}}}$

${\displaystyle {\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. Значення найпростіших формул для різних завдань істинності можна обчислювати за допомогою таблиць істинності. Наприклад:

${\displaystyle {\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}}}$

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

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

1. Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947
2. Клини С. К. Введение в метаматематику. М., 1957
3. Мендельсон Э. Введение в математическую логику. М., 1976
4. Enderton, H. B., A Mathematical Introduction to Logic. Harcourt/Academic Press 2002. ISBN 0-12-238452-0
5. A. G. Hamilton Logic for Mathematicians, Cambridge University Press, Cambridge UK 1978 ISBN 0-521-21838-1.

• Прийма С.М. Математична логіка і теорія алгоритмів: Навчальний посібник – Мелітополь: ТОВ „Видавничий будинок ММД”, 2008. - 134 с.
• Гасяк О.С. Формальна логіка : короткий словник-довідник. – Чернівці : Чернівецький нац. ун-т, 2014. – 200 с.
• Логічні числення // Філософський енциклопедичний словник / В. І. Шинкарук (гол. редкол.) та ін. — Київ : Інститут філософії імені Григорія Сковороди НАН України : Абрис, 2002. — 742 с. — 1000 екз. — ББК 87я2. — ISBN 966-531-128-X.
• Числення висловлювань // ФЕС, с.714
• Матвієнко М.П., Шаповалов С.П. Математична логіка та теорія алгоритмів. Навчальний посібник. – К.: Видавництво Ліра-К, 2015. – 212 с.

• УРЕ