1.7. Consistency
World cannot be built, so the axioms cannot be shown consistent by
building it. What can be built is a frame of the general vocabulary
in which every axiom's statement holds, together with the property
we intend to add and the theorems' hypotheses. That frame is
Apodictic.Model.Toy: one agent, one instant, numbers for ends, and
this preference:
The toy preference: X ≻ Y iff they differ by exactly one swap
and X's element is the more urgent (smaller number).
In it, swap dominance holds for the plan that serves the most
urgent ends, as many as there are units; that plan is actual and
homogeneous, ends are decidable, uses are independent, one-unit
steps exist within the stock, each step has a marginal end, and
preference is asymmetric. So the four axioms have a model with
strict preference, and the theorems are neither vacuous nor
trivial. That the model transfers to the World
axioms is the ordinary model-theoretic reading, which Lean cannot
check because World is opaque.