Curriculum

Foundation concepts - binary operations, the four group axioms, recognizing groups, and understanding abelian vs non-abelian structure.

Building intuition through familiar examples - integers mod n, cyclic groups, symmetric groups, dihedral groups, and more.

Subgroups, cosets, Lagrange's theorem - the fundamental counting and structural constraints of group theory.

Structure-preserving maps between groups - homomorphisms, kernels, images, isomorphisms, and automorphisms.

Normal subgroups, quotient groups, the first isomorphism theorem, and simple groups.

Groups acting on sets - orbits, stabilizers, and the connection between algebra and combinatorics.

Beyond groups - algebraic structures with two operations, from rings to fields.

Connecting abstract algebra to the real world - cryptography, physics, puzzles, and error correction.

The conceptual framework for thinking about organizations adversarially—attack surfaces, threat taxonomies, and the economics of exploitation.

Controlling what people believe—disinformation mechanics, narrative manipulation, credibility attacks, and epistemic warfare against organizational decision-making.

Exploiting human psychology in organizational contexts—authority, trust, pretext, elicitation, and influence at scale.

Attacks from within—insider threat types, recruitment, access exploitation, concealment, exfiltration, and sabotage that looks like incompetence.

Attacking organizations through markets, resources, and economic relationships—supply chains, financial systems, talent, and standards as weapons.

Using legitimate systems as weapons—regulatory capture, lawfare, compliance weaponization, and strategic litigation.

Attacking morale, cohesion, and will—systematically degrading an organization's capacity to function through psychological means.

Getting inside and changing things—placement techniques, access escalation, network mapping, and institutional capture.

Where technical and organizational attacks intersect—exploiting human-system interfaces, processes, and trusted channels.

When the goal is destruction rather than exploitation—market exit, reputation destruction, death spirals, and scorched earth.

Historical examples analyzed through the adversarial lens—learning from real operations.

Detecting, disrupting, and defending against organizational attacks—the defensive counterpart to adversarial operations.

Defeating defensive measures—how sophisticated adversaries evade detection, exploit resilience mechanisms, and degrade incident response.

Reading derivative information to describe function behavior: critical points, monotonicity, concavity, and synthesis.

Existence guarantees and the closed interval method: EVT, Fermat's Theorem, absolute extrema on closed and open intervals.

The theoretical backbone bridging local derivative information to global function behavior: Rolle's Theorem, MVT, consequences, and applications.

Strategic deployment of derivative tools in modeling contexts: problem setup, constraint reduction, domain classification, and applied problems.

Applying the chain rule to implicitly time-dependent equations: setup, relating variables, differentiation with respect to time, and solving.

The tangent line as universal tool: linearization, differentials, error estimation, Newton's method, and the bridge to integration.

Master deterministic and nondeterministic finite automata—the simplest model of computation that recognizes patterns.

Explore regular expressions, their equivalence to finite automata, and the fundamental limits of pattern recognition.

The universal model of computation that defines the limits of what can be computed.

Automata for infinite words—Büchi automata, temporal logic, and model checking.

Automata over semirings—computing values instead of just accepting/rejecting.

The primitive elements of Boolean logic - truth values, NOT, AND, and OR - the building blocks of all digital logic.

Combining operations into compound expressions, understanding logic gates, and exploring extended operations like XOR.

Laws and properties for transforming and simplifying Boolean expressions - the algebraic toolkit for logical manipulation.

Standard representations of Boolean functions - canonical forms that enable systematic analysis and comparison.

Techniques for reducing Boolean expressions to simpler equivalent forms - algebraic methods and visual tools.

Boolean logic in practice - truth tables, circuit analysis, and proving equivalence between different implementations.

Categories, morphisms, composition, and the basic language of categorical reasoning.

Structure-preserving maps between categories. The morphisms of the category of categories.

Maps between functors. The key notion that makes category theory work.

Characterizing objects by their relationship to all other objects. The categorical way.

The general framework for universal constructions. Refining and gluing.

Pairs of functors that are optimal approximations of each other. The heart of category theory.

The Yoneda lemma and embedding. Objects known by their relationships.

Monads, equivalences, Kan extensions, and categorical logic.

2-categories, string diagrams, enriched categories, and bicategories reveal category theory's higher-dimensional nature.

Play tiny games by hand. Discover that position structure determines outcome. Meet the simplest game. Learn to analyze game trees backward.

Classify positions formally as P or N. Discover the XOR pattern in multi-heap Nim. Build the binary/XOR tool. Prove Bouton's theorem.

Grundy values, game sums, the Sprague-Grundy theorem, and applications to non-Nim games. The periodic table of impartial games is complete.

Left and Right have different moves. Game values, negation, the four outcome classes, and the philosopher's stone — games ARE numbers.

The world is richer than numbers. Simplification, canonical form, temperature, and where the theory leads. The alchemist's magnum opus.

The fundamental rules of counting - addition for OR, multiplication for AND.

Arrangements where order matters - factorials, k-permutations, and counting with structure.

Selections where order does not matter - C(n,k), binomial coefficients, and Pascal's triangle.

Powerful counting methods - stars and bars, inclusion-exclusion, pigeonhole.

Mixed problems, error detection, and conceptual integration across all combinatorics topics.

Defining and solving recurrence relations, with applications to counting problems.

Using formal power series to solve counting problems and recurrences.

The basic model of communication complexity - parties, inputs, protocols, and cost measures.

Fundamental problems in communication complexity - equality, disjointness, and their variants.

Methods for proving that problems require many bits of communication.

Communication with randomness - public coins, private coins, and error bounds.

Restricted communication models and their connection to streaming algorithms.

Communication among three or more parties with various input distributions.

Links between communication complexity and circuit depth, data structures, and proofs.

Applying communication complexity to analyze and optimize Bitwit's client-server architecture.

Bridge from computability. Time and space complexity, asymptotic analysis, the fundamental polynomial/exponential divide.

Decision problems, polynomial time, Cobham's thesis. Problems solvable efficiently and why polynomial is the threshold.

Verification vs search. The class NP via verifiers, classic NP problems, P vs NP, co-NP.

The tool for comparing difficulty. Polynomial-time reductions, reduction direction, techniques, and composition.

NP-hardness, Cook-Levin theorem, Karp's reductions, the web of NP-complete problems, coping strategies.

Memory as a reusable resource. L, NL, PSPACE, Savitch's theorem, space class relationships.

Beyond NP. Quantifier alternation as adversarial planning depth. Oracles, relativization, hierarchy structure.

Probabilistic computation. BPP, RP, ZPP, the BPP=P conjecture, connections between randomness and hardness.

Non-uniform computation. Boolean circuits, circuit families, P/poly, uniformity, Shannon's counting argument, circuit lower bounds.

Barriers to resolving P vs NP (relativization, natural proofs, algebrization). Known separations, consequences, and connections to practice.

The clerk in the infinite corridor—formalizing mechanical procedure, encoding, and the Universal Bureau Chief.

The limits of administration—which requests can the Bureau always resolve, and which circulate forever?

Forwarding protocols—how impossibility spreads from one department to another.

Degrees of impossibility—even undecidability has structure, with some questions more impossible than others.

The model — interleaving semantics, adversarial nondeterminism, and the formal infrastructure of concurrent execution.

The damage — shared state interference, race conditions, and the safety/liveness framework for reasoning about correctness.

The engineering response — critical sections, mutual exclusion, semaphores, monitors, and condition variables.

The archetypes — dining philosophers, producer-consumer, readers-writers — and the general theory of deadlock.

The formalization — sequential specifications, linearizability, progress conditions, and lock-free techniques.

The limits — consensus numbers, the synchronization hierarchy, and FLP impossibility.

The language — CCS notation, bisimulation equivalence, CSP contrast, and a glimpse of the pi-calculus.

Act I: What We Lose. Establishes the BHK interpretation, reframes constructive logic from constraint to capability, and catalogs what classical reasoning loses.

Act II: What We Build. Formalizes IPC, builds proof fluency, and discovers the remarkable properties that constructive restriction gives you.

Act II continues. The reconciliation: constructive logic doesn't ban classical reasoning, it asks you to earn it. Decidable propositions get classical tools back.

Interlude: Seeing the Structure. A classical semantic framework that makes the failure of LEM visible through worlds of growing knowledge.

Act III: What We Gain. The climax. BHK was a type system all along. Every constructive proof is a program. Blueprints ARE programs; artifacts ARE outputs.

Coda. The quiet walk home. Intermediate logics, constructive mathematics, and the frontiers where this subject leads.

From data to mathematics. Relations as sets of tuples over named attributes with domains. Database instances as finite relational structures. Keys as minimal identifying sets. Queries as domain-independent functions.

The operational language. Five primitive operators plus rename and derived operations. The draftsman's plotting instruments: mechanical procedures for combining survey sheets.

The declarative language. Tuple and domain relational calculus as first-order logic over databases. The safety problem and syntactic safety as computable approximation.

The crown jewel. Relational algebra and safe relational calculus define exactly the same class of queries. Both proof directions. Then the computational consequences: conjunctive queries and data vs. combined complexity.

The design thread begins. Functional dependencies as constraints on admissible instances. Armstrong's axioms, closure computation, covers and keys. Territorial laws governing what observations the bureau's surveys can record.

Redundancy, anomalies, and progressive reorganization. Normal forms as conditions on schemas relative to their FDs. The impossibility: cannot always achieve both lossless-join and dependency-preserving BCNF decomposition.

Beyond relational algebra. Transitive closure motivates recursion. Datalog syntax and semantics via least fixed point. Stratified negation. Datalog can express queries RA cannot.

Why dependent types exist, what problems they solve, the phase distinction collapse

Types indexed by values—the motivating examples before formal machinery

Dependent function types—universal quantification in the type system

Dependent pair types—existential quantification in the type system

Propositional equality, identity types, and reasoning about equality

Where dependent types live—Coq, Agda, Lean. The specification compiler.

Finite structures as the fundamental objects of study. Queries as isomorphism-invariant classification tasks. The startling discovery that classical metatheorems all fail over finite structures.

What can first-order logic express over finite structures? Quantifier rank as the instrument's sensitivity setting. The fundamental limitation — FO can only see local neighborhoods.

The Ehrenfeucht-Fraisse game — proving that the local probe has limits. Spoiler and Duplicator. The fundamental theorem connecting game indistinguishability to logical equivalence.

Order transforms FO from embarrassingly weak to surprisingly powerful. Serial-numbered atoms enable counting, indexing, and canonical encoding. FO with order and BIT captures uniform AC0.

When local probing fails, iterate. Inject a marker dye at a starting point and watch it spread monotonically. LFP captures P on ordered structures — the Immerman-Vardi theorem.

Suppose hidden structure exists — does it explain the measurements? Existential second-order quantification. Fagin's theorem — ESO captures NP on ALL finite structures, no order needed.

Extending the instrument suite with counting. The CFI barrier — even combined analysis cannot capture P on unordered structures. The clean correspondence has limits. The field is alive.

Average and instantaneous rates of change, the limit definition, differentiability, the derivative as a function, notation systems

Constant and power rules, linearity, product rule, quotient rule, higher-order derivatives, tangent lines

Composition review, single-layer chain rule, nested chains, combining with other rules

Derivatives of trig, exponential, and logarithmic functions, rule selection strategy

Implicit vs explicit functions, implicit technique, inverse trig derivatives, tangent lines on implicit curves, logarithmic differentiation

Indeterminate forms, applying the rule, repeated application, converting other indeterminate forms

Local linearity, Mean Value Theorem, increasing/decreasing, motion interpretation, differential notation

The new world. Establishes the distributed computing model by breaking assumptions from concurrency: shared memory disappears, failure becomes partial, time becomes unreliable. The lighthouse world is introduced here.

The temporal crisis. Physical clocks fail, Lamport shows causality without physical time, and vector clocks characterize causality exactly. The progression from broken clocks to logical time to causal ordering.

Three impossibility results that block every naive escape route. Two Generals, FLP, and CAP — then the precisely characterized gaps that let you climb the wall.

The earned hope. After impossibility, discover that the wall has precisely characterized gaps. Failure detectors, quorums, Raft, and Byzantine agreement show consensus is achievable under realistic assumptions.

The spectrum. With consensus understood, appreciate what it costs and why you might want less. From linearizability to eventual consistency, understood as different prices for different guarantees. CRDTs as algebraic escape from coordination.

The mechanisms. Consistency models defined what guarantees are possible; replication strategies show how to achieve them. State machine replication, primary-backup, quorum replication, and anti-entropy.

The capstone. Atomic commitment as consensus with unanimity. Two-phase commit and its blocking problem. Distributed snapshots to observe system state without stopping it.

Set notation, number system hierarchy ($\mathbb{N},\mathbb{Z},\mathbb{Q},\mathbb{R}$), intervals, inequalities, and absolute value as distance.

Order of operations, factoring patterns, rational expressions, exponent rules, and radical expressions.

Relations vs functions, domain and range, function notation, piecewise functions, and function equality.

Linear, quadratic, polynomial, rational, and radical function families — behavior, zeros, and asymptotes.

Arithmetic of functions, composition, decomposition, and the difference quotient as a derivative preview.

Vertical and horizontal shifts, stretches, reflections, transformation sequences, and even/odd symmetry.

One-to-one functions, finding inverses algebraically, inverse function graphs, and restricting domain for invertibility.

The vocabulary and mechanics of strategic games - players, strategies, payoffs, and game representations.

Analyzing games using dominant and dominated strategies, including iterated elimination.

The central solution concept - strategy profiles where no one wants to deviate.

Randomizing over pure strategies to achieve equilibrium.

Games where players move in sequence, observing previous moves.

Games where players have private information about types, payoffs, or actions.

Repeated games, bargaining, voting, social choice, and behavioral game theory.

Archetypes that illustrate fundamental strategic structures - PD, coordination, chicken, matching pennies, stag hunt.

The building blocks - vertices, edges, directions, weights, degree, and graph representations.

Walks, paths, cycles, and what it means for a graph to be connected - the study of traversal and reachability.

Connected graphs without cycles - the elegant structures underlying hierarchies, search, and optimization.

Named graph families and their distinctive properties.

Computational methods for graph problems including traversal, shortest paths, and minimum spanning trees.

Matching, network flow, isomorphism, and deeper graph theory.

Connecting graph theory to other subjects and its historical origins.

Quantifying uncertainty and surprise—the foundation of information theory.

Information shared between sources and the uncertainty that remains after observation.

Encoding messages efficiently—prefix codes, Kraft inequality, and optimal compression.

Reliable communication over noisy channels—Shannon's fundamental limits.

Practical compression algorithms and the ultimate limits of description.

The grammar of lambda calculus. Three forms, no computation.

Free and bound variables, scope, shadowing, alpha equivalence.

The definition of substitution, beta reduction, capture avoidance. Taught correctly from the start.

Functions of multiple arguments via currying and partial application.

Normal forms, reduction strategies, divergence, eta, bridge to encodings.

TRUE and FALSE as selectors. Building logic from nothing.

Numbers as iteration counts. Successor, predecessor, zero test.

Addition, multiplication, exponentiation, and subtraction from pure lambda.

Pairs and lists from pure lambda.

Self-application, fixed points, the Y combinator — patterns that produce themselves.

Named combinators, SK completeness, lambda vs combinatory logic.

Confluence, normalization, Church-Turing thesis, brief types overview.

Why named representations fail and what replaces them. De Bruijn indices eliminate names by counting binders.

Computing with De Bruijn terms. Shifting, nameless substitution, and the bridge to explicit substitution calculi.

Data as behavior. Church encodings were one answer; Scott, Parigot, and Mogensen-Scott reveal that encoding is a choice.

From substitution to memory. Environments defer substitution; closures capture it. De Bruijn indices reveal their implementation payoff.

How reduction becomes execution. Krivine, CEK, and other machines implement specific evaluation strategies through mechanical transition rules.

The shape of computation. Redundant work, redex families, sharing, and the frontier of optimal reduction.

The foundational rupture: evaluation and limit are different questions with potentially different answers.

The machinery: direct substitution, arithmetic of limits, and indeterminate forms.

The repair kit: factoring, conjugates, squeezing, and trig identities for evaluating limits.

From local behavior to global: limits at infinity, infinite limits, and asymptotic behavior.

The formal definition of limits as a challenge-response game between precision and placement.

The payoff: continuous means the limit keeps its promise — and every break has a name.

Limits are the machine that turns infinite processes into finite values.

Understand what exists in Lisp—atoms, lists, and s-expressions. Learn how Lisp reads and evaluates expressions, and how quoting prevents evaluation.

Extract pieces from lists using car and cdr. Learn to reach into nested structures and handle edge cases when lists are empty.

Construct new lists using cons, list, and append. Understand how cons is the inverse of car/cdr—what they take apart, cons puts together.

Test properties with predicates like null?, atom?, and eq?. Learn to make decisions with conditionals based on the answers.

Name values and procedures with define. Create anonymous functions with lambda. Use let for local bindings. Understand scope.

Master the fundamental technique for processing lists—recursion. Learn the pattern of base case plus recursive case, trace execution, and debug.

Look for things in collections. Learn search patterns with member?, find, and position. Understand when searching succeeds or reaches the end.

Create new lists by transforming each element. Learn the map pattern—same structure, different values. Build toward the map abstraction.

Select elements that match criteria. Learn to remove first or all occurrences. Build toward the filter abstraction.

Master the accumulator pattern and fold operations. Learn to build up results efficiently, understand tail recursion, and see how fold captures list processing patterns.

Use functions as data. Pass them as arguments, return them from other functions. Understand closures—functions that remember their origin.

Understand numbers as recursive structures. Build arithmetic operations from add1, sub1, and zero?. See that recursion works on numbers too.

Process arbitrarily nested lists (trees). Learn when to recur into sublists versus just into the rest. Handle deep structures with double recursion.

Build a tiny Lisp interpreter in Lisp. Programs are data (lists), so we can write an evaluator as a recursive function. This is the deepest magic.

The atomic concepts of logic programming - facts declare world state, rules encode game mechanics, queries ask what's true, and the closed world assumption says what we can't prove is false.

The heart of pattern matching - how the engine determines whether two terms can be made identical through substitution, and how to find the most general such substitution.

How the engine answers queries - SLD resolution chains rules together, the search tree explores possibilities, backtracking tries alternatives when paths fail, and cut prunes the search space.

Practical patterns for logic programming - list processing, accumulators for tail recursion, difference lists for efficient concatenation, generate-and-test for search, and arithmetic evaluation.

Beyond the basics - meta-predicates that treat programs as data, definite clause grammars for parsing, constraint logic programming for richer domains, and tabling for memoization.

Integration and connections - mixed problems testing multiple concepts, error detection for common misconceptions, and bridges to predicate logic, Lisp, miniKanren, automata theory, and real-world applications.

The mechanism design problem, private information, incentive compatibility, and the revelation principle.

First-price, second-price, and optimal auctions: when truthful bidding emerges and when manipulation thrives.

Voting rules, Arrow's impossibility theorem, strategic voting, and the limits of democratic mechanism design.

Stable matching, Gale-Shapley algorithm, school choice, and kidney exchange: two-sided markets that save lives.

VCG mechanisms, dominant strategy implementation, budget balance, public goods, bilateral trade, and the fundamental tradeoffs in mechanism design.

Screening, adverse selection, moral hazard, and the art of designing contracts when agents hold private information.

What modal logic is and why it matters. Introduces necessity (□) and possibility (◇), the questions modal logic answers, and how it extends propositional logic into reasoning about what must be, what might be, and what could have been.

The formal language of modal logic. Covers modal formulas, well-formedness, operator scope and precedence, subformulas, and common abbreviations. Building the grammar before we ask what it means.

The possible worlds interpretation of modal logic. Covers Kripke frames and models, accessibility relations, truth at worlds, validity, and the frame properties that give different modal logics their character. The architecture of the precinct.

The major modal axiom systems: K, T, D, B, S4, S5. Each system captures different assumptions about necessity and possibility. Covers the axioms, their meanings, and the correspondence between axioms and frame properties.

Proving things in modal logic. Covers Hilbert-style axiom systems, the necessitation rule, the distribution axiom (K), natural deduction for modal logic, and modal tableaux. How to establish what's necessary without visiting every world.

Modal logic applied to knowledge and belief. Covers the knowledge operator K, the belief operator B, their different properties, multi-agent systems, common knowledge, and classic epistemic puzzles. What the detective knows, what the suspect knows, and what neither of them knows they don't know.

Modal logic applied to time. Covers future and past operators, linear vs branching time, the Until operator, and the basics of LTL. The basement is 1943; the roof is next Tuesday. A bridge toward program verification.

Modal logic in the wild. Covers philosophy of modality (de re vs de dicto), counterfactual reasoning, deontic logic (obligation and permission), provability logic, and connections to program verification. Why this machinery matters beyond the precinct.

Programs as modalities. PDL (Propositional Dynamic Logic) treats programs as first-class citizens: [α]φ means "after executing α, φ holds."

Combining quantifiers with modality. The Barcan formula, rigid designators, and the puzzles of quantifying into modal contexts.

Alternative to Kripke semantics using sets of propositions.

The logic of obligation, permission, and prohibition.

Modal logic of mathematical provability (GL).

Fixed points in modal logic for verification.

Algorithmic verification of modal properties.

Cross-cutting connections between modal logic topics.

The foundation of number theory - when one integer divides another evenly.

The atoms of arithmetic - prime numbers, factorization, and primality testing.

Clock arithmetic - congruences, operations, and solving equations mod n.

The landmark results - Fermat, Euler, Chinese Remainder, and Wilson.

Units, orders, primitive roots, and the multiplicative group mod n.

RSA, Diffie-Hellman, and the mathematics of modern cryptography.

Mixed problems, connections to other areas, and open questions.

Partial orders, total orders, preorders, and the fundamental concepts of ordering relations.

Hasse diagrams, diagram patterns, isomorphism recognition, and poset construction.

Extremal elements, bounds, chains, antichains, covers, and well-founded orders.

Core lattice theory - meet, join, lattice laws, sublattices, and bounded lattices.

Distributive, modular, complemented, complete lattices, and semilattices.

Order-preserving maps, isomorphisms, lattice homomorphisms, and Galois connections.

Fixed-point theory, Knaster-Tarski theorem, iteration methods, and applications.

Pattern recognition, problem solving, and connections to other areas of mathematics and computer science.

Who can act? Who is responsible? Who can see? The foundational diagnostic lens for organizational dynamics.

How information flows, and what happens when it doesn't. Reinforcing loops, balancing loops, and the pathologies of delayed consequences.

What gets measured gets managed—and gamed. Goodhart's Law, Campbell's Law, and how agents rationally subvert intent.

How financial and contractual structures constrain behavior. Commitment devices, sunk costs, and the value of preserving flexibility.

The eternal trade-off between coordination and adaptation. Local knowledge, requisite variety, and why organizations oscillate.

How systems fail and what failures reveal. Normal accidents, latent conditions, drift, and the Swiss cheese model.

When things go wrong, what happens next? Recovery capacity as distinct from prevention. Blast radius, containment, graceful degradation.

How policy and infrastructure interact—and why they often diverge.

You can only control what you can see—and the costs of making things visible.

The difference between owning risk consciously and hiding it from view.

Canonical failures analyzed through multiple diagnostic lenses.

The formal structure of first-order logic formulas. Covers terms, predicates, functions, quantifiers, variable binding, scope, and well-formed formulas.

The meaning of first-order formulas. Covers structures, interpretations, variable assignments, satisfaction, validity, logical equivalence, and consequence.

Converting between English and first-order logic. Covers basic patterns, quantified statements, nested quantifiers, relations, and common pitfalls.

Laws for manipulating quantifiers. Covers negation, distribution over connectives, quantifier order, and vacuous quantification.

Standardized formula representations. Covers prenex normal form, Skolemization, Skolem constants and functions, and clausal form for resolution.

Proof methods for first-order logic. Covers universal and existential introduction and elimination rules, eigenvariable conditions, and proof strategies.

The identity predicate and its properties. Covers equality axioms, distinctness, uniqueness, counting with identity, and identity in proofs.

Theoretical properties of first-order logic. Covers soundness, completeness, compactness, Lowenheim-Skolem theorems, and undecidability.

Practical uses of first-order logic. Covers mathematical modeling, database queries, software specification, knowledge representation, and automated reasoning.

Sample spaces, events, and the axioms that govern chance - the bedrock of probabilistic reasoning.

How new information changes what we know - the mathematics of "given that..."

Updating beliefs with evidence - the skill humans systematically get wrong and can learn to get right.

Numbers that depend on chance - expected values, variance, and the language of uncertainty.

The recurring patterns of randomness - binomial, geometric, Poisson, and their applications.

Making choices when outcomes are unknown - expected value, risk, and the limits of rationality.

Joint distributions, conditional expectation, and the beginnings of stochastic processes.

The formal structure of propositional formulas. Covers propositional variables, logical connectives, well-formed formulas (WFFs), parse trees, operator precedence, and subformula relationships.

What formulas mean; truth and consequence.

Canonical representations of propositional formulas.

Proof construction using inference rules; the heart of propositional logic.

Systematic search for counterexamples using signed formulas and tree-based decomposition.

Refutation-based proof method using clauses; foundation of SAT solvers.

Properties of propositional logic itself; soundness, completeness, compactness.

Practical applications of propositional logic including SAT solving, logic puzzles, and automated reasoning.

Axiomatic proof systems using minimal inference rules. Covers axiom schemas, the deduction theorem, metatheory, and comparison with other proof systems.

Gentzen's proof system using sequents. Covers structural and logical rules, cut elimination, the subformula property, and comparison with other systems.

Bridge to modal logic covering the limits of propositional logic, modal operators, possible worlds semantics, and applications in epistemics and verification.

The atomic concepts of term rewriting - signatures, terms, positions, substitution, and rewrite rules.

Abstract away from terms to study reduction properties in general - sequences, normal forms, and joinability.

The central property of rewriting systems - different reduction paths converge to the same result.

When and why rewriting processes stop - the foundations of termination analysis.

Unification and critical pairs for analyzing confluence.

Knuth-Bendix completion and related algorithms.

Integrating rewriting concepts through mixed problems, error detection, and deeper understanding.

Set notation, membership, subsets, equality, and the special sets that form the foundation of mathematics.

Combining and manipulating sets through union, intersection, complement, difference, and Cartesian product.

The algebraic laws governing set operations - commutative, associative, distributive, and De Morgan's laws.

Binary relations and their properties - reflexivity, symmetry, transitivity, equivalence relations, and orders.

Functions as special relations - domain, codomain, range, injectivity, surjectivity, and composition.

Counting finite sets - cardinality basics, pigeonhole principle, and inclusion-exclusion.

Infinite cardinals, the diagonal argument, and the stunning hierarchy of infinities.

Well-ordered sets and transfinite counting.

ZFC axioms and the Axiom of Choice.

Building number systems from sets.

Well-orders, lattices, and order theory.

How set theory is used in programming, databases, and logic.

What is a topology? Establish the axioms, the visual language, the canonical examples, and the tools for generating topologies.

How does a point relate to a set? Interior, closure, boundary, limit points, convergence, and neighborhoods.

What does it mean for a function to respect topology? Continuous maps, homeomorphisms, and the Hausdorff property.

Tools for building new spaces from old: subspace and product topologies.

Can the lens split the terrain? Connected spaces, path-connectedness, and components.

Can the lens survey everything at once? Open covers, compact spaces, and sequential compactness.

The most familiar lens — grounded by a ruler. Metrics, metric topology, countability, completeness, metrization.

How well can the lens distinguish? The T0-T4 hierarchy and the classification of niceness.

Building new lenses from old: infinite products, quotient spaces, and constructions synthesis.

The geometry of the unit circle — measuring angles in radians, locating points, naming coordinates, and discovering the Pythagorean identity as a geometric fact.

The functions that the circle generates — definitions, properties, and their graphs. The wave IS the circle, unrolled.

The algebraic relationships between trig functions — Pythagorean family, angle addition engine, and derived identities.

Reversing the functions — why restriction is needed, how the inverses work, and compositions.

Solving equations using everything that came before — identities to simplify, inverses to extract angles, periodicity to enumerate all solutions.

Trigonometry meets the world — triangle solving, periodic modeling, and the bridge to calculus.

What types are, why we need them, and the distinction between typed and untyped systems.

Base types, function types, type checking rules, and the foundations of typed programming.

Progress, preservation, and soundness - what type systems guarantee.

Parametric polymorphism, System F, and type abstraction.

Product types, sum types, recursive types, and pattern matching.

Types as propositions, programs as proofs - the deep connection between logic and computation.

Type constructors, higher-kinded types, functors, monads, and advanced abstraction patterns.