Структура обчислення предикатів, правила відділення та узагальнення, правила " і $-введення, перейменування вільних і зв'язаних змінних
Аналогічно обчисленню висловлень в логіці предикатів існує формальна система — обчислення предикатів, яка займається конструюванням формул і доведенням їх загальнозначущості. Обчислення предикатів має ідентичну обчисленню висловлень структуру, а саме: мову, систему аксіом і правила висновку.
Аксіоми обчислення предикатів можна поділити на дві групи:
1) Аксіоми обчислення висловлень (можна обрати будь-яку з формальних систем S1, S2).
2) Предикатні аксіоми, де змінна х у формулі F(x) є вільною і жодного разу не піддається дії квантора за у:
P1) 
;
P2) 
.
Формула F(н) одержана з F(x) заміною х на у.
Для з'ясування сенсу вимоги до входжень х у F(x)розглянемо як F(x) формулу $у Р(у, х), в якій вільне входження х знаходиться в області дії квантора $у, тобто зазначена вимога не задовольняється. Підстановка даної формули до аксіоми Р1 дає таку формулу: 
.
Якщо одержану формулу проінтерпретувати на множині натуральних чисел N з предикатом Р «бути більше», то одержимо висловлення: «якщо для всякого х знайдеться у, який більше нього, то знайдеться і у, більший за самого себе». Зановок цієї імплікації істинний на N, а його висновок хибний, тому всі висловлення є хибними.
В обчисленні предикатів використовуються такі правила висновку:
1) Правило відділення (Modus Ponens), сформульоване у п. 5.3 (див. таблицю 5.5), повністю переноситься з обчислення висловлень.
2) Правило узагальнення ("-введення):
де G(x) містить вільні входження х, a F їх не містить.
3) Правило $-введення:
при тих же вимогах до F і G, що й у попередньому правилі.
Правило перейменування вільних змінних
В обчисленні предикатів з вивідності формули F(x), що містить вільні входження х, жодне з яких не знаходиться в області дії квантора за у, виходить вивідність F(y).
Приклад. Довести справедливість правила перейменування вільних змінних.
Розв'язок.
1. F(x) (за умови).
2. F(x)® (G ® F(x)) (аксіома 1 формальної системи S2; тут як G можна обрати будь-яку довідну формулу, що не містить вільних входжень змінних х;довідність цієї формули знадобиться на кроці 5, а обмеження на х — на кроці 4).
3. G ® F(x) (за правилом відділення, кроки 1, 2).
4. G ® "x F(x) (за правилом узагальнення, крок 3).
5. "x F(x) (наслідок з кроку 4, оскільки G — істинна формула).
6. F(y)(крок 5, аксіома Р1)
Правило доведено.
Правило перейменування зв'язаних змінних
В обчисленні предикатів з вивідності "x F(x)виходить вивідність " у F(y),а з вивідності $х F(x)— вивідність $у F(y) за умови, що F(x) не містить вільних входжень у і містить вільні входження х, жодне з яких не входить до області дії квантора за у.
Приклад. Довести правило перейменування зв'язаних змінних для квантора загальності.
Розв'язок.
1. "x F(x) (за умови).
2. "x F(x) ® F(y) (аксіома P1).
3. "x F(x) ® "y F(y) (правило узагальнення, крок 2).
4. "y F(y) (кроки 1, З).
Необхідно зауважити, що доведення для квантора $ здійснюється аналогічно, але використовує аксіому Р2 і правило $-введення.
Теорема 1
Будь-яка довідна формула обчислення предикатів тотожно істинна.
Ця теорема аналогічна відповідній теоремі обчислення висловлень і показує, що правила висновку в обчисленні предикатів зберігають загальнозначущість, тобто їх застосування до загальнозначущих формул знов дає загальнозначущі формули.
Запитання
1. Сформулюйте призначення обчислення предикатів.
2. Запишіть формули аксіом обчислення предикатів.
3. Поясніть обмеження аксіом обчислення предикатів.
4. Назвіть правила висновку обчислення предикатів.
5. Побудуйте схему правила узагальнення.
6. Визначте правило $-введення за допомогою схеми.
7. Які обмеження необхідні для правила узагальнення і $-введення? До яких наслідків може призвести недотримання вказаних обмежень?
8. Яку особливість здобуває правило підстановки в обчисленні предикатів?
9. Сформулюйте правило перейменування вільних змінних.
10.В чому полягає сутність правила перейменування зв'язаних змінних?
11.Сформулюйте твердження теореми про загально значимості правил висновку обчислення предикатів.
Завдання
1. Доведіть нелогічність таких міркувань:
1.1.Всі студенти нашої групи — члени клуба «Динамо». А деякі члени клуба «Динамо» займаються спортом. Отже, деякі студенти нашої групи займаються спортом.
1.2.Деякі студенти нашої групи — вболівальники «Динамо». А деякі вболівальники «Динамо» займаються спортом. Отже, деякі студенти нашої групи займаються спортом.
1.3.Кожний першокурсник знайомий кимось з студентів другого курсу. А деякі другокурсники — спортсмени. Отже, кожний першокурсник знайомий з кимось із спортсменів.
2. Показати, що формула G не є логічним наслідком множини формул К:
а) 
, 
;
б) 
, 
;
в) 
,
