apodictic machine-checked praxeology

1.5. The conditions🔗

The theorems take three assumptions besides the claim. Each says something about the situation rather than about action as such, and each is written into the statement, so a reader can point at it and say: that is the one that did not hold. Where one fails, the law says nothing — it is silent, not wrong.

  • stock.OneMore fewer more: the two piles compared are both on hand and differ by exactly one unit. The plan says nothing about piles the man does not hold, and neither does the law.

  • IndependentUses agent time: what one want is worth does not depend on which other wants are being served.

  • plan.Homogeneous: the plan depends only on how many units there are, not on which ones. Only the size-based form of the law needs it.

Nothing here has to say which plan is the man's. A theorem is handed a plan and makes its claim about that one, so there is no rival plan anyone could build to refute it.

All three are given in full here, in the order they are listed above, because these are the assumptions a reader has to judge.

🔗def
Apodictic.Stock.OneMore {praxis : ActionFrame} {agent : praxis.Agent} {time : praxis.Time} (stock : Stock praxis agent time) (fewer more : Finset praxis.Means) : Prop
Apodictic.Stock.OneMore {praxis : ActionFrame} {agent : praxis.Agent} {time : praxis.Time} (stock : Stock praxis agent time) (fewer more : Finset praxis.Means) : Prop

more is fewer plus one unit, both inside the stock. It is said with an inclusion and a count rather than by naming the extra unit, so that sub-stocks are only ever supposed and never constructed — which is why nothing here needs to decide when two units are the same unit.

🔗def
Apodictic.ActionFrame.IndependentUses (praxis : ActionFrame) (agent : praxis.Agent) (time : praxis.Time) : Prop
Apodictic.ActionFrame.IndependentUses (praxis : ActionFrame) (agent : praxis.Agent) (time : praxis.Time) : Prop

Independence of uses — a condition on the situation, NOT a universal claim. If two bundles differ in exactly one slot, then preferring one bundle to the other carries down to preferring the one end to the other. It fails where uses are complementary: where B is worth having only alongside A. It is named here so that the theorems that need it carry it as a hypothesis, and so a reader can point at it where it does not hold.

This is NOT a premise Rothbard spends. He ranks wants against each other directly, off a scale that is already ranked (MES pp. 25–26, Figure 3), and never argues from bundles at all. It is what OUR decomposition costs. Where he makes one fused claim, we make a claim about bundles plus this condition — and complementarity, which his wording never has to face, lands here once the pieces are pulled apart. To assert this rather than hypothesize it would be to assert that complementarity never happens.

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

Interchangeability of units — a condition on the situation, NOT a praxeological claim. The plan depends only on how many units there are, not on which ones: any two sub-stocks of the same size would serve the same ends.

Without it, the phrase "the plan at n units" — and so the marginal utility of a supply of n — picks out nothing in particular. Rothbard makes interchangeability part of what a supply IS: "If a specific unit is differently evaluated from all other units, then the supply of that good is only one unit" (MES p. 23). Where it fails, the units are not one good, and the supply-size form of the law does not treat them as one. Like the plan it constrains, it speaks of sub-stocks the agent may not hold.