On Praxeology: The Concrete and the Universal, Deduction and Computation

§ 1The concrete and the universal

Generalizing is not something we choose to do; it is a consequence of how minds are constituted. To perceive at all is already to sort — to assign properties and notice what recurs across otherwise different occurrences. In this sense every human being carries a working classification apparatus from birth, and living a human life requires nothing more than that. Our daily traffic with the world is a traffic with concretes: this bread, that road, the person in front of me now.

What is not required for ordinary life, and is instead a deliberate and somewhat unnatural discipline, is the methodical extraction of universals — the search for abstract laws to which the concrete occurrences are subject. This is what the scientist does on purpose, and it is a different activity from the effortless classifying we all do. The interesting question is which of these two the study of human action belongs to.

That question already contains a fork, because “praxeology” names two different projects that happen to share a word (and, across traditions, a spelling):

• Praxeology as a general theory of efficient action — how to act well, given ends and means. This is close to engineering, management, and planning. Its home is the Polish tradition of Tadeusz Kotarbiński (often spelled praxiology).
• Praxeology as the foundation of the social sciences — the deductive core from which economic law is derived. This is the Austrian project of Ludwig von Mises.

The spelling tracks the split. Praxis + -logy gives the regular form praxiology, which the Polish school keeps; English naturalized the Austrian form as praxeology (via Louis Bourdeau's 1882 praxéologie), and — because Mises and Austrian economics drive most usage — the e-form dominates. This essay follows that convention: praxeology throughout, praxiology only for Kotarbiński's tradition.

The first is more relevant to daily life; the second makes the stronger claim about valid knowledge. Much of the confusion around praxeology comes from not saying which one is on the table. As we will see in §3, the two projects also imply two different computational shapes — and a system can host both without conflating them.

A third thread runs underneath both and reappears in §4 and §5: the intersection with the empirical study of how people actually decide — Herbert Simon's bounded rationality and the Kahneman–Tversky heuristics and biases program. Whether that research refutes praxeology, complements it, or simply operates on a different layer is one of the load-bearing questions of this essay.

§ 2What praxeology claims

Praxeology, as Mises formulated it in Human Action (1949), is the deductive study of human action built on a single foundational axiom: individual human beings act purposefully. To act is to engage in conscious, purposeful behavior — to employ chosen means toward chosen ends. It is distinguished from involuntary or reflexive movement, which is behavior but not action.

From that starting point the theory proceeds by four commitments:

• The Action Axiom. Humans act. The proposition is offered not as a hypothesis but as a self-evident truth about what action is.
• A priori reasoning. Economic law is derived from the axiom by logical deduction, not induction from data. Its conclusions are held to have the epistemic character of mathematics or geometry — necessary, not contingent. In Mises's own words, praxeology's “statements and propositions are not derived from experience … [they are,] like those of logic and mathematics, a priori … not subject to verification or falsification on the ground of experience and facts” (Human Action, p. 32).
• Methodological individualism. Social and economic phenomena are explained as the outcome of the actions and interactions of individuals; there is no collective actor over and above them.
• Subjectivism. Value is not a property of goods but an ordering imposed by an acting mind for a purpose. Worth is conferred, not discovered.

From the bare category of action, Mises and the Austrians deduce a surprising amount: the law of marginal utility, time preference and originary interest, the logic of supply and demand, the theory of the business cycle. The claim is that these are not empirical regularities that might have been otherwise, but implications of what it means to act — true in any possible world containing actors.

Yet the base is not quite a lone axiom mechanically generating the rest — and Mises is careful about this. Action presupposes a small set of a priori categories: causality (“acting requires and presupposes the category of causality … causality is a category of action,” and “the category means and ends presupposes the category cause and effect”), time, and value. These are implied in the concept of acting, not deduced from it. And not everything is a priori: Mises explicitly flags the disutility of labor as “not of a categorial and aprioristic character — we can without contradiction think of a world in which labor does not cause uneasiness,” so that “experience teaches that there is disutility of labor” (Human Action, ch. I §5 and ch. II). It is a contingent empirical premise doing real work in the theory of production and leisure (Rothbard would later name such subsidiary postulates explicitly). Praxeology's foundation is therefore graded — a necessary axiom, its presupposed categories, and a few acknowledged empirical postulates — which is exactly the distinction Axioma's grounding ladder makes executable (§7), and the honest answer to the “one self-evident axiom, therefore everything” caricature.

Two boundaries are deliberate. First, praxeology brackets the “why.” Purposeful, goal-directed behavior could be ascribed to much besides human beings — animals, even (metaphorically) stars and systems — but that is the province of physics, biology, and metaphysics; praxeology neither explains what enables purposeful action nor builds a theory of the mind behind it. “The theme of praxeology is action as such” (Human Action, p. 11); the psychological mechanism that produces the action is set aside. Action begins in felt uneasiness and the belief that some means will remove it, and praxeology asks only which means the actor will employ toward the end — not why the end was chosen. Second, and for the same reason, it is not cognitive science or AI: it neither models nor simulates intelligence; it takes purposive action as given and derives what that fact entails. The restriction to human action is exactly what lets the social sciences — economics first — be founded on it.

That is a large claim, and it is precisely the size of the claim that draws the criticism in §4.

§ 3Two praxeologies, two computational shapes

Before the criticism, it is worth cashing out the fork from §1, because it is the single most useful idea for anyone trying to build a praxeology rather than argue about one.

Kotarbiński's praxiology is, computationally, a planning engine. Its subject matter — effectiveness, efficiency, economy of action, the anatomy of good work — is the logic of getting from a state to a goal through means under constraints. That is exactly the territory of means–ends analysis, partial-order planning, and the classic “general problem solver.” Give it ends, an inventory of means, and a cost structure, and it searches for efficient action. Its outputs are plans. (Strip the value language from this fork — no “better” or “worse,” not even “uneasiness,” just an agent moving from a current state to a chosen other — and you reach a still leaner base: action as pure state transition, derivable from the laws of thought. That is the most minimal cousin of Mises's action axiom, and it is exactly what a planner mechanizes.)

Mises's praxeology is, computationally, a proof engine. Its subject matter is not “what should this actor do?” but “what necessarily follows from the fact that any actor acts at all?” That is entailment-checking: given the action axiom and a rule of inference, derive the consequences and certify that the derivation is valid. Its outputs are theorems, tagged with the provenance of their derivation.

The two are not rivals; they are different machines answering different questions. The Kotarbiński machine runs a scenario forward to find good action. The Mises machine checks a deduction to certify a law. Keeping them apart is the key that unlocks the simulation problem in §6 — and a language for executable philosophy can carry both, so long as it never mistakes a plan for a proof.

§ 3.5Neighbors and lineage

Four neighbors put action theory on a more exact footing, and they are easy to conflate — worth keeping apart, because “executable praxeology” is routinely mistaken for the computational program when it belongs with the formal-deductive one.

• Formal praxeology renders the theory in logical notation: the logic of action and deontic logic — G. H. von Wright (Norm and Action, 1963), after Anscombe and Davidson. Rigor comes from the formal language; the theory is written down, not run.
• The analytic theory of efficient action — the Polish praxiology of Kotarbiński and Gasparski (the Lvov–Warsaw school; §3's planner fork). Analytic and precise in its concepts, but empirical and normative in method: its theorist “build[s] his generalizations mainly on … practical experience,” settles for “persistent frequency” rather than certainty, and aims at “the technique of good, efficient work” (Praxiology, ch. I). By Mises's own line that makes it technology, not praxeology — he refuses to call praxeology “empirical” (“not derived from experience … like those of logic and mathematics, a priori”, Human Action, pp. 32, 57). A different discipline that shares the Greek root, not the enterprise.
• Computational praxeology runs the theory as simulation — agent-based models, big data, emergent dynamics. It is a scattered, emerging label (a recent working paper by Martin Kresák applies it to AGI under the coinage “praxeocybernetics”; its established academic home is agent-based computational economics, ACE). Crucially it relaxes apriorism — admitting uncertainty and studying emergent tendencies rather than deriving certain theorems — the very empirical turn §6 warns against calling praxeology.
• Executable praxeology — this project — renders the theory as machine-checked deduction. Rigor comes from the proof engine and its provenance ladder; apriorism is preserved and mechanized, not relaxed.

The apriorism column is where the fault line of §6 runs, which is why the four are worth keeping apart. “Executable praxeology” is not a rebrand of the computational program, nor a formalization of the efficient-action one: it sits with the formal-deductive lineage, and its distinctive move — executability as verification — occupies a cell no neighbor fills. Von Wright's tradition is formal but unexecuted; Kotarbiński's is empirical and normative, not apriorist; computational praxeology is executed, but as simulation, not proof. The term itself appears to be this project's own coinage; the Austrian tradition, wary of formalism since Mises, largely left the cell empty.

§ 4The critics — and the replies

The document this revises presented the standard critique in the mainstream's own voice, with no rejoinder. That is not a fair map of the debate. Each objection has a well-developed Austrian reply, and the honest position is that some replies are strong and at least one buys its safety at a real price.

4.1 “It rejects the scientific method / it is not falsifiable”

The most common charge (associated with Thomas Mayer among others) is that praxeology is unscientific because it derives conclusions from an axiom rather than testing them against observation. Sharpened through Karl Popper, the charge becomes: a theory that forbids no observation is not falsifiable, and an unfalsifiable theory is closer to dogma than science.

The reply. The demand presupposes that all knowledge worth the name is empirical and falsifiable — which is itself a contestable philosophical thesis, not a neutral standard. We do not “falsify” the Pythagorean theorem, and its immunity to refutation does not make it dogma; it makes it a different kind of knowledge. Mises's claim is that praxeological law is of that second kind — apodictic, not conjectural. One may reject that claim, but one cannot refute it merely by assuming falsificationism, on pain of begging the question. The real disagreement is not about method but about whether synthetic a priori knowledge of action exists at all — which is §4.2.

4.2 “The action axiom is a tautology / is really empirical”

Two objections travel together. First: the axiom is a tautology — true by definition, like “all bachelors are unmarried” — and tautologies carry no substantive content, so the elaborate deductions cannot be as robust as advertised. Second: the axiom is actually an empirical generalization about observed human behavior, dressed up as a priori truth.

The reply (and the figure the original omitted: Hoppe). The Austrian answer is that the axiom is neither analytic-tautological nor empirical but synthetic a priori in Kant's sense — informative about the world, yet knowable without observation. Hans-Hermann Hoppe (Economic Science and the Austrian Method, 1995) gives this its sharpest form with the a priori of argumentation: the action axiom cannot be coherently denied, because the very act of arguing against it is itself an instance of purposeful action — choosing words (means) to establish a conclusion (end). The denial refutes itself in the performing. This dissolves the “is it really empirical?” worry directly: you do not need to observe actors to know the axiom, because you cannot so much as dispute it without instantiating it.

Mises himself was less crisply Kantian — he sometimes called the category of action a “law of thought,” hedging between Kant and something more psychological. Hoppe is the one who plants the flag firmly in synthetic-a-priori ground, and any serious treatment of this criticism has to go through him.

4.3 The middle ground the debate actually occupied: Machlup, Hutchison, Rothbard

The apriorism-vs-empiricism framing is too clean, because the most careful twentieth-century participants stood between the poles. Terence Hutchison (The Significance and Basic Postulates of Economic Theory, 1938) pressed economics toward operational testability. Fritz Machlup — a student of Mises but methodologically close to Popper — answered in “The Problem of Verification in Economics” (1955) with an instrumentalist middle position: the fundamental postulates of economics are not directly testable in isolation, but are heuristically indispensable and are tested only through the joint empirical implications of the theories built on them. His memorable formulation is that the basic postulates are “not to be challenged for the time being” — provisionally insulated from direct refutation, not because they are apodictic, but because challenging them piecemeal is methodologically unproductive.

Rothbard (“In Defense of ‘Extreme Apriorism’”, Southern Economic Journal, 1957) pushed back toward pure Mises, insisting the axiom's certainty is not a mere working convenience. The Hutchison–Machlup–Rothbard exchange is the real texture of the verification debate, and it maps with unusual directness onto a system that tracks grounding: one and the same law can be run at three different premise tiers — apodictic (Rothbard/Mises), provisionally-fixed postulate (Machlup), operational hypothesis (Hutchison) — and the tiers, not the law, are what the parties disagree about. (This is not a hypothetical: it is exactly the shape of the executable Verification-Debate treatment already built on the Axioma engine.)

Bruce Caldwell's Beyond Positivism (1982) is the standard scholarly frame for all of this and should anchor the reading list; it takes the Austrian method seriously without either endorsing or dismissing it wholesale.

4.4 The problem of human irrationality — and where it really bites

Behavioral economics — Simon's bounded rationality, the Kahneman–Tversky heuristics and biases, prospect theory — shows that people systematically deviate from ideal rationality. The objection: praxeology's actor is too simple to be real.

The reply, and an honest limit. Praxeology's “rationality” is formal, not substantive. It claims only that action is purposeful selection of means toward ends — not that the ends are wise or the means optimal. A person in the grip of loss aversion still acts: they still select means toward an end. So cognitive biases, which concern the content and quality of choices, do not touch the action axiom at all. On this layer, behavioral economics is a complement — it describes the empirical texture of choices whose formal structure praxeology has already characterized — not a refutation. Mises would say that even colloquially “irrational” behavior is action.

But the clean version overstates the case, and it is worth being honest about where the critique does bite. Some downstream praxeological theorems — the derivation of the law of marginal utility via Rothbard's “demonstrated preference,” for instance — lean on an auxiliary premise that the preference ordering revealed in action is consistent enough to carry the deduction. Behavioral findings of preference reversal and framing effects put pressure precisely there. The Austrian move is to narrow “demonstrated preference” to the preference revealed in this specific act at this moment, so that reversals across contexts never contradict it. That defense works — but it works by making the premise nearly unfalsifiable by construction, which is the very charge of §4.1 returning at the level of the auxiliary assumptions. The action axiom is genuinely untouched; some of the deductions built on it are more exposed than the strong Austrian reading admits.

4.5 The internal limits: Hayek and Lachmann

The most instructive boundaries on what praxeology can deduce come not from outside but from inside the Austrian school. Friedrich Hayek is the bridge figure: he shared Mises's subjectivism and worked within the broad Austrian framework, yet kept a studied distance from strict apriorism — he “never embraces apriorism,” as Caldwell's survey of the critics puts it (Praxeology and Its Critics, 1984) — closer in temperament to an evolutionary, fallibilist view of knowledge than to Mises's apodictic certainty. His knowledge problem (“Economics and Knowledge”, 1937; “The Use of Knowledge in Society”, 1945) marks a limit of a distinctive shape: the form of the price mechanism may be a praxeological truth, but the content it coordinates — the dispersed, tacit, ever-changing knowledge held across millions of minds — is deducible from no axiom and can be discovered only by the market process itself. Deduction supplies the skeleton; it cannot supply the data the skeleton coordinates.

Ludwig Lachmann pushed that subjectivism to its edge, extending it from preferences to expectations (The Market as an Economic Process, 1986) — his methodology, Caldwell notes, has “more in common with the radical subjectivism of G. L. S. Shackle than with the apriorism of Mises.” Once expectations are themselves subjective and divergent, the future is genuinely open — a “kaleidic” society — and the determinate equilibrium results that praxeology sometimes reaches for are not guaranteed. Lachmann marks the honest edge of the program: the action axiom is secure, but the more the deductions promise determinacy, the more they smuggle in assumptions that radical subjectivism denies. Any computational praxeology should treat determinacy as something to be earned per-derivation, not assumed.

4.6 Bunge: is it just egoism, detached from ethics and science?

The philosopher of science Mario Bunge — a career opponent of pseudoscience — leveled a two-part charge: that Mises's praxeology is “nothing but the principle of maximization of subjective utility — a fancy version of egoism,” and that, “conceived in extremely general terms and detached from both ethics and science,” it “has hardly any practical value.”

The reply. The first half misreads the formalism. Praxeology's “maximization” is wertfrei and purely formal — the actor pursues whatever end he ranks highest, and Mises is explicit that the end may be another's welfare (action removes felt uneasiness, which can be uneasiness at a stranger's suffering as readily as at one's own hunger). It assumes no egoism; an altruist and a miser instantiate the action axiom alike. Bunge has confused the structure of choice with a substantive motive — the error §4.4 warns against. The second half lands a fairer blow: a maximally general, purely a priori praxeology does risk floating free of application. But that indicts the detached core, not the program — Rothbard reconnected it to ethics (natural law, §4.3), and the executable, applied-layer reading of this essay (§7–§8) is an attempt to reattach it to rigor and use. The way to answer “little practical value” is to make it do work; that is what a proof engine and its applications are for.

§ 5Can praxeology be computed?

Given all that, what does it mean to put praxeology on a computer? There are three distinct approaches, and the original notes ran them together. Here they are on one clean spine.

5.1 Symbolic / deductive — a logic machine

Encode the axioms and inference rules; let the engine derive consequences. In a rule-based idiom:

% purposeful action: an actor employs a means M believed to serve end E
acts(Actor, E) :- feels_uneasiness(Actor), believes(Actor, M, serves(M, E)).

% mutually beneficial exchange: each party values what the other holds more
exchange(A, B, G1, G2) :- prefers(A, G2, G1), prefers(B, G1, G2).

(Note that even this toy needs care: a body variable like the means M must actually be bound and used, or the clause is unsafe — a foreshadowing of why the engine's treatment of relations, heads, and rule variables has to be principled rather than illustrative.)

This does not predict behavior numerically. It derives the necessary consequences of action — a logic machine, not a forecaster. This is the faithful realization of the Mises fork from §3.

5.2 Agent-based modeling — a scenario machine

Give each agent a subjective value scale, an endowment, and the ability to exchange, then run the population forward and watch patterns emerge: price signals, shortages under price controls, clearing under free exchange. Frameworks like NetLogo or Mesa fit here. This is the Kotarbiński fork made dynamic — it runs scenarios rather than checking deductions, and (crucially, see §6) it is a quasi-empirical activity.

5.3 Neuro-symbolic — where §1's third thread comes home

A hybrid keeps a symbolic layer for the apodictic skeleton and adds a neural layer for empirical detail. This is exactly where the Simon/Kahneman thread from §1 belongs:

• Symbolic layer: the Misesian a priori structure — the deductions, the impossibilities, the invariant form of action.
• Neural / empirical layer: the Simon/Kahneman detail — actual frequency distributions, bounded-rationality effects, framing, noise.

The symbolic layer says what must hold of any actor; the neural layer says how these actors, with their biases and limits, tend to fill in the contingent blanks. Behavioral economics stops being a refutation and becomes the empirical stratum riding on top of an untouched logical skeleton — the reconciliation §4.4 promised.

§ 6The category error: simulation is not deduction-checking

Here is the crux the original notes circled but never landed. The “limits of simulation” section posed a dilemma:

• Mises: simulating praxeology generates no new truths, only illustrates them.
• Critics: but if you can simulate it, then it is testable — and therefore closer to empirical science after all.

The critics' inference is a non-sequitur, and naming why is essentially the whole thesis. It conflates two things a computer can do that have nothing epistemically in common:

1. Simulation — running a model forward to generate trajectories that can be compared against data. This is what the ABM of §5.2 does. It is quasi-empirical by nature; its outputs are contingent on inputs and can, in principle, match or miss the world.
2. Deduction-checking — verifying that a conclusion follows from premises. This is what a proof assistant (Coq, Lean, Isabelle) does, and what the logic machine of §5.1 does. It generates no empirical content whatsoever; its outputs are entailment facts.

Mechanizing a proof does not make its subject matter empirical. Coq checking a theorem about the integers does not turn number theory into a laboratory science. So the correct resolution of the dilemma is: Mises is right that the deductive engine discovers no new truths (it certifies, it does not observe), and the critic is wrong that computability implies testability (a proof-checker is computable and not empirical). The word “simulation” was doing all the illicit work; drop it, distinguish the two machines, and the dilemma dissolves.

The payoff is a precise statement of what an executable praxeology is: not a forecaster, not an empirical test, not a discovery procedure, but a mechanized derivation-checker with provenance — an instrument that certifies that the laws Austrians claim to deduce really do follow from the action axiom, and shows the chain by which they follow.

§ 7Praxeology in Axioma

This is where the generic discussion should become concrete, because the deduction engine of §5.1 and §6 is not hypothetical — it is what the Axioma language is for.

Axioma treats the action axiom as a first-class, grounded fact and the economic laws as derivations whose provenance is tracked, not asserted. The relevant surface:

• Concepts and relations model actors, ends, means, preferences.
• Strict rules (head <= body) carry apodictic derivation; defeasible rules (head <~~ body) carry provisional inference — the Machlup tier of §4.3.
• An epistemic grounding ladder records how each fact is known: axiom > postulate > theorem > conjecture > hypothesis > datum. A strict rule applied to an axiom yields a theorem — provenance is preserved, not laundered into fresh axiom status.
• why and proof(...) render the derivation chain back to the originating axioms — the deduction-checking of §6 made inspectable.

Sketch, in Axioma's idiom:

# The action axiom, asserted at the strongest tier — and, per Hoppe (§4.2),
# the one premise that cannot be coherently denied.
axiom acts_purposefully("homo_agens")

# Praxeological laws as strict derivations (`<=`), not posits: action
# presupposes scarcity; and two parties who each value what the other
# holds will exchange.
faces_scarcity(H) <= acts_purposefully(H)

relation prefers(agent, wants, gives)
exchange(A, B) <= prefers(A, "wine", "grain") and prefers(B, "grain", "wine")
axiom prefers("alice", "wine", "grain")
axiom prefers("bob",   "grain", "wine")

# Query the provenance rather than assert the conclusion:
grounding("faces_scarcity", "homo_agens")   # -> "theorem"  (derived, not assumed)
grounding("exchange", "alice", "bob")        # -> "theorem"
why exchange("alice", "bob")                 # -> prints the derivation chain

Two things about this are worth underlining against the criticisms of §4:

• It is a proof engine, the Mises fork of §3 — it certifies entailment; it does not forecast. That is precisely why “you simulated it, so it's empirical” (§6) does not apply: nothing here is run forward against data. What it mechanizes is Mises's a priori deduction — praxeology proper — not the empirical efficiency-recipes he classes as technology (§3.5); the grounding ladder keeps that line visible in every proof.
• The grounding ladder is the executable form of the verification debate (§4.3). The same premise can be entered as an axiom (Rothbard/Mises), a postulate held “for the time being” (Machlup), or a hypothesis (Hutchison). A strict derivation always labels its conclusion a theorem — recording how it was reached (strict inference), not how firmly its premise is held — while the proof() chain surfaces the premise tier each conclusion actually rests on. So the methodological dispute becomes a choice of premise tier, visible in the provenance, not an argument conducted in the abstract. (The Axioma showcase already carries a worked Mises praxeology script and a full Hutchison–Machlup–Rothbard verification-debate pass on exactly this machinery; the companion script to this essay re-derives the point and asserts it.)

The Kotarbiński fork (§3) is available too, but as a different facility — Axioma's planning and problem-solving engines answer “what is the efficient action?” and must never be confused with the proof engine that answers “what necessarily follows?” Keeping those two straight, in the tool as in the theory, is the discipline this whole essay is about.

§ 7.5The Austrian objection: does formalizing it lose the meaning?

There is a sharper challenge, and it comes from inside the Austrian camp rather than from the mainstream critics of §4. It runs: if praxeology really is a chain of deductions from a single axiom, then it should be mechanizable — expressible in symbolic logic and checked by a machine. Yet the Austrians themselves refuse all formalism, insisting on verbal exposition, because they hold that in symbols and equations the meaning is lost. Physics can mathematize because it abstracts away everything but the measurable; human action has no such measurable core, so the science is qualitative, not quantitative — and formalizing it, they say, falsifies it.

The objection is half right, and the half it gets right is the half Axioma honors. Mises's actual complaint is against quantification: “there are no constant relations” in human action, so economics “is not quantitative and does not measure because there are no constants” (Human Action, p. 56). An executable praxeology that rendered action as magnitudes, utility functions, and equations would betray it — and Axioma introduces none: no numbers, no measurement, no functional forms.

But logical formalization is not mathematization, and conflating the two is the error. Mises himself locates praxeology's theorems “like those of logic and mathematics, a priori” — the medium of deduction is symbolic logic, not arithmetic. Axioma formalizes only that: the qualitative categories (uneasiness, ends, means, preference, exchange) as named relations, and the deductive steps as rules whose provenance the grounding ladder records. Nothing is quantified; the concepts travel under their own names — an end is the relation end, not a number — so the “meaning” the Austrians fear losing is exactly what is kept. What gets mechanized is the entailment, the very thing Mises says praxeology is made of.

Concretely, the core deductions are a chain of qualitative implications — action → choice → scarcity → cost; purpose → subjective value; action → time-preference — from which opportunity cost, marginal utility, and originary interest fall out as theorems. Not a number appears; each arrow is a <= rule, and the companion script executes exactly this chain and traces every conclusion back to the action axiom. The formalization is Euclidean in structure, not econometric.

So the executable approach turns the objection into a test. If a purported praxeological law can be derived mechanically from the axiom, the apriorist claim is vindicated in the strongest possible way — the deduction is checked, not merely asserted in prose. And if it cannot — if a step secretly needs an empirical premise — the failure is diagnostic, exposing exactly where verbal exposition smuggled experience in under cover of “self-evidence.” Mechanization is not the enemy of verbal praxeology; it is its auditor. (The one genuine residue is the interpretive understanding of ends — Mises's thymology, the historian's verstehen — which is not deductive and not the target here; the grounding ladder marks where a claim leaves the a priori core for the empirical or motive kinds, §3.5.)

§ 8What it is, and what it is not

Praxeology can be put on a computer — but only if we are exact about which computer. Of its a priori core:

• It is not a statistical forecaster.
• It is not an empirical test of human behavior; being mechanically checkable does not make it empirical (§6).
• It is not a discovery machine; it certifies deductions, it does not find new laws (Mises was right about this).

It is a mechanized derivation-checker with provenance — a playground for exploring, and verifying, the logical consequences of action. The empirical study of how people actually decide (Simon, Kahneman, Tversky) is not a rival to this but the stratum that rides alongside it (§5.3): the neural detail atop the a priori skeleton. It is there — in that applied, data-fed layer, not in the deductive core — that verifiable prediction belongs: the core certifies what any actor must do; the applied layer, given the measured biases and circumstances of these actors, forecasts what they will tend to do, and is testable exactly where the core is not. The apriorist “the test is valid deduction” and the pragmatist “the test is prediction” are then not rivals but a division of labor across the two layers. The economist Antony Davies sharpens that division from the empirical side: because a statistical test presupposes an independently developed theory to select and interpret its model, some praxeology is prior to the econometrics rather than displaced by it — the a priori core is what the applied layer runs on. Steven Horwitz makes the converse point: Mises's apriorism does not make Austrian economics anti-empirical — modern applied Austrian work draws on history, institutions, and both qualitative and quantitative evidence; what is a priori is the core, not the application. And the sharpest limits are internal (Hayek and Lachmann, §4.5) — determinacy is to be earned per-derivation, never assumed.

That is the resolution the concrete/universal framing of §1 was pointing at all along. Daily life needs only the classification apparatus we are born with. Science reaches for universals on purpose. Praxeology's peculiar claim is that some universals about action can be reached not by observation but by deduction — and an engine that checks those deductions, without pretending to forecast or to falsify, is the faithful computational form of that claim.

§ 9In this project: the executable corpus

This essay is the conceptual companion to a body of runnable praxeology already built on the Axioma engine. Unless noted, paths are in the axiomalang repository.

• tests/axioma/showcase/executable-praxeology/executable_praxeology.ax — the verified companion to this essay: the action axiom, the strict derivations of §5.1/§7, the proof/why traces of §6, the verification-debate tiers of §4.3, and the behavioral-kind point of §4.4, each asserted with expect(...) (15/15 pass).
• tests/axioma/showcase/executable-praxeology/Time and Uncertainty in Axioma.md — the companion essay that puts this machine on the categorial doctrine of Human Action ch. V (time) and ch. VI (uncertainty): the “two modes of one fact” thesis with uncertainty as defeasibility, the class/case distinction drawn as a kind difference, and profit/loss as the residual of a defeasible expectation. Its verified script time_and_uncertainty.ax (13/13) sits beside it, backed by a six-script book-pass under tests/axioma/showcase/books/mises-human-action/ (44 assertions + a --typecheck ordinal discipline) working ch. I/V/VI section by section.
• tests/axioma/showcase/books/rothbard-mes/ — a book-pass corpus over Rothbard's Man, Economy, and State. Several scripts are the executable form of arguments made here: 01_action_axiom.ax, 03_demonstrated_preference.ax (the §4.4 consistency point), 07_apriorism_dial.ax (the §4.3 premise-tier choice), and 09_double_inequality.ax (the exchange law of §5.1/§7). The companion above complements these — it isolates the deduction-checking thesis — rather than duplicating them.
• tests/axioma/showcase/books/menger-principles/ and .../robbins-nature-significance/ — the marginalist and methodological bookends: Menger's subjective-value origin and Robbins's scarcity / means–ends definition of the discipline.
• tests/axioma/showcase/13_mises_praxeology.ax — the action axiom → catallactic cascade in Axioma's natural-language surface, with proof() traces back to the axiom.
• resources/docs/claude/PRAXEOLOGY_FORMALIZATION_LITERATURE.md — the literature grounding.
• docs/Logic of Praxeology.md (in the sibling axioma repo) — an earlier formal derivation stack from the action axiom down to the micro-laws.

Together these realize the §3 claim in practice: the proof engine is not a proposal but a working artifact, and this essay is its methodology.