the second hundred · metaphor 213

The price a belief
charges you.

Two convictions can feel equally certain and still cost wildly different amounts to hold. The honest question isn't only is this true? — it's what did I have to assume to earn it?

We usually audit our beliefs for truth: is it right, is the evidence good. But every belief also has a hidden bill of materials — the deeper assumptions it quietly rests on. Some convictions are nearly free; they follow from things you'd grant anyway. Others look modest and turn out to cost you a whole worldview. You can't read the price off the surface. Two claims can sound equally reasonable while one commits you to almost nothing and the other drags in a cathedral of premises.

Mathematicians hit the same problem and built a tool for it. Ordinary proof runs forwards: from axioms to theorems. Reverse mathematics runs the arrow backwards — it asks, for a given theorem, exactly which axioms are necessary to prove it, no more and no less. The startling result is that a huge sweep of mathematics sorts into just a handful of strength levels, and a theorem often turns out to be equivalent to the very axiom it needs — so holding it costs you precisely that, and buys you everything weaker for free.

Belief auditor · the Big Five subsystems of arithmetic
Strength granted → (click a rung)
Theorems (click to audit)
strength grantedRCA₀
proof-theoretic ordinalω^ω
theorems earned2 / 13
still out of reach11
audit
Switch to Audit a belief and click any theorem to see the minimal axiom it charges you — and what comes free once you've paid.
Grant mode: click a rung to grant that axiom and everything below it. Watch the theorems it earns light up. Strength comes in discrete jumps, not a smooth dial.
What this is: the strengths and equivalences below are established reverse-mathematics results (Simpson, Subsystems of Second Order Arithmetic), read live from an explicit dependency table — the table is the model. The widget looks up known placements; it does not re-derive the proofs, which are the actual mathematics.

The idea

Run the proof arrow backwards.

Normal mathematics is forward: fix your axioms, then see what theorems fall out. Reverse mathematics fixes the theorem and hunts for the axioms — specifically, the weakest axiom system strong enough to prove it. The program works over a deliberately feeble base theory, RCA₀, that can only build computable objects, and then asks: what extra strength must we add?

The punchline, discovered over and over since the 1970s, is a kind of miracle of tidiness. Across analysis, algebra, topology and combinatorics, the theorems don't scatter across a continuum of strengths — they clump onto a short ladder of five main systems, the Big Five. And again and again, a theorem turns out not merely to follow from its rung but to be logically equivalent to it, over the base: prove the theorem and you can prove the axiom back, and vice-versa. The theorem is its price.

That reverses how we usually rank axioms. We tend to think axioms are the suspicious part and theorems are the safe payoff. Reverse math shows the payoff and the premise are often the same commitment wearing two faces. Bolzano–Weierstrass — an innocent line about bounded sequences — secretly costs you the full jump to ACA₀. The intermediate value theorem, which sounds just as basic, costs nothing beyond the base at all.

What to try

Grant a little, then read the bill.

In grant mode, click up the ladder one rung at a time. Each rung adds one characteristic axiom — and, crucially, everything below comes with it. Watch how theorems switch on in tiers, not one by one: nothing, then a burst at WKL₀, another at ACA₀. The count of what you've earned jumps in steps. That stepped structure is the whole surprise — the mathematical universe is not a smooth gradient of difficulty but a short staircase.

Then switch to audit mode and click individual beliefs. The auditor names each theorem's minimal axiom — its price — and, because the two are equivalent, tells you what you're forced to buy and what then comes free. Notice how badly surface intuition mispredicts cost: the compactness of the unit interval and Gödel's completeness theorem sit on the same modest rung; a plain statement about convergent subsequences sits two rungs higher. You cannot audit a belief by how obvious it feels — only by tracing what it actually requires.

The mapping

Auditing a conviction, not defending it.

Take a belief you hold about how the world works — that people are basically trustworthy, say, or that hard work is repaid, or that your community has your back. The usual argument is about truth: is it borne out, what's the counter-evidence. Reverse math suggests a different, sharper interrogation: what does holding this actually commit me to? Strip it to the weakest set of prior assumptions from which it follows — and see whether you're willing to own those.

The lesson is that beliefs come in strength tiers, and the tier is often invisible from the belief itself. A comforting conviction may be nearly free — it follows from things you already grant. Another, equally comforting, may quietly require you to assume a whole benevolent order to the universe. Doing reverse mathematics on yourself means refusing to be charged for a cathedral of premises without noticing the bill — and, sometimes, discovering that a belief you cherish and one you resist are secretly the very same axiom, equivalent, standing or falling together.

Read as life lessons

How to price a conviction.

01

Price isn't obviousness

How self-evident a belief feels tells you nothing about its cost. Two claims can sound equally basic while one is free and the other buys a worldview. Only tracing the requirements reveals the tier.

02

Equivalence cuts both ways

If a belief is equivalent to its premise, you can't keep one and drop the other. Reject the premise and the cherished conclusion goes with it — they're one commitment, two faces.

03

Weaker is a virtue

The goal isn't the most powerful axioms but the fewest that still earn what you need. A conviction resting on a light base is robust; one resting on a cathedral falls with any stone.

In the wild

Where minimal assumptions matter.

FOUNDATIONS

Reverse math maps which parts of ordinary mathematics genuinely need infinite or non-computable machinery — and which are, at heart, finitistic or computable. It calibrates the real cost of the infinite.

COMPUTABILITY

The base system RCA₀ corresponds to computable mathematics; each rung up measures exactly how much non-computable “oracle” power a theorem demands. Strength becomes a resource you can meter.

PROOF & AI

Automated reasoning and proof assistants care about minimal hypotheses: the leanest assumption set makes proofs reusable and trustworthy. Charging only for what a result needs is good engineering, not just taste.

The mapping, exactly

Reverse math ↔ life.

Reverse mathLife
the base theory RCA₀What you'd grant anyway — the assumptions so cheap you don't notice paying them.
a theoremA belief or conviction you actually hold about how things are.
its minimal subsystemThe price: the weakest set of prior commitments that earns the belief.
equivalence over the baseBelief and premise are the same commitment — you can't keep one and disown the other.
the discrete Big FiveConvictions come in a few strength tiers, not a smooth gradient — cheap, or suddenly expensive.
everything weaker comes freePay for the strong premise and a whole layer of lesser beliefs is settled at once.

Where the metaphor tears

Three honest failures.

Beliefs aren't theorems.

Reverse math works because theorems and axioms have exact, formal statements and a precise notion of “proves.” A human conviction has no canonical formalization, no fixed base theory, and no agreed logic. The auditor gives you a discipline of asking — what does this rest on? — not a literal number for the cost of trusting your friend.

Not everything is one of five.

The Big Five are gloriously tidy, but they aren't the whole story: some theorems (many in combinatorics, like Ramsey's theorem for pairs) fall stubbornly between the rungs, or off the ladder entirely, in a wild zoo of incomparable strengths. Real life is more like the zoo than the staircase — clean tiers are the lucky case, not the rule.

Cheapest isn't truest.

A belief that requires few assumptions is more robust, but robustness is not correctness. You can hold a wrong belief on a feather-light base and a right one only at great cost. Auditing the price sharpens what you're committing to; it does not, on its own, tell you what's true — that audit is a separate one.