1.9. The vocabulary
Reference. These are the definitions the statements above are written in; nothing earlier depends on having read them.
The basic vocabulary is deliberately bare. Preference is just a relation: not assumed transitive, not assumed to rank every pair, and time is not assumed ordered. Properties get added when a theorem forces them, and so far none has.
The vocabulary everything else is built from: bare types and bare
relations. Nothing here has any property. Preference is not assumed
transitive, not assumed to rank every pair, and Time is not assumed
ordered. A property gets added only when some theorem forces it, and
every such 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 agent time means want: at that time, the agent
believes that using those means helps bring about that want. Nothing
links a means to an end here except what the agent believes.
Prefers : self.Agent โ self.Time โ Set self.End โ Set self.End โ Prop
Prefers agent time X Y: at that time, the agent values the
bundle of ends X above the bundle Y. This is the ranking behind
the agent's choices, read as strict โ but that reading is not
assumed anywhere: NO properties are imposed on this relation, strict
or otherwise, and a theorem that needs one says so. It is kept apart
from what the agent actually does; nothing in the library bridges
the two, and the claim that would (demonstrated preference) is
parked, carried by no theorem.
It ranges over SETS of ends rather than single ends. The tradition
draws no line between an end and a composite of ends โ "atomic"
only ever means "not divided further by this action", the same
relativity as the size of a unit of supply (MES p. 28). So there
is ONE ranking, over bundles at whatever grain the problem has, and
an end in the ordinary sense is a bundle with one member
(PrefersEnd). Ranging over bundles is what lets independence of
uses โ bundle preference breaking down into preference between
ends โ be a named hypothesis, instead of something the
vocabulary quietly enforces.
Shape claim (audit): a bundle is a Set, so it carries no
multiplicity and no order.
Apodictic.ActionFrame.PrefersEnd (praxis : ActionFrame) (agent : praxis.Agent) (time : praxis.Time) (want other : praxis.End) : PropApodictic.ActionFrame.PrefersEnd (praxis : ActionFrame) (agent : praxis.Agent) (time : praxis.Time) (want other : praxis.End) : Prop
Preference between two single ends. This is bundle preference between two one-member bundles โ a definition, not a second relation.
The law is about a stock of units and what the agent would do with more or fewer of them.
A stock of some good, held by one agent at one time: finitely many units the agent believes will do the same jobs.
"The same jobs" is the whole of what homogeneity means here. Each
unit is believed to serve exactly the ends in serves, and that is a
claim about BELIEF, not about preference. Nowhere is it said that the
agent is indifferent between units. So preference can stay strict,
and Rothbard's denial that indifference is ever demonstrated in
action is not contradicted. Whether doing the same jobs is enough for
the law, or whether indifference between units is needed after all,
is then something to check rather than something assumed away.
What counts as a unit is left open: units lists whatever enters the
action as one thing. Rothbard holds that the law works "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 make 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 exactly one unit.
Constructor
Apodictic.Stock.mk
Fields
units : Finset praxis.Means
The units of the good on hand.
serves : Set praxis.End
The ends this good can serve, by the agent's lights.
unitsAlike : โ unit โ self.units, โ (want : praxis.End), praxis.Believes agent time unit want โ want โ self.serves
Every unit is believed to serve exactly the ends in
serves.
Apodictic.AllocationPlan {praxis : ActionFrame} {agent : praxis.Agent} {time : praxis.Time} (stock : Stock praxis agent time) : TypeApodictic.AllocationPlan {praxis : ActionFrame} {agent : praxis.Agent} {time : praxis.Time} (stock : Stock praxis agent time) : Type
The agent's plan for the stock: for each subStock โ each set
of units he might have โ the ends he WOULD serve with exactly those
units, at the stock's single time.
This is something new, over and above Action, and it has to be. A
single act of allocating cannot tell the served ends apart from one
another โ they all sit inside the one package chosen. So what the law
of marginal utility rests on is not action at all: the plan is a
separate thing, and no act of the agent's exhibits it.
The plan is indexed by WHICH units, not by how many. To say it depends
only on the number of them is to say the units are interchangeable,
and that is not built in here: it is the named condition
Homogeneous, assumed only where a theorem needs it.
Field-shape claim (audit): servesOnlyWhatItCan is the one condition
left in field position, and it is definitional โ a plan that puts a
unit to an end the good is not believed able to serve is not a
coherent plan, rather than a situation that might obtain.
One unit to one end is NOT here, and is nowhere: no theorem needs it. Rothbard assumes it and says he is assuming it โ "each unit of means is capable of serving one of the ends", introduced with "We assume for simplicity" (MES p. 26) โ and the ordering the law asserts turns out not to want it. Where an extra unit adds no new end, the law is silent, which costs nothing.
Constructor
Apodictic.AllocationPlan.mk
Fields
wouldServe : Finset praxis.Means โ Finset praxis.End
The ends the agent would serve with exactly the units in
subStock, and no others.
servesOnlyWhatItCan : โ (subStock : Finset praxis.Means), โ want โ self.wouldServe subStock, want โ stock.serves
A unit is only ever put to an end the good is believed able to serve.
Two conditions sit a level down, as fields of the two structures every
theorem above takes as arguments. servesOnlyWhatItCan says a unit is
only ever put to an end the good is believed able to serve.
unitsAlike, a field of the stock, says every unit is believed to
serve exactly the same ends โ and that is what fixes the range of
stock.serves, which is in turn what the one claim quantifies over.
Neither is a binder in any statement, and both are on the manifest
regardless: #manifest reads one level in and reports them, because
whoever supplies the argument has already discharged them.
The two are not alike, and the manifest does not pretend otherwise. A
plan that puts a horse to a job the man does not believe a horse can
do is not a situation that might obtain โ it is an incoherent plan, so
servesOnlyWhatItCan assumes nothing about the world. A lame horse is
a situation that might obtain, so unitsAlike does. Which of the two
a carried condition is cannot be read off the term; it is ruled by
hand, and this is the ruling.
A third used to sit here, and now sits nowhere. One unit to one end can fail of a real stable โ two horses to one wagon, or a horse standing idle โ so it could not stay a field. Taking it out showed that no theorem wants it, so it was not made a hypothesis either. See the findings.
Interchangeability of units is not hidden down there. The plan is
indexed by which exact units the man holds; that it depends only on how
many of them there are is a separate named condition,
AllocationPlan.Homogeneous, given in full under The conditions
along with the other two.