Bounded Arithmetic

Arithmetic is the study of the natural numbers. Most of us learn it as a domain of absolute truths — "you can always add one more" and "every number has a unique factorization." But what if you are only allowed to count up to a polynomial? What theorems survive?

Bounded arithmetic is a family of weak logical theories that answer exactly this question. Instead of allowing full mathematical induction over all formulas, each theory restricts induction to a tightly bounded class of predicates — predicates that correspond to checking membership in a specific complexity class.

The result is a beautiful mirror: the classic complexity ladder (P, NP, the polynomial hierarchy) reappears inside logic as a ladder of theories, each able to prove slightly more than the one below. The foundational hierarchy was introduced by Samuel Buss in 1986, and the study of these theories — called proof complexity — is now central to understanding P vs NP.

Each theory in the bounded arithmetic hierarchy can prove statements about numbers, but only using predicates from a matching complexity class. Pick a statement below and see which level of the hierarchy is strong enough to prove it — and which levels fall short.

<p class="hint">{{hint}}</p>
<div class="controls">
  <label for="stmt-select">{{choose_stmt}}</label>
  <select id="stmt-select"></select>
</div>
<div class="hierarchy" id="hierarchy"></div>
<div class="detail-box" id="detail-box">
  <div class="detail-title" id="detail-title"></div>
  <div class="detail-body" id="detail-body"></div>
</div>
<div class="btns">
  <button id="btn-check" type="button">{{btn_check}}</button>
  <button id="btn-reset" type="button" class="ghost">{{btn_reset}}</button>
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; font-size: 14px; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .7rem; line-height: 1.45; }
.controls { margin-bottom: .8rem; }
label { font-weight: 600; margin-right: .5rem; }
select { font: 14px system-ui, sans-serif; padding: .35rem .5rem; border: 1px solid #aaa;
         border-radius: 6px; background: #f8f9fa; cursor: pointer; max-width: 100%; }
.hierarchy { display: flex; gap: 6px; flex-wrap: wrap; margin: .6rem 0 .8rem; align-items: center; }
.theory { padding: .35rem .7rem; border-radius: 8px; border: 2px solid #cdd9e3;
          background: #e8eef3; font-weight: 700; font-size: .85rem; cursor: pointer;
          transition: all .18s; user-select: none; min-width: 52px; text-align: center; }
.theory:hover { border-color: #1d3557; }
.theory.can-prove { background: #0a7d33; border-color: #087d2f; color: #fff; }
.theory.cannot-prove { background: #e63946; border-color: #c92f3c; color: #fff; }
.theory.unknown { background: #f4a261; border-color: #e07b35; color: #fff; }
.arrow { color: #aaa; font-size: 1.1rem; line-height: 1; }
.detail-box { background: #f0f4f7; border: 1px solid #cdd9e3; border-radius: 8px;
              padding: .6rem .8rem; min-height: 54px; margin-bottom: .7rem; }
.detail-title { font-weight: 700; margin-bottom: .25rem; color: #1d3557; font-size: .9rem; }
.detail-body { font-size: .85rem; line-height: 1.45; color: #333; }
.legend { display: flex; gap: .8rem; flex-wrap: wrap; margin-top: .5rem; }
.leg { display: flex; align-items: center; gap: .35rem; font-size: .78rem; }
.leg-dot { width: 12px; height: 12px; border-radius: 3px; flex-shrink: 0; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; }
button { font: 600 13px system-ui, sans-serif; padding: .45rem .9rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }

// Code not found

Notice the pattern: polynomial-time predicates live in $S_2^1$ (the base theory corresponding to P), NP predicates live in $T_2^1$ (matching NP $\cap$ co-NP), and higher levels shadow $\Sigma_2^p, \Pi_2^p$ and so on. Just as in P vs NP, we strongly believe these theories form a strict hierarchy, but no one has proved the separations.

How hard is it to understand bounded arithmetic? In a very precise sense, as hard as the biggest open problem in computer science.

• The Buss hierarchy (1986). Samuel Buss defined a sequence of theories $S_2^1 \subseteq T_2^1 \subseteq S_2^2 \subseteq T_2^2 \subseteq \cdots$ where each $S_2^i$ (resp. $T_2^i$) allows induction over $\Sigma_i^b$ (resp. $\Pi_i^b$) predicates — exactly the bounded formulas that capture the $i$-th level of the polynomial hierarchy $\Sigma_i^p$.
• Status: open. We do not know whether these theories are genuinely distinct. It is widely believed they form a strict hierarchy, but no separation proof exists. Proving $S_2^1 \subsetneq T_2^1$ would already be a landmark result — it would imply P $\neq$ NP or at minimum a major structural insight about the polynomial hierarchy.
• The Witnessing Theorem. Buss proved that every function provably total in $S_2^1$ is computable in polynomial time (P), and every function provably total in $T_2^1$ is in FNP (polynomial-time verifiable). This is the formal bridge: the theorems of a bounded theory perfectly capture the computations of the matching complexity class.
• Cook–Nguyen (2010). A later landmark — the book Logical Foundations of Proof Complexity by Stephen Cook and Phuong Nguyen — extended the framework with a single base theory V⁰ for AC⁰ and a whole two-sorted hierarchy matching each level of NC and the log-space classes, making the mirror between logic and complexity almost perfectly clean.

This is an open problem — the separations are as conjectured, not proven. But the framework is already enormously useful: it gives a formal language for asking what kind of reasoning is truly needed to prove a given computational fact.

"What can be proved with only polynomial-time reasoning?" turns out to be one of the most practically loaded questions in logic:

• Proof complexity: every propositional proof system (Resolution, Frege, Extended Frege…) corresponds to a fragment of bounded arithmetic. Understanding proof length is equivalent to asking which bounded theory proves the relevant tautology. This is the main lens for attacking P vs NP from the logical side.
• Cryptographic hardness: one-way functions, pseudorandom generators and public-key cryptography rest on the assumption that certain problems have no polynomial-time solutions. Bounded arithmetic gives a logical home for these assumptions — if $S_2^1 = T_2^1$ (theories collapse), the cryptographic world would crumble.
• Automated reasoning: SAT solvers and automated theorem provers implicitly work inside fragments of bounded arithmetic. Understanding the limits of these fragments explains why some tautologies are hard to find short proofs for — and guides the design of better proof strategies.
• Feasible mathematics: the field asks which classical theorems of number theory, combinatorics and analysis can be proved without non-constructive existence arguments. Bounded arithmetic is its formal framework — a theorem provable in $S_2^1$ is one whose proof can be turned into a polynomial-time algorithm.

The hierarchy also illuminates integer programming and SAT: the reason short proofs of NP-hardness reductions are so elusive is precisely that they require induction axioms beyond the base theory.

Bounded arithmetic is the place where mathematical logic and computational complexity shake hands. By restricting induction to bounded predicates, Buss's 1986 hierarchy created a formal mirror of the polynomial-time universe — a ladder of theories, each provably total function in $S_2^i$ landing exactly in the matching complexity class.

The hierarchy is conjectured to be strict, but every attempted separation runs into the same wall as P vs NP. That is not a coincidence: the two questions are deeply intertwined, and progress on one would almost certainly illuminate the other.

So the next time you wonder whether a mathematical proof is truly efficient, ask which bounded theory it lives in. The answer tells you not just how hard the computation is, but how much logical power the reasoning actually consumed.