In this post, I present a new desirable property in Asymptotic Logical Uncertainty. The property is the analog of satisfying the Benford test, but with a collection of undecidable sentences mixed in. I do not know of any algorithm that satisfies this property yet. I give a proof that a similar stronger property is actually impossible to satisfy.

Consider an algorithm $M$ which on input $n$ runs in $f\left(n\right)$ time, and outputs a probability interpreted as the probability to assign to ${\varphi }_n$.

We say that a subset of natural numbers $S$ is $(p,q)$-irreducible pattern if it is possible to quickly determine if $n$ is in $S$, and the provability/disprovability of elements of $S$ appears (relative to $f\left(n\right)$ time) indistinguishable from a coin which outputs "true" with probability $p$, "false" with probability $q$, and "undecidable" with probability $1-p-q$.

I am purposefully being vague about the exact definition of irreducible pattern here. You could define it similarly to how we defined it before, but I am open to other definitions. It should at least be the case that if the theorem prover was randomly determining whether elements of the sequence are provable, disprovable, or undecidable with the corresponding probabilities, then the resulting sequence should almost surely be a $(p,q)$-irreducible pattern.

We say that $M$ passes the Benford test with gaps if whenever $S$ is a $(p,q)$-irreducible pattern, the limit as $n\in S$ goes to infinity of the distance between $M\left(n\right)$ and the interval $[p,1-q]$ is 0.

At first, this property may appear weaker than it has to be. One might be tempted to instead require that the probability converges to $\frac{p}{p+q}$. However, this property would be too strong.

To see that this is too strong, consider an environment in which the $n$th sentence is true with probability $1/3$, false with probability $1/3$, and otherwise undecidable.

We would need that with probability 1, the probabilities converge to $1/2$. In fact, take a random sequence like this, and change finitely many of the undecidable sentences to true, the probabilities would still have to converge to 1/2.

Now, imagine that for the $n$th sentence, ${\varphi }_n$, you replace it with the sentence "${\varphi }_n$ or $M$ outputs a probability less than 3/5 at least $n$ times." (We assume that $\varphi$ was such that if $\varphi$ is undecidible, and the second condition is false, the new sentence is still undecidable).

If $M$ only outputs probabilities less than 3/5 finitely often, then only finitely many sentences what would be undecidable are now true, so with finitely many exceptions, the environment is true, false, or undecidable with probability 1/3 each, so $M$ must converge to probability 1/2, contradicting the assumption that $M$ is only less than 3/5 finitely often.

Therefore, $M$ must be less than $3/5$ infinitely often. This means that actually, none of the sentences are undecidable, so we are in a (2/3,1/3)-irreducible pattern. But $M$ cannot converge to 2/3, since it outputs probabilities less than 3/5 infinitely often.

The reason I care about this new property is that right now, all the ways I know of to pass the Benford test depend on stopping that analysis of a gives subsequence as soon as you encounter one sentence in that subsequence that appears undecidable. This trick is useful for removing biases that come from the length of the shortest proof or disproof of sentences being correlated with their truth values. However, it appears that using this trick is interfering with the ability for these algorithms to be coherent.