Search

How an algebra of classes became a calculus of relations and quantifiers, through Boole, De Morgan, Peirce, and Schröder.

Why variables, scope, and explicit inference changed the representation of mathematical proof, and how Frege's project differed from modern first-order logic.

How analysis, infinite sets, arithmetic, and alternative geometries changed the questions mathematicians asked about foundations.

Russell's contradiction, Frege's Basic Law V, ramified types, predicativity, and axiomatic set theory as distinct responses to foundational problems.

Formalization, finitary reasoning, and the attempt to justify infinitary mathematics through a mathematical analysis of finite derivations.

Brouwer, Heyting, constructive evidence, realizability, and the different mathematical programs behind the word constructive.

The distinction between derivability and semantic consequence, from formal syntax and Tarski's semantics to Gödel's theorem, Henkin's construction, and nonstandard models.

How arithmetic represents proofs, how diagonalization produces an undecidable sentence, and what the two incompleteness theorems establish.

Church, Turing, Kleene, Post, and the mathematical analysis of algorithms, undecidability, relative computation, and Diophantine equations.

Natural deduction, sequent calculus, cut elimination, ordinal analysis, and the continuing investigation of the strength and computational content of proofs.

Definability, quantifier elimination, ultraproducts, nonstandard analysis, and classification as tools for understanding mathematical structures.

Choice, the continuum hypothesis, Gödel's constructible universe, Cohen's forcing, and the continuing question of which axioms to adopt.

How the study of implication developed into a family of logics whose operators express different kinds of necessity.

Four distinct reasons to reconsider classical inference, illustrated through truth values, relevant implication, inconsistent information, and structural rules.

How substitution became a theory of computation, and how typed terms came to represent proofs with computational behavior.

How types came to express specifications that depend on values, and why equality, induction, and universe rules became foundational decisions.

How categories provided structural interpretations of proof, function types, quantifiers, and mathematical foundations.

From Lisp and lambda-based language design to mathematical accounts of recursion, polymorphic type inference, and abstraction.

How proof procedures turn a mathematical problem into a search, and why representation, inference rules, and search strategy each matter.

Why decidable reasoning can be difficult, how conflict-driven solvers exploit structure, and how Boolean search cooperates with mathematical theories.

How proof search can compute answers, and why a program's logical consequences must be distinguished from the behavior of its execution strategy.

The distinct histories of Automath, LCF, Mizar, inductive provers, dependent-type systems, Metamath, and Lean—and what each architecture asks us to trust.

How assertions became a logic of programs, and how proofs of loops, heap operations, compilers, and kernels depend on precise specifications.

How logics of time became tools for checking ongoing systems, and how symbolic representations and abstraction address the growth of possible behaviors.

How mechanically checked mathematics grew from individual texts and landmark proofs into shared infrastructure for further mathematical work.

How identity types acquired a geometric interpretation, why equivalence can induce identification, and how cubical theories address computation.

How statistical guidance works with formal checking, from premise selection to AlphaProof and research formalization, with careful distinctions about evidence and novelty.

Aristotelian demonstration, syllogistic inference, Stoic arguments, and the commentators and translators who shaped their later study.

Translation, demonstration, Avicennan innovations, later teaching traditions, and the movement of logical ideas across Arabic, Hebrew, and Latin.

How medieval logicians analyzed the use of terms, the force of logical particles, valid consequences, and self-referential statements.

Nyāya, Buddhist theories of inference, and Navya-Nyāya's technical language, examined through the justification and failure of inferential signs.

Mohist standards of reasoning, the School of Names, the white-horse discussion, and Xunzi's account of naming and orderly discourse.

Early-modern projects for improving inquiry and calculation, followed by Bolzano's account of propositions, variation, consequence, and explanation.

Notes on the mistakes I keep making in Apex and how I try to stop repeating them. This is only part of game sense, and only the part I have managed to name so far.

Part 0 introduces the series, its reading order, and routes through foundations, computation, formalization, and earlier logical traditions.

Everything I have written about Apex Legends, from my settings to notes on how I try to play better.

Standard textbooks use sets to define first order logic, then define set theory inside first order logic. Where that apparent circularity resolves, and what the metatheory consists of.

The settings, keybinds, sensitivity, and gear I actually play on.

Notes from the move off WordPress to a static Astro site, what I gained, and what I gave up.

Unrestricted comprehension is inconsistent. Separation replaces it, and the relative Russell set is a subset of its base set but never an element of it.

Squaring both sides keeps every original solution, but differentiating does not. The difference comes from the type of the function you apply.

How local inertial frames connect Lorentz transformations in special relativity to curved spacetime.

How microscopic reversibility, probability, and coarse-graining produce macroscopic irreversibility.

A derivation of Lorentz linearity from the structure of inertial frames and spacetime transformations.

What the constancy of light speed means, how it is tested, and where variable-speed ideas would have to differ.

How first-derivative actions lead to second-order motion, and what Ostrogradsky’s theorem does—and does not—exclude.

How phasors turn sinusoidal circuit equations into algebra, and what their components represent physically.

An introduction to generalized coordinates and why they simplify constrained mechanical systems.

A derivation and interpretation of the virial theorem through the mathematics of classical mechanics.

A reading list for approaching classical mechanics with greater mathematical rigor.

How partial derivatives of a Lagrangian differ from differentiation along a time-dependent trajectory.

A mathematical look at Norton's dome, non-unique motion, and determinism in classical mechanics.

A probabilistic and optimization-based explanation of why squared error is so common in loss functions.

A bilingual guide to repositories, forks, clones, branches, commits, and pull requests, with a complete local workflow.

The story of the kitten my family rescued in February 2022, with a 2024 video update.

Using mathematical logic and Python to reason through a logic-gate construction challenge in Turing Complete.

A practical record of building a family VPN with Raspberry Pi, SSH, DNS, and Cloudflare.

Notes from the 2023 move from a Jekyll site on GitHub Pages to WordPress.

A structured guide to polynomial factorization, identities, methods, and proofs for mathematical competitions.

Preparation ideas, references, and expectations for the William Lowell Putnam Mathematical Competition.

Why nonemptiness and scalar closure force a subspace to contain the ambient zero vector.

An intuitive route from motion with changing acceleration to the structure of a Taylor series.

A concise introduction to Colemak, its layout choices, and the process of learning it.

A first-person account of preparing for and completing a U.S. visa interview in Guangzhou.

An introduction to summation by parts and its role as the discrete analogue of integration by parts.

Practical advice about editors, IDEs, and learning habits for people beginning Python.

A practical mental model for distinguishing terminals, shells, TTYs, and consoles.