Loading AI tools
З Вікіпедії, вільної енциклопедії
Чи́слення висло́влень (логіка висловлень, пропозиційна логіка, англ. propositional calculus) — формальна система в математичній логіці, в якій формули, що відповідають висловленням, можуть утворюватись шляхом з'єднання простих висловлень із допомогою логічних операцій, та система правил виводу, які дозволяють визначати певні формули як «теореми» формальної системи.
Численням висловлень є формальна система , де:
Мовою числення висловлень є множина формул, що визначаються рекурсивно за допомогою наступних правил:
Нехай деяка множина формул , а — деяка задана формула, то кажуть, що формула виводиться з множини формул (позначається ), якщо існує така скінченна послідовність формул де для кожної формули :
Якщо при цьому множина — пуста (формула виводиться лише за допомогою аксіом і правил виводу), то формула називається теоремою (для цього використовується позначення ).
В численні висловлень визначають такі схеми аксіом:
Єдиним правилом виводу є:
У даних схемах аксіом та правила виводу символи можна заміщувати усіма допустимими формулами, після чого і отримуються конкретні аксіоми.
Користуючись поданими аксіомами і правилом виведення покажемо, що () є теоремою в даній формальній системі для будь-якої формули .
Приклад виводу | ||
---|---|---|
Номер | Формула | Спосіб одержання |
1 | Аксіома 2 з заміною на відповідно | |
2 | аксіома 1(заміна на ) | |
3 | 1, 2 і modus ponens. | |
4 | аксіома 1(заміна на відповідно) | |
5 | 3, 4 і modus ponens. |
Наступну просту систему аксіом запропонував польський логік Ян Лукашевич:
Єдиним правилом виводу є:
(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 не є теоремою.
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.