1. Мова l теорії першого порядку t.

1.1. Символи L .

а) службові символи ( , );

б) злічена множина змінних: x₁, x₂ , ... ;

в) порожня, скінчена або злічена множина індивідних констант: а₁, а₂ , ...;

г) непорожня скінчена або злічена множина предикатних літер A_i^j, де j - місткість;

д) порожня, скінчена або злічена множина функціональних символів f_i^j, де j - місткість;

е) символи логічних зв'язок: 7,  ;

ж) символ квантора: .

1.2. Довільна послідовність символів мови L називається виразом мови L. Нас цікавлять не довільні вирази, а вирази визначеного типу, що називаються формулами. Ними ми будемо оперувати. Для їхнього визначення спочатку введемо терми.

1.3 Визначення терма:

а) константа або змінна - це терм;

б) якщо f_i^j - функціональний символ, а t₁, t₂, ... , t_j - терми, то f_i^j (t₁, t₂, ... , t_j ) - терм;

в) інших термів у мові L немає.

1.4. Елементарною формулою будемо називати будь-який вираз вигляду A_i^j(t₁, t₂, ... ,t_j ), де A_i^j - предикатна буква, t₁, t₂, ... , t_j - терми.

1.5. Формули мови L визначаються в такий спосіб:

а) елементарна формула є формулою мови L;

б) якщо А, В - формули, то 7А, А  В, x_i А - теж формули мови L;

в) інших формул у L немає.

Символи: предикатні, функціональні або константи називаються нелогічними, всі інші символи називаються логічними.

2. Аксіоми теорії першого порядку т.

Звичайно виділяється дві множини аксіом.

2.1. Логічні аксіоми.

Нехай A, B, C - довільні формули. Тоді наступні формули – аксіоми:

(A1) A  (B  A)

(A2) (A  (B  C)  (A  B)  (A  C))

(A3) (7 B 7 A)  ((7B  A)  B)

(A4) x _i A(x _i)  A(t) , де t - терм вільний у формулі A для змінної x _i.

Будемо називати терм t у формулі A вільним для змінної x_i, якщо в A немає квантора по змінній x _j, такого що t містить x _j і потрапляє в зону дії цього квантора. Якщо не виконується умова, що терм вільний у формулі для змінної x_i, то можна побудувати у вигляді (А4) таку формулу, яка не буде логічно істинною.

(А5)  x _j (AB)(A x _j B), де формула А не містить вільних входжень змінної x_i.

Якщо не враховувати це обмеження, то можна побудувати формулу вигляду (А5), що не буде логічно істинною.

2.2. Нелогічні аксіоми.

Нелогічні аксіоми залежать від конкретизації теорії першого порядку T і визначаються властивостями тих областей інтепретації, на які розрахована дана конкретизація теорії. Іншими словами, вони змінюються від однієї конкретизації до іншої.

3. Правила виведення.

3.1. MP : A  B, A | B - правило Modus Ponens;

3.2. Gen : A | x _i A - правило узагальнення.

Якщо ми конкретизуємо теорію, то повинні вказати нелогічні символи і сформулювати нелогічні аксіоми.

Теорія першого порядку без нелогічних аксіом називається численням предикатів першого порядку.

Таким чином, числення предикатів можна розглядати як базу для визначення теорій першого порядку, що досліджують особливості, властиві тільки окремим областям інтепретації.

Числення предикатів першого порядку без констант і функціональних символів, але з нескінченною кількістю предикатних літер звичайно називають чистим численням предикатів першого порядку.

Означення теорії першого порядку Т₁.

В означенні теорії першого порядку T1 ми наведемо тільки відмінності від попереднього означення. В мові відмінність виявляється у використанні іншого набору зв’язок (7) та квантору . Крім того, в Т1визначений предикат рівності “=“. Особливістю теорії Т₁ є використання широкого набору правил виведення, що дуже зручно для виведення теорем.

1. Логічні аксіоми.

(A1) Пропозиціональна аксіома: 7A A;

(A2) Аксіома підстановки: A(x[t])   x A(x), де x[t] - це підстановка терму t замість змінної x якщо x має вільне входження;

(A3) Аксіома тотожністі: x _i = x _i;

(A4) Аксіома рівності: x _i = y _i  x ₂ = y₂ ...  x _n = y _n f_iⁿ(x _i ,... , x _n ) = f_iⁿ (y _i ,... , y _n) або x _i = y _i  x ₂ = y ₂  ...  x _n = y _n A_iⁿ(x _i , ... , x _n )  A_iⁿ( y _i , ... , y _n );