Застосування лог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агонального методу Кантора).