1.10. The ladder as a history🔗

Both routes read the ladder at one moment. The man holds six horses, and the law holds them up against the five he might have held. There is another way to read it, and Rothbard tells it that way himself: "suppose that the isolated individual successively finds one horse, then a second, then a third" (p. 24). Mises's ladder runs in the same direction, from n–1 units to n. Read like that, the law is not about a plan at all. It is about two things the man actually did: what he served when he held n–1 units, and what he serves once he holds n. No stock he does not hold comes into it, and nothing answers in advance for every stable he might cut from his own.

The library carries this reading in a module of its own, which imports the claims and neither route's theorems. Its objects are two actual allocations, the wants he served with the stock he held at each moment, and a supply that grew from one moment to the other by one unit. Both definitions are under The vocabulary.

What it spends in place of a plan is the fourth claim under The claims, ActsInOrder, and the only claim in the library that runs from what a man ranks to what a man actually does: in what he serves with the stock he holds, he never passes over a want he prefers, and believes the good can serve, for one he ranks lower.

The question the reading forces. Rothbard goes on: "When the second horse is found, he will be put to work satisfying the most urgent of the wants remaining. These wants, however, must be ranked lower than the wants that the previous horse has satisfied." Ranked lower on which scale? The man ranks at every moment he acts. He ranked when he held one horse, and he ranks again when he holds two. The sentence does not say which ranking it means, and neither does Mises's. A proof assistant will not let that go unsaid, so the ladder takes the moment whose scale does the ranking as an argument:

Apodictic.Temporal.Ladder {praxis : ActionFrame} {agent : praxis.Agent}
  {earlierTime laterTime : praxis.Time}
  {earlier : Stock praxis agent earlierTime}
  {later : Stock praxis agent laterTime} (before : Allocation earlier)
  (after : Allocation later) (judged : praxis.Time) : Prop
Apodictic.Temporal.Ladder
  {praxis : ActionFrame}
  {agent : praxis.Agent}
  {earlierTime laterTime : praxis.Time}
  {earlier :
    Stock praxis agent earlierTime}
  {later : Stock praxis agent laterTime}
  (before : Allocation earlier)
  (after : Allocation later)
  (judged : praxis.Time) : Prop

The two answers come apart.

Judged on the earlier scale, the ladder is a theorem — and a short one. Read it as acting in order restated about a want the next horse happens to serve, not as a route to the law; the manifest below is where that shows.

Apodictic.Temporal.ladder_judged_earlier {praxis : ActionFrame}
  {agent : praxis.Agent} {earlierTime laterTime : praxis.Time}
  {earlier : Stock praxis agent earlierTime}
  {later : Stock praxis agent laterTime} (before : Allocation earlier)
  (after : Allocation later) (order : ActsInOrder before)
  (comparable : earlier.ComparableServiceable)
  (noNewUses : earlier.NoNewUses later) :
  Temporal.Ladder before after earlierTime
Apodictic.Temporal.ladder_judged_earlier
  {praxis : ActionFrame}
  {agent : praxis.Agent}
  {earlierTime laterTime : praxis.Time}
  {earlier :
    Stock praxis agent earlierTime}
  {later : Stock praxis agent laterTime}
  (before : Allocation earlier)
  (after : Allocation later)
  (order : ActsInOrder before)
  (comparable :
    earlier.ComparableServiceable)
  (noNewUses : earlier.NoNewUses later) :
  Temporal.Ladder before after earlierTime

manifest of Apodictic.Temporal.ladder_judged_earlier

  praxeological claims:
    order : ActsInOrder before

  situational conditions:
    comparable : earlier.ComparableServiceable
    noNewUses : earlier.NoNewUses later

  vocabulary (what the claims are about):
    praxis : ActionFrame
    agent : praxis.Agent
    earlierTime : praxis.Time
    laterTime : praxis.Time
    earlier : Stock praxis agent earlierTime
    later : Stock praxis agent laterTime
    before : Allocation earlier
    after : Allocation later
    least : praxis.End

  conditions carried by the vocabulary (not binders: discharged by
  whoever supplies the argument):
    earlier.unitsAlike : ∀ unit ∈ earlier.units, ∀ (want : praxis.End), praxis.Believes agent earlierTime unit want ↔ want ∈ earlier.serves
    later.unitsAlike : ∀ unit ∈ later.units, ∀ (want : praxis.End), praxis.Believes agent laterTime unit want ↔ want ∈ later.serves
    before.servesOnlyWhatItCan : ∀ want ∈ before.served, want ∈ earlier.serves
    after.servesOnlyWhatItCan : ∀ want ∈ after.served, want ∈ later.serves

  logical background: [propext, Quot.sound]

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

Read what is not on it. The supply growing is not a hypothesis: added as one, the linter refuses it as unused. Nothing about the later scale appears, nothing about how the later allocation was chosen, and nothing about which moment came first. One condition does span the two moments. NoNewUses says that whatever the good is believed to serve later, it was believed to serve earlier. He may stop believing in a use; he may not start. What the plan held fixed has moved from the scale to belief about the good. Without it the new horse's want need not have been on the earlier scale, and nothing could be said of it there. It is under The conditions with the rest.

That makes it a short theorem, and it should be read as one. What it says is about the earlier act: whatever he passed over then ranked below whatever he served then. The want the second horse later goes to is simply one of the wants he passed over. The increment is narration. On this reading the ladder is acting in order, restated about a want the next horse happens to serve.

Judged on the later scale, it does not follow. Grant everything a premise about one moment can give, at both moments: he acts in order, the good's wants are comparable, preference is asymmetric. Grant across them that the supply grew by one and that the good is believed to serve the same wants. Then ask for the ladder on the later scale:

Apodictic.Temporal.LadderJudgedLaterFromOrder : Prop
Apodictic.Temporal.LadderJudgedLaterFromOrder :
  Prop

Apodictic.Model.later_judged_ladder_fails :
  ¬Temporal.LadderJudgedLaterFromOrder
Apodictic.Model.later_judged_ladder_fails :
  ¬Temporal.LadderJudgedLaterFromOrder

The frame that refutes it is small. Two moments, two wants, one horse and then two. With one horse he serves the want most urgent then. With two he serves both, and by then the other want has become the more urgent. Each act is in order on its own scale. But on the later scale the want the second horse went to outranks the want the first horse served, and the ladder, judged there, fails.

What would close the gap, and why it is not assumed. A relation between the man's scales at the two moments: that the later ranks what the earlier ranked, the same way. Both authors deny it. Mises: "value judgments are not immutable" (Human Action, ch. V, §4). Rothbard's own actor, a few pages before the horses, changes his mind between moments, and "the ranking on his preference scale shifts to this order" (p. 18). So the history reading does not assume constancy, as a claim or as a condition. Where the reading would need it, the frame above shows what goes missing. Rothbard, for his part, would not judge on the earlier scale at all: when his man must give up one of six horses, "he deals only with his presently available stock", in "disregard of past events" (p. 27). Judged that way, the ladder is the one-moment law at the later time — which is the plan again, and the circle with it.

They deny more than that, and it bears on the claim this reading does spend. Both hold that a scale of value exists only as it is read off what a man does, so a scale and the act it was read from cannot disagree. The passages are quoted in ActsInOrder's docstring under The claims. The library keeps the ranking apart from the act, so that the claim can say something an act could contradict, and that is why its status is our reconstruction and not theirs.

The trade. The counterfactual routes need a plan that no act exhibits. The history needs a scale that no act can show to have stayed put — or, on the reading that is a theorem, a man who learned no new use for the good between the two acts. Neither author addresses that condition: nothing in the texts grants it, and nothing refuses it. So the two routes pay in different coin. The counterfactual routes rest on something their authors refuse; the history route rests on something they never examined. Reading the ladder as a history moves the cost; it does not remove it.

What a failure would point at. Where the ladder read as a history fails of a real case, its manifest says where to look, and it names three places: the man did not act in order (ActsInOrder); he learned a new use for the good between the moments (NoNewUses); or two of the good's wants were never ranked against each other (comparability). A scale that moved is not on the list, because no theorem on this reading assumes it stayed put. That is what the reading pays in.