Терм (математическая логика)

Терм (от лат. terminus — граница, предел) — в математической логике формальное выражение, обозначающее элемент предметной области (индивид) или функцию, отображающую элементы предметной области в неё же. Термы являются синтаксическими конструкциями, из которых, наряду с предикатами и кванторами, строятся формулы логики первого порядка. В отличие от формул, которые могут быть истинными или ложными, термы не имеют истинностного значения; они лишь обозначают объекты.

Определение

В формальной системе сигнатура (или язык) первого порядка задаётся набором символов, включающим:

Константы — символы, обозначающие фиксированные элементы предметной области (например, \(0\), \(1\), \(a\)).
Функциональные символы — символы, обозначающие операции над элементами, каждый из которых имеет фиксированную арность (число аргументов). Например, символ \(+\) с арностью 2, символ \(f\) с арностью 1.
Переменные — символы, обозначающие произвольные элементы предметной области (например, \(x, y, z\)).

Термы определяются рекурсивно:

Базовый случай: любая переменная или константа является термом.
Индуктивный шаг: если \(t_1, t_2, \dots, t_n\) — термы, а \(f\) — функциональный символ арности \(n\), то \(f(t_1, t_2, \dots, t_n)\) — терм.
Других способов построения термов нет.

Таким образом, термы — это замкнутые или открытые выражения, построенные из переменных, констант и функциональных символов. Например, в сигнатуре арифметики Пеано с константой \(0\) и функцией следования \(S\) термом является \(S(S(0))\), обозначающий число 2.

Классификация термов

По наличию переменных

Замкнутые термы (основные термы) — не содержат переменных. Например, \(f(a, b)\), где \(a\) и \(b\) — константы. В интерпретации такой терм обозначает конкретный элемент предметной области.
Открытые термы — содержат хотя бы одну переменную. Например, \(x + y\). Их значение зависит от приписывания значений переменным.

По сложности

Атомарные термы — переменные или константы.
Составные термы — функциональные применения к другим термам.

По типу

Термы-индивиды — обозначают элементы предметной области (например, числа, точки, множества).
Термы-функции — в некоторых расширениях логики (например, в логике высшего порядка) термы могут обозначать функции, но в классической логике первого порядка термы всегда обозначают индивиды.

Синтаксис и семантика

Синтаксис

Термы образуют индуктивно определённое множество выражений языка. Формально, пусть \(\Sigma\) — сигнатура, состоящая из множества констант \(C\) и множества функциональных символов \(F\) с указанием арности. Множество термов \(T(\Sigma, V)\) над сигнатурой \(\Sigma\) и множеством переменных \(V\) определяется как наименьшее множество, такое что:

\(V \subseteq T(\Sigma, V)\),
\(C \subseteq T(\Sigma, V)\),
если \(f \in F\) имеет арность \(n\) и \(t_1, \dots, t_n \in T(\Sigma, V)\), то \(f(t_1, \dots, t_n) \in T(\Sigma, V)\).

Семантика

Семантика термов задаётся через интерпретацию (модель). Модель \(\mathcal{M}\) состоит из:

Носителя (предметной области) \(D\) — непустого множества.
Интерпретации констант: каждой константе \(c \in C\) сопоставляется элемент \(c^{\mathcal{M}} \in D\).
Интерпретации функциональных символов: каждому символу \(f\) арности \(n\) сопоставляется функция \(f^{\mathcal{M}}: D^n \to D\).

Значение терма \(t\) в модели \(\mathcal{M}\) при оценке переменных \(s: V \to D\) (приписывании значений переменным) определяется рекурсивно:

Если \(t = x\) (переменная), то \([t]^{\mathcal{M}, s} = s(x)\).
Если \(t = c\) (константа), то \([t]^{\mathcal{M}, s} = c^{\mathcal{M}}\).
Если \(t = f(t_1, \dots, t_n)\), то \([t]^{\mathcal{M}, s} = f^{\mathcal{M}}([t_1]^{\mathcal{M}, s}, \dots, [t_n]^{\mathcal{M}, s})\).

Замкнутые термы имеют одно и то же значение при любой оценке, поэтому их значение определяется только моделью.

Примеры термов в различных теориях

Арифметика Пеано

Сигнатура: константа \(0\), функциональные символы: \(S\) (унарный), \(+\) и \(\times\) (бинарные).

Термы: \(0\), \(S(0)\), \(S(S(0))\), \(x + S(y)\), \((x + y) \times z\).
Замкнутый терм \(S(S(0))\) обозначает число 2.

Теория множеств (ZFC)

Сигнатура: бинарные предикаты \(\in\) и \(=\) (предикаты, а не функции), но для построения термов используются константы (например, \(\emptyset\)) и функциональные символы, вводимые определениями (например, операция объединения \(\cup\)).

Термы: \(\emptyset\), \(\{\emptyset\}\), \(x \cup y\).

Алгебра

Сигнатура: константа \(e\) (нейтральный элемент), функциональные символы: операция \(\cdot\) (бинарная), обратный элемент \(^{-1}\) (унарный).

Термы: \(e\), \(x \cdot y\), \((x \cdot y)^{-1}\), \(x \cdot (y \cdot z)\).

Термы и подстановка

Подстановка — это замена переменных в терме на другие термы. Формально, подстановка \(\sigma\) — это отображение из множества переменных в множество термов, такое что \(\sigma(x) = t\) для конечного числа переменных. Результат применения подстановки к терму \(t\) обозначается \(t\sigma\) и определяется рекурсивно:

Если \(t = x\), то \(t\sigma = \sigma(x)\).
Если \(t = c\) (константа), то \(t\sigma = c\).
Если \(t = f(t_1, \dots, t_n)\), то \(t\sigma = f(t_1\sigma, \dots, t_n\sigma)\).

Подстановка играет ключевую роль в правилах вывода, таких как модус поненс и обобщение, а также в унификации — алгоритме нахождения наиболее общего унификатора, используемом в автоматическом доказательстве теорем.

Термы в логике высшего порядка

В логике высшего порядка (например, в логике второго порядка) термы могут включать переменные, обозначающие функции или предикаты. Например, в логике второго порядка можно записать терм \(F(x)\), где \(F\) — переменная, обозначающая функцию из индивидов в индивиды. Однако в классической логике первого порядка такие конструкции не допускаются: функциональные символы фиксированы, а переменные обозначают только индивиды.

Применение в информатике

Термы широко используются в:

Формальных языках и грамматиках — для описания синтаксиса языков программирования (например, абстрактные синтаксические деревья).
Логическом программировании (язык Prolog) — программы состоят из фактов и правил, которые манипулируют термами. Унификация термов — основа механизма вывода.
Автоматическом доказательстве теорем — термы представляют объекты и функции, а алгоритмы резолюции и унификации оперируют ими.
Теории типов — термы являются основой для построения типизированных лямбда-исчислений, где каждый терм имеет тип.

Связь с формулами

Термы и формулы различаются по синтаксической роли:

Термы обозначают объекты.
Формулы выражают утверждения об объектах и могут быть истинными или ложными.

Формулы строятся из термов с помощью предикатов (например, \(t_1 = t_2\), \(P(t_1, \dots, t_n)\)), логических связок (\(\land, \lor, \neg, \to\)) и кванторов (\(\forall, \exists\)). Например, выражение \(x + y = z\) является формулой, где \(x + y\) и \(z\) — термы, а \(=\) — предикат.

Интересные факты

Понятие терма восходит к работам Готлоба Фреге, который ввёл различие между «именем» (термом) и «предложением» (формулой) в своей «Исчислении понятий» (1879).
В русскоязычной литературе термин «терм» иногда путают с «термином» (словом, обозначающим понятие), но в математической логике это строго формальное выражение.
В теории моделей термы используются для определения «определимых множеств»: множество \(A \subseteq D\) определимо, если существует формула \(\phi(x)\) такая, что для любого элемента \(a \in D\) выполнение \(\phi(a)\) равносильно \(a \in A\). Термы при этом служат для построения таких формул.

Источники

Мендельсон Э. «Введение в математическую логику» (глава 2, «Исчисление предикатов»).
Клини С. К. «Математическая логика» (раздел «Формальные системы»).
Ершов Ю. Л., Палютин Е. А. «Математическая логика» (глава «Язык логики первого порядка»).
Такеути Г. «Теория доказательств» (глава «Синтаксис и семантика логики первого порядка»).

BFOmetr — база данных и аналитика по компаниям России.

На главную BFOmetr →