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

Матеріал з Вікіпедії — вільної енциклопедії.
(Перенаправлено з Логіка висловлень)
Перейти до навігації Перейти до пошуку

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

Формальне визначення[ред. | ред. код]

Численням висловлень є формальна система , де:

У цьому розбитті є множина операторів арності (також позначено ).
Найчастіше використовуються оператори:
  • Множина є скінченною множиною правил виводу, що дозволяють одержувати одні формули з інших.
  • Множина є скінченною множиною, елементи якої називаються аксіомами. В окремих прикладах дана множина може бути пустою.

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

  1. всі елементи множини є формулами;
  2. якщо є формулами та , тоді теж є формулою.
  3. інших формул, ніж побудовані за правилами 1 і 2 немає.

Виведення формул і теорем[ред. | ред. код]

Нехай деяка множина формул , а  — деяка задана формула, то кажуть, що формула виводиться з множини формул (позначається ), якщо існує така скінченна послідовність формул де для кожної формули :

  1. є аксіомою, або
  2. належить множині або
  3. виводиться з попередніх формул послідовності за допомогою котрогось із правил виводу.

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

Приклади аксіоматики[ред. | ред. код]

Приклад 1[ред. | ред. код]

  1. Алфавіт (елементи множини ) числення висловлень складається з елементарних висловлень (пропозиційних змінних): (можливо з індексами), логічними операціями є .
  2. Поняття формули визначається аналогічно алгебрі висловлень.
    1. всі пропозиційні змінні та елементарні висловлення є формулами;
    2. якщо A і B — формули, то вирази (слова) також є формулами;
    3. інших формул, ніж побудовані за правилами 2.1 і 2.2 немає.

Аксіоми[ред. | ред. код]

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

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

(Modus ponens)

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

Приклад виведення теореми[ред. | ред. код]

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

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

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

  1. Алфавіт (елементи множини ) числення висловлень складається з елементарних висловлень (пропозиційних змінних): (можливо з індексами), логічними операціями є .
  2. Поняття формули визначається аналогічно алгебрі висловлень.
    1. всі пропозиційні змінні та елементарні висловлення є формулами;
    2. якщо A і B — формули, то вирази (слова) також є формулами;
    3. інших формул, ніж побудовані за правилами 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 проблеми:

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

Проблема несуперечливості[ред. | ред. код]

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

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

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

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

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

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

Наслідок:

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

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

Проблема повноти[ред. | ред. код]

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

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

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

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

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

Проблема незалежності[ред. | ред. код]

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

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

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

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

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

ІІa∧b → b

|- b → b

ІІ(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 не є теоремою.

Див. також[ред. | ред. код]

Джерела[ред. | ред. код]

  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.

Література[ред. | ред. код]

Посилання[ред. | ред. код]