JustinShovelain comments on Metaphilosophical Mysteries - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (255)
I haven't studied algorithmic probability literature in-depth, but it naively seems to me that one can straightforwardly extend the idea of universal probability to arbitrary logical languages, thus becoming able to assign plausibility to all mathematical structures. The same principle as with universal prior, but have a statement valued by the length of the shortest equivalent statement (from no non-logical axioms), and consequently a class of structures gets value from a statement describing it. This takes care of not noticing halting oracles and so on, you just need to let go of the standard theory/model of programs-only.
Are you trying to express the idea of adding new fundamental "terms" to your language describing things like halting oracles and such? And then discounting their weight by the shortest statement of said term's properties expressed in the language that existed previously to including this additional "term?" If so, I agree that this is the natural way to extend priors out to handle arbitrary describable objects such as halting oracles.
Stated another way. You start with a language L. Let the definition of an esoteric mathematical object (say a halting oracle) E be D in the original language L. Then the prior probability of a program using that object is discounted by the description length of D. This gives us a prior over all "programs" containing arbitrary (describable) esoteric mathematical objects in their description.
I'm not yet sure how universal this approach is at allowing arbitrary esoteric mathematical objects (appealing to the Church-Turing thesis here would be assuming the conclusion) and am uncertain whether we can ignore the ones it cannot incorporate.
Why "new terms"? If the language can finitely express a concept, my scheme gives that concept plausibility. Maybe this could be extended to lengths of programs that generate axioms for a given theory (even enumerable sets of axioms), rather than lengths of individual finite statements, but I guess that can be stated within some logical language just as well.
By new "term" I meant to make the clear that this statement points to an operation that cannot be done with the original machine. Instead it calls this new module (say a halting oracle) that didn't exist originally.
What machine???