7. Правило існування:

введення вилучення

Г ├ А (у) . Г, х А (х) ├ С

х А (х) Г, А (у) ├ С ˙ У формулі вилучення квантора існування А (у) означає для деякого у F, а саме правило дозволяє вирішити, що х А (х) є істинним тоді і тільки тоді, коли відомий деякий елемент у, для якого істинне А (у).

У формулі вилучення квантора існування А (у) означає для деякого у F, а саме правило полягає в позначенні імені елемента у, для якого А (у) є істинне.

Усі розглянуті вище правила відповідають звичайним прийомам математичного міркування. Наприклад, у правилі існування вилучення квантора відповідає правилу одиничного вибору. Припустимо, що є х А (х) і необхідно вивести С. Оскільки є х таке, що А (х), то можна розглянути (вибрати) одне із таких х. Позначимо його через у. Це означає, що для цього у дійсне А (у). Таким чином, достатньо вивести формулу С із А (у). Аналогічно можна розглянути й інші правила.

8. Правило перейменування вільних змінних

У логіці предикатів у виведенні формули А (х), що містить вільні входження х, жодне з яких не знаходиться в області дії квантора за у, виходить вивідність А (х).

Приклад 4.1.1. Довести справедливість правила перейменування вільних змінних.

Розв’язання

а) А (х) – гіпотеза;

б) А (х) → ( В → А (х)) – аксіома АП1: тут як В можна обрати будь-яку довідну формулу, що не містить вільних входжень змінних х;

в) В → А (х) – МР, із а), б) ;

г) В → x А (х) – правило узагальнення із в) ;

д) x А (х) – наслідок з кроку г), оскільки В – істинна формула ;

у) А (у) – аксіома АП4 із д) .

9. Правило перейменування пов’язаних змінних

У логіці предикатів у виведенні x А (х) виходить вивідність y А (у), а у виведенні x А (х) – вивідність

y А (у) за умови, що А (х) не містить вільних входжень у, а містить вільні входження х, жодне з яких не входить до області дії квантора за у.

Приклад 4.1.2 Довести правило перейменування пов’язаних змінних для квантора загальності.

Розв’язання

а) x А (х) – гіпотеза ;

б) x А (х) → А (у) – аксіома АП4 ;

в) x А (х) → y А (у) – правило узагальнення із б) ;

г) x А (у) – МР із а), в) .

Приклад 4.1.3 Довести правило перейменування пов’язаних змінних для квантора існування.

Розв’язання

а) А (у) – гіпотеза;

б) А (у) → х А (х) – правило 7;

в) у А (у) → х А (х) – правило існування із а) і б);

г) х А (х) – МР із а) і в).

4.2. Випереджені нормальні форми

У логіці висловлювань були введені дві нормальні форми: кон’юнктивна і диз’юнктивна. В аксіоматичній системі логік вводиться третя нормальна форма, яку називають випередженою нормальною формою.

Означення 4.2.1. Формула Ф у логіці предикатів знаходиться у випередженій нормальній формі (ВНФ) тоді і тільки тоді, коли вона може бути зображена у вигляді ( )… ( ) (А), де ( ) є або ( х), або ( х) і всі різні для різних і = 1, …, п, а А – формула, що не містить квантора. Приставку ( ) називають префіксом, а А – матрицею формули Ф. Якщо формула А залежить від вільної змінної х, то це записується як А (х), якщо ні, то – А.

Теорема 4.2.1. Для будь-яких формул F, G, H теорії числення першого порядку справедливі такі еквівалентності:

а) х F(x) х ( F (x));

б) х F(x) х ( F(x));

в) х F(x) G х (F(x) G);

х F(x) G х (F(x) G);

г) х F(x) G х (F(x) G);

х F(x) G х (F(x) G);

д) х F(x) х Н (х) х (F(x) Н (х));

е) х F(x) х Н (х) х (F(x) Н (х));

є) х F(x) х Н (х) х у (F(x) Н (у));

ж) х F(x) х Н (х) х у (F(x) Н (у)).

Доведення . Виконаємо доведення еквівалентності.

а) х F(x) х ( F(x)). Нехай r – довільна інтер-претація на деякій області R. Якщо ( х F(x)) істинна в інтерпретації r, то х F(x) хибна в r. Це означає, що існує такий елемент k(x) R, для якого F ( k (x) ) хибна, або те саме, що F (k (x) ) істинна в r. Отже, х ( F(x)) істинна в r.

Якщо ( х F(x)) хибна в r, то х F(x) істинна в r. Це означає, що F(x) виконується на всіх послідовностях із R або що F(x) не виконується на жодній такій послідовності з R. Отже, х ( F(x)) хибна в r. Таким чином,

( х F(x)) х ( F(x)).

Доведення еквівалентності б) аналогічне доведенню еквівалентності а).

Доведемо еквівалентність в) х F(x) G

 х (F(x) G). Нехай маємо хF(x) G ( хF(x))→ →G х ( F(x)) → G.

Отже,

1) х ( F(x)) → G – гіпотеза;

2) F(x) → х ( F(x)) – правило 7;

3) F(x) → G – транзитивність із 1) і 2) ;

4) x ( F(x) → G) x (F(x) G) – загальнозначність із 3).

І навпаки:

1) x (F(x) G) x ( F(x) → G) – гіпотеза ;

2) F(x) → G – правило 6 із 1;

3) ( F(x) → G) → ( G → F(x)) ‒ тавтологія ;

4) G → F(x) – МР із 2) і 3) ;

5) x ( G → F(x)) – узагальнення із 4 ;

6) х ( G → F(x)) → ( G → х F(x)) – схема аксіом АП5 ;

7) G → x F(x) – МР із 5 і 6 ;

8) ( G → xF(x)) → ( x F(x) → G) – тавтологія ;

9) x F(x) → G x F(x) G – МР із 7) і 8).

Доведемо спочатку першу еквівалентність г).

1) х F(x) G х ( F(x)) → G – гіпотеза ;

2) ( F(x)) → G – правило 6 ;

3) ( F(x)) → G) → х ( F(x) → G) – правило 7 ;

4) х ( F(x) G) х (F(x) G) – МР із 2) і 3).

І навпаки:

1) х ( F(x) → G) – гіпотеза;

2) х ( F(x) → G) → ( F(x) → G) – правило 7 ;

3) F(x) → G – МР із 1) і 2) ;

4) x ( F(x)) → F(x) – правило 6 ;

5) x ( F(x)) → G x ( F(x)) G х (F(x)) G – транзитивність із 3) і 4).

Доведення інших еквівалентностей із в) і г) тепер легко випливає із законів де Моргана.

x F(x) G ( x F(x) G)

 (( х F(x)) G ( х ( F(x) G)

 ( х (F(x) G) x (F(x)) G).

x F(x) G ( x F(x) G)

( х ( F(x)) G) ( х ( F(x) G)  ( х (F(x) G) x (F(x) G).

Аналогічно доводяться й інші еквівалентності із г).

Доведення решти еквівалентностей пропонуються як вправи.

Теорема доведена.

Із теореми 4.2.1 випливає такий метод побудови ВНФ. Для зведення формули Ф до випередженої нормальної форми використовують такі дії:

а) вилучення логічних зв’язок “ →” і “ ” :

А В = (А → В) (В → А) ; А → В = А В ;

б) вилучення і перенесення знака “ ” всередину формул:

( x F(x)) = х ( F(x)); ( х F(x)) =

= x ( F(x)); F = F;

в) перенесення кванторів:

Q x Р(х) G = Q x (F(x) G);

Q x Р(х) G = Q x (F(x) G);

х F(x) х Н (х) = х (F(x) Н (х));

х F(x) х Н (х) = х (F(x) Н (х));

Q1 х F(x) х Н (х) = х у (F(x) Н (у));

Q1 х F(x) х Н (х) = х у (F(x) Н (у)).

Виходячи із методу побудови ВНФ, алгоритм отримання випередженої нормальної форми матиме такі кроки.

1. Вилучити логічні зв’язки еквіваленції “ ” та імплікації “ →” за допомогою правил а).

2. Перенести знак операції заперечення “ ” всередину формул, користуючись правилами: (F G) =

F G; (F G) = F G, і правилами б).

3. Виконати перейменування пов’язаних змінних, якщо є така необхідність.

4. Винести квантори на початок формули, використовуючи правила в).

Обґрунтуванням цього алгоритму є твердження, що безпосередньо випливає з теореми 4.2.1.

Теорема 4.2.2. Алгоритм випередженої нормальної форми перетворює будь-яку формулу А теорії числення предикатів першого порядку АП в таку формулу В, яка знаходиться у ВНФ, що ├ А В у ПL.

Приклад 4.2.1. Звести формулу х F(x) → х Н (х) до ВНФ.

Розв’язання. Користуючись кроками 1, 2, 4 алгоритму, отримаємо

х F(x) → х Н (х) = ( х F(x)) х Н (х) =

= х ( F(x)) х Н (х) = х ( F(x) Н (х)).

Приклад 4.2.2. Отримати ВНФ для формули

х у z (Р (х, у) Р(у, z)) → z R(x, y, z).

Розв’язання. Користуючись кроками 1, 2, 3, 4 алгоритму, отримаємо

х у z (Р (х, у) Р (у, z)) → z R(x, y, z) =

=( z y ( z (Р(х, у) Р(у, z)) z R(х, у, z) =

= x y z ( Р(х, у) Р(у, z)) u R(х, у, и) =

= x y z u ( Р(х, у) Р(у, z) R(х, у, и)).

Оскільки матриця А формули Ф не містить кванторів, то її можна подати у кон’юнктивній нормальній формі (КНФ). Формула Р знаходиться у кон’юнктивній нормальній формі, якщо вона має вигляд Р = … ,

де = … , і кожне ‒ це атомарна формула або її заперечення.

Алгоритм побудови КНФ має такі кроки.

1. Вилучити зв’язки “ ” і “ →” з формули А за допомогою правила а), як в алгоритмі ВНФ.

2. Вилучити подвійне заперечення за допомогою правила ( F) = F, і перенести знак “ ” до атомів, користуючись законами де Моргана, як у алгоритмі побудови ВНФ.

3. Для отримання нормальної форми формули А використати дистрибутивні закони:

F (G Н) = (F G) (F Н);

F (G Н) = (F G) (F Н).

Приклад 4.2.3. Задану формулу (Р (Q → R)) → S перетворити у КНФ.

Розв’язання. Використовуючи кроки алгоритму 1, 2 і 3, отримаємо

(Р (Q→R))→S=(Р ( Q R))→S= (Р ( Q R)) S = =( Р ( Q R)) S=( Р Q) ( Р R) S= = ( Р Q S) ( Р R S).

Приклад 4.2.4. Задану формулу (Р Q) → R перетворити в КНФ.

Розв’язання. Використовуючи кроки наведеного вище алгоритму, отримаємо (Р Q)→R= (Р Q) R = =( Р ( Q)) R = ( Р Q) R.