Some MIRI Workshop Stuff

It's great that MIRI had some success with probabilistic reflection. But I'm still not sure if it matches the pattern of "waging war on an established result". Lob's theorem, like Russell's paradox, is one of those counterintuitive problems where the answer we "feel" must be right is provably wrong. When someone tells me such a problem can be solved with probabilities but not with certainties, I get suspicious. Why would we be so lucky when going against the grain?

Sorry for the unhelpful comment. I do really wish the best of luck to such efforts.

What's your current opinion on whether Sawin's proved statement that "any logically coherent, approximable probability distribution over statements in arithmetic which assigns probability 1 to true pi-1 statements will assign probability 0 to some true pi-2 statements" is a special case of Theorem 3.7 of Gaifman & Snir (1982)? Alex Mennen looked at it and thinks "probably not," but I'm not in a position to tell.

Cool!

But I can't help but think that there's some more elegant way to formulate the "chance that an unknown consistent logical theory would contain statement A" than by generating a billion apparently-consistent logical theories and counting how many have A. Then again, maybe not. shrug

I do see another problem - it seems like the amount of resources used when generating and checking all those logical theories is more than you'd need to just prove A and remove any need for probability. After all, if you sample a thousand logical theories, and the logical probability of A is 0.7, then I think the Monte Carlo algorithm has just proved A 700 times, among all its other work.

EDIT: More thoughts. How would updating on a pool of trusted statements work here? E.g. what if we want to condition our logical probability on the fact that 1+1=2? The obvious method is just to start with "1+1=2" when randomly generating a new logical theory, and toss out anything inconsistent with it.

But this becomes really troublesome if you want to start with a complete set of axioms. E.g. what if you know how to do arithmetic, you just don't know the last digit of the trillionth prime number? The rules of arithmetic are statements like "for all numbers a and b, ab = (a-1)b+b", which should fit into the pool of statements defining a possible logical theory just fine. But if you start with a complete theory already in the pool, he space you're sampling is just a point, and checking whether the random logical theory contains A collapses to being a theorem-prover for a known theory.

So what do you do? The "know arithmetic, don't know all the consequences" situation should be right in logical probability's wheelhouse. Do you only allow arithmetic hierarchy level 0 statements to enter the pool, maybe? So you can demand that 1+1=2, but you can't demand that for all x, x+x=2x. But on the other hand, what if you want the probability given arithmetic of something really easy, like "does 2+2=4?", and can start with "1+1=2" in the pool, but not any of the heirarchy-level-1 statements that actually define addition. Then you end up assigning 2+2=4 some probability depressingly close to 50% just because you can't handle too much starting knowledge.