Теорії першого порядку. Побудова теорій першого порядку.

Числення предикат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.

Нехай U₁, U₂, ..., U_S F- вивід формули F з множини формул Г,A.

База індукції: s = 1. У цьому випадку U₁ 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, має місце: Г А->U_k, а для формули U_S є такі можливості:

§ а) F Г

§ б)F- аксіома

§ в)F = А

§ г)існують i,j : 1 < i,j < s такі, що U_j= U_i ->U_s, тобто U_s отримана за правилом modus ponens;

§ д)F= і отримано застосуванням правила Gen.

У перших трьох випадках міркування, проведені при доведенні бази індукції, дослівно повторюються. У випадку г), користуючись припущенням індукції, отримуємо Г А->U_i, Г А->(U_i->U_S). За схемою аксіом А2, отримуємо (A->(U_i->U_S))->((A->U_i)->(A->U_S)

Застосувавши два рази modus ponens отримуємо Г А-> U_S, а U_S=F.

У випадку д) за припущенням індукції маємо Г А->U_i.

За зробленим припущенням х не є вільною змінною формули А. Тоді за А5 .

Оскільки Г A-> U_i , то за правилом Gen: Г x (A-> U_i) Звідки застосувавши М.Р. маємо потрібний результат.

⇐ Назад