1.1. Vocabulary🔗

The primitive vocabulary is a bare structure. Nothing in it has any property: no transitivity, no totality, no order on time. Strength is added only when a theorem forces it, and so far none has.

structure

Apodictic.ActionFrame : Type 1
Apodictic.ActionFrame : Type 1

The primitive vocabulary of the action framework: bare types and bare relations. Nothing here has any structural property — no transitivity, no totality, no order on Time. Strength is added only when a theorem forces it, and each forcing is a finding.

Constructor

Apodictic.ActionFrame.mk

Fields

Agent : Type

Acting persons.

End : Type

Ends: states of affairs an agent may value.

Means : Type

Means: scarce resources an agent may employ.

Time : Type

When action happens. Explicit from the start; no order assumed yet.

Believes : self.Agent → self.Time → self.Means → self.End → Prop

Believes a t m e: at t, agent a believes that employing means m conduces to end e. Means–ends links go only through belief — there is no belief-independent means–ends data.

Prefers : self.Agent → self.Time → Set self.End → Set self.End → Prop

Prefers a t X Y: at t, agent a values the bundle of ends X more highly than the bundle Y. The latent ordinal ranking, strict. Kept distinct from choice; any bridge between them is an axiom in Apodictic.Axioms. No properties assumed.

Over SETS of ends, not ends: the tradition draws no line between an end and a composite — "atomic" only ever means "not further divided by this action", the same relativity as the unit of supply (MES p. 28). So there is ONE ranking, over bundles at the grain of the problem, and an end in the ordinary sense is a singleton bundle (PrefersEnd). This is what makes independence of uses — bundle preference decomposing into end preference — statable as a named hypothesis instead of being enforced silently by the vocabulary. Shape commitment (audit): a bundle is a Set — no multiplicity, no order.

def

Apodictic.ActionFrame.PrefersEnd (F : ActionFrame) (a : F.Agent)
  (t : F.Time) (e e' : F.End) : Prop
Apodictic.ActionFrame.PrefersEnd
  (F : ActionFrame) (a : F.Agent)
  (t : F.Time) (e e' : F.End) : Prop

Preference between ends in the ordinary sense: singleton-bundle preference. Definition, not a second relation.

The law of marginal utility is about a stock of interchangeable units and what the agent would do with more or fewer of them.

structure

Apodictic.Stock (F : ActionFrame) (agent : F.Agent) (t : F.Time) : Type
Apodictic.Stock (F : ActionFrame)
  (agent : F.Agent) (t : F.Time) : Type

A stock of a good, for one agent at one time: finitely many unit-means the agent believes equally serviceable. Homogeneity is serviceability-homogeneity: each unit is believed to conduce to exactly the ends in serves — a BELIEF notion, not a preference notion. No indifference between units is asserted anywhere, so the strict-only Prefers stands and Rothbard's denial that indifference is demonstrable in action is not contradicted. Whether serviceability-homogeneity suffices for the law — Nozick (1977, p. 371) says the law needs indifference — stays checkable rather than assumed away.

What a unit IS is not fixed here: units lists whatever enters the action as one thing. Rothbard: the law holds "regardless of the size of the unit considered. The size of the unit will be the one that enters into concrete human action" (MES p. 28) — pairs of horses are a different stock with a "new and shorter scale of ends", and a good that "cannot be divided into homogeneous units for purposes of action" is a stock of one unit.

Constructor

Apodictic.Stock.mk

Fields

units : Finset F.Means

The units of the good on hand.

serves : Set F.End

The ends this good is serviceable for, by the agent's lights.

homog : ∀ u ∈ self.units, ∀ (e : F.End), F.Believes agent t u e ↔ e ∈ self.serves

Equal serviceability: every unit is believed serviceable for exactly serves.

structure

Apodictic.AllocationDisposition {F : ActionFrame} {agent : F.Agent}
  {t : F.Time} (s : Stock F agent t) : Type
Apodictic.AllocationDisposition
  {F : ActionFrame} {agent : F.Agent}
  {t : F.Time} (s : Stock F agent t) :
  Type

The agent's counterfactual allocation disposition over a stock: for each sub-stock U — each set of units the agent might have — the ends the agent would serve with exactly those units, at the stock's single time. A NEW PRIMITIVE beyond Action, because a single actual allocation action cannot discriminate among the served ends (they are all inside the chosen package); whatever the law of marginal utility rests on, it is not actual action alone.

Indexed by WHICH units, not how many: that the plan depends only on the count is interchangeability of units, and it is not built in — it is the named condition Homogeneous, hypothesized where a theorem needs it.

Field-shape commitment (audit): card_eq is the one-unit-per-end idealization — with the units U (within the stock on hand), exactly as many ends would be served as there are units; units are not split, pooled, or left idle. Rothbard: "each unit of means is capable of serving one of the ends" — "We assume for simplicity" (MES p. 26). The definitional shape is our-reconstruction.

Constructor

Apodictic.AllocationDisposition.mk

Fields

wouldServe : Finset F.Means → Finset F.End

With exactly the units U, the ends that would be served.

serves_subset : ∀ (U : Finset F.Means), ∀ e ∈ self.wouldServe U, e ∈ s.serves

Allocation only to ends the good is believed serviceable for.

card_eq : ∀ U ⊆ s.units, (self.wouldServe U).card = U.card

One unit, one end; no idle units — within the actual stock.

One commitment hides in a field shape here, where the receipt cannot see it: card_eq is Rothbard's "we assume for simplicity" (p. 26), one unit, one end, no idle units. Interchangeability of units does not hide: the plan is indexed by which units, and that it depends only on how many is the named condition below.

def

Apodictic.AllocationDisposition.Homogeneous {F : ActionFrame}
  {agent : F.Agent} {t : F.Time} {s : Stock F agent t}
  (A : AllocationDisposition s) : Prop
Apodictic.AllocationDisposition.Homogeneous
  {F : ActionFrame} {agent : F.Agent}
  {t : F.Time} {s : Stock F agent t}
  (A : AllocationDisposition s) : Prop

Interchangeability of units — a situational applicability condition, NOT an axiom: the plan depends only on how many units, not which. Two sub-stocks of the same size would serve the same ends. This is what makes "the plan at n units" — and so the marginal utility of a supply of n — a function of n. Rothbard makes it definitional of a supply: "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 law in its supply-size form does not apply to them as one. Subjunctive, like the disposition it constrains.

def

Apodictic.Stock.OneMore {F : ActionFrame} {agent : F.Agent} {t : F.Time}
  (s : Stock F agent t) (U V : Finset F.Means) : Prop
Apodictic.Stock.OneMore {F : ActionFrame}
  {agent : F.Agent} {t : F.Time}
  (s : Stock F agent t)
  (U V : Finset F.Means) : Prop

V is U plus one unit, within the stock. Stated by inclusion and cardinality, so that the sub-stocks are hypothesized, never constructed — no decidable equality on units is needed anywhere.