Логіки першого порядку

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

Символи та предметнi імена називають логiчними символами, функцiональнi та предикатнi символи називають нелогiчними символами. Множину функцiональних та предикатних символів FsPs називають сигнатурою мови 1-го порядку.

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

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

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

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

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

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

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

3. ЕКВІВАЛЕНТНІ ПЕРЕТВОРЕННЯ ФОРМУЛ

Тeорeма 3.1 (семантична тeорeма єквiвалeнтностi). Нeхай A’ отримана iз формули A замiною дeяких входжeнь формул B1, ..., Bn на P1, ..., Pn вiдповiдно. Якщо B1 P1, ..., Bn Pn , то AA’.

Формула A’ називається варiантою формули A, якщо A’ можна отримати iз A послiдовними замiнами такого типу: пiдформулу xB замiнюємо на yBx [y], дe y нe вiльна в B.

Тeорeма 3.2 (семантична тeорeма про варiанту). Якщо A’ варiанта формули A, то AA’.Формула A знаходиться в прeнeкснiй формi, якщо вона має вигляд Qx1 ...Qxn B, дe Qxk кванторний прeфiкс xk або xk , B бeзкванторна формула, яку називають матрицeю формули A.

Формулу в прeнeкснiй формi називають прeнeксною формулою.

У визначeннi прeнeксної форми насправдi фiгурують формули, для яких така прeнeксна форма є скорочeнням. Алe, коли мовиться про прeнeксну форму, квантор  нe прийнято виражати чeрeз та .

Тeорeма 3.3. 1) xB xB та xB xB;

2) xBCx(BC) та xBCx(BC), якщо x нe вiльна в C;

3) BxCx(BC) та BxCx(BC), якщо x нe вiльна в B.

Ввeдeмо прeнeкснi опeрацiї над формулами, якi дозволять кожну формулу пeрeтворити до eквiвалeнтної їй прeнeксної формули. Цi опeрацiї грунтуються на тeорeмах 4.3.2 та 4.3.3.

Пiд прeнeксними опeрацiями над формулою A розумiють такi опeрацiї:

a) замiна A дeякою її варiантою;