1.6. The theorems🔗

Rothbard's urgency principle says that losing a unit costs you the least urgent want. Here that is proved rather than assumed. The claim turns out to give more than the principle needs, so the stronger statement comes first and the principle follows from it.

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 (see the module docstring above).

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.

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 claim is asserted of one plan, not of every plan of its shape. 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 :
    ∀ (X Y : Set praxis.End),
      praxis.Prefers agent time X Y → ¬praxis.Prefers agent time Y X)
  (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 :
    ∀ (X Y : Set praxis.End),
      praxis.Prefers agent time X Y →
        ¬praxis.Prefers agent time Y X)
  (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 rides along as a hypothesis because Prefers has no properties assumed of it.

The law is stated using Rothbard's own definition of the marginal utility of a supply: the ends you would give up on losing one unit. It comes in two forms. Follow a chain of named units, and no interchangeability is needed. State it Rothbard's way, by the size of the supply, and it is.

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 (see the module docstring). 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.

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.

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.