Payor’s Lemma holds in provability logic, distributivity is invoked when moving from step 1) to step 2) and this can be accomplished by considering all instances of distributivity to be true by axiom & using modus ponens. This section should probably be rewritten with the standard presentation of K to avoid confusion.
W.r.t. to this presentation of probabilistic logic, let’s see what the analogous generator would be:
Axioms:
all tautologies of Christiano’s logic
all instances of (x→y)→(□px→□py) (weak distributivity) --- which hold for the reasons in the post
Rules of inference:
Necessitation ⟨x,□px⟩
Modus Ponens ⟨x→y,x,y⟩
Then, again, step 1 to 2 of the proof of the probabilistic payor’s lemma is shown by considering the axiom of weak distributivity and using modus ponens.
(actually, these are pretty rough thoughts. Unsure what the mapping is to the probabilistic version, and if the axiom schema holds in the same way)
Thanks.
Do you have a reference for this? Or perhaps there is a quick proof that could convince me?
Payor’s Lemma holds in provability logic, distributivity is invoked when moving from step 1) to step 2) and this can be accomplished by considering all instances of distributivity to be true by axiom & using modus ponens. This section should probably be rewritten with the standard presentation of K to avoid confusion.
W.r.t. to this presentation of probabilistic logic, let’s see what the analogous generator would be:
Axioms:
all tautologies of Christiano’s logic
all instances of (x→y)→(□px→□py) (weak distributivity) --- which hold for the reasons in the post
Rules of inference:
Necessitation ⟨x,□px⟩
Modus Ponens ⟨x→y,x,y⟩
Then, again, step 1 to 2 of the proof of the probabilistic payor’s lemma is shown by considering the axiom of weak distributivity and using modus ponens.
(actually, these are pretty rough thoughts. Unsure what the mapping is to the probabilistic version, and if the axiom schema holds in the same way)