Propositional Logic

The attention mask in GPT is a boolean matrix $n \times n$. `mask[i][j] = True` means token i attends to token j. GPT-4's decoder computes the logical AND of two masks at every step: the causal mask (no peeking into the future) and the padding mask (no attending to empty positions). One boolean operation - and the model is blind to what it should not see. Propositional logic running on 8192 variables, executed billions of times per second.

• **Attention masking (GPT, BERT)**: boolean masks are AND-ed before softmax. Causal mask AND padding mask = final attention mask. No propositional logic - no transformers.
• **SAT solvers (Z3, CaDiCaL)**: verification of Intel circuits, Rust borrow rule checking, smart contract analysis. SAT is NP-complete, but CDCL solvers handle formulas with millions of variables.
• **SQL WHERE**: `WHERE age > 18 AND (role = 'admin' OR role = 'editor')` - conjunction and disjunction straight from theory. PostgreSQL optimizes via logical equivalences: De Morgan's laws.
• **Feature flags in production**: `if feature_enabled AND user_in_cohort AND not maintenance_mode` - three propositions, one conjunction. Flipt, LaunchDarkly - systems for managing boolean conditions at scale.

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

• Sets and Operations

Propositions: what can be evaluated as true or false

The attention mask in BERT is literally a boolean matrix: 1 = token visible, 0 = token hidden. `attention_mask[i][j] = True` is a proposition. Every `if` in production code is a proposition. Every SQL `WHERE` clause too. But not every sentence qualifies, and that distinction matters.

**Proposition** - a statement that is either **true (True)** or **false (False)**, but not both simultaneously. Denoted by lowercase letters: p, q, r, s...

Propositions can be **atomic** (indivisible: "it is raining") or **compound** (built from atomic propositions via connectives: "it is raining **and** it is cold"). Compound propositions are the topic of the next concept.

**Principle of bivalence:** every proposition has exactly one of two values - True or False. This is the foundation of classical logic. Multi-valued logics (fuzzy, three-valued) exist, but digital circuits - and GPUs - run on bivalent logic.

Logical connectives: ¬, ∧, ∨, →, ↔

PyTorch applies masks via `mask & valid_mask`. Elasticsearch builds boolean queries through `bool: {must: [...], should: [...], must_not: [...]}` - AND, OR, NOT wrapped in JSON. Formal logic gave programming its entire vocabulary of conditions.

**Operator precedence** (highest to lowest): 1. ¬ (negation) - highest 2. ∧ (conjunction, AND) 3. ∨ (disjunction, OR) 4. → (implication) 5. ↔ (biconditional) - lowest Therefore `¬p ∧ q → r` is read as `((¬p) ∧ q) → r`.

**Implication p → q is the most counter-intuitive connective!** It is false ONLY when p = True and q = False. When the antecedent is false, implication is ALWAYS true. "If 2 + 2 = 5, then the King of England am I" - this is a **true** statement! From a false premise, anything follows (ex falso quodlibet).

A useful analogy: p → q is a **guarantee**. "If the model passes tests (p), deployment is safe (q)". The guarantee is violated only if tests passed (p = True) yet deployment broke everything (q = False). If tests never ran - the guarantee is not violated regardless of outcome.

Truth Tables

Intel verifies processors before manufacturing. Billions of transistor states - manual checking is impossible. Formal verifiers build truth tables for critical circuits and automatically hunt for counterexamples. This is not academic exercise: it is how the Pentium FDIV bug - which cost the company 475 million USD in 1994 - is prevented from ever shipping again.

A **truth table** exhaustively enumerates all possible variable values and computes the formula's result for each combination. With n variables there will be $2^n$ rows - the same number from the power set lesson.

**Algorithm for building a truth table:** 1. Identify all atomic variables (p, q, r, ...) 2. Write all $2^n$ combinations of values 3. Evaluate intermediate sub-formulas (following operator precedence) 4. Compute the final result for each row

A truth table is pure **brute force**. For 3 variables - 8 rows; for 10 - already 1024. The same $2^n$ growth as in the power set. For real circuits with thousands of variables, SAT solvers take over: DPLL, CDCL. Microsoft's Z3 underpins code verification in Dafny and parts of the Windows testing infrastructure.

**Connection to sets:** the truth table for p ∧ q looks identical to the definition of intersection A ∩ B. For p ∨ q - like union A ∪ B. For ¬p - like complement. Not a coincidence: Boolean algebra is the shared foundation for both logic and set theory.

Tautologies, Contradictions, and Equivalences

Contrapositive is one of the most common techniques in mathematical proofs and in proof assistants (Coq, Lean). Instead of proving "if p then q", one proves "if not q then not p" - logically equivalent, sometimes orders of magnitude easier. DeepMind uses Lean to verify mathematical theorems. Every proof step is a logical equivalence.

**Key logical equivalences** (denoted ≡): - **De Morgan's Laws:** ¬(p ∧ q) ≡ ¬p ∨ ¬q and ¬(p ∨ q) ≡ ¬p ∧ ¬q - **Contrapositive:** p → q ≡ ¬q → ¬p - **Implication via disjunction:** p → q ≡ ¬p ∨ q - **Double negation:** ¬¬p ≡ p - **Distributivity:** p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)

**Contrapositive vs converse - do not confuse them!** - p → q (if rain - wet road) - **Contrapositive:** ¬q → ¬p (dry road - no rain) - **equivalent!** - **Converse:** q → p (wet road - rain) - **NOT equivalent!** The road could have been wetted by a street cleaner.

SAT solvers are industrial satisfiability checkers. Z3, MiniSat, CaDiCaL - they sit under the hood of Rust compilers (borrow rule checking), smart contract verifiers, and job schedulers. SAT is NP-complete, yet modern CDCL solvers handle formulas with millions of variables in practice. Tautologies and contradictions are the two extremes: they resolve immediately.

Key Ideas

• **Proposition** - a statement with a definite truth value (True/False). Questions, imperatives, paradoxes - not propositions
• **5 connectives:** ¬ (NOT), ∧ (AND), ∨ (OR), → (IMPLIES), ↔ (IFF). Implication is false ONLY for True → False
• **Truth table** - exhaustive enumeration of all $2^n$ combinations. Brute force for verifying formulas; SAT solvers are the smart industrial-scale version
• **Tautology** - always True (p ∨ ¬p). **Contrapositive** p → q ≡ ¬q → ¬p - the equivalence used in proofs and proof assistants like Lean and Coq
• **Boolean algebra** = logic = set theory: AND = ∩, OR = ∪, NOT = complement. One mathematical object, three interfaces

Related Topics

Propositional logic is the bridge between sets and predicate logic:

• Sets and Operations — ∪ = OR, ∩ = AND, complement = NOT - an isomorphic structure
• Predicate Logic — Adds quantifiers ∀ and ∃ - the next level of expressiveness
• Boolean Functions — Every truth table defines a Boolean function {0,1}^n → {0,1}

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

• Find a condition with 3+ AND/OR clauses in recent production code. Can it be simplified via De Morgan's law or contrapositive?
• Why is the defendant "innocent until proven guilty"? How does this connect to the fact that anything follows from a false premise?
• JavaScript has && and || with short-circuit evaluation. In what situations does short-circuit behavior matter for program correctness?

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

• dm-01 — Sets are the previous lesson; ∩/∪ mirror AND/OR
• dm-03 — Predicate logic adds quantifiers ∀ and ∃
• dm-06 — Boolean functions turn truth tables into circuits
• alg-01-big-o — SAT solvers are analyzed via Big O to understand NP
• alg-21-dp — DP correctness relies on logical invariants
• comp-23-local-optimization
• comp-22-ssa