1.8. Mises's route🔗

Rothbard's is not the only derivation the tradition offers. Mises reaches the same law in Human Action (ch. VII, §1) by an argument of a wholly different shape, and the library carries his route as a second target. It is built in a module that cannot see Rothbard's theorems at all, so that whatever his argument spends has to be stated there, and shows on the signature. A proof that could reach for Rothbard's lemmas would have assumed the answer to the question this part exists to ask.

His statement of the law:

If the supply available increases from n–1 units to n units, the increment can be employed only for the removal of a want which is less urgent or less painful than the least urgent or least painful among all those wants which could be removed by means of the supply n–1.

Two things differ from Rothbard's wording. The ladder runs upward, from n–1 to n, where Rothbard takes a horse away; and it singles out a least urgent want, where Rothbard compares two named steps. It is read here as Rothbard's is read — two supplies held up against each other at one time — because Mises's own definition has that shape: the marginal employment is the one a man makes at n units "but would not make if, other things being equal, his supply were only n–1 units". A reading on which the ladder is a history of acquisitions is a separate target, set out under The ladder as a history.

def

Apodictic.Mises.marginalEmployment {praxis : ActionFrame}
  {agent : praxis.Agent} {time : praxis.Time}
  {stock : Stock praxis agent time} (plan : AllocationPlan stock)
  (fewer more : Finset praxis.Means) : Set praxis.End
Apodictic.Mises.marginalEmployment
  {praxis : ActionFrame}
  {agent : praxis.Agent}
  {time : praxis.Time}
  {stock : Stock praxis agent time}
  (plan : AllocationPlan stock)
  (fewer more : Finset praxis.Means) :
  Set praxis.End

Mises's marginal employment — the ends served at the larger supply and not at the smaller.

"We call that employment of a unit of a homogeneous supply which a man makes if his supply is n units, but would not make if, other things being equal, his supply were only n–1 units, the least urgent employment or the marginal employment, and the utility derived from it marginal utility" (Human Action, ch. VII, §1).

Stated as the DIFFERENCE of two counterfactual allocations at one time, which is what "other things being equal" asks for.

Restates MarginalUtility.marginalEnds deliberately: see the module docstring on isolation. That the two coincide is a theorem for a module importing both, not an import here.

A definition, not a claim — Mises introduces it as one ("We call that employment ..."), and says in the next breath that establishing it costs nothing praxeological.

def

Apodictic.Mises.LeastUrgentServed {praxis : ActionFrame}
  {agent : praxis.Agent} {time : praxis.Time}
  {stock : Stock praxis agent time} (plan : AllocationPlan stock)
  (subStock : Finset praxis.Means) (want : praxis.End) : Prop
Apodictic.Mises.LeastUrgentServed
  {praxis : ActionFrame}
  {agent : praxis.Agent}
  {time : praxis.Time}
  {stock : Stock praxis agent time}
  (plan : AllocationPlan stock)
  (subStock : Finset praxis.Means)
  (want : praxis.End) : Prop

Least urgent among those served — Mises's "the least urgent or least painful among all those wants which could be removed by means of the supply n–1".

A situational condition, NOT a claim about action: it says of a given end that nothing else served at that sub-stock ranks below it. It is stated of an end handed to a theorem, never asserted to exist — whether such an end exists at all is a separate question, and one that cannot be answered without saying more about Prefers than the library assumes.

That this is a hypothesis rather than a derived object is the first place the two routes visibly differ. Rothbard's derivation never needs a minimum: it compares two named steps. Mises's sentence names one.

def

Apodictic.Mises.LadderHolds {praxis : ActionFrame}
  {agent : praxis.Agent} {time : praxis.Time}
  {stock : Stock praxis agent time} (plan : AllocationPlan stock) : Prop
Apodictic.Mises.LadderHolds
  {praxis : ActionFrame}
  {agent : praxis.Agent}
  {time : praxis.Time}
  {stock : Stock praxis agent time}
  (plan : AllocationPlan stock) : Prop

Mises's ladder — his statement of the law, written out as a target so that what proves it, and from what, is legible.

"If the supply available increases from n–1 units to n units, the increment can be employed only for the removal of a want which is less urgent or less painful than the least urgent or least painful among all those wants which could be removed by means of the supply n–1" (Human Action, ch. VII, §1).

A def of a Prop, not a theorem, and deliberately so: it is reached twice below from two different premise sets. ladder_holds derives it from Rothbard's premise, and ladder_from_order from Mises's own bridge. Which premises each spends is on each theorem's signature.

His conclusion is Rothbard's. Before asking what Mises's argument spends, ask whether it has to spend anything. Does the ladder follow from Rothbard's premise outright? It does, and the proof is a few lines. Two things fall out of it. The upward direction is narration. And the least-urgent qualifier does no work at all: the proof consumes only that the want was served at the smaller supply, and the machine can show as much, because the same conclusion goes through for every want served there, not only the least urgent.

theorem

Apodictic.Mises.ladder_for_every_served {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 : praxis.End) :
  kept ∈ plan.wouldServe fewer →
    ∀ added ∈ Mises.marginalEmployment plan fewer more,
      praxis.PrefersEnd agent time kept added
Apodictic.Mises.ladder_for_every_served
  {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 : praxis.End) :
  kept ∈ plan.wouldServe fewer →
    ∀
      added ∈
        Mises.marginalEmployment plan
          fewer more,
      praxis.PrefersEnd agent time kept
        added

The ladder holds for EVERY end served at the smaller supply — not only for the least urgent one.

This is the control, and it is deliberately stated in the strong form Mises does not state. His sentence singles out "the least urgent or least painful among all those wants which could be removed by means of the supply n–1"; this theorem drops the qualifier and keeps the conclusion. Whatever the extra unit adds is less urgent than ANYTHING the smaller supply serves.

What it spends: SwapDominant plan — Rothbard's premise, and the whole of the warrant problem — plus IndependentUses and decidable equality of ends. Nothing Misesian at all.

theorem

Apodictic.Mises.ladder_holds {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) :
  Mises.LadderHolds plan
Apodictic.Mises.ladder_holds
  {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) :
  Mises.LadderHolds plan

Mises's ladder, derived from Rothbard's premise — the control comes back positive.

LadderHolds follows outright from SwapDominant and IndependentUses. Mises's own derivation — the dilemma about intermediate stages, the appeal to the category of action — supplies nothing the conclusion needs, once the conclusion is read counterfactually.

And his minimality qualifier does no work. The hypothesis LeastUrgentServed plan fewer least is a conjunction; only its first half (that least is served at the smaller supply) is consumed. The second half — that nothing served there ranks below it — is destructured as _minimality and never used. The linter cannot see this, because it works a whole binder at a time and both halves arrive in one binder; ladder_for_every_served above is what makes the idleness a machine fact instead of a comment.

So of the two things Mises's sentence adds to Rothbard's — the upward direction and the "least urgent" restriction — the first is a narration and the second is idle.

The marginal employment, meanwhile, is Rothbard's marginal ends under another name — the same set, by definition. So there is one law on the table, not two, and what differs between the authors is only the argument for it.

theorem

Apodictic.Contrast.marginalEmployment_eq_marginalEnds
  {praxis : ActionFrame} {agent : praxis.Agent} {time : praxis.Time}
  {stock : Stock praxis agent time} (plan : AllocationPlan stock)
  (fewer more : Finset praxis.Means) :
  Mises.marginalEmployment plan fewer more =
    marginalEnds plan fewer more
Apodictic.Contrast.marginalEmployment_eq_marginalEnds
  {praxis : ActionFrame}
  {agent : praxis.Agent}
  {time : praxis.Time}
  {stock : Stock praxis agent time}
  (plan : AllocationPlan stock)
  (fewer more : Finset praxis.Means) :
  Mises.marginalEmployment plan fewer
      more =
    marginalEnds plan fewer more

The two definitions of the marginal ends coincide. Mises's "marginal employment" (Mises.marginalEmployment, the employment a man makes at n units and would not make at n–1) and Rothbard's marginal utility of a supply (marginalEnds, the ends the larger stock serves and the smaller does not) are the same set, definitionally. Each module states its own because Apodictic.Mises is isolated; that they agree is proved here, where both are in scope, and it is what licenses saying the two routes reach the same law.

His argument is a dilemma. Mises does not assert an ordering premise the way Rothbard does. He holds that the law "is already implied in the category of action", and argues it so:

There are only two alternatives. Either there are or there are not intermediate stages between the felt uneasiness which impels a man to act and the state in which there can no longer be any action … In the second case there could be only one action; as soon as this action is consummated, a state would be reached in which no further action is possible. This is manifestly incompatible with our assumption that there is action; this case no longer implies the general conditions presupposed in the category of action. Only the first case remains.

The dilemma is encoded as it stands, with the second horn read through its stated consequence — there could be only one action — rather than through an invented measure of how much uneasiness remains. That keeps the vocabulary as it was. Two small frames then check the two steps of the argument, one each.

First, the refutation of the second horn. Mises says one action followed by a terminal state is incompatible with "our assumption that there is action". It is not. A frame admitting exactly one action satisfies both halves he calls incompatible. What his step needs is that action is plural — that two distinct actions occur — and the bare claim that there is action does not deliver it. This is the first time the library has put that claim to any work, and it was too weak for the job.

theorem

Apodictic.Model.existence_does_not_refute_second_horn :
  ¬Mises.ExistenceRefutesSecondHorn
Apodictic.Model.existence_does_not_refute_second_horn :
  ¬Mises.ExistenceRefutesSecondHorn

Existence does not refute the second horn. Mises calls one action followed by a terminal state "manifestly incompatible with our assumption that there is action". The frame above satisfies both halves he calls incompatible, so the step is not valid as stated.

What his argument needs is Mises.ActionRecurs — that two distinct actions occur — and nothing in "there is action" delivers it. His own wording gestures past bare existence ("this case no longer implies the general conditions presupposed in the category of action") without saying what those conditions are. Naming them is the suppressed premise of his derivation.

Second, grant him the horn. Let action be plural, so the dilemma is won. The ladder still does not follow. A frame with two actions, a preference that is asymmetric and not empty, and a plan that serves the less urgent want first meets everything the dilemma establishes and breaks the law.

theorem

Apodictic.Model.recurs_does_not_deliver_ladder :
  Mises.ActionRecurs Model.Plural ∧ ¬Mises.LadderHolds Model.pluralPlan
Apodictic.Model.recurs_does_not_deliver_ladder :
  Mises.ActionRecurs Model.Plural ∧
    ¬Mises.LadderHolds Model.pluralPlan

Refuting the second horn does not deliver the ladder. In a frame where action is plural — Mises's dilemma won outright — the ladder fails.

And it fails for a substantive reason, not a degenerate one. Preference here is asymmetric (plural_asymmetric) and non-empty (plural_prefers_nontrivial); what goes wrong is that the agent's plan serves the less urgent end first, so the unit he adds brings in something MORE urgent than what he was already serving. Mises's sentence is false of this agent, and everything the dilemma establishes is true of him.

So the step from "there are intermediate stages" to the law is not valid on its own. What has to be added is that the plan respects the ordering — which is SwapDominant, Rothbard's premise, arriving with Rothbard's circular warrant. In Mises's own text the addition is a single unargued sentence: "It is nothing else than the reverse of the statement that what satisfies more is preferred to what gives smaller satisfaction."

This does not show Mises's derivation is unsalvageable. It shows the dilemma is not the premise, and that whatever is has not been stated by him or by anyone since.

So the dilemma is not the premise. What carries Mises from it to the law is a single sentence, offered as though it added nothing: "It is nothing else than the reverse of the statement that what satisfies more is preferred to what gives smaller satisfaction." That sentence is where his premise lives, and it is unargued.

His premise, reconstructed. The tempting reading of that sentence adds a scale of satisfaction to the vocabulary — a second ordering, on states, by how much uneasiness each removes. That was refused. It would enlarge the ontology on one sentence's authority, it invites cardinal degrees through the back door, and a satisfaction scale would still have to be connected to which want a unit serves, which is the premise all over again. The reading used instead is the most generous one the existing vocabulary allows: the agent serves in order of urgency. If the good can serve a want, and that want is more urgent than one on his plan, the plan has it too. That is a praxeological claim, subjunctive throughout like Rothbard's, and it is the second of the four under The claims.

One thing more is needed, and it is a condition, not a claim: that every pair of wants the good can serve is ranked, one way or the other. Where a pair is not, the theorem is silent. It is the fourth under The conditions, and the one Rothbard's route never asks for.

theorem

Apodictic.Mises.ladder_from_order {praxis : ActionFrame}
  {agent : praxis.Agent} {time : praxis.Time}
  {stock : Stock praxis agent time} (plan : AllocationPlan stock)
  (order : ServedInOrder plan)
  (comparable : stock.ComparableServiceable) : Mises.LadderHolds plan
Apodictic.Mises.ladder_from_order
  {praxis : ActionFrame}
  {agent : praxis.Agent}
  {time : praxis.Time}
  {stock : Stock praxis agent time}
  (plan : AllocationPlan stock)
  (order : ServedInOrder plan)
  (comparable :
    stock.ComparableServiceable) :
  Mises.LadderHolds plan

The ladder, derived the Misesian way.

Neither SwapDominant nor IndependentUses appears. In their place: the agent serves in order of urgency, and the ends the good can serve are comparable. That is a genuinely different premise set for the same conclusion — which is what the second theorem target was for.

The argument is Mises's own, made honest. The added end is serviceable and unserved at the smaller supply. Were it MORE urgent than something already served there, serving in order would have admitted it — so it is not more urgent. Comparability turns "not more urgent" into "less urgent", and that step is where the route pays.

Mises's minimality qualifier is idle here too: least need only be served at the smaller supply, exactly as in ladder_for_every_served. Two different premise sets, the same idle qualifier.

Its manifest, printed by the same command as Rothbard's:

manifest of Apodictic.Mises.ladder_from_order

  praxeological claims:
    order : ServedInOrder plan

  situational conditions:
    comparable : stock.ComparableServiceable

  vocabulary (what the claims are about):
    praxis : ActionFrame
    agent : praxis.Agent
    time : praxis.Time
    stock : Stock praxis agent time
    plan : AllocationPlan stock
    fewer : Finset praxis.Means
    more : Finset praxis.Means

  conditions carried by the vocabulary (not binders: discharged by
  whoever supplies the argument):
    stock.unitsAlike : ∀ unit ∈ stock.units, ∀ (want : praxis.End), praxis.Believes agent time unit want ↔ want ∈ stock.serves
    plan.servesOnlyWhatItCan : ∀ (subStock : Finset praxis.Means), ∀ want ∈ plan.wouldServe subStock, want ∈ stock.serves

  logical background: [propext, Quot.sound]

  (5 trailing binders belong to the conclusion, not the signature)
#manifest Mises.ladder_from_order

manifest of Apodictic.Mises.ladder_from_order

  praxeological claims:
    order : ServedInOrder plan

  situational conditions:
    comparable : stock.ComparableServiceable

  vocabulary (what the claims are about):
    praxis : ActionFrame
    agent : praxis.Agent
    time : praxis.Time
    stock : Stock praxis agent time
    plan : AllocationPlan stock
    fewer : Finset praxis.Means
    more : Finset praxis.Means

  conditions carried by the vocabulary (not binders: discharged by
  whoever supplies the argument):
    stock.unitsAlike : ∀ unit ∈ stock.units, ∀ (want : praxis.End), praxis.Believes agent time unit want ↔ want ∈ stock.serves
    plan.servesOnlyWhatItCan : ∀ (subStock : Finset praxis.Means), ∀ want ∈ plan.wouldServe subStock, want ∈ stock.serves

  logical background: [propext, Quot.sound]

  (5 trailing binders belong to the conclusion, not the signature)

Hold it against the manifest of marginal_utility. Swap dominance is gone, and so is independence of uses; in their place, one claim and one condition, neither of which the Rothbard route carries. The two carried conditions and the logical background are the same. This is what the second target was for: not a verdict on one reconstruction but a trade between two, computed from the signatures rather than argued.

The two premise sets, related. Are the routes independent, then? Not quite, and the relation runs one way. Given Rothbard's premise, independence of uses, and asymmetry of preference, the agent serves in order of urgency. Rothbard's premises entail Mises's bridge. The asymmetry is the third claim under The claims, and this is the theorem that spends it — the first in the library to force any property on preference at all; it is recorded as ours, because no sentence of either author states it.

theorem

Apodictic.Contrast.rothbard_entails_servedInOrder {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)
  (asymmetric : AsymmetricPreference praxis agent time) :
  ServedInOrder plan
Apodictic.Contrast.rothbard_entails_servedInOrder
  {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)
  (asymmetric :
    AsymmetricPreference praxis agent
      time) :
  ServedInOrder plan

Rothbard's premises entail Mises's bridge.

Given swap dominance, independence of uses and asymmetry, the agent serves in order of urgency — which is exactly Mises.ServedInOrder, the premise the Misesian route was built on.

So the two routes are NOT independent. Whatever else is true of Mises's derivation, its premise is available to anyone who already has Rothbard's, and the second route buys no premise the first lacked.

The proof is the contrapositive of served_over_unserved. Suppose the more urgent end were left unserved. Then Rothbard's workhorse says the served end is preferred to it — and asymmetry contradicts the assumption that it was the more urgent of the two. The case split on whether the end is served is decidable, not classical: plan.wouldServe subStock is a Finset, so membership is decidable given [DecidableEq praxis.End], which the route already carries.

The converse fails. A frame can rank wants and serve them in order and still be too coarse to rank bundles, and then serving in order holds where swap dominance does not.

theorem

Apodictic.Model.servedInOrder_not_entail_swapDominant :
  ServedInOrder Model.coarsePlan ∧ ¬SwapDominant Model.coarsePlan
Apodictic.Model.servedInOrder_not_entail_swapDominant :
  ServedInOrder Model.coarsePlan ∧
    ¬SwapDominant Model.coarsePlan

The two premise sets are not equivalent. Rothbard's entails Mises's bridge (Contrast.rothbard_entails_servedInOrder); this frame shows the converse fails. So the Mises route, reconstructed as generously as the vocabulary allows, rests on a STRICTLY WEAKER allocation premise than Rothbard's — while paying for it with comparability of ends, which Rothbard's route never needs.

So on the allocation Mises's premise is strictly the weaker. The premise sets are still incomparable, because his route pays for the weaker premise with comparability of wants, which Rothbard's never needs. Mises asks less of the agent's plan and more of his value scale. And the price is paid in situations: there are agents to whom Rothbard's law applies and Mises's does not. The gap is narrow, and the reason it is narrow is itself a small finding — swap dominance already ranks each served want against each unserved one the good could reach, so the only pairs left unranked are those that never sit on opposite sides of a margin.

theorem

Apodictic.Model.rothbard_applies_where_mises_is_silent :
  SwapDominant Model.marginPlan ∧
    ¬Model.marginStock.ComparableServiceable
Apodictic.Model.rothbard_applies_where_mises_is_silent :
  SwapDominant Model.marginPlan ∧
    ¬Model.marginStock.ComparableServiceable

A situation where Rothbard's law applies and Mises's does not.

Swap dominance holds, so marginal_utility_chain and the Rothbard route apply to this agent in full. ComparableServiceable fails, so Mises.ladder_from_order does not apply at all — its premise is unavailable.

Comparability is a condition, so this is what "Mises's law covers fewer situations" means concretely: an agent with two ends he has never had occasion to rank against each other. Were comparability a claim, praxeology would assert that no such agent exists, and this frame would be a counter-example to the claim rather than a gap in the theorem's reach.

Where this leaves the question. The finding ended on whether praxeology may help itself to a standing plan. Mises's route does not escape that question; it meets it in another form. His premise is as counterfactual as Rothbard's — it says what the agent would serve at every smaller supply — and he restricts value scales exactly as Rothbard does, three chapters earlier: "These scales have no independent existence apart from the actual behavior of individuals" (ch. IV, §2). Where Rothbard exempts the law by name, Mises simply announces that the counterfactual costs nothing: "We do not transcend the sphere of praxeological reasoning in establishing the following definition". Neither warrants the premise. That is as far as this part goes.