рмулою В (або між двома формулами А і В) і чи є деяка формула А законом логіки. Ця специфіка логіки предикатів характеризується як нерозв'язність цієї теорії щодо універсальної общезначимости формул. Ця обмеженість наших можливостей тут є платою за відмову від прийнятих в логіці висловлювань абстракцій щодо структур деяких висловлювань.
Як і в логіці висловлювань, ми маємо тут зв'язок між відношенням слідування та законами логіки. Вона дозволяє зводити питання про наявності або відсутності відносини прямування для кінцевих множин формул до питання про те, чи є деяка формула універсально загальнозначущої. Мається на увазі зв'язок
А1, .... Аn вЉЁ У е. тобто вЉЁ (А1 вЉѓ (А2 вЉѓ (А2 вЉѓ ... (Аn вЉѓ В) ...));
остання ж, як ми бачили раніше, рівносильна вЉЁ ((А1 & А2 & ... & An) вЉѓ В) - за будь-якої розстановці дужок у кон'юнкції згідно з правилами побудови формул.
У зв'язку із зазначеною нерозв'язністю логіки предикатів особливого значення набуває тут формалізація понять прямування і закону логіки допомогою побудови логічних числень. Саме числення дає можливість у багатьох випадках синтаксичним чином вирішувати питання, чи є деяка формула законом, або відповідно чи є деяке відношення прямування, коли ми не можемо вирішити це питання за допомогою семантичного аналізу. Для логіки висловлювань числення висловів, взагалі кажучи, не є необхідним. Воно скоріше потрібно як частина логічного числення для формул ЯЛП.
Обчислення предикатів
В основі обчислення предикатів лежить мова логіки предикатів. В іншому воно є розширенням числення висловів. p> аксіоматичні систему числення предикатів ми отримаємо, додавши до перерахованих вище схемами аксіоматичного числення висловлювань (маючи на увазі, звичайно, перехід до мови логіки предикатів) наступні чотири схеми і одне правило:
1. в€Ђ x A (x) вЉѓ A (t) - схема в€Ђ і. p> 2. A (t) вЉѓ в€ѓ х А (х) - схема в€ѓ в.
3. в€Ђ x (В вЉѓ С (х)) вЉѓ (У вЉѓ в€Ђ x С (х)) схема введення в€Ђ в консеквент.
4. в€Ђ x (С (х) вЉѓ В) вЉѓ (в€ѓ x вЉѓ C (x) вЉѓ В) - схема введення в€ѓ в антецедент.
A (t) - результат правильної підстановки терма (замість х в А (х); В - не містить х вільно.
Правило в€Ђ в (Правило введення квантора спільності, інше
A (t) назва: правило узагальнення): - (з А безпосередньо виводиться в€Ђ x A).
Формально ми зберігаємо колишнє визначення виводу і докази (ясно, що, по суті, зміна полягає в тому, що тепер можуть використовуватися нові аксіоми і нове правило), однак, якщо ми хочемо, щоб відношення формальної виводимості було аналогом семантичного поняття прямування, необхідно обмежити застосування в€Ђ в: воно може застосовуватися до деякої формулою А (х) для узагальнення лише за такими змінним х, які не містяться вільно в припущеннях, від яких залежить ця формула. Щоб сенс цього обмеження був ясним, ми повинні визначити поняття залежності деякої формули в...
