Apodictic: Machine-Checked Praxeology
Mises claimed that the theorems of praxeology are "perfectly certain and incontestable, like the correct mathematical theorems" (Human Action, ch. II, §3). They follow, he held, from the plain fact that people act, as strictly as a theorem follows from its axioms, and from that he drew a consequence: they are "not subject to verification or falsification on the ground of experience and facts" (ch. II, §1). The consequence holds only if the deduction does. That is what is tested here — whether the deduction runs from the fact of action alone, and if not, what else it needs.
The test is run on one law, the law of marginal utility, and on both derivations the tradition gives it: Rothbard's in full, and Mises's beside it, each rebuilt in Lean 4, a proof assistant. The law itself is not Rothbard's. It is ordinary economics — he calls it "this fundamental law of economics" and notes it is "sometimes known as the law of diminishing marginal utility", and he is emphatic that other writers reach it too, wrongly in his view, from psychology. What is his is how it is got: deduced, he says, from the axiom of human action. The deduction is what is supposed to carry the law to certainty, so the deduction is what is audited here.
Spoken arguments run on enthymemes — steps that leave a premise unstated because a reader will supply it without noticing. A proof assistant supplies nothing. Anything the argument passes over in silence has to be written down before the proof will go through, and written somewhere a reader can find it.
What the audit found. The derivation goes through, and it needs one praxeological claim to do it. That claim is not about anything the man does. It credits him with a settled answer, held in advance, to what he would do with every stock of horses smaller than the one he has — and Rothbard's own restriction is that a man needs no such scale in advance, because it shows up only in his concrete choices. He named this law as the one exception to that rule, and what he offered to warrant the exception is the derivation that needs it. A second demand, weaker, is what the law's usual wording needs, and he grounds that one elsewhere. Nothing here shows the law false, and nothing in the proof runs in a circle. What is left is a question about the warrant — and Mises, who gets to the law by another road, arrives at a premise of the same shape and offers it none.
The case for all of it — the passages, the claim, the conditions, the theorems, and the manifest each theorem carries — is in The Result.