1.15. 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 one has: asymmetry, spent under Mises's route and by the rival-plan theorem under The theorems.
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. The one claim that bridges the
two (DemonstratedPreference) is stated of a trade, not of action in
general, and only the exchange theorems carry it.
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 structures the
theorems take as arguments โ the stock, the plan, and on the history
reading an allocation. servesOnlyWhatItCan says no unit
is put to a job the man does not believe the good can do.
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 claims quantify 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, and the same
field on an allocation, said of what he did, assumes nothing either. 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 others.
The history reading, under The ladder as a history, puts an actual allocation where the plan was, and reads the supply growing as something that happened. The second is carried by no theorem: added as a hypothesis of the earlier-judged ladder, the linter throws it out, and it appears only in the statement the counter-model refutes.
Apodictic.Allocation {praxis : ActionFrame} {agent : praxis.Agent} {time : praxis.Time} (stock : Stock praxis agent time) : TypeApodictic.Allocation {praxis : ActionFrame} {agent : praxis.Agent} {time : praxis.Time} (stock : Stock praxis agent time) : Type
An actual allocation โ what the agent does with the stock he holds at its time: the ends he serves with it, and nothing else.
This is the object of the TEMPORAL reading of the law
(Apodictic.Temporal). Where AllocationPlan assigns served ends to
every sub-stock at once โ the standing disposition the counterfactual
reading needs โ this records one allocation of one stock at one
time. It is indexed by nothing: not by sub-stock, not by size. What
the agent would have done with fewer units is not in it and cannot be
asked of it. Mises's history โ "if the supply available increases
from nโ1 units to n units" โ is then two of these at two times, not
one plan read at two sizes.
Field-shape claim (audit): servesOnlyWhatItCan, as for the plan, is
definitional โ putting a unit to an end the good is not believed able
to serve is not an allocation of that good.
Like the plan, it is a thing over and above Action. An Action has
one chosen end; a stock of several units serving several ends is
several actions, or one action whose end is a bundle. Which of those
it is the library does not say, and no theorem asks.
Constructor
Apodictic.Allocation.mk
Apodictic.Stock.Grows {praxis : ActionFrame} {agent : praxis.Agent} {earlierTime laterTime : praxis.Time} (earlier : Stock praxis agent earlierTime) (later : Stock praxis agent laterTime) : PropApodictic.Stock.Grows {praxis : ActionFrame} {agent : praxis.Agent} {earlierTime laterTime : praxis.Time} (earlier : Stock praxis agent earlierTime) (later : Stock praxis agent laterTime) : Prop
The supply grows by one โ Mises's "the supply available increases from nโ1 units to n units", read as a history: the stock at the later time holds every unit of the stock at the earlier time and one more.
Says nothing about the order of the two times. Time carries no
order, and this definition does not ask for one: "earlier" and
"later" are the names of the two arguments, not a relation between
their indices. Whether any theorem needs the order is exactly what
leaving it out will show.
The words of exchange โ a trade, an exchange, and what a holding counts for โ are defined under Exchange, where they are used. The dates time preference needs โ a bare "before", the time an end is attained, and which ends are the same satisfaction โ are defined under Time preference; the frame above has none of them.