apodictic machine-checked praxeology

2.5. swap_dominance: the one praxeological premise🔗

🔗axiom
Apodictic.swap_dominance {agent : World.Agent} {t : World.Time}
  {s : Stock World agent t} (A : AllocationDisposition s)
  (hA : actual_disposition A) (U : Finset World.Means)
  (hU : U ⊆ s.units) (e : World.End) :
  e ∈ A.wouldServe U →
    ∀ e' ∈ s.serves,
      e' ∉ A.wouldServe U →
        World.Prefers agent t (↑(A.wouldServe U))
          (insert e' (↑(A.wouldServe U) \ {e}))
Apodictic.swap_dominance
  {agent : World.Agent} {t : World.Time}
  {s : Stock World agent t}
  (A : AllocationDisposition s)
  (hA : actual_disposition A)
  (U : Finset World.Means)
  (hU : U ⊆ s.units) (e : World.End) :
  e ∈ A.wouldServe U →
    ∀ e' ∈ s.serves,
      e' ∉ A.wouldServe U →
        World.Prefers agent t
          (↑(A.wouldServe U))
          (insert e'
            (↑(A.wouldServe U) \ {e}))

Swap dominance — subjunctive preference over allocations, in one-swap form, for the agent's actual disposition. With any sub-stock U of the units on hand, the bundle the agent would serve is preferred to the bundle obtained by withdrawing one served end e and serving in its place a serviceable end e' that was not served.

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 is our-reconstruction. The preference asserted is subjunctive — what the agent WOULD serve — which Rothbard's demonstrated-preference doctrine says "makes no sense apart from an actual choice made" (Nozick 1977, p. 370, thesis 3), and which Nozick argues the Austrians need anyway (pp. 373–374). This axiom is where that collision lives.

Does not say: (1) anything about actual action — the bridge from action to preference is not in the base; (2) anything about alternatives differing by more than one swap; (3) anything about independence of uses, which is the hypothesis IndependentUses of the theorems; (4) anything about units not on hand (U ⊆ s.units), which is all the disposition is data for; (5) anything about interchangeability of units — that two sub-stocks of the same size would serve the same ends is the hypothesis Homogeneous, not part of this axiom.

Rothbard's argument on pp. 24–27 is one step from a premise he asserts. The premise: "action uses scarce means to satisfy the most urgent of the not yet satisfied wants" (p. 24), offered as a "universal fact" that "follows from" action, with no derivation shown. The step: on losing one unit, "he gives up the least urgent of the wants which the larger stock would have satisfied" (p. 25), introduced with "Obviously" and backed by the reallocation argument on p. 27. Our first encoding asserted the conclusion of that step as the axiom, and the human noticed that the famous law then followed in one line. The one-line proof was in fact faithful to Rothbard; the audit point was upstream, in what the premise had compressed. Cutting it finer gave this axiom plus two hypotheses, and the urgency principle became a theorem.

What it does not say is listed in its docstring. The first item matters most and is taken up in the last section: it says nothing about actual action. The second is that the general form, "preferred to every same-size bundle", was tried and is not needed; the weaker one-swap axiom is also the more faithful, since Rothbard's p. 27 argument is a one-unit reallocation. Independence of uses is a hypothesis, below. And the supply bound: the axiom this one replaced claimed every supply level, which is more than the tradition's argument delivers.

2.5.1. What Nozick actually says🔗

Nozick's 1977 paper is this project's adversarial reader, and until 2026-09-04 the notes and docstrings called this axiom "Nozick's target". Having read §III of the paper, that was inverted.

Nozick lists three Austrian theses about preference and action (p. 370). First, doing A shows A was preferred to every alternative believed available. Second, no evidence can establish a preference against a choice. Third, "the notion of preference makes no sense apart from an actual choice made". He argues the first fails because of indifference: doing A shows willingness to do A, not unwillingness to do B. And he argues the third fails by the Austrians' own lights, because cost is the value of the best rejected alternative, which requires ranking among alternatives none of which was chosen. His positive account is subjunctive: "to say a person prefers A to B at a time is to say he would choose A over B if he were given a choice between (only) A and B at that time" (p. 373). "'Prefers A to B' is like 'soluble'; 'chooses A over B' is like 'dissolves'" (p. 374).

swap_dominance is subjunctive preference in exactly Nozick's sense. What the agent would serve at each supply, preferred to what he would serve after a swap. So the axiom is Nozick-shaped, and what it collides with is Rothbard's third thesis. The receipt above then says something sharper than the notes had claimed: Rothbard's derivation of marginal utility uses, at its only load-bearing step, the notion his demonstrated-preference doctrine forbids. That is Nozick's cost argument replayed on marginal utility, and machine-checked.

Two smaller alignments. Nozick allows subjunctives to be undetermined (p. 373), which is the reason actual_disposition asserts no existence. And he holds that irreflexivity and asymmetry "seem to be part of the notion of preference" (p. 377), while transitivity is a violable rationality condition. Asymmetry is the one property we intend to add; transitivity has not been needed.