Very neat!!

Your use of the Bayes score is reminiscent of what I'm trying to do here, only that I'm working in the context of complexity theory (and consider only efficiently computable things) whereas you work in the context of logic (and consider incomputable things). I think that (assuming my optimal estimators actually exist) it might be useful to try to find a formal connection between the two. The direction I see so far is observing that my estimator can be used to assign a probability to "sentence phi has a proof of length at most n" by considering the NP problem of deciding, given input (phi, x), whether a proof of length at most |x| exists.

Btw, I think your post can be great content for the FAI google group... wink wink... :)