apodictic machine-checked praxeology

1.2. Axioms๐Ÿ”—

Every axiom carries three fields. 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 formalization decision the tradition never faced). Does not say lists the nearby stronger claims the axiom deliberately omits.

Two rules govern the list. An axiom enters at the point of first use, so nothing is here that no theorem cites. And only claimed-universal facts about action are axioms; conditions under which a law applies are hypotheses of the theorem, below.

๐Ÿ”—axiom
Apodictic.World : ActionFrame
Apodictic.World : ActionFrame

The world of human action โ€” the frame the praxeological axioms speak of. Opaque by design: nothing over World is constructible, so an axiom about its actions and dispositions cannot be refuted by a cooked-up instance. Every action, stock, or disposition over it is either supplied by an axiom or hypothesized in a theorem statement.

Source: tacit โ€” Mises's theory is about actual purposeful behavior, action as such, not about a class of models (Human Action, chs. 1โ€“2 passim).

Status: our-reconstruction. The distinguished-frame architecture is a formalization decision, not a doctrine of the tradition. It was chosen because it is the only arrangement under which #print axioms keeps reporting the commitments; the Misesian reading is a consequence one may accept, not the reason.

Does not say: that any action exists in World. Existence is a separate claim, not in the base.

๐Ÿ”—axiom
Apodictic.ends_distinguishable : DecidableEq World.End
Apodictic.ends_distinguishable :
  DecidableEq World.End

Ends are distinguishable: identity of ends is decidable โ€” of any two ends it is settled whether they are the same end.

Source: tacit. The reallocation argument (MES p. 27) withdraws one unit and asks which want is thereby given up; "the bundle minus this end" presupposes that each end either is or is not the one withdrawn. Mises's actor chooses between alternatives he tells apart; nothing in the tradition contemplates ends whose identity is undecided.

Status: suppressed-premise. A data axiom, like World. It is what makes "the bundle minus e" constructible; without it that step is available only classically, and the library keeps Classical.choice off the receipt so that every case split is either named praxeological content or absent.

Does not say: anything about preference. It is identity of ends, not indifference between them.

๐Ÿ”—axiom
Apodictic.actual_disposition {agent : World.Agent} {t : World.Time}
  {s : Stock World agent t} : AllocationDisposition s โ†’ Prop
Apodictic.actual_disposition
  {agent : World.Agent} {t : World.Time}
  {s : Stock World agent t} :
  AllocationDisposition s โ†’ Prop

The agent's actual disposition โ€” which allocation plan is the one the agent would follow. AllocationDisposition s is a type, inhabited by every function from sub-stock to served ends that meets the bookkeeping conditions; this predicate names the agent's own plan, so that an axiom can be restricted to it instead of speaking of every conceivable plan.

Source: tacit. Rothbard's argument presupposes ONE value scale and ONE allocation per actor ("the" marginal unit, "the" least urgent want, MES pp. 24โ€“27); the tradition never contemplates rival plans for the same actor because it never quantifies over plans.

Status: our-reconstruction. Opaque, Prop-valued, on the receipt. It asserts a fact of the matter about WHICH plan is the agent's.

Does not say: that such a plan exists for every stock, or that it is unique. On Nozick's subjunctive account of preference the subjunctive may be undetermined (1977, p. 373), so whether a complete counterfactual table exists is left open. Theorems about dispositions take actual_disposition A as a hypothesis.

๐Ÿ”—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.