Логіки першого порядку, Детальна інформація

\xF02D символи логiчних операцiй \xF0D8, \xF0DA та (.

В множині Fs може виділятися підмножина константних символів Сп(Fs. Символ рівності завжди інтерпретуватиметься як предикат рівності, причому таку рівність трактуватимемо як тотожність.

Символи \xF0D8, \xF0DA, \xF024, = та предметнi імена називають логiчними символами, функцiональнi та предикатнi символи називають нелогiчними символами. Множину функцiональних та предикатних символів \xF073=Fs(Ps називають сигнатурою мови 1-го порядку.

Основними конструкціями мови 1-го порядку є терми та формули. Терми використовують для позначення, назви суб’єктiв, формули \xF02D для запису тверджень про суб’єкти.

Індуктивне визначення терма таке:

1) кожне предметне ім’я та кожна константа є термом; такі терми назвемо атомарними;

2) якщо t1,..., tn \xF02D терми, f \xF02D\xF020 n-арний функцiональний символ, то ft1...tn \xF02D терм.

Атомарною формулою називається вираз виду pt1...tn, де p - n-арний предикатний символ, t1, ..., tn \xF02D терми.

Індуктивне визначення формули таке:

1) кожна атомарна формула є формулою;

2) якщо ( та ( \xF02D формули, то \xF0D8( та ((( \xF02D формули;

3) якщо ( \xF02D формула, x \xF02D\xF020предметне iм’я, то \xF024x( \xF02D формула.

Аналогiчно мовi ЛВ, вирази (&(, (\xF0AE( та ((( вважаємо вiдповiдно скороченнями формул \xF0D8\xF0DA\xF0D8(\xF0D8(, \xF0DA\xF0D8(( та \xF0D8\xF0DA\xF0D8\xF0DA\xF0D8((\xF0D8\xF0DA\xF0D8((. Користуємося також символом (, вважаючи вираз (x( скороченням формули \xF0D8\xF024x\xF0D8(.

Для бiнарних функцiональних та предикатних символiв i символiв \xF0DA, &, \xF0AE та ( звичайно застосовуємо iнфiксну форму запису. Прiоритет символiв логiчних зв’язок вважаємо нижчим за прiоритет предикатних символiв, а прiоритет предикатних символiв нижчим за прiоритет функцiональних символiв. Використовуючи додатковi символи \xF02D кому , і дужки ( та ), для термiв вигляду ft1...tn вживатимемо скорочення f(t1...tn), або t1ft2, якщо символ f бiнарний. Те ж для атомарних формул. Для атомарних формул вигляду \xF0D8=t1(t2 вживатимемо скорочення t1(t2.

Скорочення термiв та формул будемо називати просто термами та формулами. Множини термів та формул мови 1-го порядку звичайно позначатимемо вiдповiдно як Тr та Fr. Формули мови 1-го порядку сигнатури \xF073 називатимемо формулами 1-го порядку сигнатури \xF073.

Можна вказати 2 рiвнi вiдмiнностi мов 1-го порядку:

1) варiанти мови одної сигнатури, що вiдрiзняються наборами символiв логiчних операцiй та способами запису термiв i формул;

2) iстотно рiзнi мови, що вiдрiзняються сигнатурами.

Мова 1-го порядку L’ сигнатури (’ називається розширенням мови 1-го порядку L сигнатури \xF073, якщо \xF073’(\xF073.

В формулi вигляду \xF024x( або (x( формулу P називають областю дiї квантора по x. Вираз вигляду \xF024x або (x називають кванторним префiксом.

Входження імені (змінної) x в формулу \xF046 зв’язане, якщо воно знаходиться в областi дiї деякого квантора по x, iнакше таке входження x в \xF046 вiльне.

Якщо iснує вiльне входження імені x в формулу \xF046, то x \xF02D вiльне ім’я (вільна змiнна) формули \xF046.

Формулу \xF046 iз вiльними іменами x1,.., xn позначаємо \xF046(x1,.., xn).

Формула замкнена, якщо вона не має вiльних імен.

Терм, який не мiстить входжень предметних імен, називається замкненим термом. Зокрема, таким є кожний константний символ.

Наведемо кiлька прикладiв мов 1-го порядку.

Приклад 1. Мова арифметики Lar визначається сигнатурою \xF073ar={0, 1, +, (, =}, де 0 та 1 \xF02D константні символи, + та ( \xF02D бiнарнi функцiональнi символи, = \xF02D бiнарний предикатний символ.

Терм мови арифметики назвемо арифметичним термом.

Формулу мови арифметики назвемо арифметичною формулою.

Наприклад, 1+1 \xF02D замкнений арифметичний терм; x((y+z) \xF02D арифметичний терм; \xF024z(x+z=y) \xF02D арифметичнa формула.