Модуль I·Статья I·~5 мин чтения
Синтаксис и семантика пропозициональной логики
Пропозициональная логика
Превратить статью в подкаст
Выберите голоса, формат и длину — AI запишет аудио
Синтаксис и семантика пропозициональной логики
Мотивация: зачем формализовывать рассуждения?
Математические доказательства состоят из шагов, в которых одни утверждения выводятся из других. Но что такое «правильный» шаг? Пропозициональная логика даёт точный язык: синтаксис (как записывать формулы) и семантику (что они означают). Это фундамент, на котором стоят автоматические доказатели, компиляторы и системы верификации программ.
Синтаксис
Алфавит:
- Пропозициональные переменные: p, q, r, p₁, p₂, ...
- Логические связки: ¬ (отрицание), ∧ (конъюнкция — «и»), ∨ (дизъюнкция — «или»), → (импликация — «если... то»), ↔ (эквиваленция — «тогда и только тогда»).
- Скобки: (, ).
Индуктивное определение формул:
- Каждая переменная p — формула.
- Если φ — формула, то ¬φ — формула.
- Если φ и ψ — формулы, то (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ) — формулы.
- Ничто другое не является формулой.
Семантика: таблицы истинности
Интерпретация (оценка): функция 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-е годы предложил модельно-теоретическую трактовку истины, где семантика пропозициональной логики формулируется через оценки и структуры.
§ Акт · что дальше