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

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

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

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

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

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

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

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

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

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

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

Приклад 1 ред.

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

Аксіоми ред.

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

  1.  
  2.  
  3.  
  4.  
  5.  
  6.  
  7.  
  8.  
  9.  
  10.  

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

  (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 немає.

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

  1.  
  2.  
  3.  

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

  (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.

Література ред.

Посилання ред.