1.10. Claims no theorem uses
Two claims at the centre of the doctrine are used by no theorem here, and so are not on the list. The first is the bridge from what a man actually does to what he prefers — demonstrated preference, in Rothbard's sense. It is written out below in the form it would take, and then set aside:
/-- PARKED: the bridge from actual action to preference. Carried by
no theorem; lives in the document, not the library. -/
structure DemonstratedPreference (praxis : ActionFrame) : Prop where
bridge : ∀ act : Action praxis, ∀ givenUp ∈ act.forgone,
praxis.Prefers act.agent act.time {act.chosen} {givenUp}
The second is the claim that there is any action at all. Action itself is a definition here, and no theorem uses it yet.
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 theorem uses it yet; the law of marginal utility rests on the counterfactual plan alone.
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.