Модуль I·Статья I·~5 мин чтения

Синтаксис и семантика пропозициональной логики

Пропозициональная логика

Превратить статью в подкаст

Выберите голоса, формат и длину — AI запишет аудио

Синтаксис и семантика пропозициональной логики

Мотивация: зачем формализовывать рассуждения?

Математические доказательства состоят из шагов, в которых одни утверждения выводятся из других. Но что такое «правильный» шаг? Пропозициональная логика даёт точный язык: синтаксис (как записывать формулы) и семантику (что они означают). Это фундамент, на котором стоят автоматические доказатели, компиляторы и системы верификации программ.

Синтаксис

Алфавит:

  • Пропозициональные переменные: p, q, r, p₁, p₂, ...
  • Логические связки: ¬ (отрицание), ∧ (конъюнкция — «и»), ∨ (дизъюнкция — «или»), → (импликация — «если... то»), ↔ (эквиваленция — «тогда и только тогда»).
  • Скобки: (, ).

Индуктивное определение формул:

  1. Каждая переменная p — формула.
  2. Если φ — формула, то ¬φ — формула.
  3. Если φ и ψ — формулы, то (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ) — формулы.
  4. Ничто другое не является формулой.

Семантика: таблицы истинности

Интерпретация (оценка): функция I: {переменные} → {0, 1}. Расширяется на все формулы:

  • I(¬φ) = 1 − I(φ)
  • I(φ ∧ ψ) = min(I(φ), I(ψ)) — истинно, если оба истинны
  • I(φ ∨ ψ) = max(I(φ), I(ψ)) — истинно, если хотя бы одно
  • I(φ → ψ) = max(1−I(φ), I(ψ)) — ложно только при φ=1, ψ=0
  • I(φ ↔ ψ) = 1 тогда и только тогда, когда I(φ) = I(ψ)

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

  • Тавтология: I(φ) = 1 при всех интерпретациях. Обозначение: ⊨ φ.
  • Противоречие (антитавтология): I(φ) = 0 при всех интерпретациях.
  • Выполнимость: I(φ) = 1 для некоторой I.

Логическое следование и эквивалентность

Следование: Γ ⊨ φ, если любая I, делающая все ψ ∈ Γ истинными, делает истинным φ.

Логическая эквивалентность: φ ≡ ψ, если I(φ) = I(ψ) при всех I. Примеры:

  • ¬¬p ≡ p (двойное отрицание)
  • (p → q) ≡ (¬p ∨ q) (импликация через дизъюнкцию)
  • ¬(p ∧ q) ≡ (¬p ∨ ¬q) (закон де Моргана)
  • ¬(p ∨ q) ≡ (¬p ∧ ¬q) (закон де Моргана)

Законы дистрибутивности:

  • p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)
  • p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r)

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

Задача: Доказать тавтологию «закон силлогизма»: (p → q) → ((q → r) → (p → r)).

Шаг 1. Допустим, что всё выражение ложно. Тогда (p → q) = 1 и ((q → r) → (p → r)) = 0.

Шаг 2. (q → r) → (p → r) = 0 → (q → r) = 1 и (p → r) = 0.

Шаг 3. (p → r) = 0 → p = 1 и r = 0.

Шаг 4. (q → r) = 1 с r = 0 → q = 0.

Шаг 5. (p → q) = 1 с p = 1 → q = 1. Но из шага 4: q = 0. Противоречие!

Вывод: Допущение о ложности приводит к противоречию → формула тождественно истинна ⊨ (p→q)→((q→r)→(p→r)).

Таблица истинности (сокращённая): При p=1, q=0, r=0: (p→q) = (1→0) = 0. Всё выражение: 0 → ... = 1 ✓. При p=1, q=1, r=0: (p→q)=1, (q→r)=(1→0)=0, (q→r)→(p→r)=0→0=1, итог: 1→1=1 ✓.

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

Верификация аппаратуры: логические схемы (AND/OR/NOT/NAND) реализуют пропозициональные формулы. Инструменты типа CBMC (Bounded Model Checker) автоматически проверяют, что схема удовлетворяет спецификации — по сути, проверяют тавтологию.

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

Пропозициональная логика — это не только теоретический фундамент, но и практический инструмент: SAT-солверы (Z3, MiniSAT, CryptoMiniSAT) ежедневно решают миллионы пропозициональных формул в задачах верификации схем, планирования действий, криптоанализа и автоматического доказательства теорем. Теоретическая граница — NP-полнота проблемы SAT (теорема Кука–Левина 1971 г.) — означает, что в худшем случае любой алгоритм требует экспоненциального времени, но современные эвристики (CDCL — conflict-driven clause learning, restarts, watched literals) делают практически разрешимыми задачи с миллионами переменных. На стыке логики и математики пропозициональная логика лежит в основе булевых сетей и моделей биологической регуляции генов.

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

Пропозициональная логика естественно интерпретируется как частный случай булевых алгебр, описанных Дж. Буля в середине XIX века и аксиоматизированных М. Стоуном. Теорема Стоуна о репрезентации булевых алгебр связывает синтаксис логики с топологическими пространствами: каждой булевой алгебре соответствует компактное тотально несвязное пространство (пространство ультрафильтров), а логические операции реализуются через операции над замкнутыми множествами. Эта конструкция используется в теории динамических систем с дискретными состояниями, где логические формулы кодируют инварианты и множества траекторий.

Связь с алгеброй появляется и через решётки: законы дистрибутивности и де Моргана являются частным случаем общих фактов о дистрибутивных решётках, изучаемых в универсальной алгебре. В теории вероятностей логические связки моделируют события и их комбинации: классическая формализация Колмогорова опирается на σ-алгебры, которые являются «σ-версиями» булевых алгебр. Тавтологии пропозициональной логики превращаются в тождественные вероятностные равенства для любых моделей, например правила суммирования и условной вероятности.

В численных методах, особенно при решении дифференциальных уравнений с условиями переключений, логические формулы задают области в пространстве фазовых переменных, где действует та или иная система уравнений. Гибридные системы описываются как сочетание непрерывной динамики и дискретной логики, и здесь используются логико-алгебраические методы верификации: логические инварианты, вычисляемые через абстрактную интерпретацию, гарантируют корректность численных схем. В комбинаторной оптимизации пропозициональные ограничения переводятся в SAT-задачи; далее линейное и целочисленное программирование (работы Дж. Гомори, Р. Карпа) комбинируется с логическими решателями, образуя так называемые SMT-методы, применяемые в современном анализе алгоритмов и моделей.

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

Первая строгая система пропозиционального исчисления была фактически сформирована Фреге в «Begriffsschrift» (1879), где он ввёл формальный язык для представления математических рассуждений. Однако идея чёткого разделения синтаксиса и семантики была систематизирована уже в начале XX века Гильбертом и его школой; их курс «Grundlagen der Mathematik» (1934–1939) дал аксиоматические системы для пропозициональной и предикатной логики. Альфред Тарский в 1930-е годы предложил модельно-теоретическую трактовку истины, где семантика пропозициональной логики формулируется через оценки и структуры.

§ Акт · что дальше