🔢 mathematics

Toward a Characterization of Simulation Between Arithmetic Theories

This paper investigates the conditions under which a sound arithmetic theory efficiently simulates its true extensions by establishing unconditional constraints on such simulations, linking them to interpretability and Busy Beaver functions, and proposing a central conjecture that the failure of elementary consistency implications implies super-polynomial proof complexity for bounded consistency statements.

Original authors: Hunter Monroe

Published 2026-07-21

📖 7 min read🧠 Deep dive

CC BY 4.0

Original authors: Hunter Monroe

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are a detective trying to solve a mystery inside a giant, infinite library. This library isn't filled with books about dragons or space travel, but with the fundamental rules of math itself. In this world, there are different "rulebooks" (called theories) that tell you what is true and what is false. Some rulebooks are small and simple, while others are massive and powerful. The big question in this corner of science—called computational complexity and logic—is: Can a smaller, simpler rulebook quickly prove that a bigger, more powerful rulebook isn't broken?

Think of a "broken" rulebook as one that accidentally proves that 2 + 2 = 5. If a rulebook is "sound," it never makes that mistake. But sometimes, a small rulebook might not be able to prove that a big rulebook is safe. It's like a junior detective trying to prove that the Chief Detective is innocent. The junior detective has a limited toolkit and a strict time limit. If the Chief Detective is actually innocent, can the junior detective find a quick, short proof of that fact, or does the proof have to be so long and complicated that it would take a million years to write down? This paper asks: When does the junior detective have a shortcut, and when are they stuck with a mountain of work?

The Great Detective Game: Can a Small Rulebook Simulate a Big One?

In this paper, Hunter Monroe acts like a detective investigating the relationship between these mathematical rulebooks. The goal is to figure out when a smaller theory (let's call it S) can "simulate" a bigger theory (let's call it S + ϕ). In detective speak, "simulating" means: Can S quickly prove that S + ϕ is safe from contradictions?

The paper explores a specific scenario: S is a sound (never wrong) theory that can check its own rules quickly. ϕ (phi) is a true statement that S doesn't know about yet. When we add ϕ to S, we get a new, stronger theory. The question is: Does S have a fast, efficient way to prove that this new, stronger team isn't going to crash and burn?

The "Easy" Case: When the Junior Detective Has a Map

The paper starts by confirming something we already know: sometimes, the junior detective does have a shortcut. If the bigger theory is just a "translation" of the smaller one (mathematicians call this an "interpretation"), then S can easily prove the bigger theory is safe. It's like if the Chief Detective's rulebook was just the Junior Detective's rulebook written in a different language. The Junior Detective can just translate the rules back and forth to prove everything is fine.

The authors prove that if a weak, basic math system (called EA) can see that adding ϕ doesn't break the rules, then the Junior Detective S can definitely find a fast proof. This is the "easy zone."

The "Hard" Case: The Busy Beaver Trap

But what if the bigger theory is not just a translation? What if ϕ is a truly new, mysterious fact? The paper argues that in these cases, the Junior Detective is usually stuck.

To prove this, the authors use a clever trick involving something called the Busy Beaver function. Imagine a contest where you build a tiny robot (a Turing machine) with a specific number of states (like buttons or switches). The goal is to make the robot run for as long as possible before it stops. The "Busy Beaver number" for a robot with k buttons is the maximum number of steps it can take before stopping.

Here's the kicker: For a large enough k, knowing the exact Busy Beaver number is like holding a magic key that unlocks the secrets of almost any math system. The paper shows that if the Junior Detective S fails to simulate any true, hard extension, it will also fail to simulate the theory that includes the Busy Beaver number for a sufficiently large k.

It's as if the Junior Detective is trying to prove the Chief is innocent, but the Chief's safety depends on a secret that only a super-computer with a million buttons could figure out. The Junior Detective, with their small toolkit, simply cannot access that information quickly. The paper suggests that these "Busy Beaver" facts are the ultimate test: if you can't handle them, you can't handle the hard stuff.

The Big Conjecture: The "No Free Lunch" Rule

The paper doesn't just list examples; it proposes a grand theory called Higher Relative Consistency (HRC). This is the paper's main idea, though it's presented as a strong guess (a conjecture) rather than a proven fact.

The HRC conjecture says: There is no magic shortcut.

If the weak, basic math system (EA) cannot prove that adding ϕ keeps the rules safe, then the Junior Detective S will never be able to find a fast proof that the new theory is safe. The only time a fast proof exists is when the safety of the new theory is already visible to the weakest, most basic math system.

Think of it like this: If the Junior Detective can't see the safety of the new team using their basic flashlight, they aren't going to find a secret tunnel to the answer. The paper suggests that "hard" problems are hard precisely because the information needed to solve them is hidden from the basic math system.

The "Busy Beaver" and "Random String" Barriers

The paper also looks at two other types of "hard" information:

Busy Beaver values: As mentioned, these are the maximum runtimes of tiny robots.
Kolmogorov-random strings: These are strings of numbers that are so random they have no pattern or short description. You can't compress them; you just have to write them all out.

The authors suggest that if you try to add a Busy Beaver number or a truly random string to your rulebook, and the basic math system can't explain why it's safe, then the Junior Detective will be stuck with a proof that takes forever. It's like trying to prove a random sequence of numbers is "safe" without a pattern to follow; you just have to check every single possibility, which takes too long.

What the Paper Rules Out

The paper is careful to say what it doesn't prove. It doesn't say that fast proofs definitely don't exist for these hard cases; it just says that if they do exist, they would be a total mystery. The paper rules out the idea that there could be a "hidden" fast proof that the basic math system can't see. If a fast proof exists, the basic system must be able to see why it works. If the basic system is blind to the safety of the new theory, then the fast proof doesn't exist.

The Bottom Line

This paper is a map of the "easy" and "hard" zones in the world of mathematical proofs. It suggests that the boundary between easy and hard is drawn by a simple rule: Can the weakest math system see that the new theory is safe?

If the answer is yes, the Junior Detective has a fast shortcut. If the answer is no, the Junior Detective is stuck with a mountain of work that grows exponentially. The paper proposes that this rule (HRC) is the key to understanding why some math problems are easy and others are impossibly hard, using the "Busy Beaver" robot contest as the ultimate test of who has the real power.

While the paper doesn't solve the mystery completely (it leaves the final verdict as a conjecture), it provides a very strong framework for thinking about it. It tells us that if we ever find a fast proof for a truly hard problem, it will be because we finally found a way to explain it using the simplest tools of math. If we can't explain it simply, we probably can't prove it quickly.

Technical Summary: Toward a Characterization of Simulation Between Arithmetic Theories

Problem Statement
The paper addresses the "Characterization Problem" in proof complexity: determining when a sound arithmetic theory $S$ (where $S \supseteq S^1_2$ and axioms are polynomial-time decidable) efficiently proves the bounded consistency statements $\text{Con}_{S+\phi}(n)$ for a true sentence $\phi$ independent of $S$ . Here, $\text{Con}_{S+\phi}(n)$ asserts that $S+\phi$ has no proof of $0=1$ within $n$ symbols.

From the perspective of proof complexity, this asks when $S$ , viewed as a proof system, simulates $S+\phi$ . The paper distinguishes between:

Simulation: $S \vdash^{n^{O(1)}} \text{Con}_{S+\phi}(n)$ , meaning there exist polynomial-size $S$ -proofs for the family of bounded consistency statements.
Non-simulation (Hardness): For every constant $c$ , $S \nvdash^{n^c} \text{Con}_{S+\phi}(n)$ , meaning no polynomial-size proofs exist.

The central challenge is to identify a necessary and sufficient criterion for $\phi$ that governs whether simulation occurs. While independence alone does not preclude simulation (as some independent $\phi$ allow polynomial-time interpretation), the existence of optimal proof systems is unknown; if none exist, non-simulation must occur for some $\phi$ .

Methodology and Framework
The paper operates within sound arithmetic theories extending $S^1_2$ , utilizing standard arithmetization of syntax. It distinguishes between:

External Simulation: The existence of short proofs in the standard model.
Internal Certification: Whether a base theory $B$ (e.g., Elementary Arithmetic, EA) proves the existence of such proofs.
Relative Consistency: The implication $\text{Con}_S \to \text{Con}_{S+\phi}$ formalized in a weak base theory like EA.

The methodology relies on:

Proof Translation: Using interpretations to translate proofs between theories.
Busy Beaver Reductions: Utilizing exact Busy Beaver values ( $\phi_{BB(k)}$ ) as canonical sources of unprovable information.
Kolmogorov Complexity: Analyzing random axioms ( $x \in R$ ) to isolate information-theoretic obstructions.
Certification Theorems: Establishing unconditional links between a base theory proving a simulation statement and that base proving a relative-consistency implication.

Key Contributions and Results

1. Unconditional Constraints on Characterization
The paper establishes several unconditional results that constrain any potential characterization of simulation:

Sufficient Condition for Simulation (Theorem 3.4): For finitely axiomatized sequential theories $S$ , if $\text{EA} \vdash \text{Con}_S \to \text{Con}_{S+\phi}$ , then $S$ simulates $S+\phi$ . This relies on the Friedman–Visser interpretability criterion and proof translation, showing that relative consistency in a weak base implies feasible relative consistency (polynomial-time proof translation).
Busy Beaver Transfer (Theorem 3.10): If there exists any true sentence $\phi$ for which $S$ fails to simulate $S+\phi$ , then for all sufficiently large $k$ , $S$ also fails to simulate $S^1_2 + \phi_{BB(k)}$ . This demonstrates that non-simulation, if it exists, is witnessed by canonical Busy Beaver extensions of the weak base.
Extension Normal Form (Lemma 3.14): Any hardness for a consistent target theory $T$ can be recoded as hardness for the one-sentence extension $S + \text{Con}_T$ .
Certification Barriers (Theorem 6.3): If a base theory $B$ proves that $S$ simulates $U$ (uniformly for large $n$ ), then $B \vdash \text{Con}_S \to \text{Con}_U$ . Consequently, if $B$ cannot prove the relative-consistency implication, it cannot certify the simulation. This yields unconditional results that EA cannot certify simulations for extensions by $\text{Con}_S$ , exact Busy Beaver facts, or most Kolmogorov-random axioms.

2. The Central Conjecture: Higher Relative Consistency (HRC)
Motivated by the gap between the sufficient condition (Theorem 3.4) and Pudlák's conjecture (that $S$ does not simulate $S+\text{Con}_S$ ), the paper proposes Higher Relative Consistency (HRC) as a characterization:

HRC (Conjecture 5.1): For a sound, finitely axiomatized sequential $S$ and true $\phi$ , if $\text{EA} \nvdash \text{Con}_S \to \text{Con}_{S+\phi}$ , then for every constant $c$ , $S \nvdash^{n^c} \text{Con}_{S+\phi}(n)$ .
Equivalence to Feasible Reflection (FR): HRC is the contrapositive of Feasible Reflection, which posits that if $S$ simulates $S+\phi$ , then $\text{EA} \vdash \text{Con}_S \to \text{Con}_{S+\phi}$ .
Implications: Under HRC, simulation occurs exactly when the weak base can certify that adjoining $\phi$ $ϕ$ preserves consistency. This unifies various hardness phenomena:
- Pudlák's Conjecture: Follows immediately, as $\text{EA} \nvdash \text{Con}_S \to \text{Con}_{S+\text{Con}_S}$ .
- Kolmogorov Hardness (KH): For random axioms $x \in R$ , simulation fails unless $\text{EA} \vdash \text{Con}_S \to \text{Con}_{S+(x \in R)}$ . By Chaitin's Incompleteness Theorem, this holds for only finitely many $x$ , implying almost all random axioms yield hard extensions.
- Busy Beaver Hardness: For sufficiently large $k$ , $\phi_{BB(k)}$ yields non-simulation unless the relative consistency is visible in EA.

3. Finite-Scale and Pairwise Extensions
The paper explores stronger, finite-scale conjectures (SETH-K-Finite) suggesting that hardness is not just asymptotic but exponential beyond a uniform threshold. It further proposes "Pairwise SETH-K-Finite," asserting that independently random axioms do not help one another; adjoining $y \in R$ does not yield short proofs for $\text{Con}_{S+(x \in R)}(n)$ if $x$ and $y$ are mutually conditionally random.

4. Distinction Between External Simulation and Internal Certification
A significant technical contribution is the separation of external simulation (truth in the standard model) from internal certification (provability in a base theory). The paper proves that while a counterexample to Feasible Reflection would require an externally true simulation that EA cannot certify, the mere failure of EA to certify a simulation does not prove that the simulation fails externally. This distinction clarifies that the "Certification Barriers" are limits on what weak bases can prove, not necessarily absolute lower bounds on proof lengths.

Significance and Claims
The paper does not claim to solve the Characterization Problem or prove HRC. Instead, it claims to:

Isolate Constraints: Identify unconditional structural constraints (Busy Beaver transfer, certification barriers) that any successful characterization must satisfy.
Propose a Structural Picture: Offer HRC as a "natural" organizing principle where the failure of weak-base relative consistency is the exact obstruction to simulation.
Unify Hardness Sources: Demonstrate that canonical sources of unprovable information (Busy Beaver values, Kolmogorov randomness) are not merely convenient encodings but reflect a structural barrier: simulation fails when it requires access to true information that the base theory cannot recover via public proof-theoretic descriptions.
Refine the Landscape: Show that if HRC holds, the problem of finding hard tautologies reduces to a relative-consistency classification problem, where "easy" extensions are exactly those explained by weak-base relative consistency, and all others are hard.

The paper concludes that proving HRC would be a major breakthrough, converting relative consistency from a sufficient condition into a full characterization, but acknowledges that such a proof would likely require resolving central open problems in complexity theory (e.g., the non-existence of optimal proof systems).