This post explores a draft paper by Paul Christiano et al (06/10/2013 draft), produced at a workshop hosted by the Machine Intelligence Research Institute. My intent is to go thoroughly through the main argument, to ensure that I fully understand it. Also, on my first or second reading, I had some worries that the argument seemed to produce something for nothing, possibly violating a “conservation of depth” in mathematics. I am no longer worried about this.
Towards the end of this post, I discuss the non-constructive nature of the proof given, but show that it can at least be modified so as not to rely on the Axiom of Choice.
A one-sentence summary of the paper is: Although a logical theory can’t contain its own Truth predicate, it can contain its own “subjective probability function” which assigns reasonable probabilities to sentences of the theory, including of course statements about the probability function itself.
Or to quote the conclusion of the paper:
Tarski’s result on the undefinability of truth is in some sense an artifact of the infinite precision demanded by reasoning about complete certainty.
One starts with some theory in a countable language that can interpret rational and integer arithmetic (say it extends Peano Arithmetic), and in particular admits Gödel numbering of its sentences. Append to the language another symbol to get a language , and consider now as an -theory. For the most part, we will think of as a one-place function symbol taking Gödel numbers of -sentences to real values, but actually just needs to be a relation between Gödel numbers and pairs of rational numbers (which we think of as saying that the probability of a sentence lies in the specified range).
Now at the meta-level, think of Borel probability distributions over some space of models of as an -structure (the basic open sets in the model space are determined by satisfaction of particular -sentences). These induce (finitely additive) probability measures on the set of -sentences, the measure of a sentence being the measure of the set of models in which it holds. Such a measure will have desirable properties allowing us to reason intelligently at the level of sentences, such as:
- assigning probability to any theorem of ,
- assigning probability to any sentence refuted by , and
- for all -sentences , (many of which include the for-now-unrelated symbol ).
In fact, Christiano et al show that any function from -sentences to satisfying the above is induced by some measure on the model space, and they call such functions coherent probability measures. Note however, that any coherent must be uncomputable, as it assigns probability to the theorems of Peano Arithmetic, and probability to the refuted sentences.
We’d like to have a coherent which says things about the -sentences which include as if . If we are thinking of as an algorithm (despite the uncomputability mentioned above), perhaps it can compute the probabilities of statements up to arbitrary precision, and so it can determine in finite time whether a probability lies in an open set (the important characteristic of open sets here is that they provide a little wiggle room in either direction).
This is the reflection principle that the authors found to work: at the meta-level, for all rational and , and all ,
where denotes the Gödel number of in . Intuitively, if is actually in , then will surely recognize this about itself. We sometimes call a coherent distribution satisfying this schema reflective.
Of course, we’d like for the statements that makes about to have some grounding in reality, i.e. something like a converse to the reflection schema. We’ll see shortly that a full converse would be too strong, but actually from the contrapositives of the above schema, one can derive for coherent and all , , :
We shall now take a quick look at what reflection means, and see why the converses of the reflection schema can’t hold for coherent . Fix rational , and using Gödel’s diagonal lemma, construct an -sentence which asserts that its own probability is less than . That is, proves
Informally, If is small, says “this sentence is probably false”. Assuming is reflective:
- If , then “knows” it, i.e. . Since is coherent, we have by the definition of that , and so , contradiction.
- Similarly, cannot be less than , or else would “know” that was actually .
- Thus the only value can take is the boundary point , where isn’t really in the interval , but cannot verify this with finite precision and must simply settle on “maybe I am less than “.
- The special case where , is somewhat analogous to the classic liar sentence. By the above analysis, . Here we see that the converse to the reflection schema is inconsistent, for it would derive from that .
This state of affairs, in which the modified liar sentence is assigned probability , may not be intuitive, and you may still wonder whether you could deduce a contradiction with a more clever argument (perhaps with ). The main result proved by Christiano et al is that you could not: the reflection schema is consistent.
Here’s a statement of the Theorem:
Theorem 1 Let be a consistent theory in a countable language , powerful enough to interpret Peano and rational number arithmetic. Then there exists a coherent probability measure satisfying the reflection schema; in particular the -theory obtained by adding the reflection schema to remains consistent.
At the highest level, the construction of a coherent, reflective looks something like this: start with an arbitrary coherent , making no attempt whatsoever at reflection, and iteratively replace it with some from the (non-empty) set of coherent probability measures which treat as an acceptable interpretation for . By this, I mean (for all , , ):
Call such a an immediate revision of ; a coherent distribution is reflective iff its is an immediate revision of itself. Then the sequence above is constructed so that a limit can be taken to produce a fixed point.
But this is not really correct. It is not clear that an arbitrary sequence , as above should actually converge, and in fact we’ll see that the “most obvious” such sequence does not.
- We first show that any real-valued function on sentences of admits at least one immediate revision (including but not limited to coherent probability distributions). Since is consistent, take any model , and interpret as (by which we really mean for every rational and and every , iff ). Since says nothing about the symbol , remains a model of . One can then define an immediate revision of in a trivial way,
Here we certainly have
and moreover is coherent, because it is induced by the “point mass at the model ” (technically it’s the point mass at the elementary equivalence class of ).
- Thus one could simply define a sequence of immediate revisions with arbitrary, say , and successors determined as above given some fixed model . It is tempting at this point to argue that
- Valuations of the countably many -sentences can be thought of as infinite-length vectors in the Hilbert cube , which is compact by Tychonoff’s Theorem.
- The set of coherent probability distributions is a closed subset of , by the alternate characterization mentioned in section 1, thus has a subsequence converging to a coherent probability distribution.
- The function taking a coherent probability distribution to the set of its immediate revisions has an analogue of continuity known as the closed graph property: if a sequence and a sequence (in the product topology of course), with , then . The proof is that for any , if , then for all large , thus for all large , so .
- Furthermore, by compactness of the product, the paired sequence admits a convergent subsequence
By the closed graph property in (3), is an immediate revision of .
- Hopefully . (fingers crossed!)
- After some thought, you may realize that (5) cannot hold (though the reasoning in (1)-(3) will be helpful for the correct proof). This is because the particular sequence we built in the above bullet point is too trivial: it only takes the extreme values and . Thus if , we’d have a -valued coherent and reflective distribution. This is basically the forbidden Truth predicate, and in any case, it certainly can’t handle the sentences like from section 2.
Thus something more must go into producing a reflective and coherent distribution. The key to obtaining coherent distributions with values throughout is taking convex combinations of old distributions. That is, if and are coherent distributions induced by measures and on the model space, then is a coherent distribution induced by for any . Moreover, if and are actually immediate revisions of , then so is , so the set of immediate revisions of a function is convex.
Since there are many point mass measures in the model space (even if is complete as an -theory, different interpretations of will yield continuum-many distinct elementary equivalence classes among -structures), convexity guarantees a fairly rich space of immediate revisions from which to pick our sequence, as known measures can be mixed via convex combination to produce new ones. But how shall we handle all this mixing and choosing?
The missing ingredient, which intelligently makes the choices in a way that guarantees convergence, is the Kakutani-Fan-Glicksberg fixed point theorem.
Theorem 2 (Kakutani, Fan, Glicksberg) Let be a non-empty, compact, convex subset of a locally convex Hausdorff space. Let be a set-valued function on which has a closed graph and the property that is non-empty and convex for all . Then the set of fixed points of (meaning ) is non-empty and compact.
The KFG theorem is the very last piece of this puzzle. So although the above reasoning failed to produce a fixed point, we have already done all the work of checking that the KFG hypotheses are met:
- Let be the set of coherent probability distributions, which we have already seen is compact, convex, and non-empty (viewed as a subset of the locally convex space ).
- The function mapping a coherent probability distribution to its set of immediate revisions similarly has convex and non-empty for each .
So a coherent and reflective distribution is produced as fixed point by the KFG theorem.
As written, the proof is non-constructive in that KFG relies (at least mildly) on the Axiom of Choice and so proves that a fixed point exists without explicitly exhibiting one. My knee-jerk reaction is that in any separable complete metric space (that is, in any Polish space), this mild reliance on the Axiom of Choice can usually be eliminated: the regularity of the domain should be enough to uniquely specify arbitrary choices when they must be made, so that one should be able to uniquely specify one particular fixed point (though there may be many) with a single formula in ZF set theory.1
Thus one could probably develop a constructive version of the KFG theorem for . I put a bit of thought into this (it’s easy for the -dimensional Kakutani fixed point theorem anyway), though I’d not been terribly motivated to complete it, because it seemed long and tedious for a rather minor improvement: so long as we’re stuck with uncomputability, undefinability just didn’t seem that much worse.
I later realized there’s a much easier (albeit higher-level) way to remove the reliance on Choice here. From whatever set-theoretic universe we’re living in, look “inward” to Gödel’s constructible universe , which provides a definable well-ordering of itself via some two-variable set-theoretic formula . Now the KFG theorem (relative to ) can pick out a single fixed point with some formula involving . Thus the main theorem (relative to ) defines via some formula an object which believes to be a coherent, reflective distribution. Step back out of , and we are done when we recognize that agrees that is a coherent, reflective distribution defined by the relativized formula . (That is, by standard absoluteness arguments, agrees that is an -sequence of reals satisfying the countably many coherence and reflection axioms. Also, following that absoluteness link, it sounds like I really ought to learn about Shoenfield’s absoluteness theorem to automate these kinds of arguments. I had not heard of that before.)
Is the above of much practical use? Well, probably not!
To dodge the more serious problem of uncomputability, a “subjective probability function” would have to allow for logical uncertainty (perhaps in the sense of Gaifman), in which all true theorems are not automatically derived from the axioms. For instance, I may believe that the -th digit of –say, for Graham’s number— has a chance of being odd. A reasonable mathematical theory like ZF clearly either proves or disproves this statement, but (barring the discovery of a very simple rule for calculating digits of ) there is not enough computation in the universe to find out which.
Hopefully there’s a more practical analogue of this theorem, out there and waiting to be discovered. I’ve already indicated that the one ought to be able to frame the process of finding a fixed point as a converging sequence of revisions, with the current proof just relying on the KFG theorem to do this work behind the scenes. Totally speculating here, I wonder whether one might be able to start the process with a “prior” distribution over some finite set of sentences, and alternately update the distribution in two directions:
- by increasing the coherence and reflectiveness of the distribution, and
- by expanding the set of sentences in the domain.
All the obvious disclaimers apply, including
- I just made this up without too much thought as to how it would be implemented, and
- I would expect any limit point produced by such a process to depend rather strongly on the arbitrary choices that would have to be made in a proper specification (e.g. how much of step (1) should we do before switching to step (2) and vice versa?). In particular, if one made obviously wrong choices here, I would not expect any convergence at all.
Still, I think the above is at least a fair model of what a computable reflective reasoning process should look like.
In any case, Christiano et al have written a nice draft paper demonstrating that a logic can reason probabilistically about its own truth without crashing and burning at the liar’s paradox. In a vast sea of logical impossibility results, this kind of thing is refreshing.
- The classic example here is the Baire Category Theorem, extremely useful for existence proofs in analysis, which states for complete metric spaces that the intersection of countably many open dense sets remains dense (and in particular is non-empty). The BCT is known to be equivalent to the Axiom of Dependent Choice (weaker than the full Axiom of Choice, but not a theorem of ZF), but the BCT can be proved for Polish spaces in ZF alone. The trick: given an enumeration for a countable dense subset of a Polish space, I can construct an enumeration of the rational-radius open balls centered around these points, and I can prove that these balls form a base for the Polish topology. The proof of the BCT relies on choosing a sequence of open balls with ZF-checkable properties; I now have an enumeration (aka well-ordering) to guide my hand.