The Organon as a Test Suite: Lineage and Novelty in Axioma, a Programming Language for Computational Philosophy

1. Introduction

There is a familiar failure mode in papers that introduce a system: the related-work section arrives late, reads as a threat assessment, and concedes as little as possible. This paper inverts that structure on purpose. Axioma will be compared to its ancestors whether or not we name them — the comparisons are obvious to anyone who knows the history — so we name them first, at length, and with the inheritances stated as inheritances. What remains after that exercise is a short list of things for which we could find no precedent. The paper's thesis is that the list is short but not empty, and that its two entries are worth the field's attention: one because it turns a language into a generator of philosophical decisions, and one because it is a portable method rather than a feature of our artifact.

The artifact itself can be stated briefly. Axioma is an interpreted language (with a partial bytecode VM) implemented in Go, in the set-theoretic and logic-programming lineage of SETL and Prolog, with a natural-language-inflected surface descended from REBOL and a stack sublanguage descended from Pop-11 and Forth. It is a general-purpose language — sets, functions, comprehensions, pattern matching, algebraic data types, macros — but its distinguishing layer is philosophical: facts carry a six-tier epistemic grounding (axiom > postulate > theorem > conjecture > hypothesis > datum) on one axis and a five-member Schopenhauerian kind (logical, empirical, transcendental, metalogical, motive) on an orthogonal axis; rules are strict or defeasible, and the tier of a derived fact records which (theorem for strict derivation, conjecture for defeasible); retraction can cascade along recorded justifications; a single copula is is type-dispatched across the senses Russell distinguished; one fact can carry divergent value-laden framings (qua); five propositional logic kinds — classical Boolean, Kleene K3, Łukasiewicz Ł3, Belnap B4, Gödel G3 — are first-class value types dispatched by the ordinary connectives, with Priest's LP as a designation-variant of B4; and modal, epistemic, deontic, and temporal operators evaluate over user-built Kripke models. The reasoning surface is deliberately a portfolio of decidable fragment engines — a sound ALC tableau, a DPLL satisfiability core, an answer-set solver, a natural-deduction kernel, decision procedures for the assertoric and modal syllogistic — rather than a uniform first-order oracle, for reasons rehearsed in §3.3.

Two framing commitments govern everything that follows. First, Axioma is a competence model, not a performance model. It formalizes the normative structure of epistemic acts — what makes a revision warranted, when a default is defeated, what a reframing changes — at what Marr (1982) called the computational level. It makes no claims about human processing, fits no reaction times, and should not be read as a cognitive architecture in the ACT-R or Soar sense (Anderson et al. 2004; Laird 2012); the comparison to those systems is drawn in §3.4 precisely to mark the difference. Second, every claim made below about the artifact's behavior is pinned: it corresponds to an executable assertion in the repository's regression corpus (2,685 scripts at the time of writing), which the author re-runs, with baseline diffing, on every change to the engine. This is not a rhetorical flourish; it is the second novelty claim in operation, and §5 is about it.

The paper proceeds as follows. Section 2 describes the artifact in just enough detail to give the lineage and novelty sections their referents. Section 3 is the lineage, named first. Sections 4 and 5 defend the two novelty claims — co-residence and the book-pass method — each against its nearest kin. Section 6 argues that the two claims need each other. Section 7 answers objections, and Section 8 concludes.

2. The artifact, briefly

2.1 Primitives as epistemic acts

In most languages the semantic atoms are machine operations — assign, call, allocate — and any epistemic vocabulary is metaphor layered above them. Axioma inverts the layering. The following is ordinary surface code, not a library DSL:

relation free(p)
relation judges_bad(p)

axiom free("sage")                    # posit at tier: axiom
assert judges_bad("novice")           # posit at tier: datum (the default)

tranquil(P) whenever free(P)                    # strict rule — derived facts are theorems
typically disturbed(P) whenever judges_bad(P)   # defeasible rule — derived facts are conjectures

grounding("tranquil", "sage")         # → "theorem"   (provenance, queryable)
cancel("disturbed", "novice")         # → canceled    (conjectures are defeasible)
cancel("tranquil", "sage")            # → "refused: … is a theorem …"
                                      #   (defeasance respects the ladder; force_cancel overrides)
why tranquil("sage")                  # prints the derivation chain back to the axiom

departed("estate") qua "lost"         # one fact, two value-laden framings —
departed("estate") qua "given_back"   #   rules can key on either (intensionality)

Assertion, derivation, justification, defeasance, reframing: the verbs of epistemology are the verbs of the language. The design sources for each construct are published theory, not improvisation: the defeasible layer is Reiter's (1980) default logic; the three-valued strong tables are Kleene's (1952); the four-valued substrate is Belnap's (1977) "useful four-valued logic," with its two bilattice orders both exposed (truth-order connectives and knowledge-order evidence combination ⊕/⊗); the intuitionistic kind is the smallest of Gödel's (1932) finite matrices, G3; the paraconsistent designation-variant is Priest's (1979) LP; the aspectual qua construct implements the Fregean distinction between a fact and its mode of presentation; the grounding ladder's tier/kind orthogonality descends from Schopenhauer's fourfold root by way of the a priori / a posteriori demarcation. Where the repository documents a construct, it documents the source once and then treats the construct as the language's own.

2.2 One surface

The load-bearing engineering fact, on which §4 rests, is that all of this shares a single value space. A Belnap value can be an element of a set, a key in a comparison, an operand of the ordinary and, the valuation of an atom at a Kripke world, and the subject of an expect() assertion, without ever leaving the language's one equality operator or its one truthiness relation (truthiness for a logic value is designation, so if agrees with designated() everywhere). The regression corpus and its parallel test runner treat all subsystems identically; there is a single documentation and reflection layer (doc, describe, signature, source, ast) covering all of them; and the VM, where it compiles a construct at all, is held to byte-identical output by differential tests.

2.3 Acknowledged surface genealogy

Because §3 is about intellectual lineage, we note here, once, the implementation genealogy, which the project's manual also credits once and then absorbs: the interpreter's original skeleton follows Ball's Writing an Interpreter in Go; SETL contributes Ω (om) and the set-former; REBOL contributes colon binding, refinements, and block syntax; Pop-11 and Forth contribute the open stack; Prolog contributes clause syntax; Mathematica contributes the *form introspection family; Python contributes the comprehension surface it is a superset of. None of this is hidden, and none of it is the subject of the novelty claims.

3. The lineage, named first

The organizing question for each entry is the same: what did this line contribute, what does Axioma inherit from it, and where does Axioma depart? The section ends with the residue — what the lineage does not contain.

3.1 Leibniz, the ancestral program

The ancestral slogan is Leibniz's calculemus: disputes settled by calculation over a characteristic notation. Every project in this section is downstream of it, and Axioma is explicit about the debt — to the point of implementing its ancestors as content: the repository's leibniz package contains Leibniz's own arithmetical encoding of the syllogism, Porphyry's tree, and a 24-mood decision procedure for the assertoric syllogistic, extended (as Leibniz could not) to a decidable de re reconstruction of Aristotle's modal syllogistic. The lineage is not an epigraph; it is executable and regression-pinned. What Axioma inherits from Leibniz is the ambition and the honesty condition that comes with it: a calculus must actually decide, which is why the language's logic surface is confined to decidable fragments with the boundaries named (§3.3, §7).

3.2 Sloman and the POP family: philosophy by building programs

The clearest single ancestor of the stance is Aron Sloman's The Computer Revolution in Philosophy (1978), which argued — polemically, and in 1978 — that philosophy done well and artificial intelligence done well converge, and that philosophers who ignore computing are neglecting their own subject matter. Sloman's vehicle was the POP family: Burstall and Popplestone's POP-2, later Pop-11 within the Poplog environment, an AI language designed for exactly the kind of exploratory model-building his program required. Axioma carries a literal inherited gene here: its user-accessible stack and open interpreter stack are the Pop-11/Forth design, down to stacklength and the Forth shuffle vocabulary. The departure is methodological. Sloman's program was exploratory: build models to sharpen philosophical intuition, with the program's behavior as a source of insight. Axioma adds the discipline Sloman's era lacked the infrastructure to impose: every philosophical behavior claim is pinned by a regression assertion, so the model cannot drift out from under the insight. One way to describe this paper's second novelty claim (§5) is: Sloman's stance, plus a standing regression discipline.

3.3 McCarthy's logicist line: common sense as assertions

McCarthy's "Programs with Common Sense" (1959) proposed the advice taker: a program whose competence is carried by declarative sentences it manipulates, so that telling it something new is an act of assertion rather than reprogramming. Axioma's fact store, its NL source clauses (axiom/motive acts_purposefully("agent") by mises), and its insistence that assertions carry queryable provenance are all recognizably advice-taker descendants. From the same line comes nonmonotonicity: McCarthy's circumscription (1980) and, more directly for Axioma, Reiter's (1980) default logic, which the defeasible rule layer (typically, <~~, cancellation, extension-style conflict handling) implements; Hayes's naive physics manifesto (1985) supplies the precedent for large-scale axiomatization of common-sense domains. The departure is architectural and deliberate: the logicist dream of one uniform first-order (or richer) substrate is rejected in favor of a portfolio of decidable fragment engines — ALC tableau, DPLL, ASP, modal natural-deduction kernel, syllogistic decision procedures — with an explicit doctrine that what cannot be decided is marked as a boundary rather than approximated silently. Full first-order validity is only semi-decidable; a language that promises execution must budget for that, and Axioma budgets by fragmentation. The repository documents this as a stance, not a limitation discovered late.

3.4 Newell and Simon: symbols, with the empirical claim subtracted

The physical symbol system hypothesis (Newell and Simon 1976) holds that symbol manipulation suffices for general intelligent action — an empirical hypothesis about minds, offered in the same lecture that argued computer science is an empirical discipline. Axioma inherits the symbolic commitment wholesale: its facts, rules, proofs, and framings are symbol structures, inspectable and rewritable (the language is homoiconic, with a macro layer and a runtime ast()/compile() reflection surface). It subtracts the empirical claim. Where the cognitive-architecture descendants of this line — ACT-R (Anderson et al. 2004), Soar (Laird 2012) — model human performance and are answerable to psychological data, Axioma models the normative structure of epistemic acts and is answerable to the texts and theories it formalizes (§5). This is the competence/performance line drawn in §1: the cognition Axioma models is competence at Marr's computational level, never chronometry.

3.5 The industrial knowledge-representation line: Cyc, KM, SNePS, conceptual graphs

Four systems define the mature KR tradition Axioma most resembles at the frame-and-concept layer, and the resemblances are documented in the repository rather than left for reviewers to discover. CycL (Lenat and Guha 1990) contributed scale and, most relevantly, microtheories — contexts within which assertions hold — which are kin to Axioma's qua framings and its possible-world models; the repository's Cyc comparison also drove specific borrowings (argument-type checking, strict relation refinements). KM, Clark and Porter's knowledge machine, is the closest frame-language relative; the repository maintains an explicit KM-comparison document and, as of 2026, implements a superset of KM 2.0's signature reasoning vocabulary (automatic classification via defines, slot metadata such as inverse and transitive slots, partitions, intensional classes, coreference merging) — with defeasible variants KM lacks. SNePS (Shapiro and Rapaport 1987) is the precedent for a fully intensional propositional network — every node a distinct intensional entity — and Axioma's dual-aspect facility (one designatum under two co-referring signs; qua at the fact level) is the same Fregean commitment enforced with different machinery. Conceptual graphs (Sowa 1984) are simply implemented: the cg package and the graphform(rel, "cg") renderer emit Sowa's linear notation. The departure from all four is strategic: instead of one monolithic curated knowledge base as the product, Axioma is a small general-purpose language whose scripts build their own knowledge states, with persistence as an optional bridge. The KR line's lesson that Axioma takes most seriously is negative: we read the Cyc experience as a cautionary case of curated content outrunning any regression discipline that could keep it audited. Axioma's answer is §5.

3.6 Logic programming: Kowalski's equation, restricted on purpose

From Kowalski (1974, 1979) and the Prolog tradition Axioma inherits the clause as a programming construct and the conviction that predicate logic is a usable surface. It departs by subtraction: the rule engine is deliberately Datalog-flat and deterministic — no cut, no unbounded backtracking, no negation-as-failure in the Prolog style; queries return complete solution sets computed to a fixpoint, and structural unification (compound terms, list patterns, reverse-mode queries) is confined to a goal-directed SLD path that terminates on the corpus it serves. The trade is expressiveness for the properties the book-pass method needs: determinism, replayability, and answers whose completeness is a theorem of the evaluation strategy rather than a prayer. Where Prolog's semantics and its operational behavior famously diverge, a regression corpus of philosophical texts cannot afford the divergence.

3.7 Procedural reflection: Smith's ambition, domesticated

Brian Cantwell Smith's procedural reflection (1982; 1984) — a language able to inspect and act on its own interpretation — is the ancestor of Axioma's reflection campaign: runtime doc, describe, signature, source, functions(Type), ast(), compile(), a self-describing builtin catalog, and a homoiconic quote/eval layer. Smith also belongs in this lineage twice over, since "The Limits of Correctness" (1985) is a founding document of the philosophy-of-computing debate that §5 engages. The departure is one of temperament: Smith's 3-Lisp pursued a semantically complete reflective tower; Axioma's reflection is domesticated into a reference-documentation discipline — every reflective card is verified by running, and the reflective surface exists to keep the language honest about itself rather than to model self-reference as such.

3.8 Computational philosophy: the argument-as-code wing

The academic field Axioma belongs to has a name and a canon. The SEP's Computational Philosophy (Grim and Singer 2024) divides it into a simulation wing — Thagard's (1988) computational philosophy of science, Grim, Mar and St. Denis's (1998) Philosophical Computer, Skyrms (1996) and Zollman (2007) on evolved conventions and epistemic networks — and an argument-as-code wing: Fitelson and Zalta's (2007) computational metaphysics; Oppenheimer and Zalta's (2011) prover-discovered simplification of the ontological argument; Benzmüller and Woltzenlogel Paleo's (2014, 2016) mechanization of Gödel's ontological proof, which confirmed the modal collapse and exposed an inconsistency in one axiom set — the standing demonstration that implementation discovers, not merely checks; Rushby's (2013) PVS analysis of Anselm; and, closest of all, the LogiKEy program (Benzmüller, Parent and van der Torre 2020), which hosts multiple ethical and deontic logics as shallow embeddings in Isabelle/HOL. Axioma is squarely in this wing and pushes it in one direction: from mechanizing an argument in a prover to making the philosophical vocabulary itself the semantics of a general-purpose vernacular language, and from one-shot verification to a standing regression corpus. The precise relationship to LogiKEy — the nearest kin of the co-residence claim — is treated in §4.4, where it belongs.

3.9 The phrase, the collisions, and priority

Honesty requires a note about the term "executable philosophy," which the project used informally for years. The best-documented public use of the exact phrase is Yudkowsky's (c. 2015; the Arbital page is undated), in a different sense: an adequacy standard for philosophy precise enough to program into an AI, not a medium in which philosophy is written. A separate, independent name-collision is Phillips's ExPhil (2015–16), a small, abandoned Python library encoding philosophical theories as flag-dictionaries — a sketch of the genre, not a language. The technical ancestor of the idea is the executable-specification tradition of formal methods; the philosophical ancestor is §3.1. The design program documented in this paper predates both 2015 uses by many years; the relationships recorded throughout this section are convergences and shared ancestors, not sources, except where an inheritance is explicitly flagged as such (the POP stack, the surface genealogy of §2.3). In academic contexts we prefer the field's established term — computational philosophy, argument-as-code mode — and reserve "executable" for the medium property it literally names.

3.10 What the lineage does not contain

The inheritances and departures, summed:

Each line contributes; none contains either of the following: (i) a vernacular surface in which the breadth of formal-philosophy machinery listed in §4.1 co-resides as first-class native values under one equality, one designation, and one regression discipline; (ii) canonical texts across contested domains maintained as permanent executable regression fixtures under a failure-classification trichotomy. Those are the two claims, and they are defended next — separately, because they are different kinds of claim: the first is a property of this artifact; the second is a method anyone can take.

4. Novelty I: Co-residence

4.1 The catalog

The following subsystems are simultaneously present in the current engine. Each is grounded in a named published theory; none is a stub — each carries its own test files in the regression corpus, and the load-bearing ones carry soundness oracles (the ALC tableau is checked against the atomic hierarchy walk; the modal syllogistic collapses onto the assertoric decision procedure when all modalities are assertoric, across all 64 form combinations; the market-clearing scripts check against Shapley–Shubik cores).

Any three rows of this table co-occur in existing research prototypes, and several frameworks host arbitrarily many logics as encoded object theories (§4.4). The claim is therefore not bare breadth. It is that, to our knowledge, no prior vernacular language carries this machinery as first-class native values dispatched by its ordinary operators under a single equality and a single designation relation — and that this arrangement, not the inventory, is what forces the border decisions of §4.3, which are the claim's real payoff.

4.2 What "one surface" means, operationally

Co-residence is cheap to claim and expensive to mean. Operationally it means four things here. One value space: logic values, groundings, kinds, concepts, and facts are ordinary first-class values; a Belnap glut can sit in a set beside an integer. One equality and one truthiness: the engine's single structural equality has explicit arms for every logic kind (with cross-logic comparisons decided, not crashed), and truthiness for logic values is designation — if and designated() cannot disagree. One test discipline: a parallel runner sweeps the corpus — 2,685 scripts, of which 309 legacy scripts are quarantined and roughly 190 known failures are tracked by an explicit manifest — with baseline-diff support; the author runs the sweep on every corpus-affecting change, so a change to any subsystem is audited against all of them ("zero regressions" means no new failure against the committed baseline, a maintained discipline rather than a CI automation). Where the bytecode VM compiles a construct, differential tests hold it to byte-identical output. One reflection layer: the same doc/describe/signature surface answers for a Belnap value, a relation, a modal model, or a stack.

4.3 Interaction decisions as philosophical output

The philosophical payoff of co-residence is that subsystems which never meet in the literature must agree on their borders, and every border is a decision — contestable, documented, and pinned. Five examples from the repository's history, chosen because in each case the isolated literatures had no need to decide the question at all:

1. Truthiness is designation. When a many-valued logic and a conditional live in one language, if belnap("false") must do something. The engine's answer — the truthiness of a logic value is its membership in the designated set, uniformly across K3, Ł3, B4, G3 — is a theory of the interface between logic and control flow. No paper on B4 alone ever needed one.
2. Worlds carry many-valued values. Widening Kripke valuations from booleans to arbitrary truth-value objects makes □ and ◇ designation-aware, so a glut at a world is possible and paraconsistency survives the modal layer (□ of a glutted atom holds; explosion does not follow). This composes Priest's chapter 9 rather than reimplementing it — and the composition existed as a design decision before it existed as a feature.
3. Defeasance respects provenance. cancel refuses to defeat a strictly derived theorem, while conjectures and base posits stay cancelable — the grounding ladder is load-bearing for mutation, not just display. Default logic alone has no ladder; provenance systems alone have no defeat. Their intersection forced a norm: what may be defeated is a function of how it was derived.
4. Tier is provenance; kind propagates. The engine's history contains a documented episode in which the "obvious" rule — cap a derived fact's tier at the minimum of its premises' tiers — was implemented and then refuted by the corpus: thirty-five regressions showed it conflates provenance with confidence and breaks defeasance, entrenchment, and belief revision. The repair moved the a priori/empirical distinction to the orthogonal kind axis, where it propagates by contamination (any empirical premise makes the conclusion empirical, mirroring an epistemic meet), leaving the tier to record derivation type. That is a substantive epistemological thesis — derivational pedigree and evidential strength are different dimensions — discovered because two subsystems had to share a fact store, and now permanently enforced by tests.
5. Object-language and metalanguage equality split. G3's == originally returned the object-language biconditional (a truthy ?ⁱ for unknown-vs-true), silently corrupting validity checks written in the metalanguage. The repair — == is metalanguage Boolean everywhere; the object-language biconditional lives at iff — is Tarski's distinction enforced as an API boundary, and it was forced precisely because five logics share one operator namespace.

None of these is a theorem in the traditional sense. Each is what we mean by calling the artifact an instrument: co-residence converts interface engineering into philosophical position-taking, and the regression corpus converts position-taking into something that cannot silently drift.

A deflationary reading deserves a direct answer: are these not simply API conventions any competent implementer would converge on? For some taken singly, yes. Examples (1) and (5) are forced consistency choices more than discoveries, and we present them as such; example (4) is the strongest — a falsifiable epistemological thesis proposed, refuted by thirty-five failing tests, and repaired; (2) and (3) sit between. The philosophical content does not live in each micro-decision but in the arrangement: a single namespace forces every such border to be decided uniformly, explicitly, and revisably — written down, pinned, and contestable by diff — where the isolated literatures never take the decision at all.

4.4 Nearest kin, and the precise differentiation

Four literatures come close, and the claim must be stated against all of them. Metalogical frameworks — LF and Twelf, Isabelle used as a framework, Maude (rewriting logic used as a metalanguage "in which many different logics can be specified and executed"; Basin, Clavel and Meseguer 2000), HETS with its institution-based graph of logics and translations (Mossakowski, Maeder and Lüttich 2007), and MMT's foundation-independent theory graphs (Rabe and Kohlhase 2013) — host arbitrarily many logics, and any survey of "many logics in one system" must begin with them. But they host logics as represented object theories: the logic is data reached through an encoding; a value of one encoded logic does not flow through the host's ordinary connectives, comparisons, and control flow into everyday programs; and no single designation relation decides truthiness across them. LogiKEy (Benzmüller, Parent and van der Torre 2020) is the closest single project: multiple deontic and ethical logics as shallow embeddings in Isabelle/HOL, explicitly for normative-theory experimentation. The differences are the surface and the discipline: LogiKEy's user writes HOL against a prover, per study, with the embedding as expert infrastructure; Axioma's user writes a vernacular language in which the logics are ambient value kinds, and the standing corpus (not a per-paper appendix) audits their interactions permanently. Multiparadigm ecosystems — SWI-Prolog with constraint, answer-set, and s(CASP) engines co-installed (Arias et al. 2018), Racket's #lang tower, Oz — co-host computation and reasoning paradigms in one runtime, the nearest engineering analogue; but the co-residents are evaluation strategies, not truth-value kinds under one equality and one designation. Combining-logics theory — fibring and its relatives (Gabbay 1998; Carnielli and Coniglio 2007) — is the mathematics of what happens when logics merge, including the collapse theorems that make naive combination dangerous. Axioma is not a contribution to that theory; it is an engineered instance that makes specific combination choices (strict operand validation with a canonical embedding matrix; loud errors for pairs without one) and pins each choice with tests. The honest statement of Novelty I, hedged as its §5 sibling is: to our knowledge, no prior vernacular programming language carries many-valued, modal, description-logic, defeasible, and axiological machinery as first-class native values dispatched by its ordinary operators under a single equality and a single designation relation — as opposed to object theories represented in a metalogical framework or embeddings maintained in a prover — and §4.3's border decisions are what that arrangement, specifically, forces. We flag this as a novelty claim awaiting a counterexample.

5. Novelty II: The book-pass method

5.1 The protocol

A book pass takes a canonical text and turns it into a permanent, executable regression suite. The protocol, stabilized over two years of practice:

1. Select and read the text; fix the edition; read primary sources for every claim that will be cited (the house rule is that secondary summaries are never symbolized on their own authority).
2. Symbolize in the text's own order, chapter by chapter, into scripts whose comments quote or cite the passage being formalized.
3. Pin every claim: each symbolized assertion is an expect(label, actual, expected) — a machine-checked equality whose failure fails the run. No claim ships as a println and a hope.
4. Classify every divergence into exactly one of three ledgers:
   • Engine gap — the text says something the language cannot yet express or gets wrong; recorded in a gap ledger, which feeds the language's feature funnel (several major features, from tuple-target relational projection to the keywords() catalog to the :: Ordinal discipline, entered the language because book passes hit the same wall repeatedly);
   • Textual erratum — execution reveals an error in the published text; recorded in an errata ledger (the pass over Fischer and Grodzinsky's The Anatomy of Programming Languages produced a seven-entry errata ledger, each entry verified by running the book's own exhibits);
   • Honest boundary — the content is genuinely outside the executable fragment; recorded as an explicit NONE with reasons (late Wittgenstein's language-games carry an honest NONE; so does the relevance-logic conditional in the Priest pass).
5. Adversarial review before commit — independent review passes attack the symbolization (invented quotes, misattributed page numbers, and too-charitable readings have all been caught this way), and the suite then joins the permanent corpus, re-run on every engine change thereafter.

5.2 The corpus

At the time of writing the corpus holds 55 texts and 812 scripts (within the 2,685-script regression corpus), carrying 14,199 expect() sites of which 14,156 are live assertion calls (the remainder are commentary mentions), spanning roughly 2,300 years — Aristotle's Organon and Stoic logic through Boole, Jevons, Peirce, Frege, Russell, the Tractatus, Carnap, Ayer, and Quine, to contemporary textbooks in logic (forall x: Calgary; Priest; Sider; Hughes–Cresswell), mathematics (Hammack; Velleman; Schaum's; Rosen; Graham–Knuth–Patashnik), AI and computation (AIMA; Luger; Levesque; Sipser; Genesereth–Nilsson), programming languages (Touretzky; Fischer–Grodzinsky), economics and its methodology (Menger; Robbins; Mises; Rothbard; Rodrik; the Hutchison–Machlup–Rothbard verification debate), and non-Western logical traditions (Indian, Buddhist, and Jewish logic). Representative scale, per pass (all counts re-taken on the front-matter date): Schaum's discrete mathematics, 2,360 assertions; Hammack's Book of Proof, 1,248; Fischer–Grodzinsky, 599 with Pascal-oracle differential tests; forall x, 511 (and five engine fixes); AIMA, 439; Spinoza's Ethics Part I as a machine-checked proof graph, 120; the Tractatus, 113 assertions against 526 propositions; the Organon, 100, including the modal syllogistic. The corpus is deliberately tiered, and the tiers should not be conflated: a primary philosophical and logical canon (the Organon, Boole, Frege, the Tractatus, Mises) carries the paper's thesis; pedagogical textbooks (forall x, Hammack, Priest) audit breadth; and computational drill books (Schaum's, interview preparation) — which contribute the largest raw assertion counts — stress the computational kernel rather than the philosophical machinery. The novelty claim of §5.4 is made for the first two tiers; the third is included for what it is.

5.3 What the method yields

Four products, in ascending order of philosophical interest:

(i) Regression semantics for the language. The texts stand between the engine and its next change: a modification that would silently alter the meaning of one construct is caught by whichever of 2,685 scripts exercises it, and the norm for shipped changes is zero regressions, verified by an author-run baseline diff — a maintained discipline executed on every corpus-affecting change, not a CI automation. The language's semantics is thereby answerable to Aristotle and Boole in the most literal sense available to engineering. Where De Millo, Lipton and Perlis (1979) argued that mathematical proof lives by social processes, and Fetzer (1988) that program verification cannot close the gap to a causal artifact, the corpus offers a third practice: fourteen thousand executable pins whose checking is mechanical, repeatable, and public.

(ii) Discovery. The method finds things. The de re reconstruction of Aristotle's modal syllogistic was forced, by the discipline of shipping a decision procedure, to decline the second-figure apodeictic moods — including ecthesis-proved Baroco LLL — and to say why: no uniform de re semantics covers them. That is a philosophical finding about where the text outruns a semantics, produced by implementation pressure, in the same genre as Benzmüller and Woltzenlogel Paleo's (2016) prover-discovered inconsistency — but generated by a corpus discipline rather than a one-off mechanization. The tier-propagation episode of §4.3(4) is another: a plausible epistemological principle refuted by thirty-five failing tests. Each is Naur's (1985) "programming as theory building" run in reverse — theory building as programming.

(iii) Errata for the texts. Execution audits the books themselves — misprinted derivations, tables that do not compute, exercises whose stated answers are wrong. The errata ledgers are small, and print scholarship has always produced errata; what these add is the witness — each entry is accompanied by a re-runnable failing execution of the book's own exhibit.

(iv) A map of the executable fragment. The honest-NONE ledgers record, text by text, what resisted execution and why. Aggregated over 55 texts, this is data about the boundary of the executable fragment of philosophy — which is itself a philosophy-of-computing question (§3.8's field asks it abstractly; the corpus answers it empirically, one text at a time).

5.4 Nearest kin, and the precise differentiation

Several traditions run texts and machines together, and two properties this paper might seem to claim must be conceded to them at once. Proof-checked pedagogy — from Suppes' EXCHECK courses at Stanford in the 1970s, the genre's progenitor, which machine-checked student proofs against an axiomatic logic and set-theory curriculum (Suppes 1981), to Leach-Krouse's Carnap platform (2018) and the Open Logic Project — attaches machine checking to logic teaching, with the direction inverted: the student's derivations are checked by the system; the system's semantics is not audited against the text, there is no failure trichotomy, and the text plays no regression role. Book-scale formalization requires larger concessions. Permanence and regression-gating are not novel: mathlib is a permanent, continuously maintained corpus against which the Lean language itself is tested (The mathlib Community 2020), and Mizar's library is revised in step with its verifier — large formal corpora demonstrably do stand between a language and its next change. Machine-audited errata in a canonical text are not novel either: GeoCoq's proof-checking of Euclid corrected errors in the Elements with machine-checked witnesses (Beeson, Narboux and Wiedijk 2019), and Naproche checks the controlled-natural-language prose of Landau's Grundlagen and of Euclid directly (Cramer et al. 2010) — the closest existing thing to running a text's own words. The lineage runs from the QED Manifesto (1994) through Flyspeck (Hales et al. 2017) to Tao's 2025 Lean companion to his Analysis I. Single-theory formalizations — most relevantly Komendarczyk, Block, Levendis and Tipler's (2026) many-sorted axiomatization of Mises with a Lean 4 consistency proof — verify a reconstruction once; the corresponding Axioma passes (Rothbard's Man, Economy, and State; Human Action) run the same content as live, queryable, defeasible programs re-swept on every engine change, a comparison developed at length in the companion paper. Reproducibility infrastructure (executable papers, notebooks) executes a paper's own computations; literate programming (Knuth 1984) embeds documentation in programs — the book-pass embeds programs in the reading of someone else's book; digital humanities computes over texts (frequencies, networks) without executing their claims. What survives contact with all of this is a conjunction, and the precise statement of Novelty II is that conjunction: to our knowledge, no prior project maintains canonical texts across contested, largely non-mathematical domains — philosophy, economics, several logical traditions — symbolized in each text's own reading order with the source quoted at the point of formalization, under an explicit gap / erratum / boundary failure trichotomy, as standing regression fixtures between a language and its next change: "the Organon as a test suite." Per the project's own documentation standard, we flag this as a novelty claim awaiting a counterexample; the nearest misses are named above precisely so that the counterexample, if it exists, is easy to construct.

And the method is portable. Nothing in the protocol of §5.1 requires Axioma: a Lean, Isabelle, or Prolog community could adopt book passes tomorrow, trichotomy and all. We regard that as a feature of the claim, not a weakness — methods that only their inventors can use are usually not methods.

6. Why the two novelties need each other

Co-residence without the corpus would be unauditable: a language hosting five logics, a modal layer, and a defeasance system has a combinatorial interaction surface no unit-test suite designed subsystem-by-subsystem would cover. The books cover it, because canonical texts are precisely the documents that cross subsystem lines: the Priest pass exercises many-valued logic inside Kripke models; the Mises and Rothbard passes exercise the tier ladder, the kind axis, and defeasible rules against each other; the Organon pass couples the syllogistic engine to the modal layer; the Graham pass couples defeasible reasoning to the money and percent arithmetic. Conversely, the corpus without co-residence would be impossible: a text does not confine itself to one formalism, so a system of isolated prototypes could never run one whole.

The loop closes through governance. Book-pass gap ledgers are the language's documented feature funnel — a construct hand-rolled by four independent passes is a feature signal; a pass completed with zero engine changes (the thirteen-script Rothbard sequence was one) is a certification that the kernel already suffices for its domain. The language grows where the texts push, and the texts hold the language where it has grown. This co-evolution — semantics disciplined by a canon, canon made executable by the semantics — is, we think, the most transferable single idea in the project.

7. Objections

"Symbolization is interpretation; your expect() pins your reading, not the text." Correct — and that is the method's value, not its refutation. Every formalization of a text embeds a reading; the book-pass makes the reading inspectable and contestable at assertion granularity. Disagreement becomes a diff: change the symbolization, re-run, and see which downstream claims move. The corpus practices this on itself — the Mises passes encode four rival published readings of the action axiom's status as four kind-tags over one rule base and run all four; the Organon pass documents its de re choice and enumerates exactly which of Aristotle's verdicts that choice declines. Print formalizations embed readings too; they just cannot be diffed.

"Every pass comes from one pipeline — where is the independent replication?" The strongest objection we know, and it is conceded rather than rebutted. All fifty-five symbolizations, and the pre-commit adversarial reviews that gate them, come from one author working with one machine assistant; a consistent in-house pipeline can be consistently wrong in the same direction. What the method offers today is not replication but replicability: the scripts are public and pinned at assertion granularity, so an independent re-symbolization that diverges is not a dispute about prose but a diff — and we would count such a fork as the method succeeding. Until one exists, the corpus should be read as one disciplined reading of the canon, not a consensus about it.

"Executions are demonstrations, not proofs." Within the decidable fragment engines, execution is proof by decision procedure — the syllogistic verdicts, tableau results, and SAT answers are certified by soundness arguments and oracle cross-checks, not by sampling. Outside those fragments the objection stands and is accepted: finite enumeration and adversarial review approximate but do not attain universality, which is why the honest-boundary ledger exists and why claims are worded as what was run. The project's own methodological documentation states the proof/demonstration gap as a standing constraint rather than papering over it.

"A proof assistant could host all of this." It could, and to a first approximation LogiKEy is that project for the deontic fragment. Two things would still be missing: the vernacular surface (the co-residence claim is about a language people write directly, where a glut is a value and a grounding is queryable, not an embedding an expert maintains), and the corpus discipline, which no prover community currently practices in the trichotomized, regression-gating form of §5.1. Since the method is portable, this objection is really an invitation, and we extend it: run the Organon against your semantics and publish the ledger.

"Breadth at the price of depth." Each engine is held to the standards of its own literature where those standards are checkable: the ALC tableau is validated against independent reasoning paths and returns "unknown" rather than a verdict when its budget exhausts; the modal syllogistic collapses onto the assertoric oracle across all form combinations; the economic scripts check against cooperative-game cores. Depth is audited subsystem by subsystem; what the artifact declines is only the pretense that one uniform logic could carry all of it.

"Who is this for?" The primary audience is philosophy and logic education and research — people for whom "run Chapter 9" is a new way to teach or contest a text. The companion praxeology paper demonstrates domain reach into economic methodology; this paper's claim to the philosophy-of-computer-science community is different and narrower: here is a specimen whose design decisions are executable positions, and a method you can detach from the specimen.

8. Conclusion

We have tried to write the related-work section a skeptical reviewer would otherwise write for us, and to defend only the residue. The residue is two claims. Co-residence: the breadth of formal-philosophy machinery in §4.1 lives in one vernacular surface under one equality, one designation notion, and one permanent regression discipline — and the borders this forces between previously isolated formalisms are themselves philosophical decisions, five of which we documented. The book-pass method: fifty-five texts maintained as executable, failure-classified regression fixtures — fourteen thousand pinned assertions swept, baseline-diffed, on every change to the language, generating discoveries in both directions (about the semantics, and about the texts) and mapping the executable fragment of philosophy empirically. The first claim is a property of the artifact; the second is a portable practice, and its portability is the point.

The philosophy of computer science has long studied what programs are (Angius, Primiero and Turner 2021), what verification can promise (De Millo, Lipton and Perlis 1979; Fetzer 1988), and what a paradigm is (Floyd 1979). Axioma offers it an unusual object: a language that is simultaneously a specimen — every design decision a position in philosophy of language or epistemology, stated in running code — and an instrument, whose corpus makes fidelity to a canonical text something you can diff, regress, and dispute at the granularity of a single assertion. Aristotle has been read for twenty-three centuries; as of this project he is also run — swept and baseline-diffed against every change to an interpreter. We think that is a new relationship between a text and a machine, and we have tried to earn the claim by naming the nearest kin we could find and by wording it so that a counterexample, should one surface, falsifies it cleanly.

Acknowledgments and drafting disclosure

The language, the research program it embodies, and the questions this paper answers are the author's. The manuscript was drafted with the assistance of Claude (Anthropic), used as a writing and verification instrument under the author's direction; the author designed the artifact the paper describes, set the theses, directed and revised the argument, and approved the text, and is responsible for all claims. Consistent with current editorial policy across major publishers and preprint servers — which uniformly bars AI systems from authorship on accountability grounds and requires disclosure of substantive AI assistance — that assistance is disclosed here rather than reflected in the author list. Corpus statistics were machine-counted against the repository on the date given in the front matter. The disclosure extends to the evidence: the corpus's symbolization scripts and the pre-commit adversarial reviews of §5.1 were likewise produced with machine assistance under the author's direction, and admitted only through the run-and-verify discipline this paper reports.

References

Repository artifacts cited (paths relative to the Axioma repository, July 2026 tree): the book-pass corpus, tests/axioma/showcase/books/ (55 directories, 812 scripts, 14,199 expect() sites, counted 2026-07-19); the praxeology methodology essay and verified companion, tests/axioma/showcase/executable-praxeology/; the companion paper draft (withheld pending review); the terminology and phrase-lineage reference, resources/docs/claude/FORMAL_ANALYTIC_EXECUTABLE_PHILOSOPHY.md; the KM comparison, resources/docs/claude/CONCEPT_VOCABULARY_REFERENCE.md; the executed adversarial review of the engine's claims, resources/docs/claude/ADVERSARIAL_ACCOMPLISHMENTS_REVIEW_2026-07.md; the Leibniz–Porphyry–syllogistic package, leibniz/; the conceptual-graph package, cg/.