Синтаксис и семантика логики первого порядка

Мотивация: говорить о структурах, а не просто о высказываниях

Пропозициональная логика не может выразить «все натуральные числа чётны» или «существует простое число». Логика первого порядка (ЛПП, FOL) добавляет кванторы ∀ и ∃, предикатные символы и функциональные символы — это язык современной математики. В ЛПП формулируются теория групп, арифметика, теория множеств.

Синтаксис ЛПП

Сигнатура σ: множество предикатных символов P (с арностью n), функциональных символов f (с арностью n) и констант c (нульарные функции).

Термы (рекурсивное определение):

• Переменные x, y, z, ... — термы.
• Константы c — термы.
• Если f — функциональный символ арности n и t₁,...,tₙ — термы, то f(t₁,...,tₙ) — терм.

Формулы:

• P(t₁,...,tₙ) — атомарная формула (предикат P применён к термам).
• t₁ = t₂ — атомарная формула равенства.
• ¬φ, φ∧ψ, φ∨ψ, φ→ψ — из пропозициональных связок.
• ∀x φ — квантор всеобщности: «для всех x выполнено φ».
• ∃x φ — квантор существования: «существует x, для которого φ».

Свободные и связанные переменные: x свободна в φ, если она не в области действия кванторов по x. В ∀x P(x,y): x — связана, y — свободна.

Семантика: структуры первого порядка

Структура M = (D, P^M, f^M, c^M):

• D ≠ ∅ — домен (носитель), например ℕ, ℤ, ℝ, граф и т.д.
• Для каждого P арности n: P^M ⊆ Dⁿ — отношение.
• Для каждого f арности n: f^M: Dⁿ → D — функция.
• Для каждой константы c: c^M ∈ D.

Оценка переменных: μ: {переменные} → D.

Истинность M ⊨ φ[μ] (рекурсивно):

• M ⊨ P(t₁,...,tₙ)[μ] ⟺ (t₁^M[μ],...,tₙ^M[μ]) ∈ P^M
• M ⊨ ∀x φ[μ] ⟺ M ⊨ φ[μ[x↦d]] для всех d ∈ D
• M ⊨ ∃x φ[μ] ⟺ M ⊨ φ[μ[x↦d]] для некоторого d ∈ D

Ключевые понятия

Предложение (замкнутая формула): нет свободных переменных. Истинность не зависит от оценки.

Теория T: множество предложений. M — модель T, если M ⊨ φ для всех φ ∈ T.

Логически истинная формула: M ⊨ φ в любой структуре M.

Численный пример

Задача: Пусть M = (ℤ, <, S), где < — стандартный порядок, S(x) = x+1. Проверить истинность: (а) ∀x ∃y (x < y), (б) ∃x ∀y (x < y), (в) ∀x ∀y (x < y → S(x) < S(y)).

Шаг 1. (а) ∀x ∃y (x < y): для любого целого x нужен y > x. Берём y = x+1 ∈ ℤ. Истинно ✓.

Шаг 2. (б) ∃x ∀y (x < y): нужен наименьший элемент ℤ. Но в ℤ нет наименьшего целого. Ложно ✓.

Шаг 3. (в) ∀x ∀y (x < y → S(x) < S(y)): если x < y, то x+1 < y+1. Это очевидное свойство целых. Истинно ✓.

Дополнительно. Запишем «плотность порядка» на ЛПП: ∀x ∀y (x < y → ∃z (x < z ∧ z < y)). В (ℤ,<): при x=0, y=1 нет z с 0 < z < 1 в ℤ. Ложно в ℤ. В (ℚ,<) или (ℝ,<) — истинно.

Реальное приложение

Базы данных: SQL — практически ЛПП первого порядка. Запрос «выбрать всех сотрудников, у которых зарплата больше средней» — это ∀x (Empl(x) ∧ Sal(x) > Avg → Result(x)). Оптимизаторы запросов используют логические преобразования формул.

Дополнительные аспекты

Логика предикатов первого порядка добавляет к пропозициональной логике кванторы ∀ и ∃ и предикаты от переменных. Это даёт выразительность, достаточную для аксиоматизации теории чисел (арифметика Пеано), теории множеств (ZFC) и большей части обычной математики. Теорема Лёвенгейма–Скулема о том, что любая выполнимая теория имеет счётную модель, приводит к парадоксу Скулема (несчётность множества вещественных чисел в счётной модели ZFC). На практике first-order resolution-провер E, Vampire, Prover9 решают задачи в теории групп, колец, реляционных БД, верификации программ и алгебраической геометрии.

Связь с другими разделами математики

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

В топологии логика первого порядка проявляется в описании структур, где свойства типа компактности или связности формулируются через предикаты над открытыми множествами. Работы Тарского и Чейтина по топологическим полугруппам опираются на элементарные теории этих структур. В теории вероятностей ЛПП используется при аксиоматизации вероятностных пространств Колмогорова: сигма-алгебры, события и случайные величины описываются предикатами, а такие результаты, как теорема Лёви о монотонной сходимости, формализуются в логике с кванторами по событиям. В численных методах логический язык применяется для спецификации корректности алгоритмов: свойства сходимости итерационных схем, устойчивость схем конечных разностей и корректность методов Монте‑Карло записываются как универсальные и экзистенциальные высказывания о последовательностях приближений и вероятностных оценках.

Историческая справка и развитие идеи

Корни логики первого порядка уходят к Фреге, опубликовавшему в 1879 году «Begriffsschrift», где впервые была предложена формальная теория предикатов. Пеано в «Arithmetices principia» (1899) применил подобный язык для аксиоматизации натуральных чисел. Современный синтаксис и семантика ЛПП были систематизированы Гильбертом и Акерманом в книге «Grundzüge der theoretischen Logik» (1928), где обсуждались понятия модели и следования. Тарский в статье 1935 года «Der Wahrheitsbegriff in den formalisierten Sprachen» сформулировал модельно-теоретическое определение истины, положив начало семантическому подходу. В 1930‑х годах Лёвенгейм, Скулем и Малцев развили технику шкалирования моделей и доказали теоремы о компактности и счетности моделей выполнимых теорий. Поворотным моментом стали работы Гёделя: теорема полноты (1930) показала совпадение синтаксического и семантического следования, а теоремы о неполноте (1931) выявили ограничения аксиоматизации арифметики.