Benford Test with Gaps

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 which on input runs in time, and outputs a probability interpreted as the probability to assign to .

We say that a subset of natural numbers is -irreducible pattern if it is possible to quickly determine if is in , and the provability/​disprovability of elements of appears (relative to time) indistinguishable from a coin which outputs “true” with probability , “false” with probability , and “undecidable” with probability .

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 -irreducible pattern.

We say that passes the Benford test with gaps if whenever is a -irreducible pattern, the limit as goes to infinity of the distance between and the interval 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 . However, this property would be too strong.

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

We would need that with probability 1, the probabilities converge to . 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 12.

Now, imagine that for the th sentence, , you replace it with the sentence ” or outputs a probability less than 35 at least times.” (We assume that was such that if is undecidible, and the second condition is false, the new sentence is still undecidable).

If only outputs probabilities less than 35 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 13 each, so must converge to probability 12, contradicting the assumption that is only less than 35 finitely often.

Therefore, must be less than infinitely often. This means that actually, none of the sentences are undecidable, so we are in a (2/​3,1/​3)-irreducible pattern. But cannot converge to 23, since it outputs probabilities less than 35 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.