Перегляд вихідного коду сторінки Нормальна форма формули у логіці предикатів

<!-- -->
'''Нормальна форма формули у [[Предикатна логіка|логіці предикатів]]''' — це формула, яка містить лише операції [[Кон'юнкція|кон'юнкції]], [[Диз'юнкція|диз'юнкції]] та кванторні операції, а операція [[заперечення]] відноситься до елементарних формул.

З допомогою рівностей алгебри висловлень й логіки предикатів кожну формулу логіки предикатів можна привести до нормальної формули.<ref>{{Cite web |url=http://primat.org/publ/spravochnye_materialy/matematicheskaja_logika_predvarennaja_normalnaja_forma/37-1-0-738 |title=Математическая логика. Предваренная нормальная форма (рус.) |accessdate=20 листопада 2014 |archive-date=29 листопада 2014 |archive-url=https://web.archive.org/web/20141129035737/http://primat.org/publ/spravochnye_materialy/matematicheskaja_logika_predvarennaja_normalnaja_forma/37-1-0-738 }}</ref>
== Теорема про нормальну форму ==
Теорема:
Кожна формула логіки предикатів має нормальну форму.

Доведення:
Перш ніж доводити теорему, встановимо 4 равносильності, які необхідні нам надалі. В них передбачається, що формула Н не містить вільної змінної х:
# <math>\forall xW(x) \lor H = \forall x(W(x) \lor H)</math>
# <math>\exists xW(x) \lor H = \exists x(W(x) \lor H)</math>
# <math>\forall xW(x) \land H = \forall x(W(x) \land H)</math>
# <math>\exists xW(x) \land H = \exists x(W(x) \land H)</math>
                     
Встановимо першу з цих рівносильностей. Решта - аналогічно.

 
Нехай <math>\forall xW(x) \lor H </math> істинна для деякої області М. Тоді на М істинно чи <math>\forall xW(x)</math>, чи <math>H</math>. В першому випадку <math>W(x)</math> тотожно істинний на М предикат і через те, що <math>H</math> не містить х, <math>W(x) \lor H </math> теж тотожно істинний на М предикат, і тоді <math>\forall xW(x) \lor H</math> - істинно. У другому випадку, якщо істинно <math>H</math>, то істинно і <math>W(x) \lor H </math> незалежно від х, а значить <math>\forall x</math> з М.

Нехай тепер <math>\forall xW(x) \lor H </math> хибно. Тоді <math>\forall xW(x)</math> і <math>H</math> хибні. Тобто існує <math>{x_0}\in  M</math>, такий що <math>W(x_0)</math> хибно. Але тоді <math>W(x) \lor H </math> хибно, бо <math>\forall xW(x) \lor H </math> хибно.


Доведемо тепер теорему методом індукції. Для елементарних формул наше твердження істинне, бо вони самі є нормальними формами. Будь-яку формулу можна записати, використовуючи операції <math>\land, \lor, \neg,</math>, тому достатньо показати, що якщо <math>W_1</math> і <math>W_2</math> мають нормальні форми, то і <math>\neg W_1</math>, <math>W_1 \land W_2</math>, <math>W_1 \lor W_2</math> теж мають нормальні форми. Нехай <math>W_1</math> і <math>W_2</math> мають нормальні форми <math>\widetilde {W_1}</math> і <math>\widetilde {W_2}</math>, де


<math>\widetilde {W_1}=\forall x_1 ... \forall x_i \exists x_{i+1} ... \exists x_n V_1 (x_1 ... x_n)</math>

<math>\widetilde {W_1}=\exists y_1 ... \exists y_i \forall y_{i+1} ...  y_m V_2 (y_1 ... y_m)</math>

   
Тоді формулі <math>W_1 \lor W_2</math> рівносильна формула <math>\widetilde {W_1} \lor \widetilde {W_2}</math>, яка може завжди бути приведена до нормальної форми з використанням рівностей 1 – 2:


<math>\widetilde {W_1} \lor \widetilde {W_2}=\forall x_1[\forall x_2 ... \forall x_i \exists x_{i+1} ... \exists x_n V_1 (x_1 ... x_n) \lor \exists y_1 ... \exists y_i \forall y_{i+1} ...  y_m V_2 (y_1 ... y_m)]=\forall x_1 ... \forall x_i \exists x_{i+1} ... \exists x_n \exists y_1 ... \exists y_i \forall y_{i+1} ...  y_m [V_1 (x_1 ... x_n) \lor V_2 (y_1 ... y_m)] </math>
          

Таким чином, отримана нормальна форма формули <math>W_1 \lor W_2</math>. Аналогічно, з рівностей 3,4 отримаємо, що можна побудувати нормальну форму і для <math>W_1 \land W_2</math>. Нарешті, якщо відома нормальна форма <math>\widetilde {W_1}</math> формули <math>{W_1}</math>, то нормальна форма <math>\overline {W_1}</math> має вигляд:



<math>\overline {W_1}=\overline {\forall x_1 ... \forall x_i \exists x_{i+1} ... \exists x_n V_1 (x_1 ... x_n)}=\exists x_1 ... \exists x_i \forall x_{i+1} ... \forall x_n \overline {V_1 (x_1 ... x_n)}</math>
                      

Таким чином встановлено, що будь-яка формула логіки предикатів має нормальну форму.

== Алгоритм приведення формули до нормальної форми ==

Для приведення формули до нормальної форми потрібно виконати наступні операції:

# виключити операції <math>\rightarrow</math>, ~, якщо вони є;
# зменшити область знаків заперечення;
# перейменувати змінні так, щоб можна було винести квантори в початок формули.


== Приклад ==


<math>\neg (\forall xP(x) \rightarrow \exists xQ(x)) = \neg (\neg (\forall xP(x)) \lor \exists xQ(x)) = \forall xP(x) \land \forall x \neg  Q(x) = \forall xP(x) \land \forall y \neg  Q(y) = \forall x \forall y P(x) \neg  Q(y)</math>


== Примітки ==
<!--- Смотрите в [[Википедия:Сноски]] примеры использования тэгов <ref> </ref> -->
{{примітки}}


== Посилання ==
* [http://pgap.chat.ru/zap/zap136.htm Алгоритмы приведения к нормальным формам (рус.)] {{Webarchive|url=https://web.archive.org/web/20140116014113/http://pgap.chat.ru/zap/zap136.htm |date=16 січня 2014 }}
* [http://www.life-prog.ru/1_19090_ponyatie-formuli-logiki-predikatov-ekvivalentnie-sootnosheniya-prefiksnaya-normalnaya-forma.html Префиксная нормальная форма (рус.)] {{Webarchive|url=https://web.archive.org/web/20141129034918/http://www.life-prog.ru/1_19090_ponyatie-formuli-logiki-predikatov-ekvivalentnie-sootnosheniya-prefiksnaya-normalnaya-forma.html |date=29 листопада 2014 }}
* [http://itosvita.ucoz.ua/logo/pic_VUZ/chap/Diskretnaya_matematica_01.pdf Основи логіки предикатів] {{Webarchive|url=https://web.archive.org/web/20141129040438/http://itosvita.ucoz.ua/logo/pic_VUZ/chap/Diskretnaya_matematica_01.pdf |date=29 листопада 2014 }}



<!--- Категории --->

[[Категорія:Математична логіка]]