See comments. This is a rediscovery of a result from the 1980's that allow concluding $\varphi$ from ${\square }_n\left(\varphi \right)$ via a $O\left(n\right)$-length proof, and even the statement that the theory has no disproof of length $n$ or less has a single $O\left(n\right)$-length proof. This is not vulnerable to Critch's Bounded Parametric Lob proof, and was created by looking for ways to make it fail.

This result is just an idea developed very recently, and I'd put ~2:1 odds on it having a fatal flaw, but it looks extremely promising if it works out. EDIT: It works. None of the proof theory checks have been done yet, but it does causes both Lob's theorem, and Critch's Bounded Parametric Lob result to fail.

So, to begin with, if a theory thinks it is sound, then it is inconsistent. Proof by Lob's theorem.

$$⊢\square \perp \to \perp \Rightarrow ⊢\perp$$

Well that didn't work.

What if we give the theory a soundness schema over any proof which is of bounded length? Maybe the "there exists a proof" in the standard provability predicate is causing problems.

Well then Critch's Bounded Parametric Lob comes in to ruin our day. The entire proof will be reproduced below.

Let $g\left(k\right)$, $f\left(k\right)$, and $h\left(k\right)$ be such that $f\left(k\right)\ge g\left(k\right)+h\left(k\right)+\log \left(k\right)$, $Eg\left(k\right)<h\left(k\right)$, and $\log \left(f\right(k\left)\right)<g\left(k\right)$, asymptotically.

As a specific example, this can be done by $g\left(k\right)=k$, $h\left(k\right)=k^2$, and $f\left(k\right)=k^3$.

If it takes a constant number of steps to derive a specific proof regardless of $k$, the number on it will be suppressed for readability. Also, technically, the original proof has $O\log \left(k\right)$ instead of $\log \left(k\right)$, but this change doesn't alter much.

$$G(\lceil \psi \rceil ,k):={\square }_{g\left(k\right)}\psi \left(k\right)\to \perp$$ $$⊢\forall k:\psi \left(k\right)\leftrightarrow G(\lceil \psi \rceil ,k)$$ (Parametric Diagonal Lemma) $$⊢\square \forall k:\psi \left(k\right)\leftrightarrow G(\lceil \psi \rceil ,k)$$ (Bounded Necessitation) $$⊢\forall k:{\square }_{\log \left(k\right)}\left(\psi \right(k)\to G(\lceil \psi \rceil ,k\left)\right)$$ (Quantifier Distribution) $$⊢\forall k,a:{\square }_a\psi \left(k\right)\to {\square }_{a+\log \left(k\right)}G(\lceil \psi \rceil ,k)$$ (Implication Distribution) $$⊢\forall k,a,b:{\square }_a\psi \left(k\right)\to \left({\square }_b{\square }_{g\left(k\right)}\psi \right(k)\to {\square }_{a+b+\log \left(k\right)}\perp )$$ (Implication Distribution) Now specialize to a=g(k), b=h(k). Also, $f\left(k\right)\ge g\left(k\right)+h\left(k\right)+\log \left(k\right)$ for sufficiently large k above $k_1$. $$⊢\forall k>k_1:{\square }_{g\left(k\right)}\psi \left(k\right)\to \left({\square }_{h\left(k\right)}{\square }_{g\left(k\right)}\psi \right(k)\to {\square }_{f\left(k\right)}\perp )$$ $$⊢\forall k,a:{\square }_a\psi \left(k\right)\to {\square }_{Ea}{\square }_a\psi \left(k\right)$$ (Bounded Inner Necessitation) Now, Specializing to a=g(k), we get $$⊢\forall k:{\square }_{g\left(k\right)}\psi \left(k\right)\to {\square }_{Eg\left(k\right)}{\square }_{g\left(k\right)}\psi \left(k\right)$$ Now, since $Eg\left(k\right)<h\left(k\right)$ after some time $k_2$, $$⊢\forall k>k_2:{\square }_{g\left(k\right)}\psi \left(k\right)\to {\square }_{f\left(k\right)}\perp$$ Pick a specific value of k, $k^{\prime }$, which is sufficiently large. $$⊢{\square }_{g\left(k^{\prime }\right)}\psi \left(k^{\prime }\right)\to {\square }_{f\left(k^{\prime }\right)}\perp$$ By the soundness schema, ${\square }_{f\left(k^{\prime }\right)}\perp \to \perp$. The length of this proof isn't constant, because $f\left(k^{\prime }\right)$ might be really big, so then it'd take about $\log \left(f\right(k^{\prime }\left)\right)$ characters to write down the single application of the soundness schema. $${⊢}_{\log \left(f\right(k^{\prime }\left)\right)}{\square }_{g\left(k^{\prime }\right)}\psi \left(k^{\prime }\right)\to \perp$$ $${⊢}_{\log \left(f\right(k^{\prime }\left)\right)}\psi \left(k^{\prime }\right)$$ (By the definition of $\psi \left(k^{\prime }\right)$) $${⊢}_{E\log \left(f\right(k^{\prime }\left)\right)}{\square }_{\log \left(f\right(k^{\prime }\left)\right)}\psi \left(k^{\prime }\right)$$ $\log \left(f\right(k\left)\right)<g\left(k\right)$ eventually. Since $k^{\prime }$ was previously selected to be sufficiently big, $${⊢}_{E\log \left(f\right(k^{\prime }\left)\right)}{\square }_{g\left(k^{\prime }\right)}\psi \left(k^{\prime }\right)$$ Now we no longer care about $\log \left(f\right(k^{\prime }\left)\right)$'s size, because $k^{\prime }$ has been fixed, so $$⊢\perp$$

However, not all is lost. If you look carefully at this, you see that the introduction of the soundness scheme lead to a minor proof blowup. Sure, it's not enough of a blowup to surpass $g\left(k\right)$, so the proof of $\perp$ still goes through, but this seems like it might be exploitable....

So then the next step is to make sure that ${\square }_n\varphi \to \varphi$ can only ever be proved by a proof of $n$ steps or more. The agent can conclude its own soundness for bounded proofs, but it may take a while. I'm pretty sure this is doable by having an axiom schema of the form ${\square }_n\varphi \to {\square }_{n-1}\varphi$ for each individual $n$ and $\varphi$ seperately, but I'm not entirely sure of that. EDIT: Doesn't work, see comments.

Regardless, assume that any proof of ${\square }_n\varphi \to \varphi$ via iterated soundness axioms will always take $c$ or more steps. EDIT: You don't need to assume this, there's an explicit $O\left(n\right)$ proof of that statement.

Then, if we go through the proof again, something interesting happens. Instead of $\log \left(f\right(k\left)\right)$ making its way to the length of the proof, we get $f\left(k\right)$ (or more). $f\left(k\right)\ge g\left(k\right)$ in order to get an earlier step of the proof to go through, but then the resulting proof of $\psi \left(k\right)$ takes at least $f\left(k\right)$ steps to work, so that proof cannot be used with the definition of $\psi \left(k\right)$ to conclude $\perp$.

I'd suspect there's some more subtle argument that can conclude inconsistency, but breaking the proof of Lob's theorem is promising.

What's the use of this, though, if it doesn't shorten proofs?

Well, there's a lot of $n$-length proofs, but the "royal road" of abstractly establishing soundness or consistency would allow concluding the sentence directly without having to embark on an exhaustive search for the original proof.

If you spent a while proving something, and then wrote down the result in your notebook, and forgot about it, then, upon observing the notebook page, you can conclude $\square \varphi$ and, since you can bound how good you are at math, you can establish an upper bound on the length of the proof, ${\square }_n\varphi$. This provides a way to establish $\varphi$ without having to reprove the thing from scratch, by just thinking for a while about "Do I trust my own bounded proofs? Yes I do."

This solves the Notebook Problem in Vingean Reflection.