Open problem MAIS-O18 · posed in MAIS-A1 as Problem 5.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.
Löb's theorem has two strengths. The rule — from $\vdash \Box P \to P$ infer $\vdash P$ — is what the parametric bounded Löb theorem of Critch [C19] quantifies, and it is the engine of Löbian cooperation: agents with bounded compute cooperating because each finds a short proof about the other's behavior. The axiom is its internalization, $\Box(\Box P \to P) \to \Box P$, one box deeper; it is what a bounded provability logic — the natural setting for reasoning about such proof-based agents — would need as its Löb axiom. Which proof budgets make the bounded axiom hold?
Fix an efficient proof system $S$: following Critch [C19], a consistent recursively axiomatized extension of Peano arithmetic with binary numerals and proof-level abbreviations, so that proof length in symbols is a fair cost measure; the default calculus $\mathsf{PA}_{\mathrm{bin}}$ is fixed in full in MAIS-A1. For $p \in \mathrm{Lang}_1(S)$ (at most one free variable) and a budget $a$, the formula $\Box_{a(k)}\ p(k)$ asserts that the instance $p(\overline{k})$ (with $\overline{k}$ the binary numeral of $k$) has an $S$-proof of at most $a(k)$ symbols.
The budgets range over $\mathcal{B}$, a search-free term algebra generated by constants, $k$, and the numeral-length budget $\lambda(k) := |\overline{k}|+1$, closed under addition, multiplication, composition, and $x \mapsto 2^x$; each term carries a canonical graph whose totality and monotonicity $S$ proves. More generally, an internally certified represented budget is a computable budget for which $S$ proves the totality, monotonicity, and comparison facts its use consumes; the exact grammar and certificate conventions live in the agenda. Here $u \leq_S^{\ast } v$ means $S$ proves $u(k) \le v(k)$ for all $k$ beyond some standard threshold. The lower bound on $b$ in the statement removes a cheap obstruction: with $p = \bot$ and $a = c = 0$, taking $b$ the length of a fixed proof of $\Box_0 \bot \to \bot$ makes the antecedent provable and the consequent refutable.
Problem (MAIS-A1, Problem 5.1). Fix an efficient $S$. Determine for which triples of $\mathcal{B}$-terms $(a, b, c)$, and more generally which triples of internally certified represented budgets, it holds that for every $p \in \mathrm{Lang}_1(S)$ there is $\hat{k}$ with
$$S \vdash \forall k > \hat{k}\ \Bigl(\Box_{b(k)}\bigl(\Box_{a(k)}\ p(k) \to p(k)\bigr) \ \to\ \Box_{c(k)}\ p(k)\Bigr).$$
Restrict first to $\mathcal{B}$-terms satisfying $\lambda \leq_S^{\ast } b$, so the outer box is not a fixed finite search. Prove that some triple of polynomials works for $\mathsf{PA}_{\mathrm{bin}}$, and for given $(a, b)$ characterize the admissible $c$. (The admissible $c$ need not have a least element pointwise; for polynomial $c$, determine the least admissible degree.)
In words: whenever the reflection instance at budget $a$ has a proof within budget $b$, the sentence itself must have a proof within budget $c$, and $S$ proves this uniformly for all large $k$. The parametric bounded Löb theorem, in the repaired form proved by GPT 5.6 Sol [S26], is the rule form: a uniform proof of $\Box_{f(k)}\ p(k) \to p(k)$, for $f$ growing fast enough in an internally certified sense, yields a uniform proof of $p(k)$. The present problem is the statement that theorem would become if its implication moved inside the box. It is also the crux of bounded provability logic: Critch [C19] conjectured that every law of Gödel–Löb logic $\mathsf{GL}$ survives when each box receives a polynomial budget (MAIS-O19), and in the heuristic proof plan — induction on a $\mathsf{GL}$-derivation, with Critch's bookkeeping lemmas covering the other axioms and rules — the Löb axiom is the case carrying the real content. For the conventions and that reduction, see MAIS-A1.
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-O19 (bounded GL soundness, whose Löb-axiom case this is) · MAIS-O15 (the rule-form counterpart with explicit thresholds) · MAIS-O13 (the budget comparisons the certificates need).