1.16. Claims no theorem uses
One claim at the centre of the doctrine is used by no theorem here, and so is not on the list: the claim that there is any action at all. The bridge from what a man actually does to what he prefers — demonstrated preference, in Rothbard's sense — is not among the unused: exchange spends it, and it is the fifth claim under The claims.
Action itself is a definition here, and no derivation of the law uses it. The existence claim has been tried once. Mises appeals to it to close his dilemma, and a frame with exactly one action shows the appeal falls short of what he needs; the details are under Mises's route.
An action: an agent, at a time, uses means in the belief that they will bring about a chosen end, giving up at least one alternative end in doing so.
The fields hold together as a package — nothing with fewer parts
counts as an action — but this is a definition, so it asserts
nothing. Shape: our-reconstruction. No derivation of the law uses it;
on both routes the law rests on the counterfactual plan alone. Where
it does appear is in Mises's dilemma (Apodictic.Mises.ActionOccurs,
Apodictic.Mises.ActionRecurs), which is machine-checked not to
deliver the law.
Constructor
Apodictic.Action.mk
Fields
agent : praxis.Agent
The acting person.
time : praxis.Time
When the action happens.
chosen : praxis.End
The end aimed at.
means : praxis.Means
The means employed.
forgone : Set praxis.End
The ends given up by acting — the raw material of opportunity cost. Just a set: saying "the next-best alternative" would presuppose a ranking this file does not have.
forgone_nonempty : self.forgone.Nonempty
Action is choice: something is always given up, if only doing nothing.
chosen_not_forgone : self.chosen ∉ self.forgone
The chosen end is not among the forgone.
belief : praxis.Believes self.agent self.time self.means self.chosen
The agent believes the means used will bring about the chosen end.