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

Числення предикатів, тобто формальна теорія предикатів будується за вищенаведеною класичною схемою побудови формальних (математичних) теорій

1. Алфавіт числення предикатів, тобто множина вихідних символів складається з предметних (індивідних) змінних x1, x2,..., предметних (індивідних) констант a1, a2,..., предикатних букв P11, P21,..., Pkj,... і функціональних букв f11, f21,..., fkj,..., а також знаків логічних операцій Ú, Ù, Ø, ®, кванторів ", $ і розділових знаків (,),, (кома).

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

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

Спочатку означають поняття терма:

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

б). Якщо f n - функціональна буква, а t1, t2,..., tn - терми, то f n (t1, t2,..., tn) - терм.

в). Інших термів, крім утворених за правилами а) і б), немає.

Відтак, формулюють означення формули:

     

а). Якщо Pn предикатна буква, а t1, t2,..., tn - терми, то Pn (t1, t2,..., tn) - формула, яка називається елементарною. Усі входження предметних змінних у формулу Pn (t1, t2,..., tn) називають вільними.

б). Якщо F1, F2 - формули, то вирази (ØF1), (F1ÚF2), (F1ÙF2), (F1®F2) теж є формулами. Усі входження змінних, вільні у F1 і F2, є вільними й в усіх чотирьох видах формул.

в). Якщо F (x) - формула, що містить вільні входження змінної x, то "xF (x) і $xF (x) - формули.

У цих формулах усі входження змінної x називають зв’язаними. Входження решти змінних у F залишаються вільними.

г). Інших формул, ніж побудованих за правилами а), б) і в), немає.

Зауваження. Функціональні букви і терми введено в означення для потенційних потреб різноманітних конкретних прикладних числень предикатів. У прикладних численнях предметна область M є, як правило, носієм певної алгебраїчної системи, тому в численні доцільно мати засоби для опису операцій і відношень, заданих на M.

Чисте числення предикатів будується для довільної предметної області; структура цієї області і зв’язки (відношення) між її елементами не беруться до уваги, тому в ньому вводити функціональні букви і терми не обов’язково.

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

а). Першу групу складають аксіоми довільного числення висловлень (наприклад, можна взяти будь-яку з вищенаведених двох систем A1-A10 або S1-S3). Як правило, ці аксіоми є схемами аксіом.

б). У другу групу входять так звані предикатні аксіоми:

P1. "xF (x) ®F (y),

P2. F (y) ®$xF (x).

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

Останнє зауваження означає, що формула F (x) не може мати, наприклад, вигляд $yA (x, y) або "y (A (x) ®B (y)) тощо.

4. Правилами виведення у численні предикатів є такі правила:

  • а). Правило висновку (modus ponens) - те саме, що й у численні висловлень.
  • б). Правило узагальнення (правило введення квантора "): з A®B (x) виводиться A®"xB (x).
  • в). Правило введення квантора $: з B (x) ®A виводяться $xB (x) ®A.

В обох останніх правилах формула B (x) містить вільні входження x, а A їх не містить.

Правило підстановки в нашому численні відсутнє. Отже, з двох можливих методів побудови числення обрано метод зі схемами аксіом. Побудова числення предикатів з правилом підстановки можлива, однак вона є суттєво більш громіздкою через необхідність розрізняти при підстановках вільні і зв’язані входження предметних змінних. Тому частіше в логіці використовують підхід зі схемами аксіом.

Поняття виведення (доведення) формули, поняття теореми, виведення формули з множини гіпотез означаються у численні предикатів аналогічно тому, як це було зроблено у численні висловлень. Мають місце також теореми, подібні до теорем 5.5 і 5.6 числення висловлень.

Теорема 5.7. Будь-яка вивідна формула (теорема) числення предикатів є тотожно істиною (логічно загальнозначущою) формулою.

Ця теорема доводиться аналогічно теоремі 5.5. Спочатку безпосередньо перевіряється, що всі аксіоми є лзз формулами. Відтак, доводиться, що усі правила виведення зберігають властивість лзз.

Теорема 5.8. Будь-яка тотожно істинна предикатна формула є вивідною (теоремою) в численні предикатів.

Доведення цієї теореми досить складне і тут не наводитиметься.

З останніх теорем випливає твердження, подібне до твердження теореми 5.1.

Теорема 5.9. Предикатні формули A і B рівносильні тоді і тільки тоді, коли формула ((A®B) Ù (B®A)) є вивідною в численні предикатів, тобто є лзз.

Як і раніше, для скорочення виразу ((A®B) Ù (B®A)) вводять операцію ~ і записують даний вираз у вигляді (A~B). Отже, останню теорему можна переформулювати так: формули A і B рівносильні (A = B) тоді і тільки тоді, коли формула (A~B) є вивідною в численні предикатів.

Оскільки, як вже зазначалось вище, встановлення рівносильності формул у логіці предикатів є задачею значно складнішою, ніж у логіці висловлень, то дуже важливе значення останнього твердження полягає у тому, що цю задачу можна звести до пошуку формального виведення для відповідної формули.

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

У численнях другого і вищих порядків аргументами предикатів можуть бути і предикати, а квантори можуть зв’язувати і предикатні змінні, тобто допустимі вирази, наприклад, вигляду "P (P (x)). Застосування таких числень зустрічається значно рідше, тому в математичній логіці їм приділяють менше уваги.


23.10.2011

Загрузка...