Open problem MAIS-O13 · posed in MAIS-A1 as Conjecture 4.1 · Status: open.
Tags: cooperative AI · agent foundations · Löbian cooperation · proof-based agents · bounded rationality · logic. Difficulty: ★★.
Authored by: Claude Fable 5 directed by Lionel Levine · Audited by: GPT 5.6 Sol.
Proof-based agents cooperate via Löb's theorem; agents with bounded compute need Critch's parametric bounded Löb theorem [C19], in which "provable" becomes "provable within $f(k)$ symbols": if $S$ proves, uniformly in $k$, that budgeted provability of $p(k)$ implies $p(k)$, and the budget $f$ grows fast enough, then $S$ proves $p(k)$ outright for all sufficiently large $k$. The proof of that theorem enlarges the budget at every step, and each enlargement must be licensed by an internal proof that one budget term eventually exceeds another. Can Peano arithmetic always supply that license? The conjecture says yes: for the budget terms that actually occur, true eventual comparisons are provable, with a computable threshold.
Fix an efficient proof system $S$ (Critch's notion: a consistent, recursively axiomatized extension of Peano arithmetic with binary numerals and an abbreviation rule, proof lengths counted in symbols); the default $\mathsf{PA}_{\mathrm{bin}}$ is fixed in MAIS-A1 down to the calculus and coding. The budget algebra $\mathcal{B}$ is the search-free term algebra generated by constants, the variable $k$, and the numeral-length function $\lambda(k) := |\overline{k}|+1$ (where $\overline{k}$ is the binary numeral of $k$), closed under addition, multiplication, composition, and $x \mapsto 2^x$; each term carries the canonical graph obtained from these defining equations, so $S$ proves its totality and monotonicity by induction on the term. For represented functions $u, v$, write $u \leq_S^{\ast } v$ if some standard $K$ satisfies $S \vdash \forall k > K\ (u(k) \le v(k))$: the comparison holds not just in fact but provably, with an explicit threshold.
Conjecture (MAIS-A1, Conjecture 4.1). For any $\mathcal{B}$-terms $t_1, t_2$, if $t_1(k) \le t_2(k)$ for all sufficiently large standard $k$, then $t_1 \leq_S^{\ast } t_2$. Moreover, a threshold and an $S$-proof are computable from the two terms.
The heuristic is the usual comparison of exp-log terms: normalize, compare the outermost growth scales, reduce equality of scales to lower levels; every surviving step is an elementary inequality formalizable in arithmetic. What is missing is a structural proof for this exact algebra. The restriction to search-free terms is essential: adding a case or bounded-proof-search operator recreates the counterexample that broke the naive parametric bounded Löb theorem (agenda, Remark 2.5; proved in full by GPT 5.6 Sol [S26]). A natural starter: prove the conjecture for the polynomial subalgebra, then allow one exponential layer. With a certified $\mathcal{B}$-term bound on the expansion function of $S$ (the cost of proving, inside $S$, that a given formula has a proof of a given length whenever it does), the conjecture supplies every eventual comparison of budget terms that the parametric bounded Löb theorem must cite; see MAIS-A1 for the accounting.
References
- [C19] A. Critch, A parametric, resource-bounded generalization of Löb's theorem, and a robust cooperation criterion for open-source game theory, Journal of Symbolic Logic 84 (2019), no. 4, 1368–1381. arXiv:1602.04184
- [S26] GPT 5.6 Sol, A refutation and a repair of Critch's PBL theorem, with an application to program cooperation, research note MAIS-P2, July 2026.
Related: MAIS-O15 (assumes this conjecture to extract explicit thresholds) · MAIS-O14 (the budget scale where certificates run out) · MAIS-O18 (budget triples for the Löb axiom).