Here is another open question related to Logical Inductors. I have not thought about it very long, so it might be easy.
Does there exist a logical inductor \(\{\mathbb P_n\}\) over PA such that for all \(\phi\):
PA proves that \(\mathbb P_\infty(\phi)\) exists and is in \([0,1]\), and
\(\mathbb{E}_n(\mathbb{P}_\infty(\phi))\eqsim_n\mathbb{P}_n(\phi)\)?
Note that \(\mathbb{P}_\infty(\phi)\) need not be computable so this does not happen by default.
For example, consider the logical inductor described in the paper with the extra condition that if ever the deductive state is discovered to be inconsistent, all probabilities are set to 0 forever. This clause will never be executed, since PA is consistent, but since this clause exists, PA can prove that \(\mathbb P_\infty(\phi)\) exists. (PA proves that if PA is consistent, the limit exists using the proof in the paper, and if PA is inconsistent, the limit exists and equals 0.)
However, this logical inductor will not satisfy the second property. Consider the sentence \(\top\). \(\mathbb{P}_n(\top)\) will converge to 1, while \(\mathbb{E}_n(\mathbb{P}_\infty(\top))\) will converge to the probability according to \(\mathbb{P}_\infty\) that \(PA\) is consistent. (PA proves that if PA is consistent, the limit is 1 using the proof in the paper, and that if PA is inconsistent, the limit is 0.)
If a Logical Inductor with the above property is found, there are many follow up questions you could ask.
Can you make an analogue of the self trust property that works for \(\mathbb{P}_\infty\)? Does the above property imply that self trust property?
Is there some simple extra condition that could be added to the definition of a Logical Inductor, that implies everything we could want about beliefs about \(\mathbb{P}_\infty\)?
A good place to start with this question might be to analyze a logical inductor that in the spirit of the Demski prior adds sentences to the deductive state only if they are propositionally consistent with all previous sentences. This way, PA will prove that the algorithm defines a logical inductor over some consistent propositional theory (even if it does not know if that theory is PA).
