Логика высказываний

Attention-маска в GPT - это булева матрица $n \times n$. `mask[i][j] = True` - токен i видит токен j. Декодер GPT-4 при каждом шаге вычисляет логическое AND двух масок: каузальной (нельзя смотреть в будущее) и padding-маски (нельзя смотреть в пустые позиции). Одна логическая операция - и модель не «видит» то, что не должна. Это пропозициональная логика на 8192 переменных, исполняемая миллиарды раз в секунду.

• **Attention masking (GPT, BERT)**: булевы маски AND-ятся перед softmax. Causal mask + padding mask = финальная маска внимания. Без пропозициональной логики - нет трансформеров.
• **SAT-солверы (Z3, CaDiCaL)**: верификация схем Intel, проверка borrow rules в компиляторе Rust, анализ смарт-контрактов. Задача SAT - NP-полная, но CDCL-солверы решают формулы из миллионов переменных.
• **SQL WHERE**: `WHERE age > 18 AND (role = 'admin' OR role = 'editor')` - конъюнкция и дизъюнкция прямо из теории. PostgreSQL оптимизирует через эквивалентные преобразования: законы де Моргана.
• **Feature flags в production**: `if feature_enabled AND user_in_cohort AND not maintenance_mode` - три высказывания, одна конъюнкция. Flipt, LaunchDarkly - системы управления булевыми условиями.

Предварительные знания

• Множества и операции

Высказывания: что можно оценить как истину или ложь

Transformer-маска в BERT - это буквально булева матрица: 1 = токен виден, 0 = токен скрыт. `attention_mask[i][j] = True` - высказывание. Каждый `if` в production-коде - высказывание. Каждый SQL `WHERE` - тоже. Но не каждое предложение является высказыванием, и это различие принципиально.

**Высказывание (proposition)** - это утверждение, которое является либо **истинным (True)**, либо **ложным (False)**, но не тем и другим одновременно. Обозначаются строчными буквами: p, q, r, s...

Высказывания бывают **атомарные** (неделимые: «идёт дождь») и **составные** (построены из атомарных с помощью связок: «идёт дождь **и** холодно»). Составные высказывания - тема следующего концепта.

**Принцип двузначности:** каждое высказывание имеет ровно одно из двух значений - True или False. Это фундамент классической логики. Существуют многозначные логики (нечёткая, трёхзначная), но в цифровых схемах - и в GPU - господствует двузначная.

Логические связки: ¬, ∧, ∨, →, ↔

PyTorch маскирует значения через `mask & valid_mask`. Elasticsearch строит булев запрос через `bool: {must: [...], should: [...], must_not: [...]}` - это AND, OR, NOT в JSON-обёртке. Формальная логика дала программированию весь словарь условий.

**Приоритет операций** (от высшего к низшему): 1. ¬ (отрицание) - самый высокий 2. ∧ (конъюнкция, AND) 3. ∨ (дизъюнкция, OR) 4. → (импликация) 5. ↔ (эквиваленция) - самый низкий Поэтому `¬p ∧ q → r` читается как `((¬p) ∧ q) → r`.

**Импликация p → q - самая контринтуитивная связка!** Она ложна ТОЛЬКО когда p = True и q = False. Если посылка ложна - импликация ВСЕГДА истинна. «Если 2 + 2 = 5, то я - король Англии» - это **истинное** высказывание. Из лжи следует что угодно (ex falso quodlibet).

Аналогия для импликации: p → q - это **гарантия**. «Если модель прошла тесты (p), можно деплоить (q)». Гарантия нарушена только если тесты прошли (p = True), но деплой сломал всё (q = False). Если тесты не запускались - гарантия не нарушена, каким бы ни был результат.

Таблицы истинности

Intel верифицирует процессор до производства. Тысячи транзисторов, миллиарды состояний - проверить руками невозможно. Формальные верификаторы строят таблицы истинности для критических схем и автоматически ищут контрпримеры. Это не академическая игра - это способ не допустить баг Pentium FDIV, который стоил компании 475 миллионов долларов в 1994 году.

**Таблица истинности** - полный перебор всех возможных значений переменных и вычисление результата формулы для каждой комбинации. Если переменных n, строк будет $2^n$ (то самое число из урока про булеан).

**Алгоритм построения таблицы истинности:** 1. Определить все атомарные переменные (p, q, r, ...) 2. Записать все $2^n$ комбинаций значений 3. Вычислить промежуточные подформулы (по приоритету связок) 4. Вычислить итоговый результат для каждой строки

Таблица истинности - это **брутфорс**. Для 3 переменных - 8 строк, для 10 - уже 1024. Тот же $2^n$, что и в булеане из прошлого урока. Для реальных микросхем с тысячами переменных используют SAT-солверы: DPLL, CDCL. Z3 от Microsoft лежит в основе верификации кода в Dafny и части тестов в Windows.

**Связь с множествами:** таблица истинности для p ∧ q выглядит идентично определению пересечения A ∩ B. Для p ∨ q - как объединение A ∪ B. Для ¬p - как дополнение. Это не совпадение: булева алгебра - общий фундамент логики и теории множеств.

Тавтологии, противоречия и эквивалентности

Контрапозиция - один из самых частых приёмов в математических доказательствах и в proof assistants (Coq, Lean). Вместо «если p, то q» доказывают «если не q, то не p» - то же самое, но иногда на порядок проще. Deepmind использует Lean для верификации математических теорем. Каждый шаг доказательства - логическая эквивалентность.

**Ключевые логические эквивалентности** (обозначаются ≡): - **Законы де Моргана:** ¬(p ∧ q) ≡ ¬p ∨ ¬q и ¬(p ∨ q) ≡ ¬p ∧ ¬q - **Контрапозиция:** p → q ≡ ¬q → ¬p - **Импликация через дизъюнкцию:** p → q ≡ ¬p ∨ q - **Двойное отрицание:** ¬¬p ≡ p - **Дистрибутивность:** p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)

**Контрапозиция vs обращение - не путать!** - p → q (если дождь - мокрая дорога) - **Контрапозиция:** ¬q → ¬p (сухая дорога - нет дождя) - **эквивалентно!** - **Обращение:** q → p (мокрая дорога - дождь) - **НЕ эквивалентно!** Дорогу мог полить поливальщик.

SAT-солверы - это промышленные проверщики выполнимости формул. Z3, MiniSat, CaDiCaL - они лежат под капотом компиляторов Rust (проверка borrow rules), верификаторов смарт-контрактов, планировщиков задач. Задача SAT - NP-полная, но на практике современные CDCL-солверы справляются с формулами из миллионов переменных. Тавтологии и противоречия - два крайних случая: они «решаются» немедленно.

Ключевые идеи

• **Высказывание** - утверждение с определённой истинностью (True/False). Вопросы, приказы, парадоксы - не высказывания
• **5 связок:** ¬ (NOT), ∧ (AND), ∨ (OR), → (IMPLIES), ↔ (IFF). Импликация ложна ТОЛЬКО при True → False
• **Таблица истинности** - полный перебор всех $2^n$ комбинаций. Brute-force для проверки формул; SAT-солверы - умный аналог для больших формул
• **Тавтология** - всегда True (p ∨ ¬p). **Контрапозиция** p → q ≡ ¬q → ¬p - эквивалентность, которую используют в доказательствах и proof assistants
• **Булева алгебра** = логика = теория множеств: AND = ∩, OR = ∪, NOT = дополнение. Один математический объект - три интерфейса

Связанные темы

Логика высказываний - мост между множествами и предикатной логикой:

• Множества и операции — ∪ = OR, ∩ = AND, дополнение = NOT - изоморфная структура
• Предикатная логика — Добавляет кванторы ∀ и ∃ - следующий уровень выразительности
• Булевы функции — Каждая таблица истинности задаёт булеву функцию {0,1}^n → {0,1}

Вопросы для размышления

• В последнем production-коде - найдите условие из 3+ AND/OR. Можно ли его упростить через закон де Моргана или контрапозицию?
• Почему в суде обвиняемый «невиновен, пока не доказано обратное»? Как это связано с тем, что из ложной посылки следует что угодно?
• JavaScript имеет && и || с short-circuit evaluation. Когда short-circuit поведение важно для корректности программы?

Связанные уроки

• dm-01 — Множества - предыдущий урок, операции ∩/∪ зеркалят AND/OR
• dm-03 — Предикатная логика - следующий шаг с кванторами ∀ и ∃
• dm-06 — Булевы функции - таблица истинности становится схемой
• alg-01-big-o — SAT-солверы анализируются через Big O для понимания NP
• alg-21-dp — DP-рассуждения строятся через логические инварианты
• comp-23-local-optimization
• comp-22-ssa