The Ethics, Machine-Checked
Spinoza wrote Part I as a dependency graph — here it runs: 36 propositions checked acyclic and grounded, two axioms never used, and necessitarianism at proof-depth ten.
Open study →The Tractatus, Computed
The sixteen truth-functions of 5.101 recomputed, everything regenerated from N(ξ̄), probability as exact ratios, and logic decided "by mere symbolic rules."
Open study →Discrete Mathematics
Sets, logic and quantifiers, machine-checked proofs, number theory, counting and graphs — a full course, every example runnable.
Open study →Algorithms
From a factorial to a forward-chaining expert system — sorting, search, graph traversal, dynamic programming and symbolic AI.
Open study →Symbolization
Epictetus' Enchiridion rendered as executable logic — the dichotomy of control, formalized and run.
Open study →Analytical Philosophy
Frege, Russell, Carnap, Kripke, Quine — quantifiers, descriptions, belief opacity, modal worlds, and verificationism. Every example runs in your browser.
Open study →Formal Philosophy
Default logic, provability, the sea-battle, belief revision, money-pumps, deontic logic, Newcomb and voting cycles — a 39-chapter anthology, distilled into ten runnable themes.
Open study →Mises vs Ayer
The Methodenstreit, run as code — is economics a priori? Praxeology against the verification principle, adjudicated proposition by proposition.
Open study →Gaps, Gluts & the Limits of Logic
Watch the classical laws break: K3, the Logic of Paradox, FDE and Gödel G3 run natively — excluded middle, explosion, and double negation as one-line tests.
Open study →What a Claim Knows About Itself
Every fact carries its own bookkeeping — a grounding tier (how it was derived) and a kind (what it draws on), both computed automatically through inference.
Open study →Ontologies that Reason
Description-Logic ALC as a real tableau reasoner — concept algebra, satisfiability, subsumption, defined concepts and partitions. OWL-class reasoning, no XML.
Open study →Confirmation & Meaning
Carnap's inductive logic and the verifiability criterion, executable — degree of confirmation to the digit, the λ-continuum of learning, and the pseudo-statement test.
Open study →