Застосування логiки предикатiв, Детальна інформація

Дев’ять схем спец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
Часто, коли предметна область в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).

, який читається «за означенням».

За допомогою предиката x|y можна природно означити унарний предикат «x - просте число» (позначимо його через P(x)):

(y((y|x)(((y = 1)((y = -1)((y = x)((y = -x))).

Наведемо ще декiлька прикладiв означень з математичного аналiзу. Вiдоме означення границi числової послiдовностi можна записати так:

(((>0)((k(N)((i(N(i>k)(|ai -a|<().

Аналогiчно можуть бути записанi класичнi означення рiзних варiантiв поняття неперервностi дiйсної фунцiї f:



(((>0)(((>0)((x(R)((|x-a|<()((|f(a)-f(x)|<());



((c((a,b))(((>0)(((>0)((x((a,b))((|x-c|<()((|f(c)-f(x)|<());