Six Horses, Zero Action: Rothbard's Proof, Machine-Checked

A man owns six horses and has a ranked list of things a horse can do for him. Rothbard takes him through losing one, then another, and reads off the law of marginal utility: the more of a good you have, the less the last unit is worth to you. He says the law is "derived from the fundamental axiom of human action" (Man, Economy, and State, p. 27).

Mises says the theorems of Austrian economics are "perfectly certain and incontestable, like the correct mathematical theorems" (Human Action, ch. 2). His word for that certainty is apodictic. If they are like mathematical theorems, they can be checked like them, and apodictic checks this one in Lean 4, a proof checker.

What the Checker Had to Be Told

The checker refuses a proof that uses anything not in the theorem's statement or a definition it names. Here is the theorem the law follows from, as the code states it:

theorem urgency_principle {praxis : ActionFrame} [DecidableEq praxis.End]
    {agent : praxis.Agent} {time : praxis.Time}
    {stock : Stock praxis agent time}
    (plan : AllocationPlan stock) (dominance : SwapDominant plan)
    (independent : praxis.IndependentUses agent time)
    (fewer more : Finset praxis.Means) (step : stock.OneMore fewer more) :
    ∀ kept ∈ plan.wouldServe fewer, ∀ lost, lost ∈ plan.wouldServe more →
      lost ∉ plan.wouldServe fewer →
        praxis.PrefersEnd agent time kept lost

What it assumes is in the brackets or in the definitions they name: a plan, one claim about that plan, one condition on his wants, that two wants can be told apart, and two stables out of his horses, one horse apart.

The plan is what the man would do with any subset of his own horses. The claim, swap dominance, is that with any such set he prefers the wants he would serve to any one swap of them, a want he serves dropped for a want he leaves. The condition is that his wants do not depend on each other, so a preference between two bundles differing in one want is a preference between those two. That step is ours, not Rothbard's: he ranks wants directly and never argues from bundles, and where wants are complementary it fails.

The code builds Rothbard's man, proves the claim and every condition of him, and gets two of Rothbard's conclusions back as theorems: losing one of six horses costs him pleasure riding (p. 25), and which horse goes makes no difference (p. 27).

Action Is Never Used, Interchangeability Once

Rothbard says the law follows from two things. The first is action: his premise "follows from the universal fact that action uses scarce means to satisfy the most urgent of the not yet satisfied wants" (p. 24). The second is units: "This consequence follows from the defined interchangeability of units" (p. 27).

No theorem behind the law mentions an act. @claude-fable-5 began the code with the claim that choosing one thing over another shows it preferred; no theorem cited it, and @claude-fable-5.1 removed it. Rothbard gives one derivation, and action does no work in it; nobody has shown a derivation from action is impossible.

Interchangeability is used once. Told horse by horse, one application of the theorem above, the law needs nothing about it. Told by count, what the sixth horse adds against what the fifth added, it needs the plan to depend on how many horses and not on which. Where it fails the counted form says nothing.

He Licenses the Scale with the Law

Swap dominance is Rothbard's premise taken one swap at a time, and it is about what the man would do. It ranks the wants he would serve with four horses, and three, and two, while he owns six, a reach Rothbard allows himself: holding none of a good "does not affect the principle" (p. 32). What the claim adds is that he holds every one of those answers at once, before any choosing: a value scale in advance.

Rothbard says no man needs one. "Value scales do not exist in a void apart from the concrete choices of action," and there is "no need for him to formulate hypothetical value scales" (p. 33). On the same page he exempts one thing: nobody can predict a man's choices "except that they will follow the law of marginal utility, which was deduced from the axiom of action." The law is what licenses the scale, and the scale is what the law is proved from. The warrant for the premise is the conclusion.

The circle is not in the proof, where the claim is assumed and nothing reaches back. It is in Rothbard's license for the claim, and the rule, the claim, and the exemption are all his.