modal logic exercise
in [Logic]
|
Prev: proof that once Finite is precisely defined that Algebra on infinite set is nonexistent #302; Correcting Math
Next: sci.math-survey and math textbook survey of defining "finite number" #307; Correcting Math
From: Frederick Williams on 21 Jan 2010 09:50 Ken Pledger wrote: > > In article > <23e22f17-9223-4f3d-aecf-4d196c064aca(a)v25g2000yqk.googlegroups.com>, > Max <30f0fn(a)gmail.com> wrote: > > > I just started going through _Dynamic Epistemic Logic_ by van > > Ditmarsch et al. I am a little rusty on modal logic and have gotten > > stuck on an early exercise. > > > > The problem is actually misstated in the book, but I'm pretty sure > > that what they mean (or, the component of what they're asking for that > > I'm stuck on) is: > > > > Let the logic _K''_ result from the usual logic _K_ by replacing the > > axiom scheme > > > > k: L(A->B) -> (LA -> LB) > > > > with the scheme > > > > k'': L(A.B) -> LA . LB. > > > > Show that every instance of the k scheme is derivable in the logic > > _K''_. > > .... > > You say "I'm pretty sure that what they mean .... is ...." > I wonder whether you may have that wrong. If the main operator of your > k'' is material _equivalence_ rather than implication, then you're very > close to what's explained in Hughes & Cresswell, 1st edition, pp.123-5. > (They consider T rather than K, but that shouldn't matter much.) > Instead of the necessitation rule, that approach uses the rule: > if |- (A <-> B) then |- (LA <-> LB). > I haven't proved that your version above doesn't work; but it would be a > bit surprising to find that the argument in Hughes & Cresswell uses a > stronger basis than it needs. I haven't tried but I wonder if the asked for derivation can be proved invalid by using neighbourhood models. Rule A <-> B / LA <-> LB plus axiom L(A.B) -> LA . LB is what Chellas calls EM which is strictly weaker than K. -- Pigeons were widely suspected of secret intercourse with the enemy; counter-measures included the use of British birds of prey to intercept suspicious pigeons in mid-air. Christopher Andrew, 'Defence of the Realm', Allen Lane
From: Ken Pledger on 21 Jan 2010 14:54 In article <ken.pledger-B99907.11314021012010(a)news.eternal-september.org>, Ken Pledger <ken.pledger(a)mcs.vuw.ac.nz> wrote: > In article > <23e22f17-9223-4f3d-aecf-4d196c064aca(a)v25g2000yqk.googlegroups.com>, > Max <30f0fn(a)gmail.com> wrote: > > .... I'm pretty sure that what they mean .... is: > > > > Let the logic _K''_ result from the usual logic _K_ by replacing the > > axiom scheme > > > > k: L(A->B) -> (LA -> LB) > > > > with the scheme > > > > k'': L(A.B) -> LA . LB. > > > > Show that every instance of the k scheme is derivable in the logic > > _K''_. > > .... > > > You say "I'm pretty sure that what they mean .... is ...." > I wonder whether you may have that wrong. If the main operator of your > k'' is material _equivalence_ rather than implication, then you're very > close to what's explained in Hughes & Cresswell, 1st edition, pp.123-5. > (They consider T rather than K, but that shouldn't matter much.) > Instead of the necessitation rule, that approach uses the rule: > if |- (A <-> B) then |- (LA <-> LB). > I haven't proved that your version above doesn't work; but it would be a > bit surprising to find that the argument in Hughes & Cresswell uses a > stronger basis than it needs. > > Ken Pledger. On 21-1-2010, at 2.54 PM, max.morgan.weiss(a)gmail.com privately e-mailed: > .... We toyed around with using L(A.B)<->LA.LB instead of L(A.B)<->LA.LB > but still couldn't manage it.... O.K. As suggested above, I'll assume the axiom schema: (1) LA.LB -> L(A.B) and the rule: (2) if |- (A <-> B) then |- (LA <-> LB). By PC A.(A -> B) -> B Then by (2) L(A.(A -> B)) -> LB From (1) LA.L(A -> B) -> L(A.(A -> B)) From the last two formulae by PC LA.L(A -> B) -> LB By PC L(A -> B) -> (LA -> LB) q.e.d. Ken Pledger.
From: Ken Pledger on 25 Jan 2010 17:05
In article <ken.pledger-1A1D96.08540222012010(a)nothing.attdns.com>, Ken Pledger <ken.pledger(a)mcs.vuw.ac.nz> wrote: > .... > O.K. As suggested above, I'll assume the axiom schema: > (1) LA.LB -> L(A.B) > and the rule: > (2) if |- (A <-> B) then |- (LA <-> LB). > > By PC A.(A -> B) -> B > Then by (2) L(A.(A -> B)) -> LB > From (1) LA.L(A -> B) -> L(A.(A -> B)) > From the last two formulae by PC > LA.L(A -> B) -> LB > By PC L(A -> B) -> (LA -> LB) .... An e-mail from the OP pointed out (very politely) that I messed up that proof. :-( (1) needs to be (3) LA.LB �<-> �L(A.B) after all. ��The corrected proof is then: By PC A.(A -> B) �<-> �(A.B) Then by (2) L(A.(A -> B)) �<-> �L(A.B) so by (3) and PC LA.L(A -> B) �<-> �L(A).L(B) so by PC L(A -> B) -> (LA -> LB). Ken Pledger. |