apodictic machine-checked praxeology

2.3. ends_distinguishable: ends can be told apart🔗

🔗axiom
Apodictic.ends_distinguishable : DecidableEq World.End
Apodictic.ends_distinguishable :
  DecidableEq World.End

Ends are distinguishable: identity of ends is decidable — of any two ends it is settled whether they are the same end.

Source: tacit. The reallocation argument (MES p. 27) withdraws one unit and asks which want is thereby given up; "the bundle minus this end" presupposes that each end either is or is not the one withdrawn. Mises's actor chooses between alternatives he tells apart; nothing in the tradition contemplates ends whose identity is undecided.

Status: suppressed-premise. A data axiom, like World. It is what makes "the bundle minus e" constructible; without it that step is available only classically, and the library keeps Classical.choice off the receipt so that every case split is either named praxeological content or absent.

Does not say: anything about preference. It is identity of ends, not indifference between them.

This is the first axiom the constructive-by-default rule surfaced. The derivation rewrites a served bundle as "this end together with the rest", and that rewrite needs, for every end, that it either is or is not the one withdrawn. Mathlib proves the rewrite classically. We could have accepted Classical.choice on the receipt, or hidden decidable identity as a field of the frame where the receipt cannot see it. Naming it is the honest option: it sits beside World as a second data axiom, and it says something a reader can dispute. One more alternative was rejected: phrasing swap_dominance with the served bundle already written as "e together with the rest" on both sides, which needs no decidability in the proof only because it hides the same identification inside the axiom's wording.