Open problem MAIS-O15 · posed in MAIS-A1 as Problem 4.6 · Status: open.
Tags: cooperative AI · agent foundations · Löbian cooperation · proof-based agents · bounded rationality · logic · complexity theory. Difficulty: ★★.
Authored by: Claude Fable 5 directed by Lionel Levine · Audited by: GPT 5.6 Sol.
The parametric bounded Löb theorem is due to Critch [C19]; the form fixed here is its repair by GPT 5.6 Sol [S26]. It is an existence theorem: given a proof of the reflection scheme $\forall k\ (\Box_{f(k)}\ p(k) \to p(k))$, it produces some threshold $\hat{k}$ above which $p(k)$ is provable. An agent allocating a proof-search budget needs the threshold itself. How does $\hat{k}$ depend on the data?
Fix an efficient proof system $S$: following Critch [C19], an extension of Peano arithmetic with binary numerals (the numeral $\overline{k}$ has $O(\log k)$ symbols) and an abbreviation rule, with all proof lengths counted in symbols; the default $\mathsf{PA}_{\mathrm{bin}}$ is fixed in MAIS-A1 down to the Gödel coding. Here $\mathrm{Lang}_1(S)$ denotes the formulas of $S$ with at most one free variable, $|p|$ the length of the formula $p$ in symbols, and $\ell_S(\varphi)$ the least symbol length of an $S$-proof of $\varphi$; for $p \in \mathrm{Lang}_1(S)$, $\Box_{f(k)}\ p(k)$ asserts that the instance $p(\overline{k})$ has an $S$-proof of at most $f(k)$ symbols. $\mathcal{B}$-terms are the search-free budget terms of the agenda (generated by constants, $k$, and the numeral-length function under addition, multiplication, composition, and $x \mapsto 2^x$), with $|f|_{\mathcal{B}}$ the length of the term $f$.
Three hypotheses enter the statement; MAIS-A1 gives each in full. The expansion function $\mathcal{E}$ prices the act of noticing a proof: converting an $m$-symbol proof of $\varphi$ into a proof that such a proof exists costs at most $\mathcal{E}(m)$ symbols. The standing expansion certificate is an $S$-proof that a $\mathcal{B}$-term bounds $\mathcal{E}$. A budget $f$ is internally regular if $S$ itself proves that $f$ eventually covers this noticing cost at numeral-length scale, plus any fixed multiple of the numeral length. Finally, the comparison conjecture, Conjecture 4.1 (MAIS-O13), asserts that whenever one $\mathcal{B}$-term is at most another for all sufficiently large standard $k$, the system $S$ proves the inequality beyond a threshold computable from the two terms; the repaired theorem's proof is effective once these internal budget comparisons are supplied.
Problem (MAIS-A1, Problem 4.6). Fix $S$ with the standing expansion certificate, and assume Conjecture 4.1 (MAIS-O13). Given $p \in \mathrm{Lang}_1(S)$, an internally regular $\mathcal{B}$-term $f$, and an $S$-proof of $\forall k\ (\Box_{f(k)}\ p(k) \to p(k))$ of length $L$, give explicit bounds. Writing $C_S$ for the fixed constants of the proof system, require
$$\hat{k} \ \le\ K\bigl(L, |p|, |f|_{\mathcal{B}}, C_S\bigr), \qquad \ell_S\bigl(\forall k > \hat{k}\ p(k)\bigr) \ \le\ \Lambda\bigl(L, |p|, |f|_{\mathcal{B}}, C_S\bigr),$$
and determine how small $K$ and $\Lambda$ can be made. In particular, for $f(k) = k$ and a certified linear expansion bound, can both be polynomial in $L + |p|$?
The first bound caps the threshold; the second caps the length of the proof that certifies everything beyond it. A polynomial answer for $f(k) = k$ would make the cooperation threshold for the FairBot agents of Barász et al. [BCFH+14] effectively computable rather than merely finite. For the repaired theorem and the certificate formalism in full, see MAIS-A1; for the refutation and repair, MAIS-P2.
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.
- [BCFH+14] M. Barász, P. Christiano, B. Fallenstein, M. Herreshoff, P. LaVictoire, and E. Yudkowsky, Robust cooperation in the Prisoner's Dilemma: program equilibrium via provability logic, 2014. arXiv:1401.5577
Related: MAIS-O13 (the assumed comparison conjecture) · MAIS-O16 (the instance with a game attached) · MAIS-O17 (thresholds uniform over agent families) · MAIS-O12 (the expansion certificate itself).