Mathematical Logic
Propositional Logic
2003. Intel Pentium 4. A bug in the floating-point multiplication unit. Cost of the recall: 475 million dollars. After that, Intel started verifying every transistor via SAT solvers. The same formulas that prove `False -> True = True` now check that a CPU computes 2+2=4 across every one of 10^18 possible input combinations. Propositional logic is not a textbook abstraction - it is the only way to prove a chip correct before it ships.
- **SAT solvers (Z3 by Microsoft, CaDiCaL)**: verification of Intel/AMD processors - formulas with ~10^6 variables, solved in seconds despite NP-completeness
- **Amazon AWS and Microsoft Azure**: TLA+ and SMT solvers check IAM policies and distributed-system protocols - formal verification running on billions of requests
- **LLM chain-of-thought**: GPT-4 imitates logical inference (modus ponens, transitivity) during reasoning - Kahneman System 2 implemented as a probabilistic machine
- **Chip design**: AMD and Apple Silicon use SAT to verify circuit correctness - up to a billion transistors, not a single one left unchecked
Logical Connectives
Every `if (x > 0 && y != null)` is propositional logic. Every LLVM optimization that rewrites `!(a && b)` as `(!a || !b)` is De Morgan. Every SMT solver proving that an AWS IAM policy allows no unauthorized access is SAT. **Propositional logic** is the language of True/False statements and **connectives** that combine them - sitting under half of modern programming.
| Connective | Symbol | Reading | Python | Example |
|---|---|---|---|---|
| Negation | NOT p | not p | not p | it is not raining |
| Conjunction | p AND q | p and q | p and q | rain and wind |
| Disjunction | p OR q | p or q | p or q | rain or snow |
| Implication | p -> q | if p, then q | not p or q | if rain, then umbrella |
| Biconditional | p <-> q | p if and only if q | p == q | even <-> divisible by 2 |
**Operator precedence** (from highest to lowest): NOT > AND > OR > -> > <->. Without parentheses, `NOT p AND q OR r` is parsed as `((NOT p) AND q) OR r`. Parentheses always help clarify the meaning.
**Implication** is the most counterintuitive connective. `p -> q` is false ONLY when p is true and q is false. In particular, `False -> anything = True` (ex falso quodlibet - from a false premise, anything follows). This is not a bug - it's the definition required for mathematical consistency.
Propositional variables (p, q, r) are **atoms**. From atoms and connectives we build **formulas**: `(p -> q) AND (q -> r) -> (p -> r)` is the law of transitivity of implication. A formula is a **tautology** (always True), a **contradiction** (always False), or **satisfiable** (True for some assignment). SAT solvers target the third case - and that is worth billions in chip verification.
What is the value of `False -> True`?
Truth Tables
A **truth table** is the brute-force check for a formula: enumerate ALL combinations of variable values, compute the result. For n variables - 2^n rows. Always True - tautology. The method is perfect and non-scalable at the same time.
**Exponential explosion**: for 10 variables - 1,024 rows; for 20 - one million; for 100 - more than atoms in the universe. Truth tables work but don't scale. For large formulas, algorithmic methods are needed (DPLL, CDCL).
**De Morgan's laws** are foundational: NOT(p AND q) = (NOT p) OR (NOT q) and NOT(p OR q) = (NOT p) AND (NOT q). LLVM and GCC apply them thousands of times per second while optimizing conditional expressions into machine code. Programmers know De Morgan intuitively - now it has a formal name.
| Law | Formula | Programmer Example |
|---|---|---|
| De Morgan 1 | NOT(p AND q) = NOT p OR NOT q | !(a && b) == (!a || !b) |
| De Morgan 2 | NOT(p OR q) = NOT p AND NOT q | !(a || b) == (!a && !b) |
| Double negation | NOT NOT p = p | !!x == x |
| Distributivity | p AND (q OR r) = (p AND q) OR (p AND r) | Like a*(b+c)=ab+ac |
| Contrapositive | (p -> q) = (NOT q -> NOT p) | if rain→wet, then dry→no rain |
How many rows are in a truth table for a formula with 4 variables?
Normal Forms
The same logical formula can be written in many ways. **Normal forms** are canonical representations for algorithmic processing. CNF is the global standard for SAT solvers. DNF is the language of knowledge bases and classifiers. Two forms, two worlds of application.
**CNF** is the input language of every SAT solver. Z3 from Microsoft, MiniSat, CaDiCaL - all accept CNF. Any formula converts to CNF in polynomial time via the Tseytin transformation. This format is what lets engineers verify correctness of Apple M-series ARM chips.
| Property | CNF | DNF |
|---|---|---|
| Structure | AND of (OR of literals) | OR of (AND of literals) |
| SAT check | NP-complete | Polynomial (at least 1 conjunct True) |
| TAUT check | Polynomial (all clauses True) | NP-complete |
| Size | Can be exponential | Can be exponential |
| Use case | SAT solvers, verification | Knowledge bases, classification |
**Tseytin transformation** converts a formula to CNF with only polynomial size growth. The idea: introduce new variables for subformulas. The formula `(a ∧ b) ∨ (c ∧ d)` gets variables x = (a ∧ b), y = (c ∧ d), and produces CNF for x ∨ y plus definitions of x and y.
Which formula is in CNF?
Satisfiability (SAT)
Given a formula in CNF - does there exist an assignment of variable values that makes it true? This is the **SAT problem** - the first problem proven **NP-complete** (Cook, 1971). Theoretically intractable. In practice - modern solvers handle formulas with a million variables in seconds. The gap between worst-case theory and real-world instances is one of the deepest puzzles in CS.
**DPLL** (Davis-Putnam-Logemann-Loveland, 1962) is the classic SAT algorithm. Idea: choose a variable, assign True or False, simplify the formula, recurse. Optimizations: **unit propagation** (if a clause has one literal - its value is forced) and **pure literal elimination**.
Despite NP-completeness, modern SAT solvers (Z3, CaDiCaL, Kissat) handle industrial problems with **millions** of variables. Intel and AMD - processor verification. Amazon AWS and Microsoft Azure - formal verification of cloud systems via TLA+. Apple - M-series chip correctness. SMT solvers (SAT + theories) go further: symbolic execution, automated theorem proving, security analysis of code.
| SAT Application | Example | Variables |
|---|---|---|
| Chip verification | Intel CPU correctness | ~10⁶ |
| Scheduling | Exam timetabling | ~10⁴ |
| Cryptanalysis | Finding MD5 collisions | ~10⁵ |
| Configuration | Linux kernel config | ~10⁴ |
| Formal verification | Proofs of programs | ~10⁵ |
SAT is not abstract. Every problem in NP reduces to SAT: graph coloring, knapsack, Sudoku, route planning. If a problem reads as "find values satisfying a set of constraints" - it encodes as SAT. That is exactly how Qualcomm verifies Snapdragon: chip constraints become a CNF formula, the SAT solver either confirms all paths are correct or returns a concrete counterexample.
Implication p → q means a causal relationship: p causes q
Implication p → q is a logical connective equivalent to ¬p ∨ q. It is false only when the premise is true and the conclusion is false.
In everyday speech, "if it rains, the street is wet" implies causation. In logic, p → q is just a constraint: p = True and q = False cannot both hold. "If 2+2=5, the Moon is made of cheese" is logically true (False → anything = True). This is exactly what SAT solvers exploit: an UNSAT formula implies anything, including False - which is how a solver flags a contradiction in a chip's logic.
Is the formula (p) ∧ (¬p) satisfiable?
Key Takeaways
- **Connectives** (NOT, AND, OR, ->, <->) are the alphabet of formal reasoning - the same language in `if/else`, SQL WHERE, and firewall rules
- **Truth tables** give exhaustive verification in O(2^n) - tractable for 10 variables, not for 10^6
- **CNF** (AND of ORs) is the language of SAT solvers; everything from Sudoku to processor correctness is encoded in it
- **SAT** - the first NP-complete problem (Cook, 1971); Z3, MiniSat, and CaDiCaL solve industrial instances with millions of variables in seconds - theory and practice diverge sharply here
Related Topics
Propositional logic is the foundation for more powerful logical systems:
- First-Order Predicate Logic — Extends propositional logic with quantifiers (for all, there exists) and predicates
- Natural Deduction — A formal proof system for propositional and predicate formulas
Вопросы для размышления
- Why is `False -> True = True`? How does SAT solver use this property to detect contradictions in chip logic?
- Encoding Sudoku as SAT: each cell is a variable, each constraint is a clause. How many clauses does a standard 9x9 grid require?
- Why is SAT (satisfiability) NP-complete while tautology checking is co-NP? What is the practical difference for program verification?