Перегляд вихідного коду сторінки Числення висловлень

{{Правила перетворення}}

{{Приєднати з|Логіка висловлювань|обговорення=Обговорення:Логіка висловлювань|дата=грудень 2014}}
{{Приєднати з|Основні проблеми числення висловлень|дата=вересень 2015}}

'''Чи́слення висло́влень''' (логіка висловлень, пропозиційна логіка, {{lang-en|propositional logic}})&nbsp;— [[формальна система]] в [[математична логіка|математичній логіці]], в якій [[формула|формули]], що відповідають висловленням, можуть утворюватись шляхом з'єднання простих висловлень із допомогою [[логічний сполучник|логічних операцій]], та система [[правила виводу|правил виводу]], які дозволяють визначати певні формули як «[[теорема|теореми]]» формальної системи.

== Формальне визначення ==
Численням висловлень є формальна система <math>\mathcal{L} = \mathcal{L} \left( \Alpha,\ \Omega,\ \Zeta,\ \Iota \right)</math>, де:

* [[Множина]] <math>\ \Alpha</math> є [[скінченна множина|скінченною множиною]] ''символів висловлень'' (чи ''елементарних висловлювань'', ''пропозиційних змінних'', ''атомарних формул''). Для зображення атомарних формул нижче використовуються малі [[латинська абетка|латинські літери]]. За потреби можна використовувати і [[зліченна множина|зліченну множину]] символів.
* Множина <math>\ \Omega</math> — скінченна множина [[логічний сполучник|логічних зв'язок (логічних операторів)]]. Дану множину можна [[розбиття множини|розбити]] на підмножини:

:::<math>\Omega = \Omega_0 \cup \Omega_1 \cup \ldots \cup \Omega_j \cup \ldots \cup \Omega_m.</math>

:У цьому розбитті <math>\ \Omega_j</math> є множина операторів [[арність|арності]] <math>j</math> (також позначено <math>\Omega_0 = \{ 0, 1 \}.\,\!</math>).

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

:::<math>\Omega_1 = \{ \lnot \},</math>

:::<math>\Omega_2 \subseteq \{ \land, \lor, \rightarrow, \leftrightarrow \}.</math>

* Множина <math>\ \Zeta</math> є скінченною множиною [[правила виводу|правил виводу]], що дозволяють одержувати одні формули з інших.

* Множина <math>\ \Iota</math> є скінченною множиною, елементи якої називаються [[аксіома]]ми. В окремих прикладах дана множина може бути пустою.

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

# всі елементи множини <math>\ \Alpha</math> є формулами;
# якщо <math>\ p_1, p_2, \ldots, p_j</math> є формулами та <math>f \in \Omega_j</math>, тоді <math>\left( f(p_1, p_2, \ldots, p_j) \right)</math> теж є формулою.
# інших формул, ніж побудовані за правилами 1 і 2 немає.

=== Виведення формул і теорем ===
Нехай <math>\Sigma\;</math> деяка множина формул <math>\mathcal{L}</math>, а <math>A</math>&nbsp;— деяка задана формула, то кажуть, що формула <math>A</math> виводиться з множини формул <math>\Sigma\;</math> (позначається <math>\Sigma \vdash A</math>), якщо існує така [[Послідовність (математика)#Скінченна послідовність|скінченна послідовність]] формул <math>A_1, A_2 \ldots A_n = A,</math> де для кожної формули <math>A_i</math>:
# <math>A_i</math> є аксіомою, або
# <math>A_i</math> належить множині <math>\Sigma\;</math> або
# <math>A_i</math> виводиться з попередніх формул послідовності за допомогою котрогось із правил виводу.

Якщо при цьому множина <math>\Sigma\;</math>&nbsp;— пуста (формула <math>A</math> виводиться лише за допомогою аксіом і правил виводу), то формула <math>A</math> називається теоремою (для цього використовується позначення <math>\vdash A</math>).

== Приклади аксіоматики ==
=== Приклад 1 ===

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

==== Аксіоми ====

В численні висловлень визначають такі схеми [[аксіома|аксіом]]:
# <math>A \rightarrow(B\rightarrow A)</math>
# <math>(A \rightarrow B)\rightarrow ((A\rightarrow(B\rightarrow C))\rightarrow (A\rightarrow C))</math>
# <math>(A\land B)\rightarrow A</math>
# <math>(A\land B)\rightarrow B</math>
# <math>(A\rightarrow B)\rightarrow ((A\rightarrow C)\rightarrow (A\rightarrow (B\land C)))</math>
# <math>A\rightarrow (A\lor B)</math>
# <math>B\rightarrow (A\lor B)</math>
# <math>(A\rightarrow C)\rightarrow ((B\rightarrow C)\rightarrow((A\lor B)\rightarrow C))</math>
# <math>(A\rightarrow \lnot B)\rightarrow (B\rightarrow \lnot A)</math>
# <math>\lnot\lnot A\rightarrow A</math>
Єдиним правилом виводу є:

<math>\frac{A \rightarrow B, A}{B}</math> (''[[Modus ponens]]'')

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

==== Приклад виведення теореми ====
Користуючись поданими аксіомами і правилом виведення покажемо, що (<math>D\rightarrow D</math>) є теоремою в даній формальній системі для будь-якої формули <math>D</math>.

{| align="center" border="1" cellpadding="6" cellspacing="1" width:100%"
! align="center"  colspan="3" | Приклад виводу
|- 
! Номер
! Формула
! Спосіб одержання
|-
| 1 || <math>(D \rightarrow (D \rightarrow D))\rightarrow ((D\rightarrow((D \rightarrow D)\rightarrow D))\rightarrow (D\rightarrow D))</math> || Аксіома 2 з заміною <math>A,B,C\,</math> на <math>D,D \rightarrow D, D</math> відповідно
|-
| 2 || <math>(D \rightarrow (D \rightarrow D))</math> ||  аксіома 1(заміна <math>A,B\,</math> на <math>D\,</math>) 
|-
| 3 || <math>((D\rightarrow((D \rightarrow D)\rightarrow D))\rightarrow (D\rightarrow D))</math> || 1, 2 і modus ponens.
|-
| 4 || <math>((D\rightarrow((D \rightarrow D)\rightarrow D))</math> || аксіома 1(заміна <math>A,B\,</math> на <math>D,D \rightarrow D</math> відповідно)
|-
| 5 || <math>D\rightarrow D</math> || 3, 4 і modus ponens.
|}

=== Приклад 2 (аксіоми Лукашевича) ===
# Алфавіт (елементи множини <math>\Alpha</math>) числення висловлень складається з елементарних висловлень (пропозиційних змінних): <math>a,b,c,d,\dots,x,y,z</math> (можливо з індексами), логічними операціями є <math>\lnot , \rightarrow,</math> .
# Поняття формули визначається аналогічно алгебрі висловлень.
## всі пропозиційні змінні та елементарні висловлення є формулами;
## якщо A і B&nbsp;— формули, то вирази (слова) <math> (\lnot A), (A\rightarrow B)</math> також є формулами;
## інших формул, ніж побудовані за правилами 2.1 і 2.2 немає.

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

# <math>(A \to (B \to A))</math>
# <math>((A \to (B \to C)) \to ((A \to B) \to (A \to C)))</math>
# <math>((\neg A \to \neg B) \to (B \to A))</math>
Єдиним правилом виводу є:

<math>\frac{A \rightarrow B, A}{B}</math> (''[[Modus ponens]]'').

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

=== Приклад виведення теореми ===
Користуючись аксіомами Лукасевича і правилом виведення покажемо, що (<math>D\rightarrow D</math>) є теоремою в даній формальній системі для будь-якої формули <math>D</math>.

{| align="center" border="1" cellpadding="6" cellspacing="1" width:100%"
! align="center"  colspan="3" | Приклад виводу
|- 
! Номер
! Формула
! Спосіб одержання
|-
| 1 || <math>(D \rightarrow ((D \rightarrow D) \rightarrow D)) \rightarrow ((D \rightarrow (D \rightarrow D)) \rightarrow (D \rightarrow D))</math> || Аксіома 2 з заміною <math>A,B,C\,</math> на <math>D,D \rightarrow D, D</math> відповідно
|-
| 2 || <math>D \rightarrow ((D \rightarrow D) \rightarrow D)</math> ||  аксіома 1(заміна <math>A,B\,</math> на <math>D,D \rightarrow D,\,</math> відповідно) 
|-
| 3 || <math>(D \rightarrow (D \rightarrow D)) \rightarrow (D \rightarrow D)</math> || 1, 2 і modus ponens.
|-
| 4 || <math>D \rightarrow (D \rightarrow D)</math> || аксіома 1(заміна <math>A,B\,</math> на <math>D</math> )
|-
| 5 || <math>D\rightarrow D</math> || 3, 4 і modus ponens.
|}

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

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

Найчастіше вживані оператори задаються за допомогою таблиць істинності:
{| width="70%"
|- valign="top" align="center"
|
<math>\begin{array}{|c||c|}
      p & \neg p \\
      \hline
      1 & 0 \\
      0 & 1 \\
      \hline
   \end{array}</math>
|
<math>\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}</math>
|
<math>\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}</math>
|
<math>\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}</math>
|
<math>\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}</math>
|}

Зважаючи на спосіб побудови формул, кожна формула при деякому заданню істинності отримує певне значення 0 або 1. Значення найпростіших формул для різних завдань істинності можна обчислювати за допомогою [[таблиця істинності|таблиць істинності]]. Наприклад:

:<math>
\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}
</math>

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

== Основні проблеми числення висловлень ==
{{main|Основні проблеми числення висловлень}}

Для обґрунтування будь-якої аксіоматичної теорії необхідно розглянути наступні 4 проблеми:
# Несуперечливості
# Повноти
# Незалежності
# Розв'язності

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

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

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

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

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

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

'''''Наслідок: '''''
# Числення висловлень – внутрішньо-несуперечлива теорія.
# Числення висловлень – синтаксично-несуперечлива теорія.
'''''Теорема:''''' Формальна аксіоматична теорія числення висловлень є категоричною.

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

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

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

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

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

Система аксіом формальної аксіоматичної теорії називається незалежною системою аксіом, якщо всі аксіоми є незалежними.

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

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

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

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

ІІ<sub>2  </sub>a∧b → b

|- b → b

ІІ<sub>3  </sub>(a → b) → (( a→ c ) → ( a → b∧c ))

|-  ( a→ b ) → (( a → c ) → ( a → c))

ІІ<sub>1 </sub>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 с.
* Логічні числення // {{ФЕС}}
* Числення висловлювань // [[ФЕС]], с.714
* Матвієнко М.П., Шаповалов С.П. Математична логіка та теорія алгоритмів. Навчальний посібник. – К.: Видавництво Ліра-К, 2015. – 212 с.

== Посилання ==
*[http://leksika.com.ua/10800511/ure/logika_vislovlyuvan УРЕ]
{{Класична логіка}}
{{Математична логіка}}

[[Категорія:Класична логіка]]
[[Категорія:Числення висловлень| ]]
[[Категорія:Дискретна математика]]
[[Категорія:Логічні операції]]
[[Категорія:Системи формальної логіки]]