The deepest point about logic: it studies not "what is true" but "how truth necessarily yields truth." "All A are B; x is A; therefore x is B" — this inference is valid no matter what A, B, x actually mean. Strip away all the content and only the skeleton of form remains, and validity lives only in the skeleton.
The raw materials are "propositions" — statements that are true or false — and four connectives: AND ($\land$), OR ($\lor$), NOT ($\neg$), IMPLIES ($\to$). The truth table is the multiplication table of logic: given the truth of the parts, the truth of the whole is computed mechanically. Here logic first becomes something computable.
Propositional variables $p,q,\dots$ take values true/false. Implication can be defined as $p \to q \equiv \neg p \lor q$ — "$p$ implies $q$" is equivalent to "either $p$ is false, or $q$ is true." This explains the table's most counterintuitive row: when the premise is false, the implication is always true (an empty promise is never broken). A formula true under every assignment is a tautology — a law that always holds, in the logical sense.
The real shock is a triple isomorphism: inference, switching circuits, and set operations are three faces of the same structure. $\land$ corresponds to series circuits and to set intersection; $\lor$ to parallel circuits and union; De Morgan's law $\neg(p\land q)\equiv\neg p\lor\neg q$ is at once a logical law, a circuit-simplification rule, and a set identity. This shared skeleton is Boolean algebra. When Boole said "the laws of thought can be operated on like algebra," he never imagined that a century later it would become the physical blueprint of every CPU.
Digital circuits: a single NAND gate can build all of logic, and a whole processor is nothing but propositional logic realized in silicon. SAT solvers — deciding whether a pile of logical constraints can all be satisfied at once — are the core engine of chip verification, software testing, and scheduling, and SAT was the first problem proved NP-complete. A compiler's type checking and a database's predicate pushdown all run propositional logic underneath.
Propositional logic has a fatal muteness: it cannot say "for all" or "there exists." "All primes are greater than 1" is just an indivisible atom to it. Predicate logic fills this gap — it introduces quantifiers "for all $x$" ($\forall x$), "there exists $x$" ($\exists x$), and predicates $P(x)$ that carry variables ("$x$ is prime").
With just this one extension, logic can suddenly write down all of mathematics. The skeleton of a claim like "every number has a successor" is entirely a weaving of quantifiers and predicates. Predicate logic is the invisible grammar in a mathematician's head when writing rigorous statements.
$\forall x\,P(x)$ means "for every $x$ in the domain, $P(x)$ holds"; $\exists x\,P(x)$ means "at least one $x$ makes $P(x)$ hold." The core difficulty is the order of nested quantifiers:
The left says "every number has a larger one" (true); the right says "there is a number larger than all numbers" (false over the naturals). Same symbols, swap the order, and truth flips.
Almost the entire secret of mathematical rigor hides in quantifier order. The $\varepsilon$–$\delta$ definition of a limit, $\forall\varepsilon\,\exists\delta\,\forall x\,(\dots)$, took two centuries for Cauchy and Weierstrass to polish precisely because human intuition struggles with three order-dependent quantifiers: "first give me any small $\varepsilon$, then I find $\delta$." Reading quantifier order precisely is nearly the same as reading mathematics — the difference between continuity and uniform continuity is just two quantifiers changing places.
SQL queries are essentially predicate logic: `WHERE` is a predicate, `EXISTS`/`ALL` are quantifiers, and relational database theory is built directly on first-order logic. Prolog lets you "write facts and rules, and the machine reasons automatically." Proof assistants Lean and Coq use first-order (and higher-order) logic to formalize all of mathematics. AI knowledge representation, automated theorem proving, and program specifications (pre/postconditions) all take predicate logic as their lingua franca.
Picture the sentence: "This sentence cannot be proved." If it can be proved, it is false — the system has proved a falsehood and collapses. If it cannot be proved, it is exactly right — so it is true, yet the system cannot prove it. What Gödel did in 1931 was translate this self-referential sentence into a pure arithmetic statement about integers.
The trick is "Gödel coding": assign every symbol, formula, and proof a unique number. Then "some formula is provable" becomes "some number has a certain arithmetic property." The system is forced to begin talking about itself — the liar paradox acquires, for the first time, a mathematical body.
First incompleteness theorem: any consistent formal system $T$ that can express basic arithmetic and whose axioms can be mechanically enumerated contains a sentence $G$ such that $T$ can prove neither $G$ nor $\neg G$ — $G$ is undecidable (while, metamathematically, it is true).
Second incompleteness theorem: such a $T$ cannot prove its own consistency $\mathrm{Con}(T)$ from within. A system that could prove "I am consistent" would thereby already be inconsistent.
This is the deepest "look in the mirror" in the history of mathematics. Hilbert's grand dream was to mechanize all of mathematics: one set of axioms proving every truth and proving its own freedom from contradiction. Gödel shattered that dream from inside the system — "true" always exceeds "provable." The real beauty is not that it's a failure, but its revelation: incompleteness is not anyone's lack of cleverness, but an inborn limit of any sufficiently rich formal system. It is one of three faces of a single coin, along with Turing's halting problem and Tarski's undefinability of truth — once self-reference is strong enough, a system cannot fully grasp itself.
Its direct descendant is the halting problem: no program can decide whether an arbitrary program halts — so there is no "perfect universal bug detector," and programs cannot fully verify themselves, drawing a hard boundary on decidability in software engineering. In AI, the split between "true" and "provable" reminds us: however powerful a formal system (or model), there are true statements it cannot in principle reach; interpretability and alignment cannot expect a system to give complete formal guarantees about itself.
A mathematical proof is usually "an argument that convinces one's peers" — carrying intuition, omissions, and "clearly it follows." Formalization pushes this to the extreme: a proof becomes a string of symbols, each step either an axiom or mechanically derived by explicit rules from earlier steps. Meaning is stripped away entirely, leaving only form — and the proof thereby becomes an object a machine can check character by character.
This seems to squeeze the soul out of mathematics; in fact the opposite: it gives "is this proof correct?" its first verdict that depends on no authority. The judge of truth passes from human conviction to the checking of rules.
A formal system = an alphabet + a syntax of well-formed formulas + some axioms + finitely many inference rules (the classic being modus ponens: from $p$ and $p\to q$, infer $q$). A proof is a finite sequence of formulas in which each item is either an axiom or follows from earlier items by some rule; the last item is the theorem proved. Deciding "is this sequence a valid proof?" is a purely syntactic, mechanically executable process.
The deepest beauty is the Curry–Howard correspondence: a proof is a program, a proposition is a type. "Proving $A\to B$" and "writing a function that turns an input of type $A$ into an output of type $B$" are the same thing; running a program corresponds to simplifying a proof. Logic, computation, and types — three domains seemingly belonging to philosophy, engineering, and linguistics — are isomorphic at the bottom. This is why modern proof assistants are also programming languages: to them, checking a proof and running code were never different.
Lean and Coq have fully mechanically verified giant proofs "hard for humans to check line by line," such as the four-color theorem and the Kepler sphere-packing conjecture; Terence Tao is using Lean to formalize frontier papers. In engineering, the OS kernel seL4 and the C compiler CompCert have been formally verified to "mathematically guarantee the absence of certain bugs," for zero-tolerance settings. Blockchain smart contracts and cryptographic protocols increasingly rely on formal verification to plug costly logical holes.