Is there a reason why this differs from the standard presentation of K? Normally you would say that K is generated by the following (coupled with substitution):
Axioms: - All tautologies of propositional logic. - Distribution: □(x→y)→(□x→□y).
Rules of inference: - Necessitation: ⟨x,□x⟩. - Modus ponens: ⟨x→y,x,y⟩.
No particular reason (this is the setup used by Demski in his original probabilistic Payor post).
I agree this is nonstandard though! To consider necessitation as a rule of inference & not mentioning modus ponens. Part of the justification is that probabilistic weak distributivity (⊢x→y⟹⊢□px→□py) seems to be much closer to a ‘rule of inference’ than an axiom for me (or, at least, given the probabilistic logic setup we’re using it’s already a tautology?).
On reflection, this presentation makes more sense to me (or at least gives me a better sense of what’s going on / what’s different between □p logic and □ logic). I am pretty sure they’re interchangeable however.
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)
Is there a reason why this differs from the standard presentation of K? Normally you would say that K is generated by the following (coupled with substitution):
Axioms:
- All tautologies of propositional logic.
- Distribution: □(x→y)→(□x→□y).
Rules of inference:
- Necessitation: ⟨x,□x⟩.
- Modus ponens: ⟨x→y,x,y⟩.
No particular reason (this is the setup used by Demski in his original probabilistic Payor post).
I agree this is nonstandard though! To consider necessitation as a rule of inference & not mentioning modus ponens. Part of the justification is that probabilistic weak distributivity (⊢x→y⟹⊢□px→□py) seems to be much closer to a ‘rule of inference’ than an axiom for me (or, at least, given the probabilistic logic setup we’re using it’s already a tautology?).
On reflection, this presentation makes more sense to me (or at least gives me a better sense of what’s going on / what’s different between □p logic and □ logic). I am pretty sure they’re interchangeable however.
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)