4.4. Числення предикатів і теорії першого порядку

Аксіоми і правила виводу.

1. Алфавіт числення предикатів складається з предметних змінних x₁, x₂, … , предметних констант a₁, a₂, … , предикатних букв P₁¹, P₂¹, P₃¹, … , P_k^j і функціональних букв f₁¹, f₁¹, … , f_k^j, а також знаків логічних зв'язків , , ¯, , кванторів ,  і скобок (, ).

Верхні індекси предикатних і функціональних букв вказують число аргументів, їхні нижні індекси служать для звичайної нумерації букв. Змінні висловлення в численні предикатів вводяться як 0 - місцеві предикати Р₁⁰, Р₂⁰, . . ., тобто як предикати без предметних змінних.

2. 2. Формули. Поняття формули визначається в два етапи.

I - Терми:

а) предметні змінні і константи є термами;

б) якщо fⁿ - функціональна буква, а t₁, ..., t_n - терми, те fⁿ( t₁, ...,t_n) -

терм.

II - Формули :

а) якщо Рⁿ - предикатна буква, а t₁, . . ., t_n - терми, то Рⁿ( t₁, . . . , t_n) - формула; усі входження предметних змінних у формулу вигляду Рⁿ ( t₁, . . . , t_n) називаються вільними;

б) якщо F₁, F₂ - формула, то формулами є ┐F₁, (F₁&F₂), (F₁F₂), (F₁→F₂); усі входження змінних, вільні в F₁, F₂, є вільними в зазначених чотирьох виглядах формул;

в) якщо F(х) - формула, що містить вільні входження змінної х, то x F(х) і  х F(х) - формули; у цих формулах усі входження змінної х називаються зв'язаними; входження інших змінних у F залишаються вільними.

3. Аксіоми числення предикатів діляться на дві групи:

2. 1) аксіоми числення висловлень ( можна взяти будь-яку із систем I або II );

3. 2) дві такі предикатні аксіоми:

Р1.  х F ( х )  F ( у );

Р2. F ( у )   х F ( х ).

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

Щоб пояснити істотність вимоги до входжень х у F, розглянемо як F (х) формулу  у Р (у, х), де ця вимога порушена: вільне входження х знаходиться в області дії  у. Підстановка цієї формули в аксіому Р1 дає формулу  х  у Р (у, х)   у Р (у, у). Якщо її розглянути на множині N натуральних чисел із предикатом Р " бути більше“, то одержимо висловлення: " якщо для всякого х знайдеться у більший ніж х, то знайдеться у більший самого себе. “ Посилання цієї імплікації істинно на N, а її висновок хибний і, отже, саме висловлення хибно.

4. Правила виведення:

1. правило висновку (Modus Ponens) - те ж, що й у численні висловлень;

2. правило узагальнення (  - уведення) :

F  G(x) ,

F  x G(x)

де G( х) містить вільні входження х, а F їх не містить;

3) правило  - уведення:

G ( х)  F

 х G ( х)  F

при тих же вимогах до F і G, що й у попередньому правилі.

Порушення цих вимог можуть призвести до помилкових висновків із істинних висловлень. Нехай, наприклад, Р ( х) - предикат "х ділиться на 6“, Q(х) - предикат "х ділиться на 3“. Висловлення Р ( х) → Q ( х) , очевидно, істинно для довільного х , проте застосування до нього правила узагальнення дає висловлення Р ( х) →  х Q ( х) , що не є завжди істинним.

Якщо ж до Р ( х)  Q ( х) застосувати правило  - уведення, то одержимо  х Р(х)  Q(х), з якого шляхом застосування ( уже коректного ) правила узагальнення одержимо висловлення х Р(х)  х Q(х), хибне на множині натуральних чисел.

Розглянемо приклади формальних систем.

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

Розглянемо приклади формальних систем абстрактного типу.

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

Приклад 2. Розглянемо абстрактне визначення орієнтованої двополюсної схеми. Два варіанти таких схем показані на рис. 4.1.

Рис. 4.1. Двополюсні схеми

Аксіоми такої системи - елементи з виділеними полюсами, правила виведення - правила з'єднання елементів у схему.

Інтерпретація - електрична схема, графік та ін.