2.2. World: the frame the axioms speak of
Apodictic.World : ActionFrameApodictic.World : ActionFrame
The world of human action ā the frame the praxeological
axioms speak of. Opaque by design: nothing over World is
constructible, so an axiom about its actions and dispositions cannot
be refuted by a cooked-up instance. Every action, stock, or
disposition over it is either supplied by an axiom or hypothesized
in a theorem statement.
Source: tacit ā Mises's theory is about actual purposeful behavior, action as such, not about a class of models (Human Action, chs. 1ā2 passim).
Status: our-reconstruction. The distinguished-frame architecture is
a formalization decision, not a doctrine of the tradition. It was
chosen because it is the only arrangement under which
#print axioms keeps reporting the commitments; the Misesian
reading is a consequence one may accept, not the reason.
Does not say: that any action exists in World. Existence is a
separate claim, not in the base.
The vocabulary that World instantiates 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 each
forcing is a finding.
Apodictic.ActionFrame : Type 1Apodictic.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.mkFields
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.
2.2.1.Ā Rejected: axioms over every frame
The first encoding (2026-08-02) had no World. Its bridge axiom,
demonstrated preference, quantified over every frame and every action
in it. Restated over today's bundle-valued Prefers, it reads:
/-- REJECTED (2026-08-02): the bridge over every frame. Lives in the
document only; the library never had this bundle form. -/
axiom forall_frame_bridge (F : ActionFrame) (a : Action F) :
ā e ā a.forgone, F.Prefers a.agent a.time {a.chosen} {e}
A frame is an ordinary definable structure, so one can be built in
which preference is everywhere false, together with an action in it.
The axiom then yields False outright:
def badFrame : ActionFrame where
Agent := Unit
End := Bool
Means := Unit
Time := Unit
Believes := fun _ _ _ _ => True
Prefers := fun _ _ _ _ => False
def badAction : Action badFrame where
agent := ()
time := ()
chosen := true
means := ()
forgone := {e | e = false}
forgone_nonempty := āØfalse, rflā©
chosen_not_forgone := fun h => Bool.noConfusion h
belief := trivial
theorem forall_frame_inconsistent : False :=
forall_frame_bridge badFrame badAction false rfl
#print axioms forall_frame_inconsistent
The lesson is general and not about praxeology: a global axiom about all inhabitants of a definable type is refutable by construction unless the type's own fields secure the claim. The review that approved the axiom had checked its fidelity to the doctrine, not its quantifier range. Statement-fidelity review does not catch this; building the pathological model does.
Four fixes were on the table. Fold the assertion into the structure
as a field: consistent, but it hides the bridge where the receipt
cannot see it, and the bridge is the one thing the brief says must be
its own flagged axiom. State it as a hypothesis on every theorem:
honest, but then the receipt shows nothing and the method is gone.
Define preference as demonstrated preference: consistent and
hardline Rothbardian, but it erases the distinction between the
latent ranking and choice, and the dispute with Nozick becomes
unstatable. The fourth is what we did: a distinguished opaque frame.
With the axiom restated over World, the same witness no longer
type-checks:
axiom world_bridge (a : Action World) :
ā e ā a.forgone, World.Prefers a.agent a.time {a.chosen} {e}
theorem still_inconsistent : False :=
world_bridge badAction false rfl
One thing should be said plainly. The distinguished frame was chosen because it is the only option under which the receipt keeps printing the commitments. The Misesian gloss in its docstring, that praxeology is about action as such rather than about all conceivable structures, is defensible, and it was attached afterwards. The switch to a class-of-frames reading, should it ever be wanted, is mechanical: each axiom becomes a field of a frame bundle and each theorem gains a frame parameter. What does not transfer is consistency, which a class of frames gets from any model and a fixed world must earn separately. That is the price of the simpler formalism, and it is paid in the section on consistency below.