I initially played around with the idea of freezing the final probability assignments when you find a contradiction, but couldn’t get it to work. The difficulty was that if you assumed the inconsistency of PA you got that the limit was simply the assignment at some future time, but you couldn’t defer to this because the function was not computable according to PA (by the consistency results in the paper). Something along these lines might still work.
As I worked on this approach I noticed a statement that seems both true and interesting which I delayed proving because I wasn’t sure how to get everything else to work. Let χ:=Con(PA) then it seems to me that we should have for any deferral function f(n)
En(Pf(n)(ϕ)|χ)≂nPn(ϕ)
The reason why I think it’s true is that conditioning on χ which is true should only improve our estimate of Pf(n)(ϕ), but if this estimate is actually improved it will be exploited by some poly-time trader. It would be very interesting if this weren’t the case since then conditioning on a true statement might actually be bad for us, but if it is true we automatically get the same for ¬χ instead by some simple algebra (we could then say that infinitary consistency and inconsistency are irrelevant for determining probabilities at any computable times).
Edit, Proof: Let {Pn} be constructed as in the paper. Then PA+Con(PA) proves that {Pn} and {Pf(n)} are logical inductors. We get that
En(Pf(n)(ϕ)|χ)≂nEn(P∞(ϕ)|χ)≂nEn(Pn(ϕ)|χ)
Here the final expression can be expanded out as
n∑k=11nPn(Pn(ϕ)>k/n∧χ)/Pn(χ)
Fix ϵ>0 we can pick n>1/ϵ large enough that Pn believes that Pn(ϕ) is within an interval of size ϵ with probability at least 1−ϵ. Then Pn believes that Pn(ϕ)>k/n∧χ is equivalent to ⊥ or χ (depending on whether k is above or below some threshold) with probability at least 1−ϵ. In both of these cases we get that Pn(Pn(ϕ)>k/n∧χ)=Pn(Pn(ϕ)>k/n)Pn(χ) (or perhaps some extra epsilons here)
Now we can cancel and get that the expression is eventually within Cϵ (for some C<10) of
I initially played around with the idea of freezing the final probability assignments when you find a contradiction, but couldn’t get it to work. The difficulty was that if you assumed the inconsistency of PA you got that the limit was simply the assignment at some future time, but you couldn’t defer to this because the function was not computable according to PA (by the consistency results in the paper). Something along these lines might still work.
As I worked on this approach I noticed a statement that seems both true and interesting which I delayed proving because I wasn’t sure how to get everything else to work. Let χ:=Con(PA) then it seems to me that we should have for any deferral function f(n)
En(Pf(n)(ϕ)|χ)≂nPn(ϕ)
The reason why I think it’s true is that conditioning on χ which is true should only improve our estimate of Pf(n)(ϕ), but if this estimate is actually improved it will be exploited by some poly-time trader. It would be very interesting if this weren’t the case since then conditioning on a true statement might actually be bad for us, but if it is true we automatically get the same for ¬χ instead by some simple algebra (we could then say that infinitary consistency and inconsistency are irrelevant for determining probabilities at any computable times).
Edit, Proof: Let {Pn} be constructed as in the paper. Then PA+Con(PA) proves that {Pn} and {Pf(n)} are logical inductors. We get that
En(Pf(n)(ϕ)|χ)≂nEn(P∞(ϕ)|χ)≂nEn(Pn(ϕ)|χ)
Here the final expression can be expanded out as
n∑k=11nPn(Pn(ϕ)>k/n∧χ)/Pn(χ)
Fix ϵ>0 we can pick n>1/ϵ large enough that Pn believes that Pn(ϕ) is within an interval of size ϵ with probability at least 1−ϵ. Then Pn believes that Pn(ϕ)>k/n∧χ is equivalent to ⊥ or χ (depending on whether k is above or below some threshold) with probability at least 1−ϵ. In both of these cases we get that Pn(Pn(ϕ)>k/n∧χ)=Pn(Pn(ϕ)>k/n)Pn(χ) (or perhaps some extra epsilons here)
Now we can cancel and get that the expression is eventually within Cϵ (for some C<10) of
∑k1nPn(Pn(ϕ)>k/n)=En(Pn(ϕ))≂nPn(ϕ)