There may be an issue with the semantics here. I’m not entirely certain of the reasoning here, but here goes:
Reflection axiom: ∀a, b: (a < P(φ) < b) ⇒ P(a < P(‘φ’) < b) = 1 (the version in Paul’s paper).
Using diagonalisation, define G ⇔ −1<P(‘G’)<1
Then P(G)<1
⇒ −1 0)
⇒ P(-1<P(‘G’)<1)=1 (by reflection)
⇒ P(G)=1 (by definition of G).
Hence, by contradiction (and since P cannot be greater than 1), P(G)=1. Hence P(‘G’)=1 (since the two P’s are the same formal object), and hence G is false. So we have a false result that has probability 1.
But it may get worse. If we can prove P(G)=1 then (?) the logical system itself can prove P(‘G’)=1 - and from that, can disprove G. So ¬G is a theorem of the system! And yet P(¬G)=0. So the system has theorems with probability zero...
EDIT: corrected the version of reflection to the version in Paul’s paper (not the one in Eliezer’s post) by removing two ’.
P(G) is a real number in the interval [0, 1], so you shouldn’t be too sad that P(P(G) = p) = 0 for each p. More generally, you shouldn’t expect good behavior when P talks about exact statements—P can be mistaken about itself up to some infinitesimal epsilon, so it can be wrong about whether P(G) is exactly 1 or slightly less.
We can prove P(G) = 1, but the system can’t. The reflection schema is not a theorem—each instance is true (and is assigned probability 1), and the universal quantification is true, but the universal quantification is not assigned probability 1. In fact, it is assigned probability 0.
Hum… So the system is unable to prove that −1 < P(‘G’) < 1 implies P(‘-1 < P(‘G’) < 1′) (note where the ′ are)? This is a (true) statement about the function P.
So, first of all, there isn’t really a particular formal proof system in the paper, except sort of implicitly; all we get is a function P(.) from L’-sentences to real numbers. However, we can talk about the first-order theory you obtain by taking the base theory T and adding to it the reflection axioms, i.e. the axioms a < P(‘G’) < b for all G such that the function P(.) satisfies a < P(G) < b. [For anyone not paying very close attention, P(‘.’) is a function symbol in the formal language, while P(.) is a meta-language function from the formal language to the real numbers.] The main theorem is that P(.) assigns probability 1 to this theory (and therefore to all consequences of this theory), so it is interesting to ask what it entails.
Your question, if I understand correctly, is whether this theory does in particular entail
[-1 < P(‘G’) < 1] --> [P(‘-1 < P(‘G’) < 1′) = 1]
(note that this is simply a sentence in the language L’, not a meta-language statement). There’s no obvious reason that the system should be able to prove this—all we have is T and the individual axioms of the form [a < P(‘G’) < b] --, and indeed your proof shows that (unless there is an inconsistency in the paper) this is not a theorem of the system: if it were, then so would be P(‘G’) = 1, and therefore ¬G, leading to a contradiction since P(.) assigns probability 1 to all theorems of this system.
In short, yes, there are true statements about P(.) such that the corresponding statement about P(‘.’) is false in the formal system, and assigned zero probability by P(.). And yes, I do believe this is worth keeping in mind.
Here is my current preferred way of thinking about this: In non-standard analysis, there is a “standard” operator st(.) which takes a non-standard real number x and returns the standard number st(x) that x is infinitesimally close to (assuming one exists, which is the case if x is not unbounded). This operator can also be applied to functions f; st(f)(x) is the standard number which f(x) is infinitesimally close to. I imagine that there is a collection of “possible” non-standard models, each of which fulfills all the axioms that P(.) assigns probability 1, and that one of these possible non-standard models is the true one describing the real world. Then, P(.) is st(P(‘.’)), where P(‘.’) is the function in the true non-standard model. [ETA: This is always defined because we have −1 < P(‘G’) < 2, so every value of P(‘.’) is infinitesimally close to a standard number.]
How could the real world be described by a non-standard model, you ask? The following is rather handwavy, but I’m imagining the agent as computing an infinite sequence of approximations P_i(.) to the intended distribution, and the true model to be the ultrapower of some standard model of ZFC, with P(‘.’) being interpreted as P_i(.) in the i’th component of the ultrapower. Whether any leverage can be gotten out of making this idea formal, I don’t know. (And it’s certainly true that to pull off this intuition, I still need to have a free ultrafilter falling out of the sky.)
Ok, for [a < P(‘G’) < b] I see why you’d use a schema (because it’s an object level axiom, not a meta-language axiom).
But this still seems possibly problematic. We know that adding axioms like [-1 < P(‘G’) < 1] --> [P(‘-1 < P(‘G’) < 1′) = 1], would break the system. But I don’t see a reason to suppose that the other reflection axioms don’t break the system. It might or it might not, but I’m not sure; was there a proof along the lines of “this system is inconsistent if and only if the initial system is” or something?
I’m not sure whether I’m misunderstanding your point, but the paper proves that there is a coherent probability distribution P(.) that assigns probability 1 to both T and to the collection of reflection axioms [a < P(‘G’) < b] for P(.); this implies that there is a probability distribution over complete theories assigning probability 1 to (T + the reflection axioms for P). But if (T + the reflection axioms for P) were inconsistent, then there would be no complete theory extending it, so this would be the empty event and would have to be assigned probability 0 by any coherent probability distribution. It follows that (T + the reflection axioms for P) is consistent. (NB: by “the reflection axioms for P(.)”, I only mean the appropriate instances of [a < P(‘G’) < b], not anything that quantifies over a, b or G inside the object language.)
I think the point is that reflection gives an infinite collection of formal statements all of which must be assigned probability 1 (“axioms”), in analogy to how an axiom schema is a specification of an infinite collection of axioms. Whether “schema” is the right word to use here is debatable, I guess; I was happy with the choice but perhaps you could argue that “schema” should be reserved to recursively enumerable collections or something.
My point was that reflection is defined for the meta language, and quantifies over all the sentences in the object language. This is not something that can be added as an axiom in the object language at all—P (without the ’) has no meaning there.
So none of the sub-statements of reflection get assigned probability 1 - they just aren’t the kind of thing P works on. So I felt that calling this an schema distracted attention from what reflection is, which is a property of P, not axioms for the lower system.
The idea is not that this whole statement is an axiom schema. Instead, the idea is that the schema is the collection of the axioms
%20%3C%20b) for all rational numbers a,b and sentences phi such that
%20%3C%20b). The full statement above is saying that each instance of this schema is assigned probability 1. (From what I remember of a previous conversation with Paul, I’m pretty confident that this is the intended interpretation.) The language in the paper should probably be clearer about this.
Ah. I didn’t quite understand what you were trying to do there.
In general in this theory, I don’t think we have (p(phi) < 1 → p(phi) =1) → p(phi) = 1. The theory only reflects on itself to within epsilon, so what the theory would conclude if it were certain about p(phi) being less than 1 can’t be taken as the premise of a proof-by-contradiction in the same way that ~phi can be taken as a premise… ergh, I’m trying to figure out a more helpful way to state this than “I don’t think you can derive that kind of probabilistic proof by contradiction from the stated properties of the theory because the system is never supposed to know the exact probabilities it assigns”.
Stuart’s proof by contradiction goes through, as far as I can see. (The speculation in the last paragraph doesn’t, as Paul notes, and I don’t know what “Hence P(‘G’)=1” is supposed to mean, but the proof by contradiction part does work.)
ETA: I now think that “Hence P(‘G’) = 1” is supposed to mean that this statement is implied by the first-order theory (T + the reflection axioms).
There may be an issue with the semantics here. I’m not entirely certain of the reasoning here, but here goes:
Reflection axiom: ∀a, b: (a < P(φ) < b) ⇒ P(a < P(‘φ’) < b) = 1 (the version in Paul’s paper).
Using diagonalisation, define G ⇔ −1<P(‘G’)<1
Then P(G)<1
⇒ −1 0)
⇒ P(-1<P(‘G’)<1)=1 (by reflection)
⇒ P(G)=1 (by definition of G).
Hence, by contradiction (and since P cannot be greater than 1), P(G)=1. Hence P(‘G’)=1 (since the two P’s are the same formal object), and hence G is false. So we have a false result that has probability 1.
But it may get worse. If we can prove P(G)=1 then (?) the logical system itself can prove P(‘G’)=1 - and from that, can disprove G. So ¬G is a theorem of the system! And yet P(¬G)=0. So the system has theorems with probability zero...
EDIT: corrected the version of reflection to the version in Paul’s paper (not the one in Eliezer’s post) by removing two ’.
P(G) is a real number in the interval [0, 1], so you shouldn’t be too sad that P(P(G) = p) = 0 for each p. More generally, you shouldn’t expect good behavior when P talks about exact statements—P can be mistaken about itself up to some infinitesimal epsilon, so it can be wrong about whether P(G) is exactly 1 or slightly less.
We can prove P(G) = 1, but the system can’t. The reflection schema is not a theorem—each instance is true (and is assigned probability 1), and the universal quantification is true, but the universal quantification is not assigned probability 1. In fact, it is assigned probability 0.
Hum… So the system is unable to prove that −1 < P(‘G’) < 1 implies P(‘-1 < P(‘G’) < 1′) (note where the ′ are)? This is a (true) statement about the function P.
So, first of all, there isn’t really a particular formal proof system in the paper, except sort of implicitly; all we get is a function P(.) from L’-sentences to real numbers. However, we can talk about the first-order theory you obtain by taking the base theory T and adding to it the reflection axioms, i.e. the axioms a < P(‘G’) < b for all G such that the function P(.) satisfies a < P(G) < b. [For anyone not paying very close attention, P(‘.’) is a function symbol in the formal language, while P(.) is a meta-language function from the formal language to the real numbers.] The main theorem is that P(.) assigns probability 1 to this theory (and therefore to all consequences of this theory), so it is interesting to ask what it entails.
Your question, if I understand correctly, is whether this theory does in particular entail
[-1 < P(‘G’) < 1] --> [P(‘-1 < P(‘G’) < 1′) = 1]
(note that this is simply a sentence in the language L’, not a meta-language statement). There’s no obvious reason that the system should be able to prove this—all we have is T and the individual axioms of the form [a < P(‘G’) < b] --, and indeed your proof shows that (unless there is an inconsistency in the paper) this is not a theorem of the system: if it were, then so would be P(‘G’) = 1, and therefore ¬G, leading to a contradiction since P(.) assigns probability 1 to all theorems of this system.
In short, yes, there are true statements about P(.) such that the corresponding statement about P(‘.’) is false in the formal system, and assigned zero probability by P(.). And yes, I do believe this is worth keeping in mind.
Here is my current preferred way of thinking about this: In non-standard analysis, there is a “standard” operator st(.) which takes a non-standard real number x and returns the standard number st(x) that x is infinitesimally close to (assuming one exists, which is the case if x is not unbounded). This operator can also be applied to functions f; st(f)(x) is the standard number which f(x) is infinitesimally close to. I imagine that there is a collection of “possible” non-standard models, each of which fulfills all the axioms that P(.) assigns probability 1, and that one of these possible non-standard models is the true one describing the real world. Then, P(.) is st(P(‘.’)), where P(‘.’) is the function in the true non-standard model. [ETA: This is always defined because we have −1 < P(‘G’) < 2, so every value of P(‘.’) is infinitesimally close to a standard number.]
How could the real world be described by a non-standard model, you ask? The following is rather handwavy, but I’m imagining the agent as computing an infinite sequence of approximations P_i(.) to the intended distribution, and the true model to be the ultrapower of some standard model of ZFC, with P(‘.’) being interpreted as P_i(.) in the i’th component of the ultrapower. Whether any leverage can be gotten out of making this idea formal, I don’t know. (And it’s certainly true that to pull off this intuition, I still need to have a free ultrafilter falling out of the sky.)
Ok, for [a < P(‘G’) < b] I see why you’d use a schema (because it’s an object level axiom, not a meta-language axiom).
But this still seems possibly problematic. We know that adding axioms like [-1 < P(‘G’) < 1] --> [P(‘-1 < P(‘G’) < 1′) = 1], would break the system. But I don’t see a reason to suppose that the other reflection axioms don’t break the system. It might or it might not, but I’m not sure; was there a proof along the lines of “this system is inconsistent if and only if the initial system is” or something?
I’m not sure whether I’m misunderstanding your point, but the paper proves that there is a coherent probability distribution P(.) that assigns probability 1 to both T and to the collection of reflection axioms [a < P(‘G’) < b] for P(.); this implies that there is a probability distribution over complete theories assigning probability 1 to (T + the reflection axioms for P). But if (T + the reflection axioms for P) were inconsistent, then there would be no complete theory extending it, so this would be the empty event and would have to be assigned probability 0 by any coherent probability distribution. It follows that (T + the reflection axioms for P) is consistent. (NB: by “the reflection axioms for P(.)”, I only mean the appropriate instances of [a < P(‘G’) < b], not anything that quantifies over a, b or G inside the object language.)
Incidentally, why bother with a schema? Reflection belongs in the meta language, so there’s no need to use a schema (?)
I think the point is that reflection gives an infinite collection of formal statements all of which must be assigned probability 1 (“axioms”), in analogy to how an axiom schema is a specification of an infinite collection of axioms. Whether “schema” is the right word to use here is debatable, I guess; I was happy with the choice but perhaps you could argue that “schema” should be reserved to recursively enumerable collections or something.
My point was that reflection is defined for the meta language, and quantifies over all the sentences in the object language. This is not something that can be added as an axiom in the object language at all—P (without the ’) has no meaning there.
So none of the sub-statements of reflection get assigned probability 1 - they just aren’t the kind of thing P works on. So I felt that calling this an schema distracted attention from what reflection is, which is a property of P, not axioms for the lower system.
But I may be misunderstanding the setup here...
Right, here’s what’s going on. The statement in the paper is,
The idea is not that this whole statement is an axiom schema. Instead, the idea is that the schema is the collection of the axioms
That makes sense...
I think this should be “Then P(G) ⇐ 1”.
No, that’s correct. P(G)<1 is the premise of a proof by contradiction.
Ah. I didn’t quite understand what you were trying to do there.
In general in this theory, I don’t think we have (p(phi) < 1 → p(phi) =1) → p(phi) = 1. The theory only reflects on itself to within epsilon, so what the theory would conclude if it were certain about p(phi) being less than 1 can’t be taken as the premise of a proof-by-contradiction in the same way that ~phi can be taken as a premise… ergh, I’m trying to figure out a more helpful way to state this than “I don’t think you can derive that kind of probabilistic proof by contradiction from the stated properties of the theory because the system is never supposed to know the exact probabilities it assigns”.
EDIT: Retracted pending further cogitation.
Stuart’s proof by contradiction goes through, as far as I can see. (The speculation in the last paragraph doesn’t, as Paul notes, and I don’t know what “Hence P(‘G’)=1” is supposed to mean, but the proof by contradiction part does work.)
ETA: I now think that “Hence P(‘G’) = 1” is supposed to mean that this statement is implied by the first-order theory (T + the reflection axioms).
I used the axioms as stated, and any non-intuitionist logic. If we want to capture your intuition, I think we’ll have to tweak the definitions...