Застосування лог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 конкретних (iндивiдуальних) предикатних букв i предметних констант з певної предметної областi.
Найтиповiшi приклади iндивiдуальних предикатних букв - предикати  =  (рiвностi) i ? (порядку), а функцiональних букв - знаки арифметичних операцiй +, ?, ?, / тощо та iнших популярних математичних функцiй. Як предметнi областi найчастiше виступають множина N натуральних чисел, множина Z цiлих чисел, множина R дiйсних чисел, булеан ?(A) деякої множини A та iн.
Бiльшiсть прикладних числень мiстить предикат рiвностi  =  i аксiоми, що його визначають. Наприклад, аксiомами для рiвностi можуть бути такi:
E1. ?x(x = x)
E2. (x = y)?(F(x,x)?F(x,y)),
де F(x,y) отримано з F(x,x) шляхом замiни деяких (не обов’язково всiх) вõоджень x на y за умови, що y у цих входженнях також залишається вiльним.
Будь-яка теорiя, в якiй E1 i E2 є аксiомами або теоремами, називається теорiєю (або численням) з рiвнiстю.
З аксiом E1 i E2 неважко вивести теореми, що описують основнi властивостi рiвностi - рефлексивнiсть, симетричнiсть i транзитивнiсть:
?t (t = t)
(x = y)?(y = x)
(x = y)?((y = z)?(x = z)).
Аналогiчно можуть бути введенi три аксiоми, що задають бiльш загальний предикат - предикат еквiвалентностi E(x,y):
Q1. ?xE(x,x)
Q2. ?x?y(E(x,y)?E(y,x))
Q3. ?x?y?z((E(x,y)?E(y,z))?E(x,y)).
Iншим прикладним численням є теорiя часткового порядку, яка мiстить три конкретнi аксiоми для предиката ?:
O1. ?x(x?x)
O2. ?x?y(((x?y)?(y?x))?(x = y))
O3. ?x?y?z((x?y)?((y?z)?(x?z))).
Приєднавши до цих аксiом аксiому
O4. ?x?y((x?y)?(y?x)?(x = y)),
дiстанемо теорiю лiнiйного (строгого) порядку.
Ще одна аксiома (аксiома щiльностi)
O5. ?x?y((x?y)??z((x?z)?(z?y)))
формалiзує вiдношення лiнiйного (строгого) порядку у щiльних множинах (див.роздiл 1.8), наприклад, у множинi рацiональних або множинi дiйсних чисел.
Найбiльш дослiдженою на сьогоднi формальною теорiєю, яка вiдiграє визначальну роль для аналiзу проблеми обгрунтування засад математики, є так звана формальна арифметика [.......].
У формальнiй арифметицi використовують три функцiональнi букви +, ?, ?. Є також одна предикатна буква - символ бiнарного предиката рiвностi  =  i одна предметна константа 0.
Дев’ять схем спецiальних аксiом задають основнi закони формальної арифметики.
A1. F(0)??x(F(x)?F(x? ))?F(x) (принцип iндукцiї)
A2. (t1? = t2? )?(t1 = t2)
A3. ?(t1? = 0)
A4. (t1 = t2)?((t1 = t3)?(t2 = t3))
A5. (t1 = t2)?(t1? = t2? )
A6. t1+0 = t1
A7. t1+t2? = (t1+t2)?
A8. t1?0 = 0
A9. t1?t2? = t1?t2+t1.
Зауважимо, що формальна арифметика припускає так звану стандартну iнтерпретацiю, в якiй символ  =  ототожнюється зi звичним знаком рiвностi, 0 - з числом нуль, + i ? - з традицiйними знаками арифметичних бінарних операцiй додавання i множення, а ? - з унарною операцiєю «безпосередньо слiдує за». Така iнтерпретацiя відповідає звичній змістовній арифметиці. Кожен терм вiдповiдає деякому натуральному числу, а формула - твердженню про певну властивiсть натуральних чисел або числових змiнних.
Ретельнi дослiдження формальної арифметики дозволили видатному австрiйському математику i логiку Курту Гьоделю i його послiдовникам отримати у 30-х роках ХХ стол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 лише на початку 30-х рокiв к.Гьодель опублiкував досить несподiваний на той час i песимiстичний результат: жодна скiнченна система аксiом для елементарної арифметики не є повною. Точнiше у першiй теоремi Гьоделя стверджується, що будь-яка формальна теорiя T, що мiстить формальну арифметику, є неповною, а саме, в T iснує (i може бути ефективно побудована) замкнена формула F, така що ?F iстинна, однак нi F, нi ?F не є вивiдними в T. Друга теорема Гьоделя про неповноту твердить, що для довiльної несуперечливої формальної теорiї T, що включає формальну арифметику, формула, що описує несуперечнiсть T, є невивiдною в T. (Тут доречно зауважити, що при доведенн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ї теор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ки, не надається можливим висв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лах математики. Використання символ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ле число a можна роздiлити з остачею на цiле число b, яке не дорiвнює нулю, може бути записане так:
?(a?Z)?(b?Z)[(b?0)?(?(q?Z)?(r?Z)(a = b?q+r)?((r = 0)?((0<r)?(r<|b|))))].
Часто, коли предметна область вiдома i не змiнюється, замiсть ?(a?Z) записують просто ?a. У наведеному виразi всi предикатнi букви для позначення вiдношень  = , ?, <, ? i всi знаки арифметичних i логiчних операцiй мають звичайний смисл. Словесно записане твердження читається так: «Для цiлих a i b, якщо b не дорiвнює нулю, iснують цiлi числа q i r, для яких a = bq +r i r або дорiвнює 0, або r бiльше нуля i менше |b|».
Предикатнi формули зручно використовувати для запису означень рiзних понять. Вище з їхньою допомогою були означенi вiдношення (предикати) рiвностi, еквiвалентностi i порядку. Подiбним чином можна записати означення, наприклад, предиката x|y «x дiлить y» або «x є дiльником y» на множинi цiлих чисел: ?k(y = kx). Часто такi означення записують у виглядi: x|y = ?k(y = kx).
Замiсть знака рiвносильностi  =  пишуть також знак EMBED Equation.2, який читається «за означенням».
За допомогою предиката x|y можна природно означити унарний предикат «x - просте число» (позначимо його через P(x)):
P(x) EMBED Equation.2 ?y((y|x)?((y = 1)?(y = -1)?(y = x)?(y = -x))).
Наведемо ще декiлька прикладiв означень з математичного аналiзу. Вiдоме означення границi числової послiдовностi можна записати так:
lim ai = a EMBED Equation.2 ?(?>0)?(k?N)?(i?N?i>k)(|ai -a|<?).
Аналогiчно можуть бути записанi класичнi означення рiзних варiантiв поняття неперервностi дiйсної фунцiї f:
1) фунцiя f(x) неперервна в точцi a EMBED Equation.2
?(?>0)?(?>0)?(x?R)((|x-a|<?)?(|f(a)-f(x)|<?));
2) функцiя f(x) неперервна на iнтервалi (a,b) EMBED Equation.2
?(c?(a,b))?(?>0)?(?>0)?(x?(a,b))((|x-c|<?)?(|f(c)-f(x)|<?));
3) функцiя f(x) рiвномiрно неперервна на iнтервалi (a,b) EMBED Equation.2
?(?>0)?(?>0)?(c?(a,b))?(x?(a,b))((|x-c|<?)?(|f(c)-f(x)|<?)).
Означення основних теоретико-множинних операцiй i вiдношення включення для множин можуть бути записанi так:
x?A?B EMBED Equation.2 (x?A)?(x?B),
x? A?B EMBED Equation.2 (x?A)?(x?B),
x? A\B EMBED Equation.2 (x?A)?(x?B),
A?B EMBED Equation.2 ?x((x?A)?(x?B))
тощо.