Чи́слення висло́влень (логіка висловлень, пропозиційна логіка, англ. propositional calculus) — формальна система в математичній логіці, в якій формули, що відповідають висловленням, можуть утворюватись шляхом з'єднання простих висловлень із допомогою логічних операцій, та система правил виводу, які дозволяють визначати певні формули як «теореми» формальної системи.
Логічні сполучники | ||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
||||||||||||||||||||
Зв'язані поняття | ||||||||||||||||||||
Застосування | ||||||||||||||||||||
Категорія | ||||||||||||||||||||
Численням висловлень є формальна система , де:
- Множина є скінченною множиною символів висловлень (чи елементарних висловлювань, пропозиційних змінних, атомарних формул). Для зображення атомарних формул нижче використовуються малі латинські літери. За потреби можна використовувати і зліченну множину символів.
- Множина — скінченна множина логічних сполучників (логічних операторів). Дану множину можна розбити на підмножини:
- У цьому розбитті є множина операторів арності (також позначено ).
- Найчастіше використовуються оператори:
- Множина є скінченною множиною правил виводу, що дозволяють одержувати одні формули з інших.
- Множина є скінченною множиною, елементи якої називаються аксіомами. В окремих прикладах дана множина може бути пустою.
Мовою числення висловлень є множина формул, що визначаються рекурсивно за допомогою наступних правил:
- всі елементи множини є формулами;
- якщо є формулами та , тоді теж є формулою.
- інших формул, ніж побудовані за правилами 1 і 2 немає.
Нехай деяка множина формул , а — деяка задана формула, то кажуть, що формула виводиться з множини формул (позначається ), якщо існує така скінченна послідовність формул де для кожної формули :
- є аксіомою, або
- належить множині або
- виводиться з попередніх формул послідовності за допомогою котрогось із правил виводу.
Якщо при цьому множина — пуста (формула виводиться лише за допомогою аксіом і правил виводу), то формула називається теоремою (для цього використовується позначення ).
- Алфавіт (елементи множини ) числення висловлень складається з елементарних висловлень (пропозиційних змінних): (можливо з індексами), логічними операціями є .
- Поняття формули визначається аналогічно алгебрі висловлень.
- всі пропозиційні змінні та елементарні висловлення є формулами;
- якщо A і B — формули, то вирази (слова) також є формулами;
- інших формул, ніж побудовані за правилами 2.1 і 2.2 немає.
В численні висловлень визначають такі схеми аксіом:
Єдиним правилом виводу є:
У даних схемах аксіом та правила виводу символи можна заміщувати усіма допустимими формулами, після чого і отримуються конкретні аксіоми.
Користуючись поданими аксіомами і правилом виведення покажемо, що () є теоремою в даній формальній системі для будь-якої формули .
Приклад виводу | ||
---|---|---|
Номер | Формула | Спосіб одержання |
1 | Аксіома 2 з заміною на відповідно | |
2 | аксіома 1(заміна на ) | |
3 | 1, 2 і modus ponens. | |
4 | аксіома 1(заміна на відповідно) | |
5 | 3, 4 і modus ponens. |
- Алфавіт (елементи множини ) числення висловлень складається з елементарних висловлень (пропозиційних змінних): (можливо з індексами), логічними операціями є .
- Поняття формули визначається аналогічно алгебрі висловлень.
- всі пропозиційні змінні та елементарні висловлення є формулами;
- якщо A і B — формули, то вирази (слова) також є формулами;
- інших формул, ніж побудовані за правилами 2.1 і 2.2 немає.
Наступну просту систему аксіом запропонував польський логік Ян Лукашевич:
Єдиним правилом виводу є:
(Modus ponens).
Як і у попередньому прикладі дані вирази є схемами аксіом.
Користуючись аксіомами Лукасевича і правилом виведення покажемо, що () є теоремою в даній формальній системі для будь-якої формули .
Приклад виводу | ||
---|---|---|
Номер | Формула | Спосіб одержання |
1 | Аксіома 2 з заміною на відповідно | |
2 | аксіома 1(заміна на відповідно) | |
3 | 1, 2 і modus ponens. | |
4 | аксіома 1(заміна на ) | |
5 | 3, 4 і modus ponens. |
У поданих вище формальних системах атомарні формули і оператори можуть фактично мати довільну природу. Для логіки важливе значення має інтерпретація цих символів.
Інтерпретація визначається заданням істинності тобто наданням кожній атомарній формулі одного із значень 1(«Істина») чи 0(«Хиба»), а також визначенням операторів як булевих функцій від своїх операндів.
Найчастіше вживані оператори задаються за допомогою таблиць істинності:
|
|
|
|
|
Зважаючи на спосіб побудови формул, кожна формула при деякому заданню істинності отримує певне значення 0 або 1. Значення найпростіших формул для різних завдань істинності можна обчислювати за допомогою таблиць істинності. Наприклад:
Якщо для деякого задання істинності формула набуває значення 1, то кажуть, що формула задовольняє задання . Формула, що задовольняє усі можливі задання істинності (як формула з прикладу) називається тавтологією. Якщо — деяка множина формул то кажуть, що дана множина задовольняє задання істинності, якщо це задання задовольняє кожна формула цієї множини. Якщо для деякої формули з того, що множина задовольняє заданню істинності випливає що задовольняє цьому заданню то формула називається логічним наслідком множини (позначається ). У випадку якщо множина є пустою, формула є тавтологією.
Для обґрунтування будь-якої аксіоматичної теорії необхідно розглянути наступні 4 проблеми:
- Несуперечливості
- Повноти
- Незалежності
- Розв'язності
Означення: Нехай задано деяку формальну аксіоматичну теорію. Говорять, що побудована модель цієї теорії, якщо всім символам алфавіту надано деякого конкретного змісту, який описує певну неформальну теорію і відношення між елементами цієї теорії.
Формальна аксіоматична теорія називається категоричною, якщо будь-які її 2 моделі ізоморфні між собою, тобто між ними можна встановити взаємно-однозначну відповідність.
Формальна аксіоматична теорія називається несуперечливою відносно своєї моделі, якщо будь-яка теорема, що доводиться в формальній теорії є істинним твердженням для моделі.
Формальна аксіоматична теорія числення висловлень називається внутрішньо несуперечливою, якщо в цій теорії не можна довести деяку теорему (формулу) разом з її запереченням.
Формальна аксіоматична теорія називається синтаксично несуперечливою якщо в ній існує хоча б якась формула, яка не є теоремою.
Теорема: Формальна аксіоматична теорія числення висловлень є несуперечливою відносно своєї моделі алгебри висловлень.
Наслідок:
- Числення висловлень – внутрішньо-несуперечлива теорія.
- Числення висловлень – синтаксично-несуперечлива теорія.
Теорема: Формальна аксіоматична теорія числення висловлень є категоричною.
Формальна аксіоматична теорія числення висловлень називається повною у вузькому розумінні, якщо приєднання до системи аксіом цієї теорії хоча б однієї формули, яка не є теоремою веде до того, що теорія стає внутрішньо-суперечливою.
Формальна аксіоматична теорія числення висловлень є повною у широкому розумінні або повною відносно своєї моделі, якщо будь-яка формула істинна в моделі є теоремою в цій теорії, або якщо будь-яку тотожно істинну формулу можна довести.
Наслідок: Числення висловлень є повним. Справедливість цього твердження безпосередньо випливає з теореми. У математичній логіці існує й інше поняття повноти системи аксіом, що ґрунтується на неможливості доповнення системи аксіом будь-якою формулою, яку не можна вивести з даних аксіом.
Теорема: Формальна аксіоматична теорія числення висловлень є повною відносно своєї моделі алгебри висловлень.
Теорема: Числення висловлень – це формальна аксіоматична теорія, повна у вузькому розумінні.
Означення: Нехай задано деяку формальну аксіоматичну теорію, говорять, що деяка аксіома цієї теорії є незалежною, якщо її не можна довести методами самої теорії, як теорему. Система аксіом формальної аксіоматичної теорії називається незалежною системою аксіом, якщо всі аксіоми є незалежними.
Теорема: Система аксіом числення висловлень є незалежною.
Доведення: Для доведення незалежності деякої аксіоми числення висловлень використовують наступний підхід: будують таку модель формальної аксіоматичної теорії, в якій справджуються всі аксіоми окрім даної. Якщо доводиться, що така модель ізоморфна стандартній моделі формальної аксіоматичної теорії, то робиться висновок, що аксіома не є незалежною, якщо ж такого ізоморфізму немає – незалежна.
Приклад: Як модель формальної аксіоматичної теорії візьмемо
a∧b ≡ b, все інше не змінюємо, покажемо, що ІІ2 і ІІ3 справджуються, а ІІ1 ні.
ІІ2 a∧b → b
|- b → b
ІІ3 (a → b) → (( a→ c ) → ( a → b∧c ))
|- ( a→ b ) → (( a → c ) → ( a → c))
ІІ1 a∧b → a
b → a
Доведено
Наслідок: Система аксіом числення висловлень є незалежною.
Полягає в тому щоб довести існування алгоритму, який для будь-якої формули числення висловлень визначає чи можна її довести чи ні.
Теорема: Проблема розв`язності числення висловлень є розв'язною.
Теорема 1: Будь-яка тотожно істинна формула алгебри висловлень є теоремою числення висловлень.
Доведення: Нехай A - довільна формула числення числення висловлень. Побудуємо для неї таблицю істинності і розглянемо її останній стовпчик. Якщо він містить лише одиниці, то A - тотожно істинна формула і за теоремою 1 є теоремою числення висловлень. В іншому випадку (останній стовпчик таблиці істинності містить хоча б один нуль), A - не тавтологія і значить, A не є теоремою.
- Математична логіка
- Предикатна логіка
- Булева алгебра
- Логіка першого порядку
- Числення секвенцій
- Кон'юнктивна нормальна форма
- Диз'юнктивна нормальна форма
- Логічний сполучник
- Основні проблеми числення висловлень
- Символічна логіка
- Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947
- Клини С. К. Введение в метаматематику. М., 1957
- Мендельсон Э. Введение в математическую логику. М., 1976
- Enderton, H. B., A Mathematical Introduction to Logic. Harcourt/Academic Press 2002. ISBN 0-12-238452-0
- 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 с.