Замкнений вираз

У математичній логіці замкнений терм формальної системи є термом, який не містить жодної вільної змінної.

Аналогічним чином, замкнена формула - це формула, яка не містить жодної вільної змінної. У логіці першого порядку формула $\forall x(x=x)$ є замкненою фомулою.

Замкнений вираз - це замкнений терм, чи замкнена формула.

Приклади

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

• s(0), s(s(0)), s(s(s(0))) ... замкнені терми;
• 0+1, 0+1+1, ... замкнені терми.
• x+s(1) і s(x) є термами, але не замкненими;
• s(0)=1 і 0+0=0 замкнені формули;
• s(1) і ∀x: (s(x)+1=s(s(x))) замкнені вирази.

Формальне визначення

Нижче наводиться формальне визначення для мов першого порядку. Нехай є мова першого порядку з множиною $C$ константних символів, з множиною $V$ змінних, з множиною $F$ функціональних операторів та множиною $P$ предікатних символів.

Замкнений терм

Замкнені терми це терми, які не містять змінних.Вони можуть бути визначені за допомогою рекурсії.

1. елемент з C є замкненим термом;
2. Якщо f∈F є n-арною функцією і α₁, α₂, ..., α_n є замкненими термами, тоді f(α₁, α₂, ..., α_n) є замкненим термом.
3. Кожен замкнений терм може бути представлений за допомогою застосування зазначених вище двох правил (немає ніяких інших замкнених термів; предікати не можуть бути замкненими термами).

Грубо кажучи, універсум Ербрана це сукупність всіх замкнених термів.

Замкнений атом

Замкнений предікат, або замкнений атом,- це атом, всі терми якого, є замкненими.

Якщо p∈P є n-арним предікатом і α₁, α₂, ..., α_n є замкненими термами, тоді p(α₁, α₂, ..., α_n) є замкненим предікатом, або замкненим термом.

Грубо кажучи, база Ербрана - це множина усіх замкнених атомів, доки інтерпретація Ербрана приймає істинне значення для кожного замкненого атому у базі.

Замкнена формула

Замкнена формула це формула без вільних змінних. Формули з вільними змінними можуть бути визначені за допомогою рекурсії наступним чином:

1. Вільні змінні незамкненого атому - це всі змінні, що входять в нього.
2. Вільні змінні ¬p такі самі як для p. Вільні p∨q, p∧q, p→q це вільні змінні p, чи вільні змінні q.
3. Вільні змінні $\forall x$ p і $\exists x$ p - це всі вільнні змінні p окрім x.

Посилання

• Dalal, M. (2000), Logic-based computer programming paradigms, у Rosen, K.H.; Michaels, J.G. (ред.), Handbook of discrete and combinatorial mathematics, с. 68
• Hodges, Wilfrid (1997), A shorter model theory, Cambridge University Press, ISBN 978-0-521-58713-6
• First-Order Logic: Syntax and Semantics [Архівовано 3 березня 2016 у Wayback Machine.]