1.13. The regression theorem🔗

The regression theorem is the fourth target. It is Mises's account of where a medium of exchange can come from: "no good can be employed for the function of a medium of exchange which at the very beginning of its use for this purpose did not have exchange value on account of other employments" (Human Action, ch. XVII, §4). It was chosen because a case is pressed against it. Some media came into use inside a monetary economy, Bitcoin among them, and their first buyers paid money for them. What the theorem requires of such a medium depends on how its terms are read, and with the readings written separately in Lean, moving from one to another is a change of hypothesis that shows in a signature.

The theorem has two halves, and only one is here: the genetic half, about a medium's origin. The other, that today's purchasing power is formed from yesterday's, is about quantities, and nothing below has any. And the theorem is about any medium of exchange, not only money: "For all that is to be predicated of money is valid for every medium of exchange" (ch. XVII, §1).

A medium, by belief. Mises's medium of exchange is a good wanted "to keep it as a medium of exchange and to give it away at need in a later act of exchange" (ch. XVII, §4). The vocabulary grows by one bare relation to say so: an end is onward for a good when the man would reach it by giving that good itself away in a later trade.

Apodictic.MediumFrame : Type 1
Apodictic.MediumFrame : Type 1

Apodictic.MediumFrame.mk

Agent : Type

End : Type

Means : Type

Time : Type

Believes : self.Agent → self.Time → self.Means → self.End → Prop

Prefers : self.Agent → self.Time → Set self.End → Set self.End → Prop

Onward : self.Means → self.End → Prop

A man appraises a good as a medium when he believes it serves some onward end. Two other definitions were available and neither is used. One calls a good a medium when its price is being appraised; then a medium would have a price behind it by the meaning of the word, and the regress would be true by definition. The other waits for an actual later trade; but a man who holds a good meaning to pass it on already demands it as a medium, whether or not the trade comes. So demand in anticipation counts.

Apodictic.MediumFrame.AppraisesAsMedium (praxis : MediumFrame)
  (agent : praxis.Agent) (time : praxis.Time) (m : praxis.Means) : Prop
Apodictic.MediumFrame.AppraisesAsMedium
  (praxis : MediumFrame)
  (agent : praxis.Agent)
  (time : praxis.Time)
  (m : praxis.Means) : Prop

A good, here, is a kind — gold, salt — and not a unit of one. The regress is about the kind: a coin minted today was never traded before, and the theorem is not about that coin.

The regress runs back through what happened, so there is a record of it: the exchanges made on each day, with days counted from a first one.

Apodictic.History (praxis : MediumFrame) : Type
Apodictic.History (praxis : MediumFrame) :
  Type

Apodictic.History.mk

date : ℕ → praxis.Time

exchanges : ℕ → Set (Exchange praxis.toActionFrame)

Three things are read off the record: that a man acquired the good on a day, giving another for it; that he did so for an end other than passing it on; and that on a day someone appraises the good as a medium.

Apodictic.History.AcquiredAgainst {praxis : MediumFrame}
  (history : History praxis) (k : ℕ) (m : praxis.Means)
  (agent : praxis.Agent) (g : praxis.Means) : Prop
Apodictic.History.AcquiredAgainst
  {praxis : MediumFrame}
  (history : History praxis) (k : ℕ)
  (m : praxis.Means)
  (agent : praxis.Agent)
  (g : praxis.Means) : Prop

Apodictic.History.DirectAcquisitionAt {praxis : MediumFrame}
  (history : History praxis) (k : ℕ) (m : praxis.Means) : Prop
Apodictic.History.DirectAcquisitionAt
  {praxis : MediumFrame}
  (history : History praxis) (k : ℕ)
  (m : praxis.Means) : Prop

Apodictic.History.MediumAt {praxis : MediumFrame}
  (history : History praxis) (n : ℕ) (m : praxis.Means) : Prop
Apodictic.History.MediumAt
  {praxis : MediumFrame}
  (history : History praxis) (n : ℕ)
  (m : praxis.Means) : Prop

Indirect exchange needs no new claim. A man who trades for a good only to pass it on ranks what he expects to reach by passing it on above what the good he gave could do. That is the exchange theorem again, with onward ends counted like any others, and it carries the same claim and conditions plus one: that he wants the good for nothing else.

Apodictic.Trade.PurelyIndirect {praxis : MediumFrame}
  (trade : Trade praxis.toActionFrame) : Prop
Apodictic.Trade.PurelyIndirect
  {praxis : MediumFrame}
  (trade : Trade praxis.toActionFrame) :
  Prop

Apodictic.Regression.indirect_ranks_onward_ends {praxis : MediumFrame}
  (trade : Trade praxis.toActionFrame)
  (demonstrated : DemonstratedPreference trade)
  (voluntary : trade.Voluntary) (separable : trade.SeparableFromRest)
  (unique : trade.KeptServesOtherEnds) (pure : trade.PurelyIndirect) :
  praxis.Prefers trade.agent trade.time
    (praxis.OnwardEnds trade.agent trade.time trade.gets)
    (praxis.ServedBy trade.agent trade.time {trade.gives})
Apodictic.Regression.indirect_ranks_onward_ends
  {praxis : MediumFrame}
  (trade : Trade praxis.toActionFrame)
  (demonstrated :
    DemonstratedPreference trade)
  (voluntary : trade.Voluntary)
  (separable : trade.SeparableFromRest)
  (unique : trade.KeptServesOtherEnds)
  (pure : trade.PurelyIndirect) :
  praxis.Prefers trade.agent trade.time
    (praxis.OnwardEnds trade.agent
      trade.time trade.gets)
    (praxis.ServedBy trade.agent
      trade.time {trade.gives})

The claim. The hinge of the theorem is a sentence about judgment: the man considering money "cannot form a judgment about the future purchasing power of money otherwise than by looking at its configuration in the immediate past", and so "A medium of exchange without a past is unthinkable" (ch. XVII, §§4, 8). Mises's premise shuts every other ground of judgment out, and the library does not follow him that far. The docstring says what it asserts and, under Does not say, what it leaves out.

Apodictic.AppraisalFromPast {praxis : MediumFrame}
  (history : History praxis) (m : praxis.Means) : Prop
Apodictic.AppraisalFromPast
  {praxis : MediumFrame}
  (history : History praxis)
  (m : praxis.Means) : Prop

Apodictic.AppraisalFromPast.mk

fromPast : ∀ (n : ℕ) (agent : praxis.Agent),
  praxis.AppraisesAsMedium agent (history.date (n + 1)) m → ∃ k ≤ n, history.ExchangedOn k m

The regress. Mises states his conclusion in the negative, and the negative is what comes out at the lowest price. If nobody acquired the good, before a given day, for an end other than passing it on, then on that day nobody appraises it as a medium:

Apodictic.Regression.no_medium_without_direct_acquisition
  {praxis : MediumFrame} (history : History praxis) (m : praxis.Means)
  (n : ℕ) (appraisal : AppraisalFromPast history m)
  (begins : history.BeginsBeforeMedium m)
  (purposive : history.AcquisitionsPurposive m n)
  (noDirect : ∀ k < n, ¬history.DirectAcquisitionAt k m) :
  ¬history.MediumAt n m
Apodictic.Regression.no_medium_without_direct_acquisition
  {praxis : MediumFrame}
  (history : History praxis)
  (m : praxis.Means) (n : ℕ)
  (appraisal :
    AppraisalFromPast history m)
  (begins : history.BeginsBeforeMedium m)
  (purposive :
    history.AcquisitionsPurposive m n)
  (noDirect :
    ∀ k < n,
      ¬history.DirectAcquisitionAt k m) :
  ¬history.MediumAt n m

manifest of Apodictic.Regression.no_medium_without_direct_acquisition

  praxeological claims:
    appraisal : AppraisalFromPast history m

  situational conditions:
    begins : history.BeginsBeforeMedium m
    purposive : history.AcquisitionsPurposive m n
    noDirect : ∀ k < n, ¬history.DirectAcquisitionAt k m

  vocabulary (what the claims are about):
    praxis : MediumFrame
    history : History praxis
    m : praxis.Means
    n : ℕ

  logical background: []

  (1 trailing binders belong to the conclusion, not the signature)

One claim, and two conditions besides the hypothesis the sentence itself states. Neither condition is in Mises's sentence.

The first is that the regress ends. Counting days from a first one supplies half of that: from any day there are finitely many days back. The other half is that on the first day of the record the good is not yet a medium, and that is assumed. Both authors assert it; neither argues it.

Apodictic.History.BeginsBeforeMedium {praxis : MediumFrame}
  (history : History praxis) (m : praxis.Means) : Prop
Apodictic.History.BeginsBeforeMedium
  {praxis : MediumFrame}
  (history : History praxis)
  (m : praxis.Means) : Prop

The second is that whoever acquired the good wanted it for something. The proof needs it at every step back: an acquirer who believed the good served no end at all, not even resale, is neither a holder of a medium nor a direct user, and the regress stops at him with nothing to show. We found no passage in either author that states it.

Apodictic.History.AcquisitionsPurposive {praxis : MediumFrame}
  (history : History praxis) (m : praxis.Means) (n : ℕ) : Prop
Apodictic.History.AcquisitionsPurposive
  {praxis : MediumFrame}
  (history : History praxis)
  (m : praxis.Means) (n : ℕ) : Prop

The positive form, and what it adds. Turned round, the theorem says that if the good is a medium on some day, then on an earlier day someone acquired it for an end other than passing it on — and the proof finds that acquisition. This costs one claim more.

Apodictic.Regression.direct_acquisition_before {praxis : MediumFrame}
  (history : History praxis) (m : praxis.Means) (n : ℕ)
  (twoDemands : TwoPartialDemands praxis m)
  (appraisal : AppraisalFromPast history m)
  (begins : history.BeginsBeforeMedium m)
  (purposive : history.AcquisitionsPurposive m n)
  (medium : history.MediumAt n m) :
  ∃ k < n, history.DirectAcquisitionAt k m
Apodictic.Regression.direct_acquisition_before
  {praxis : MediumFrame}
  (history : History praxis)
  (m : praxis.Means) (n : ℕ)
  (twoDemands :
    TwoPartialDemands praxis m)
  (appraisal :
    AppraisalFromPast history m)
  (begins : history.BeginsBeforeMedium m)
  (purposive :
    history.AcquisitionsPurposive m n)
  (medium : history.MediumAt n m) :
  ∃ k < n, history.DirectAcquisitionAt k m

manifest of Apodictic.Regression.direct_acquisition_before

  praxeological claims:
    twoDemands : TwoPartialDemands praxis m
    appraisal : AppraisalFromPast history m

  situational conditions:
    begins : history.BeginsBeforeMedium m
    purposive : history.AcquisitionsPurposive m n
    medium : history.MediumAt n m

  vocabulary (what the claims are about):
    praxis : MediumFrame
    history : History praxis
    m : praxis.Means
    n : ℕ

  logical background: []

At each step back the proof meets an acquirer and the end he wanted the good for, and has to know which kind of end it is: onward, in which case the regress goes on, or not, in which case it has arrived. The negative form never has to decide. The positive form does, and nothing in the vocabulary or in constructive logic decides it. What decides it is a sentence of Mises's own: "Thus the demand for a medium of exchange is the composite of two partial demands: the demand displayed by the intention to use it in consumption and production and that displayed by the intention to use it as a medium of exchange". Read as saying that the two parts leave nothing over, the composite is the statement that each end is onward or is not — a case of the law of excluded middle, and the library takes no such law for granted. So it enters as a named claim rather than as logic. The sentence is Mises's; reading "composite" as leaving nothing over is ours.

Apodictic.TwoPartialDemands (praxis : MediumFrame) (m : praxis.Means) :
  Prop
Apodictic.TwoPartialDemands
  (praxis : MediumFrame)
  (m : praxis.Means) : Prop

Apodictic.TwoPartialDemands.mk

sorted : ∀ (e : praxis.End), praxis.Onward m e ∨ ¬praxis.Onward m e

Without the claim, the two parts are shown to exhaust a good's ends only up to a double negation; with it, outright:

Apodictic.Regression.partial_demands_not_not_exhaust
  {praxis : MediumFrame} (agent : praxis.Agent) (time : praxis.Time)
  (m : praxis.Means) (e : praxis.End) :
  e ∈ praxis.ServedBy agent time {m} →
    ¬e ∉ praxis.DirectEnds agent time m ∪ praxis.OnwardEnds agent time m
Apodictic.Regression.partial_demands_not_not_exhaust
  {praxis : MediumFrame}
  (agent : praxis.Agent)
  (time : praxis.Time) (m : praxis.Means)
  (e : praxis.End) :
  e ∈ praxis.ServedBy agent time {m} →
    ¬e ∉
        praxis.DirectEnds agent time m ∪
          praxis.OnwardEnds agent time m

Apodictic.Regression.partial_demands_exhaust {praxis : MediumFrame}
  (agent : praxis.Agent) (time : praxis.Time) (m : praxis.Means)
  (twoDemands : TwoPartialDemands praxis m) :
  praxis.ServedBy agent time {m} =
    praxis.DirectEnds agent time m ∪ praxis.OnwardEnds agent time m
Apodictic.Regression.partial_demands_exhaust
  {praxis : MediumFrame}
  (agent : praxis.Agent)
  (time : praxis.Time) (m : praxis.Means)
  (twoDemands :
    TwoPartialDemands praxis m) :
  praxis.ServedBy agent time {m} =
    praxis.DirectEnds agent time m ∪
      praxis.OnwardEnds agent time m

One thing is not proved in either form: that there was a last day of barter, a day before which the good was no medium and after which it was. That needs "is a medium on this day" decided for each day, which is a question about every agent at once, and no claim here settles it: it would take excluded middle outright.

Two readings of "other employments". In the theorems above, an end other than passing the good on is any such end: the direct part of the demand is whatever is not onward. Mises names something narrower, "the services it can render directly to consumption or production". He does not say which ends those are, and the library sorts no ends. So the narrow reading is a condition: whoever applies the theorem supplies the ends he counts as consumption or production, and the condition says that every other employment the good was acquired for was one of them.

Apodictic.History.OtherEmploymentsNarrow {praxis : MediumFrame}
  (history : History praxis) (narrow : praxis.End → Prop)
  (m : praxis.Means) (n : ℕ) : Prop
Apodictic.History.OtherEmploymentsNarrow
  {praxis : MediumFrame}
  (history : History praxis)
  (narrow : praxis.End → Prop)
  (m : praxis.Means) (n : ℕ) : Prop

Apodictic.Regression.narrow_acquisition_before {praxis : MediumFrame}
  (history : History praxis) (narrow : praxis.End → Prop)
  (m : praxis.Means) (n : ℕ) (twoDemands : TwoPartialDemands praxis m)
  (appraisal : AppraisalFromPast history m)
  (begins : history.BeginsBeforeMedium m)
  (purposive : history.AcquisitionsPurposive m n)
  (narrowReading : history.OtherEmploymentsNarrow narrow m n)
  (medium : history.MediumAt n m) :
  ∃ k < n, history.NarrowAcquisitionAt narrow k m
Apodictic.Regression.narrow_acquisition_before
  {praxis : MediumFrame}
  (history : History praxis)
  (narrow : praxis.End → Prop)
  (m : praxis.Means) (n : ℕ)
  (twoDemands :
    TwoPartialDemands praxis m)
  (appraisal :
    AppraisalFromPast history m)
  (begins : history.BeginsBeforeMedium m)
  (purposive :
    history.AcquisitionsPurposive m n)
  (narrowReading :
    history.OtherEmploymentsNarrow narrow
      m n)
  (medium : history.MediumAt n m) :
  ∃ k < n,
    history.NarrowAcquisitionAt narrow k m

Nothing is derived beyond the condition. The narrow theorem, and the negative form that goes with it, are the broad ones with the narrow reading passed through to the conclusion.

Rothbard's two versions. Rothbard states the origin twice, and differently. In MES a medium "can arise only out of a commodity previously used directly in a barter situation, and therefore having had an array of prices in terms of other goods" (p. 275). In Power and Market, "no money can be established on the market except as it can be exchanged for a previously existing money (which in turn must have ultimately related back to a commodity in barter)" (MES ed., p. 1021).

The first version adds, to the earlier acquisition for an end other than passing the good on, that it was made against a good not then a medium. That clause is not derived. It is a condition on every earlier acquisition of the good, and the conclusion's clause is that condition applied to the one acquisition the regress finds:

Apodictic.History.FormedInBarter {praxis : MediumFrame}
  (history : History praxis) (m : praxis.Means) (n : ℕ) : Prop
Apodictic.History.FormedInBarter
  {praxis : MediumFrame}
  (history : History praxis)
  (m : praxis.Means) (n : ℕ) : Prop

Apodictic.Regression.barter_origin {praxis : MediumFrame}
  (history : History praxis) (m : praxis.Means) (n : ℕ)
  (twoDemands : TwoPartialDemands praxis m)
  (appraisal : AppraisalFromPast history m)
  (begins : history.BeginsBeforeMedium m)
  (purposive : history.AcquisitionsPurposive m n)
  (barter : history.FormedInBarter m n)
  (medium : history.MediumAt n m) :
  ∃ k < n,
    ∃ agent g,
      history.AcquiredAgainst k m agent g ∧
        praxis.ValuesDirectly agent (history.date k) m ∧
          ¬history.MediumAt k g
Apodictic.Regression.barter_origin
  {praxis : MediumFrame}
  (history : History praxis)
  (m : praxis.Means) (n : ℕ)
  (twoDemands :
    TwoPartialDemands praxis m)
  (appraisal :
    AppraisalFromPast history m)
  (begins : history.BeginsBeforeMedium m)
  (purposive :
    history.AcquisitionsPurposive m n)
  (barter : history.FormedInBarter m n)
  (medium : history.MediumAt n m) :
  ∃ k < n,
    ∃ agent g,
      history.AcquiredAgainst k m agent
          g ∧
        praxis.ValuesDirectly agent
            (history.date k) m ∧
          ¬history.MediumAt k g

manifest of Apodictic.Regression.barter_origin

  praxeological claims:
    twoDemands : TwoPartialDemands praxis m
    appraisal : AppraisalFromPast history m

  situational conditions:
    begins : history.BeginsBeforeMedium m
    purposive : history.AcquisitionsPurposive m n
    barter : history.FormedInBarter m n
    medium : history.MediumAt n m

  vocabulary (what the claims are about):
    praxis : MediumFrame
    history : History praxis
    m : praxis.Means
    n : ℕ

  logical background: []

The second version is a theorem about the prior money: the good the new medium was first acquired against, if it was then a medium itself, had an acquisition for an end other than passing it on before that. It delivers less than the parenthesis says: an earlier acquisition of that good for an end of its own, not that the acquisition was in barter. And it carries both claims, and the conditions, for every good.

Apodictic.Regression.prior_money_relates_back {praxis : MediumFrame}
  (history : History praxis) (m : praxis.Means) (n : ℕ)
  (twoDemands : ∀ (g : praxis.Means), TwoPartialDemands praxis g)
  (appraisal : ∀ (g : praxis.Means), AppraisalFromPast history g)
  (begins : ∀ (g : praxis.Means), history.BeginsBeforeMedium g)
  (purposive : ∀ (g : praxis.Means), history.AcquisitionsPurposive g n)
  (medium : history.MediumAt n m) :
  ∃ k < n,
    ∃ agent g,
      history.AcquiredAgainst k m agent g ∧
        (history.MediumAt k g →
          ∃ k' < k, history.DirectAcquisitionAt k' g)
Apodictic.Regression.prior_money_relates_back
  {praxis : MediumFrame}
  (history : History praxis)
  (m : praxis.Means) (n : ℕ)
  (twoDemands :
    ∀ (g : praxis.Means),
      TwoPartialDemands praxis g)
  (appraisal :
    ∀ (g : praxis.Means),
      AppraisalFromPast history g)
  (begins :
    ∀ (g : praxis.Means),
      history.BeginsBeforeMedium g)
  (purposive :
    ∀ (g : praxis.Means),
      history.AcquisitionsPurposive g n)
  (medium : history.MediumAt n m) :
  ∃ k < n,
    ∃ agent g,
      history.AcquiredAgainst k m agent
          g ∧
        (history.MediumAt k g →
          ∃ k' < k,
            history.DirectAcquisitionAt k'
              g)

The detour through the prior money is not needed for the new medium. Under the broad reading the positive form already concludes, for the new medium itself, an earlier acquisition for an end other than passing it on, whatever was paid for it. The regress follows the acquirers' ends, never what they gave. The prior money's history adds a conclusion about the prior money.

"Its own past price." Mises's exclusive premise — that the appraisal rests on the good's own past price — would best be a condition separate from the claim, so that a failure could be laid to one or the other. Without quantities it cannot be kept separate. "Rests on" has no statement here; what can be stated is that an exchange of the good came earlier, and that is the claim again.

Apodictic.History.OwnPastPrice {praxis : MediumFrame}
  (history : History praxis) (m : praxis.Means) (n : ℕ) : Prop
Apodictic.History.OwnPastPrice
  {praxis : MediumFrame}
  (history : History praxis)
  (m : praxis.Means) (n : ℕ) : Prop

Apodictic.Regression.ownPastPrice_of_claim {praxis : MediumFrame}
  (history : History praxis) (m : praxis.Means) (n : ℕ)
  (appraisal : AppraisalFromPast history m) : history.OwnPastPrice m n
Apodictic.Regression.ownPastPrice_of_claim
  {praxis : MediumFrame}
  (history : History praxis)
  (m : praxis.Means) (n : ℕ)
  (appraisal :
    AppraisalFromPast history m) :
  history.OwnPastPrice m n

The case. The library builds one frame to test this on: a good first believed fit only for eating and, from the next day, also for passing on. In it both claims and every condition of the barter and narrow theorems hold together with a medium, so the theorems do not hold merely because nothing meets their hypotheses. The test is thin, and it is worth saying where: there is one agent, the good is exchanged against itself, and nothing in the frame is ranked.

What a failure would point at. Suppose a good is a medium, and no earlier acquisition of it for an end other than passing it on is to be found. Then the record began inside a monetary economy, with the good already a medium on its first day; or someone took the good believing it good for nothing; or the record is missing an exchange that happened; or the first claim failed, and someone appraised the good as a medium when it had never changed hands — on a promise, say, or an edict.

The second claim is not on that list. No case can be brought against it: that no end falls outside both parts is proved above, with no claim at all. What it adds is the right to say which part. Without it the negative form still stands.

Buying a good to resell it is not on that list as an escape. A man who holds a good in order to sell it believes it serves an onward end, so he already appraises it as a medium, and the regress asks for an acquisition earlier than his.

For a medium whose first buyers paid money, the versions come apart. Rothbard's barter version is silent: its condition fails wherever the good was bought with money before the day in question. The broad theorem is not silent on that account, since it never asks what was paid. Given its own two conditions, it asks whether some early acquirer wanted the good for an end other than passing it on, which is a question about those acquirers. The narrow theorem asks more — that what they wanted it for was consumption or production — and is silent where the good was first wanted for a game, a cause, or a test.