Числення предикатiв. Теорiя першого порядку
Числення предикатiв, тобто формальна теорiя предикатiв будується за вищенаведеною класичною схемою побудови формальних (математичних) теорiй.
1. Алфавiт числення предикатiв, тобто множина вихiдних символiв складається з предметних (iндивiдних) змiнних x1,x2,..., предметних (iндивiдних) констант a1,a2,..., предикатних букв P11, P21,...,Pkj,... i функцiональних букв f11,f21,...,fkj,..., а також знакiв логiчних операцiй (, (, (, (, кванторiв (, (i роздiлових знакiв (,),, (кома).
Верхнi iндекси предикатних i функцiональних букв вказують на число аргументiв (арнiсть), а нижнi використовують для звичайної нумерацiї букв.
2. Поняття формули означають у два етапи.
Спочатку означають поняття терма.
а). Предметнi змiннi i предметнi константи є термами.
б). Якщо f n - функцiональна буква, а t1,t2,...,tn - терми, то f n(t1,t2,...,tn) - терм.
в). Iнших термiв, крiм утворених за правилами а) i б), немає.
Вiдтак, формулюють означення формули.
а). Якщо Pn предикатна буква, а t1,t2,...,tn - терми, то Pn(t1,t2,...,tn) - формула, яка називається елементарною. Усi входження предметних змiнних у формулу Pn(t1,t2,...,tn) називають вiльними.
б). Якщо F1, F2 - формули, то вирази ((F1), (F1(F2), (F1(F2), (F1(F2) теж є формулами. Усi входження змiнних, вiльнi у F1 i F2, є вiльними й в усiх чотирьох видах формул.
в). Якщо F(x) - формула, що мiстить вiльнi входження змiнної x, то (xF(x) i (xF(x) - формули.
У цих формулах усi входження змiнної x називають зв’язаними. Входження решти змiнних у F залишаються вiльними.
г). Iнших формул, нiж побудованих за правилами а), б) i в), немає.
Зауваження. Функцiональнi букви i терми введено в означення для потенцiйних потреб рiзноманiтних конкретних прикладних числень предикатiв. У прикладних численнях предметна область M є, як правило, носiєм певної алгебраїчної системи, тому в численнi доцiльно мати засоби для опису операцiй i вiдношень, заданих на M. Чисте числення предикатiв будується для довiльної предметної областi; структура цiєї областi i зв’язки (вiдношення) мiж її елементами не беруться до уваги, тому в ньому вводити функцiональнi букви i терми не обов’язково.
3. Аксiоми числення предикатiв утворюють двi групи аксiом.
а). Першу групу складають аксiоми довiльного числення висловлень (наприклад, можна взяти будь-яку з вищенаведених двох систем A1-A10 або S1-S3). Як правило, цi аксiоми є схемами аксiом.
б). У другу групу входять так званi предикатнi аксiоми:
P1. (xF(x)(F(y),
P2. F(y)((xF(x).
У цих аксiомах F(x) - будь-яка формула, яка мiстить вiльнi входження x, причому жодне з них не знаходиться в областi дiї квантора по y. Формулу F(y) отримуємо з F(x) замiною всiх вiльних входжень змiнної x на y.
Останнє зауваження означає, що формула F(x) не може мати, наприклад, вигляд (yA(x,y) або (y(A(x)(B(y)) тощо.
4. Правилами виведення у численнi предикатiв є такi правила.
а). Правило висновку (modus ponens) - те саме, що й у численнi висловлень.
б). Правило узагальнення (правило введення квантора (): з A(B(x) виводиться A((xB(x).
в). Правило введення квантора (: з B(x)(A виводяться (xB(x)(A.
В обох останнiх правилах формула B(x) мiстить вiльнi входження x, а A їх не мiстить.
Правило пiдстановки в нашому численнi вiдсутнє. Отже, з двох можливих методiв побудови числення обрано метод зi схемами аксiом. Побудова числення предикатiв з правилом пiдстановки можлива, однак вона є суттєво бiльш громiздкою через необхiднiсть розрiзняти при пiдстановках вiльнi i зв’язанi входження предметних змiнних. Тому частiше в логiцi використовують пiдхiд зi схемами аксiом.
Поняття виведення (доведення) формули, поняття теореми, виведення формули з множини гіпотез означаються у численні предикатів аналогічно тому, як це було зроблено у численні висловлень. Мають місце також теореми, подібні до теорем 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)). Застосування таких числень зустрічається значно рідше, тому в математичній логіці їм приділяють менше уваги.
Прикладні теорії першого порядку
В даному підрозділі будуть представлені дві прикладні теорії першого порядку: теорія
рівностей та формальна арифметика.
Розглянемо теорію першого порядку T, у числі предикатних символів якої міститься
предикат рівності A^2(t,s), який для скорочення будемо позначати t=s, а замість A^2(t,s)
відповідно будемо писати t≠s.
Означення 17.3. Теорія T називається теорію першого порядку з рівністю, якщо
наступні формули є аксіомами теорії T:
А6. ∀x (x=x) рефлективність рівності;
А7.(x=y) → (A(x) → A(x){y/x}) підстановка рівності,
де x та y – предметні змінні, A(x) – довільна формула, A(x){y/x} отримується заміною яких-
небудь (не обов’язково всіх) вільних входжень x на y, якщо y вільно для тих входжень x, які замінюються.
Доведемо основні теореми теорії T.
Теорема 17.6. ├ t=t для довільного терму t.
Доведення. З A6: ├∀x (x=x) та A4: ├∀x (x=x) → (t=t) за правилом МР отримуємо t=t. ►
Теорема 17.7. ├ x=y → y=x.
Доведення. Нехай A(x) є x=x, A(x){y/x} є y=x. Тоді:
1) ├ (x=y) → ((x=x) → (y=x)) аксіома А7;
2) ├ x=x теорема 17.6;
3) ├ (x=y) → (y=x) за наслідком 2 теореми дедукції для числення L. ►
Теорема 17.8. ├ x=y → (y=z → x=z).
Доведення. Нехай A(y) є y=z, A(y){x/y} є x=z. Тоді:
1) ├ (y=x) → ((y=z) → (x=z)) аксіома А7;
2) ├ (x=y) → (y=x) за теоремою 17.7;
3) ├ x=y → (y=z → x=z) за наслідком 1 теореми дедукції для числення L. ►
Наведемо тепер означення формальної арифметики A, яка була вперше введена Пеано.
Означення 17.4. Формальна арифметика A – це числення предикатів, в якому є:
1. Предметна константа 0.
2. Двомісні функціональні символи + та ×, одномісний функціональний символ ´. Дискретна Математика:: Числення предикатів 107
3. Двомісний предикат = (= позначатимемо через ≠).
4. Власні схеми аксіом:
Е1. (P(0) ∧ ∀x(P(x) → P(x´))) → ∀xP(x)
Е2. t1´ = t2´ → t1 = t2
Е3. t´ ≠ 0
Е4. t1 = t2 → (t1 = t3 → t2 = t3)
Е5. t1 = t2 → t1´ = t2´
Е6. t + 0 = t
Е7. t1 + t2´ = (t1 + t2) ´
Е8. t×0 = 0
Е9. t1×t2´ = t1×t2 + t1
Тут P – довільна формула, а t, t1, t2 – довільні терми теорії A. Схема аксіом Е1 виражає
принцип математичної індукції.
27.Доведення в теоріях першого порядку. Доводжуваність окремих випадків ТІ–формул. Метатеорема дедукції.
теорема є тотожно істинним висловленням (тавтологією).
Доведення. Тотожна істинність усіх аксіом легко перевіряється безпосередньо побудовою відповідних таблиць істинності для кожної з них (рекомендуємо це зробити самостійно).
Відтак, доведемо, що обидва правила виведення перетворюють тотожно істинні формули у тотожно істинні.
Якщо A (p1, p2,..., pn) - тотожно істинна формула, то для довільного набору значень a1, a2,..., an її пропозиційних змінних A (a1, a2,..., an) є істинною. Отже, тотожно істинною буде і будь-яка формула A, що отримується з формули A шляхом підстановки замість пропозиційних змінних p1, p2,..., pn довільних формул B1, B2,....., Bn, оскільки останні можуть набувати лише значень 0 або 1.
Доведемо, що коли формули A і A®B є тотожно істинними, тоді формула B, яку ми дістаємо з них за правилом висновку, також є тотожно істинною. Припустімо супротивне: нехай B не є тотожно істинною формулою, тобто існує набір значень її змінних, на якому вона набуває значення 0. Тоді підставимо цей набір у формулу A®B, оскільки A є тавтологією, то дістанемо вираз 1®0, значенням якого є 0. Останнє суперечить припущенню про тотожну істинність формули A®B.
Таким чином, ми переконалися в тому, що всі аксіоми є тотожно істинними формулами алгебри висловлень, а застосування обох правил виведення (підстановки і висновку) до тотожно істинних формул знову приводить до тотожно істинних формул. Отже, всі вивідні формули (теореми) числення висловлень є тотожно істинними формулами алгебри висловлень.
Справедливою є й обернена теорема, яку подамо без доведення.
Метатеорема дедукції в численні предикатів. Нехай Г- деяка множина формул числення висловлювань і А деяка формула. Нехай Г, А├F (формула F виводиться з множини формул Г і формули А), і при цьому не застосовується правило Gen по вільним змінним формули А, тоді Г├ А→F.
Доведення. Доведення теореми проведемо методом математичної індукції по довжині виводу формули F.
Нехай U1, U2,..., US 
F- вивід формули F з множини формул Г,A.
База індукції: s = 1. У цьому випадку U1 F і це можливо лише за одної з трьох умов:
а) F 
Г;
б) F- аксіома;
в) F А.
У випадку а) маємо: 1)F(гіпотеза);2)F->(A->F)(A1,де A=G);3)A->F(MP 1,2).
У випадку б) доведення дослівно повторюється, а у випадку в) попередньо доведена теорема F->F. Цим базу індукції доведено.
Припустимо, що метатеорема дедукції має місце для формул F, довжина виводу яких з множини формул Г, А менша за s.
Тоді, за припущенням індукції, для довільного к: 1 < к < s, має місце: Г А->Uk, а для формули US є такі можливості:
§ а) F Г
§ б)F- аксіома
§ в)F = А
§ г)існують i,j: 1 < i,j < s такі, що Uj= Ui ->Us, тобто Us отримана за правилом modus ponens;
§ д)F= 
і отримано застосуванням правила Gen.
У перших трьох випадках міркування, проведені при доведенні бази індукції, дослівно повторюються. У випадку г), користуючись припущенням індукції, отримуємо Г А->Ui, Г А->(Ui->US). За схемою аксіом А2, отримуємо (A->(Ui->US))->((A->Ui)->(A->US)
Застосувавши два рази modus ponens отримуємо Г А-> US, а US=F.
У випадку д) за припущенням індукції маємо Г А->Ui.
За зробленим припущенням х не є вільною змінною формули А. Тоді за А5 
.
Оскільки Г A-> Ui, то за правилом Gen: Г 
x (A-> Ui) Звідки застосувавши М.Р. маємо потрібний результат.
