1.6. The theorems🔗

The derivation is three steps, and only the first does any work.

Start with the six horses. The man serves ends 1–6; ends 7–10 remain unsatisfied. The claim says: take that bundle, swap any served end for any unserved end a horse could have served, and he prefers what he would have had to what the swap leaves him. So {1,2,3,4,5,6} beats {1,2,3,4,5,7}. It also beats {1,2,3,4,5,8}, and it beats {2,3,4,5,6,7} if end 1 is the one swapped out. Any single swap loses.

That is a claim about bundles. The law is a claim about single ends: that pleasure riding is less urgent than leading a wagon. To pass from one to the other you need that a preference between two bundles differing in exactly one place is a preference between those two ends. That step is independence of uses, and it is ours rather than Rothbard's: he ranks ends against each other directly, off a scale already ranked (Figure 3, pp. 25–26), and the passages quoted above never compare bundles at all. We need the step because we make a claim about bundles where he makes one fused claim — and where uses are complementary the step fails, and the law is silent.

Take it, and every end he would serve with a given string of horses is preferred to every end he would leave unserved. That is already more than Rothbard claims. It does not care whether the unserved end is the one the next horse would have reached: end 6 beats end 7, and it beats end 10 just as squarely.

theorem

Apodictic.served_over_unserved {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)
  (subStock : Finset praxis.Means) (onHand : subStock ⊆ stock.units)
  (served : praxis.End) :
  served ∈ plan.wouldServe subStock →
    ∀ unserved ∈ stock.serves,
      unserved ∉ plan.wouldServe subStock →
        praxis.PrefersEnd agent time served unserved
Apodictic.served_over_unserved
  {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)
  (subStock : Finset praxis.Means)
  (onHand : subStock ⊆ stock.units)
  (served : praxis.End) :
  served ∈ plan.wouldServe subStock →
    ∀ unserved ∈ stock.serves,
      unserved ∉
          plan.wouldServe subStock →
        praxis.PrefersEnd agent time
          served unserved

Served over unserved — the workhorse. Take any sub-stock on hand. Every end the agent would serve with it is preferred to every end the good could serve but he would leave unserved.

This is everything SwapDominant gives, and it is more than Rothbard claims: it sets a served end against ANY unserved end the good could serve, not only against the one the next unit would reach. It needs the hypothesis that uses are independent, which is what carries a preference between two bundles down to a preference between two ends.

How the proof goes: swap the served want for the unserved one, and the plan beats the result. The served bundle is that one want together with the rest (insert_sdiff_self_of_mem), so the two bundles differ in exactly one place — and independence reads the preference between those two wants off that.

Urgency is that ranking, restricted to the end he loses. Take a horse away, and the end he gives up is one he would have served with six and does not serve with five — an unserved end at the smaller stock. Served-over-unserved has already ranked it below everything still served. Rothbard's horse sentence, quoted at the start, says exactly that and nothing more. That the larger stock is exactly one horse larger does no work beyond naming which end is the lost one.

theorem

Apodictic.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 : praxis.End) :
  kept ∈ plan.wouldServe fewer →
    ∀ lost ∈ plan.wouldServe more,
      lost ∉ plan.wouldServe fewer →
        praxis.PrefersEnd agent time kept lost
Apodictic.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 : praxis.End) :
  kept ∈ plan.wouldServe fewer →
    ∀ lost ∈ plan.wouldServe more,
      lost ∉ plan.wouldServe fewer →
        praxis.PrefersEnd agent time kept
          lost

The urgency principle (Rothbard), stated as a loss. Suppose the agent had more units and drops to fewer, one unit fewer. Every end he would still serve at fewer is preferred to every end he has to abandon on the way down: the loss falls on the least urgent want.

One application of served_over_unserved. An abandoned end is one the good can serve and the plan does not serve at fewer — and beyond supplying that much, the fact that more is exactly one unit larger does no work here.

The law is urgency again, said of the ends a unit adds — the ends served with the larger stock and not with the smaller, which is Rothbard's own definition of the marginal utility of a supply.

def

Apodictic.marginalEnds {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.marginalEnds
  {praxis : ActionFrame}
  {agent : praxis.Agent}
  {time : praxis.Time}
  {stock : Stock praxis agent time}
  (plan : AllocationPlan stock)
  (fewer more : Finset praxis.Means) :
  Set praxis.End

Marginal utility of a one-unit step, from fewer to more, in Rothbard's own sense: the ends the extra unit adds, which are the same ends that would be given up if it were lost. "The marginal utility of the supply is the end that must be given up as the result of a loss of the unit" (MES p. 27); "he gives up the least urgent of the wants which the larger stock would have satisfied" (p. 25).

A set of ends rather than a single end, because nothing here assumes that exactly one end drops: determinacy of the drop is not among the law's premises. It is a Set rather than a Finset for a mechanical reason: subtracting one Finset from another requires being able to decide when two ends are the same end, which an arbitrary frame does not give us — and reaching for Classical would put Classical.choice on the manifest for no praxeological reason at all.

A definition, not a claim — Rothbard introduces it as one ("is called", "is known as"). What licenses calling this the utility of the unit is imputation of value from ends back to means: "actors value means strictly in accordance with their valuation of the ends that they believe the means can serve" (p. 19).

Indexed by the step rather than by a size, because which ends a unit adds can depend on which units are already on hand — unless the plan is Homogeneous.

Along a chain of named horses, apply it at the second step: what the sixth horse adds is less urgent than what the fifth added, because what the fifth added is still being served when he has five, and what the sixth adds is not. That the first step is a one-horse step is not used. Interchangeability is not used either, because the chain names which horses.

theorem

Apodictic.marginal_utility_chain {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)
  (small medium large : Finset praxis.Means)
  (_firstStep : stock.OneMore small medium)
  (secondStep : stock.OneMore medium large) (addedFirst : praxis.End) :
  addedFirst ∈ marginalEnds plan small medium →
    ∀ addedSecond ∈ marginalEnds plan medium large,
      praxis.PrefersEnd agent time addedFirst addedSecond
Apodictic.marginal_utility_chain
  {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)
  (small medium large :
    Finset praxis.Means)
  (_firstStep :
    stock.OneMore small medium)
  (secondStep :
    stock.OneMore medium large)
  (addedFirst : praxis.End) :
  addedFirst ∈
      marginalEnds plan small medium →
    ∀
      addedSecond ∈
        marginalEnds plan medium large,
      praxis.PrefersEnd agent time
        addedFirst addedSecond

The law of marginal utility, along a chain of named units. Take three sub-stocks, small inside medium inside large, each one unit more than the last. Every end the first step adds is preferred to every end the second step adds.

No interchangeability of units is needed, because the chain names which units are involved. One application of urgency_principle.

Two things go unused, and the statement records both. _firstStep is listed and does no work at all: the underscore is how that is written down, and it is a finding — the chain form does not need the first step to be a step. And within the hypothesis that an end is marginal at the first step, only half is used; the unused half is destructured as _notNeeded inside the proof, which is a name in the proof and not a binder in the statement. The linter that keeps this list honest sees neither case: it is silenced by the underscore, and it works a whole binder at a time.

Said by the size of the supply, the two steps need not share a horse. "The plan at five" and "the plan at six" are one thing each only if any five horses get the same ends. Interchangeability is used exactly once, to say that. After it the argument is urgency over again.

theorem

Apodictic.marginal_utility {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)
  (interchangeable : plan.Homogeneous)
  (belowSmaller smaller belowLarger larger : Finset praxis.Means)
  (stepToSmaller : stock.OneMore belowSmaller smaller)
  (stepToLarger : stock.OneMore belowLarger larger) (n : ℕ)
  (smallerSize : smaller.card = n) (largerSize : larger.card = n + 1)
  (atSmaller : praxis.End) :
  atSmaller ∈ marginalEnds plan belowSmaller smaller →
    ∀ atLarger ∈ marginalEnds plan belowLarger larger,
      praxis.PrefersEnd agent time atSmaller atLarger
Apodictic.marginal_utility
  {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)
  (interchangeable : plan.Homogeneous)
  (belowSmaller smaller belowLarger
    larger : Finset praxis.Means)
  (stepToSmaller :
    stock.OneMore belowSmaller smaller)
  (stepToLarger :
    stock.OneMore belowLarger larger)
  (n : ℕ) (smallerSize : smaller.card = n)
  (largerSize : larger.card = n + 1)
  (atSmaller : praxis.End) :
  atSmaller ∈
      marginalEnds plan belowSmaller
        smaller →
    ∀
      atLarger ∈
        marginalEnds plan belowLarger
          larger,
      praxis.PrefersEnd agent time
        atSmaller atLarger

The law of marginal utility (Rothbard, MES, ch. 1, p. 27): "The greater the supply of a good, the lower the marginal utility; the smaller the supply, the higher the marginal utility."

This is the version stated by supply SIZE. Every end that is marginal at a supply of n units is preferred to every end marginal at a supply of n + 1 — and that holds for ANY two one-unit steps reaching those sizes, which need not have a single unit in common.

plan.Homogeneous is needed exactly once: to say that the plan at the n units below the second step is the same as the plan at the n units of the first. Without it the two steps could not be compared at all.

Here too only half of the marginality hypothesis is used — the unused half is destructured as _notNeeded in the proof, a proof-local name and not a binder in the statement. Every binder this theorem lists is used.

One result here is not a step in the derivation. The claim is made about a single plan rather than about every plan shaped like it. What that gives up — that the man's scale is the only one of its kind — comes back as a theorem, and it is shown here because the rest of the document leans on it.

theorem

Apodictic.no_rival_swap_dominant {praxis : ActionFrame}
  [DecidableEq praxis.End] {agent : praxis.Agent} {time : praxis.Time}
  {stock : Stock praxis agent time}
  (asymmetry : AsymmetricPreference praxis agent time)
  (plan rival : AllocationPlan stock) (dominance : SwapDominant plan)
  (rivalDominance : SwapDominant rival) (subStock : Finset praxis.Means)
  (onHand : subStock ⊆ stock.units) (served unserved : praxis.End)
  (hserved : served ∈ plan.wouldServe subStock)
  (hservedPossible : served ∈ stock.serves)
  (hunservedPossible : unserved ∈ stock.serves)
  (hunserved : unserved ∉ plan.wouldServe subStock)
  (hswap :
    ↑(rival.wouldServe subStock) =
      insert unserved (↑(plan.wouldServe subStock) \ {served})) :
  False
Apodictic.no_rival_swap_dominant
  {praxis : ActionFrame}
  [DecidableEq praxis.End]
  {agent : praxis.Agent}
  {time : praxis.Time}
  {stock : Stock praxis agent time}
  (asymmetry :
    AsymmetricPreference praxis agent
      time)
  (plan rival : AllocationPlan stock)
  (dominance : SwapDominant plan)
  (rivalDominance : SwapDominant rival)
  (subStock : Finset praxis.Means)
  (onHand : subStock ⊆ stock.units)
  (served unserved : praxis.End)
  (hserved :
    served ∈ plan.wouldServe subStock)
  (hservedPossible :
    served ∈ stock.serves)
  (hunservedPossible :
    unserved ∈ stock.serves)
  (hunserved :
    unserved ∉ plan.wouldServe subStock)
  (hswap :
    ↑(rival.wouldServe subStock) =
      insert unserved
        (↑(plan.wouldServe subStock) \
          {served})) :
  False

No rival plan, one swap away. If preference is asymmetric, then two plans over the same stock cannot both be swap-dominant while differing by a single swap at some sub-stock.

This is what Rothbard means by "the" value scale, and here it is derived rather than presupposed. He writes as though the actor's ranking were simply given — "the" marginal unit, "the" least urgent want (MES pp. 24–27) — and never argues that there is only one. Swap dominance plus asymmetry delivers it. Asymmetry is the praxeological claim AsymmetricPreference, spent here and by Apodictic.Contrast.rothbard_entails_servedInOrder; Prefers has no properties assumed of it otherwise.