I still feel like I don’t understand most things in the paper, but I think this construction should work:
Say we start with some deductive sequence {Dn} that is PA-complete. Now redefine the computation of this deductive sequence to include the condition that if ever at some stage n we find that PA is inconsistent (i.e. that Dn is propositionally inconsistent) we continue by computing {Dm:m≥n} according to Dm=Dm−1∪{ϕm} where ϕm is the lexicographically-first sentence propositionally consistent with Dm−1.
Since PA is consistent this deductive process is extensionally identical to the one we had before, but now PA proves that it’s a deductive process: assuming consistency it’s a PA-complete deductive process, and assuming inconsistency it’s over some very arbitrary, but complete and computable, propositional theory. We can now carry out the construction in the paper to get the necessary logical inductor over PA which we denote by {Pn}. Here PA proves the convergence of the logical inductor as in the paper.
Fix ϕ and ϵ>0, and write Xn:=Pn(ϕ) and X:=P∞(ϕ). We want to say that eventually |Xn−EnX|<ϵ, but by self-trust and linearity it’s enough to show that eventually En(|Xn−X|)<ϵ. This would follow from eventually having Pn(|Xn−X|≥ϵ)<ϵ (as PA proves that Xn,X∈[0,1] which gives that |Xn−X|≤1)
[edit2: this paragraph is actually false as written, I have a modified proof that works for PA+¬Con(PA), but it suggests that this construction is broken] From the proof that Xn→X we have that there is some A∈[N]<ω such that PA proves that |Xn−X|<ϵ for n∉A. Define ψn to be |Xn−X|<ϵ. This is an efficiently computable sequence of sentences of which all but finitely many are theorems, so we get that Pn(¬ψn)→0 (consider starting the inductor at some later point after all the non-theorems have passed) which means that there is some N where n>N implies Pn(¬ψn)<ϵ which proves the result. [edit: some polishing to this paragraph]
Note, this ignores some subtleties with the fact that X could be irrational and therefore not a bona fide Logically Uncertain Variable. These concerns seem beside the point as we can get the necessary behavior by formalizing Logically Uncertain Variables slightly differently in terms of Dedekind cuts or perhaps more appropriate CDFs: Cumulative Distribution Formulae.
I still feel like I don’t understand most things in the paper, but I think this construction should work:
Say we start with some deductive sequence {Dn} that is PA-complete. Now redefine the computation of this deductive sequence to include the condition that if ever at some stage n we find that PA is inconsistent (i.e. that Dn is propositionally inconsistent) we continue by computing {Dm:m≥n} according to Dm=Dm−1∪{ϕm} where ϕm is the lexicographically-first sentence propositionally consistent with Dm−1.
Since PA is consistent this deductive process is extensionally identical to the one we had before, but now PA proves that it’s a deductive process: assuming consistency it’s a PA-complete deductive process, and assuming inconsistency it’s over some very arbitrary, but complete and computable, propositional theory. We can now carry out the construction in the paper to get the necessary logical inductor over PA which we denote by {Pn}. Here PA proves the convergence of the logical inductor as in the paper.
Fix ϕ and ϵ>0, and write Xn:=Pn(ϕ) and X:=P∞(ϕ). We want to say that eventually |Xn−EnX|<ϵ, but by self-trust and linearity it’s enough to show that eventually En(|Xn−X|)<ϵ. This would follow from eventually having Pn(|Xn−X|≥ϵ)<ϵ (as PA proves that Xn,X∈[0,1] which gives that |Xn−X|≤1)
[edit2: this paragraph is actually false as written, I have a modified proof that works for PA+¬Con(PA), but it suggests that this construction is broken] From the proof that Xn→X we have that there is some A∈[N]<ω such that PA proves that |Xn−X|<ϵ for n∉A. Define ψn to be |Xn−X|<ϵ. This is an efficiently computable sequence of sentences of which all but finitely many are theorems, so we get that Pn(¬ψn)→0 (consider starting the inductor at some later point after all the non-theorems have passed) which means that there is some N where n>N implies Pn(¬ψn)<ϵ which proves the result. [edit: some polishing to this paragraph]
Note, this ignores some subtleties with the fact that X could be irrational and therefore not a bona fide Logically Uncertain Variable. These concerns seem beside the point as we can get the necessary behavior by formalizing Logically Uncertain Variables slightly differently in terms of Dedekind cuts or perhaps more appropriate CDFs: Cumulative Distribution Formulae.