Part of the Asymptotic Logical Uncertainty series. A couple weeks ago, I proposed a definition of uniform coherence. I decided to change the definition so that it applies to a more general context. This post is a self contained definition of uniform coherence designed so that people can start working on the problem with no background other than this post.
Every Turing machine discussed in this post will have two infinite blank tapes to work with in addition to an infinite write only output tape. There will be a special character # for the output tape which will separate the output tape into chunks.
A sentence enumerator is a machine which outputs an infinite number of # symbols, where between each pair of adjacent # symbols is a binary string which encodes a logical sentence . If is a sentence enumerator, we let denote the sentence written between the two most recent # symbols at time . If has not yet written two # symbols by time , we say that .
Similarly, a logical predictor is a machine which outputs an infinite number of # symbols, where between each pair of adjacent # symbols is a binary string which encodes a finite sequence of ordered pairs, with each ordered pair containing a logical sentence and a rational number . If is a logical predictor, we let denote the rational number such that when outputs its # symbol, has been output between more recently than any other pair of the form . If has not yet output any pair of the form by time it outputs # symbols, we say that .
We say that a logical predictor is uniformly coherent if the following three axioms hold:
If is a sentence enumerator such that for all the sentence is provable, then exists.
If , , and are three sentence enumerators such that for all sufficiently large, the sentence "Exactly one of , , and is true" is provable, then
Open Question: Do there exist any uniformly coherent logical predictors?
[EDIT: This problem is no longer open]
If there are uniformly coherent logical predictors, how frequently can we make a uniformly coherent logical predictor output a # symbol?
Given a logical predictor , observe that for any sentence , axiom 2 implies that there must be some real number such that
Theorem: If is a uniformly coherent logical predictor, then is a coherent computably approximable prior.
The proof is similar to the proof given for the old definition, but I encourage anyone who wants to think about this problem to verify this fact for themselves as a simple exercise. You can find a definition of coherence as definition 2 here. Computable approximability just means that the probability assigned to each sentence is the limit of numbers output by a computable process.