Looks good! As you say, it is more technical than illuminating, but it's probably a necessary step if the whole project is going to work out. I had definitely thought that this might be tricky, so it's good to see it done. Also I think that there were some natural follow-up questions that I had set aside because I didn't have this piece.
I don't think we should really care about whether the theory proves useful facts about the distribution; as long as the distribution doesn't dogmatically believe falsehoods about itself, we can just condition on explicit reflective observations and that will probably be fine.
So I'm basically fine with this diagonalization step, though I might come to share your concerns if I thought about it longer.
I think the key next step, that may or may not be possible, is getting a distribution that can assign non-zero probability to its own reflection principle while being reflective. This obviously requires weakening the reflection principle, though I think that there are some weak enough reflection principles floating around.
For example, it might be worth taking another look at the double expectation property (E[f(E)] = E[E[f(E)]] for functions f that are continuous in the product topology), and seeing what that translates into in this framework. Obviously continuity will be replaced by something different, since now E and f are both just Turing machines; hopefully we would get E[f] = E[E[f]] for all f that are approximable relative to some powerful oracle. It looks to me like this might work, and if the oracle was powerful enough to implement E I'd consider that promising as a potential basis for self-trust.
We present a Δ2-definable probability distribution Ψ that satisfies Christiano's reflection schema for its own defining formula. The strategy is analogous to the chicken step employed by modal decision theory to obfuscate itself from the eyes of PA; we will prevent the base theory T from knowing much about Ψ, so that Ψ can be coherent over T and also consistently believe in reflection statements. So, the method used here is technical and not fundamental, but it does at least show that limit-computable and reflective distributions exist. These results are due to Sam Eisenstat and me, and this post benefited greatly from extensive notes from Sam; any remaining errors are probably mine.
Prerequisites: we assume familiarity with Christiano's original result and the methods used there. In particular, we will freely use Kakutani's fixed point theorem. See Christiano et al.'s paper.
Outline
Section 1. Problem statement
Probabilistic reflection
We have some base theory T in a language L, where T is able to talk about arithmetic (e.g. PA or ZFC). We wish to find probability distributions over completions of T, or equivalently functions P:L→[0,1] satisfying ϕ∈T implies P(ϕ)=1 and probabilistic coherence conditions like P(¬ϕ)=1−P(ϕ). In particular, we want P to have accurate beliefs about itself:
∀ϕ∈L:∀a,b∈Q:P(ϕ)∈(a,b)⇒P(P(┌ϕ┐)∈(a,b))=1 ,
where P is a symbol in L. Christiano showed that there exists such a distribution P. In other words, taking an additional symbol P in the metalanguage, writing CohT(P) for the statement that P is a coherent distribution over T, and for the statement that P is reflective, we have that the theory
ZFC+CohT(P)+Refl(P)
is consistent. That consistency of this theory is equivalent to the existence of a reflective P requires an argument due to Fallenstein, wherein we take the standard part of P according to some completion of this theory. We will use this idea in Section 3 and explain it there.
Definable reflection
Christiano asked: Can we find a distribution that is definable, and furthermore reflective about its own defining formula?
This is different from the original reflective P because we had a symbol P in the language, and P reflected itself in that symbol; in that case, speaking imprecisely, P knew that P assigned the same probabilities that P assigned. Now we want a formula Ψ that defines a distribution, and that distribution assigns probability 1 to certain true statements about what probabilities Ψ assigns. (Ψ stands for P-Self-reflective.)
Formally, can we have a coherent distribution on T defined by some formula Ψ in the language L, where L now does not contain a distinguished symbol P, satisfying:
∀ϕ∈L:∀a,b∈Q: if Ψ(┌ϕ┐)∈(a,b), then Ψ(┌Ψ(┌ϕ┐)∈(a,b)┐)=1 ?
Our strategy is to apply Kakutani's fixed point theorem to the following reflection correspondence ⊲Ψ on the set Δ(T)⊂[0,1]L of coherent distributions over T. For any P,Q∈Δ(T), we write P⊲ΨQ and say that Q reflects P in Ψ if and only if, whenever P(ϕ) is in some interval, Q believes that Ψ assigns to ϕ a value in that interval. Formally, for all P,Q∈Δ(T), we have P⊲ΨQ if and only if:
∀ϕ∈L:∀a,b∈Q: if P(ϕ)∈(a,b), then Q(Ψ(┌ϕ┐)∈(a,b))=1 .
If we can obtain a fixed point of this correspondence ⊲Ψ, and have Ψ define this same distribution, then we will have a definable self-reflective distribution.
(The notation ⊲Ψ does not denote an ordering, and is meant to suggest a single point on the left with a larger corresponding set on the right; better recommendations are welcome. Also, in the following section, P and Q are actual distributions, not symbols in a language; this is distinguished by their arguments having the type of formulas rather than Gödel numbers of formulas.)
Most of the conditions for Kakutani's theorem are satisfied by ⊲ϕ for any formula ϕ just as in Christiano's proof, so we won't verify them in detail. For example, the set of distributions reflect Q in ϕ is still convex, because interpolation preserves coherence and reflection. (I can make an auxiliary post if people would like to see the details.) However, we need ⊲Ψ to satisfy the crucial non-emptiness condition:
∀P∈Δ(T):∃Q∈Δ(T):P⊲ΨQ .
In the next section, we give a definition Ψ that meets this criterion, assuming a strong background theory such as ZFC. This will illustrate the diagonalization method we will apply. Section 3 gives a Λ that uses the same strategy as Ψ, but is Δ2-definable in arithmetic, i.e. computable relative to a halting oracle. Section 4 discusses the meta-theoretic assumptions used, optimality of our results, and open questions.
Section 2. A definable, self-reflective distribution Ψ
Consider the theory TΨ=P:=T∪{Ψ(┌ϕ┐)∈(a,b) | ϕ∈L,a,b∈Q,P(ϕ)∈(a,b)} stating that Ψ behaves according to P. If TΨ=P is a consistent theory, then we can take a completion T′ of TΨ=P, and then take the 0-1-valued distribution Q(ϕ):=I{ϕ∈T′}, i.e. the indicator function for membership in the complete theory T′. This Q is coherent over T, and furthermore by fiat Q assigns probability 1 to each reflection statement for P by Ψ.
In the original existence proof of a reflective P, the analogous reflection theory Tp=P for a symbol p is consistent: the distribution P itself provides a model for Tp=P. However, in the present case, we have to be more careful. Perhaps T proves some non-trivial facts about the behavior of the function Ψ we are defining. Then TΨ=P may be inconsistent, if T proves that Ψ cannot behave according to P, e.g. if P(ϕ)∈(a,b) but T⊢Ψ(┌ϕ┐)∉(a,b).
To overcome this, we will obfuscate the behavior of Ψ from the prying proofs of T, to such an extreme extent that T cannot rule out any finite set of behaviors of Ψ; then TΨ=P will be consistent. (Unfortunately, this weakens the main potential use in reflective agents of having a definable self-reflective distribution, namely, that the theory can reason concretely about the distribution, other than what can be said about generic coherent distributions. It may be possible to have the base theory prove more about the distribution by not diagonalizing against certain behaviors, and working around that in the application of Kakutani's theorem.)
Definition of Ψ
Take the set BΨ:={⋀i∈[n](Ψ(┌ϕi┐)∈(ai,bi)) | n∈N;aj,bj∈Q∩[0,1];∀k∈[n]:ak<bk} of possible finite specifications of behaviors for Ψ. Here ϕi is some enumeration of all sentences in L. Note that BΨ is countable, and each sentence in BΨ is consistent with Ψ being a function, though not necessarily a coherent distribution. Now we can define Ψ by the following informally stated construction, which can be translated into a formula Ψ(n,r) defining the graph of a function from sentences to real numbers:
Step 1. Search for a proof in T of the negation of some statement in BΨ. If such a statement ⋀i∈[n](Ψ(┌ϕi┐)∈(ai,bi)) is found, then output some value in (ai,bi) on input ϕi, and otherwise output 0.
Step 2. Otherwise, output values according to the least fixed point of the reflection correspondence ⊲Ψ.
By the least fixed point, we mean the fixed point with minimal first coordinate; minimal second coordinate out of those with minimal first coordinate; minimal third coordinate . . . etc. This exists because the set of fixed points is closed, and therefore also compact. Note that we require L and T to be expressive enough to define fixed points of ⊲Ψ and the ordering just described. Taking T=ZFC suffices. This is not a crucial point, as we will later show that a much weaker theory suffices.
Theorem 1.
If T is a sound theory, then Ψ defines a function on L that assigns probability 1 to each sentence in T, is coherent, and is reflective.
Proof.
Suppose we have T⊢¬ξ for some ξ∈BΨ, where ξ=⋀i∈[n](Ψ(┌ϕi┐)∈(ai,bi)). Then by step 1 of Ψ, we have that Ψ(ϕ)∈(ai,bi) for all i∈[n]. This contradicts soundness of T.
Thus, by compactness, we have that for all P∈Δ(T), the theory TΨ=P is consistent. Then by the argument above, the correspondence ⊲Ψ gives a non-empty image for each point in Δ(T). By Kakutani's theorem, there is a fixed point of this correspondence.
Step 2 then outputs probabilities according to some such fixed point P. That is, ∀ϕ:Ψ(ϕ)=P(ϕ). Furthermore, P⊲ΨP, i.e. Ψ is reflective. □
In fact, we do not need to assume soundness of T in Theorem 1; we only need to assume that T is consistent. Proof: suppose that T⊢¬ξ for some ξ∈BΨ. Then there is a least such ξ. But then T can prove that ξ is the first sentence in BΨ that T refutes, so T can prove that Ψ finds this proof and outputs according to ξ. Then we have that T both proves and refutes that Ψ behaves according to ξ, contradicting the consistency of T.
Section 3. A Δ2-definable, self-reflective distribution Λ
Step 1 in Ψ as defined above is Δ2-definable, i.e. computable with a halting oracle: we just need to check the halting of the machine that searches for refutations by T of the (computably recognizable) sentences in BΨ. If the machine halts, find the proof computably, and output rational numbers given by the refuted behavior.
Step 2, however, uses set-theoretic notions; namely, it quantifies over the large and complicated set of fixed points of ⊲Ψ. In this section we replace Step 2 with a Δ2 computation, thereby defining a Δ2 formula Λ that is self-reflective. (Λ stands for Limit-computable.)
Definition of Λ
By the arguments for Theorem 1, regardless of what Λ does in Step 2, there will be some P∈Δ(T) such that P⊲ΛP. Thus, for Step 2, it suffices to run a Δ2 computation that outputs a fixed point as long as one exists. We now define Λ by the following construction, which can be viewed as an algorithm executed by a machine with a halting oracle:
Step 1. Search for a proof in T of the negation of some statement in BΛ. If such a statement ⋀i∈[n](Λ(┌ϕi┐)∈(ai,bi)) is found, then output some value in (ai,bi) on input ϕi, and otherwise output 0.
Step 2. Otherwise, enumerate a completion ¯Z of the theory Z:=ZFC+CohT(P)+P⊲ΛP in the language of set theory plus a constant symbol P. That is, list all sentences σ, and print out each σ that is consistent with Z and the finitely many sentences that have already been printed. Given a sentence ϕ and a precision 0<ε∈Q, search ¯Z for the first quadruple of rational numbers a<a′<b′<b such that ¯Z⊢P(┌ϕ┐)∈(a′,b′), and such that b−a<ε. Output (a,b).
(Note: This is the technique alluded to earlier of taking the standard part of a distribution. If we just output (a,b) with (P(┌ϕ┐)∈(a,b))∈¯Z, then we might output e.g. (0,1/n) for all n∈N, which has empty intersection. Also note that we could take a much more basic theory than Z; we could have a base theory that says all true atomic statements about Q, and take CohT(P) and P⊲ΛP to be schema of quantifier-free formulas.)
Observation: Λ is Δ2.
Proof: Step 1 is Δ2 by the argument given at the beginning of this section. Step 2 is computable, except that we need to check whether each new sentence σ is consistent with Z and the previously printed sentences. To check the consistency of a computably enumerable theory S, we ask our halting oracle whether not M halts, where M is a machine that enumerates all the theorems of S, and halts iff it prints ⊥.
Theorem 2.
Λ defines a coherent, self-reflective distribution.
Proof.
By the argument for Ψ, if T is consistent, it does not refute any behavior of Λ. So there is some fixed point P⊲ΛP, and also Λ behaves according to Step 2.
The distribution P provides an interpretation for the symbol P satisfying coherence over T and self-reflection in Λ. Hence the theory Z is consistent, and so ¯Z is non-trivial. By construction, for each ϕ there is a unique (standard) real P¯Z(ϕ) that, for all ε>0, lies in the interval output by Λ on ϕ and ε.
Now we argue that P¯Z is coherent over T and reflects itself in Λ. For any ϕ∈T, since ¯Z⊢CohT(P), we also have ¯Z⊢P(┌ϕ┐)=1. Thus, for all ε>0 we have that ¯Z⊢P(┌ϕ┐)∈(1−ε,1+ε), and therefore P¯Z(ϕ)=1. A very similar argument works to show the other coherence conditions and reflection. For example, if P¯Z(ϕ)∈(a,b), then we have ¯Z⊢P(┌ϕ┐)∈(a,b). By an instance of P⊲ΛP, also ¯Z⊢P(┌Λ(┌ϕ┐)∈(a,b)┐)=1, and hence P¯Z(Λ(┌ϕ┐)∈(a,b))=1.
Thus Λ computes a coherent distribution over T which assigns probability 1 to each reflection statement for Λ. □
Section 4. Discussion
Δ2 is roughly optimal for the properties of Λ; computable distributions can't even be coherent over essentially undecidable theories. (If we could compute a coherent distribution over T, then for each ϕ we could wait for 1 or 0 to be excluded from the intervals we output for ϕ, and thereby computably separate the provable and refutable sentences, which is impossible.) A slightly stronger statement is that for any definable completion ¯PA of PA, there is a distribution P over completions of T that is computable from ¯PA, which is reflective for the definition of P that uses ¯PA in Step 2 to complete Z.
As mentioned earlier, Λ is very obfuscated from T. In fact, if T is strong enough, then Λ(Con(T))=0. Otherwise, since Λ believes each sentence of T, by coherence and , we would have that . But this is not possible for a reflective, coherent distribution.
If our metatheory K is strong enough to prove some facts like Kakutani's theorem, then K+Con(T) proves CohT(Λ) and Refl(Λ). This likely roughly optimal: if the meta-theory even proves CohT(Λ), then it also proves Con(T). Probably PA is sufficient to prove the necessary first-order statements, since the second-order theory ACA0 is probably strong enough to prove a literal statement of Kakutani's theorem, and PA is the first-order part of ACA0. See for example Fixed point theory in weak second-order arithmetic, by Naoki Shioji and Kazuyuki Tanaka , though that paper only proves Kakutani in finite dimensions and the Tychonoff-Schauder theorem (in the weaker system WKL0).
Questions
Open questions (Christiano):