1.4. The one claim🔗

The library contains no axiom. Every praxeological claim is written as a structure, and a theorem that needs one takes it as a named assumption. So to see what a theorem rests on, you read its statement.

A linter keeps that list honest. #lint only unusedArguments breaks the build if an assumption is listed but the proof never uses it, so little can be listed for show. Little, and not nothing: the linter can be switched off, which makes keeping it on a promise rather than something the machine guarantees, and it has two further limits that let an idle hypothesis through. All three are set out with the manifest below, and one of them turns up a finding. It is never switched off here.

Each claim records three things. Source is a citation, or "tacit". Status is one of three verdicts: explicit-in-tradition (Rothbard or Mises say it), suppressed-premise (they use it without saying it), or our-reconstruction (a decision the tradition never faced). Does not say lists the stronger nearby claims it deliberately avoids.

Two rules govern the list. A claim is added only when some theorem first needs it, so every claim here is one that some theorem actually uses. And only claims meant to hold always belong here; a condition that says when a law applies is a hypothesis instead, and those have a part of their own below.

There is exactly one.

structure

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

Swap dominance — the agent's plan beats every one-swap alternative to it.

Take any sub-stock of the units on hand, and the ends the agent would serve with it. Now make one swap: drop a served end, and put in its place an unserved one that the good could have served but the plan left out. The claim is that the agent prefers the bundle he would have served to the swapped bundle.

It is asserted of one given plan, and it is subjunctive throughout — it speaks of sub-stocks the agent may not hold and swaps he does not make.

Source: Rothbard, MES, ch. 1, §5.B, pp. 24–27 (Mises Institute ed.): "action uses scarce means to satisfy the most urgent of the not yet satisfied wants" (p. 24); the counterfactual framing is Rothbard's own ("suppose ... faced with the necessity of giving up one horse"; "he gives up the least urgent of the wants which the larger stock would have satisfied", p. 25), backed by the reallocation argument (p. 27: "follows from the defined interchangeability of units and from disregard of past events"). Mises, Human Action, ch. VII.1.

Status: explicit-in-tradition as doctrine; the one-swap form, and the pulling apart of the two halves below, are our-reconstruction. Rothbard's premise fuses two claims in one sentence: that ACTION employs the means, and that the wants served are "the most urgent of the not yet satisfied wants" (MES p. 24). This claim keeps the ordering half and states it subjunctively, over what the agent WOULD serve. The subjunctive is Rothbard's own — his derivation compares a stock of six with a stock of five and asks which want "the larger stock would have satisfied" (p. 25), a comparison no single actual allocation delivers. The action half is dropped rather than answered: nothing here bridges an act to a preference.

A tension remains, and it is Rothbard's own. It is not that this claim reaches stocks the agent does not hold; that reach is his (see Anything about units not on hand, below). It is that the claim attributes a STANDING disposition. The plan is one object, at one time, assigning served ends to every sub-stock at once — a value scale formulated in advance of the choices it covers. That is the thing Rothbard says is not needed. He holds that praxeology "may deal with utilities only as deduced from the concrete actions of human beings" (MES p. 882 n. 8), and inside this very chapter he writes, in words he introduces with "It must be reiterated", that "value scales do not exist in a void apart from the concrete choices of action", adding that "there is no need for him to formulate hypothetical value scales" (MES p. 33). His actor needs no scale in advance: it is revealed choice by concrete choice as he goes. This claim gives him one up front.

Yet it is on that same page that he exempts this law from the restriction, in a subordinate clause and without argument: choices cannot be predicted "except that they will follow the law of marginal utility, which was deduced from the axiom of action". So the one thing that may be said in advance about the choices is that they follow the law — which is what licenses attributing the standing plan this claim is asserted of, and that plan is the premise the law is derived from. The warrant for the premise is the conclusion.

The circle is in the WARRANT, not in the proof. Nothing in the Lean is circular: marginal_utility derives the law from this claim, and this claim is asserted, never proved. What is circular is Rothbard's licence for asserting it.

Asserted of ONE plan, not of every plan of that shape — and that is not a hedge. Given one plan, a rival can always be defined, so a claim about all of them could be refuted just by building one. Asserted of the single plan a theorem is handed, there is no such rival to build. Whether a rival one swap away could also be swap-dominant then becomes a theorem (no_rival_swap_dominant, Apodictic.Urgency) instead of a premise.

Does not say:

Anything about actual action. The bridge from action to preference appears nowhere in the library.
Anything about alternatives that differ by more than one swap.
Anything about independence of uses — that is the theorems' hypothesis IndependentUses.
Anything about units not on hand (subStock ⊆ stock.units), which is all the plan speaks about. The reach over stocks the agent does not hold is Rothbard's own, in both directions. He builds the law upward over stocks the actor lacks — the second unit, then the third "added to a stock of two units" (MES pp. 23–24) — and downward, six horses to five (p. 25). Holding none of a good is no obstacle either: "If the actor has no units of some goods in his possession, this does not affect the principle" (p. 32). The hypothetical scales he refuses on the next page are a different thing: scales for a wholly different multi-good endowment, (3X, 4Y, 2Z) against (6X, 8Y, 5Z), where what he permits inside the actual stock is "adding and subtracting" units of it (p. 33). That line is anchored to the stock the agent has, not drawn at some distance from it, and it is closed under the single-unit steps he iterates himself — first horse, then second, then third. Taken downward from a stock, those steps reach every sub-stock of it. So quantifying over all of subStock ⊆ stock.units is that region exactly, and not a reach beyond his text.
Where this claim does depart from him is in INDEXING, not in reach: it speaks of arbitrary sub-stocks where he speaks of sizes. The gap between the two is interchangeability, which he assumes throughout and this claim does not: it is the hypothesis Homogeneous. Stated without that assumption, the claim distinguishes cases he never had to tell apart.
Anything about interchangeability of units. That two sub-stocks of the same size would serve the same ends is the hypothesis Homogeneous, and no part of this claim.
That such a plan exists, or that it is unique without further properties of Prefers.

Constructor

Apodictic.SwapDominant.mk

Fields

swap : ∀ subStock ⊆ stock.units,
  ∀ served ∈ plan.wouldServe subStock,
    ∀ unserved ∈ stock.serves,
      unserved ∉ plan.wouldServe subStock →
        praxis.Prefers agent time (↑(plan.wouldServe subStock))
          (insert unserved (↑(plan.wouldServe subStock) \ {served}))

The one-swap dominance itself.