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: Ken Pledger on 20 Jan 2010 17:31 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. Ken Pledger.
From: William Elliot on 21 Jan 2010 01:21 On Wed, 20 Jan 2010, David C. Ullrich wrote: > <marsh(a)rdrop.remove.com> wrote: >> On Sun, 17 Jan 2010, Frederick Williams wrote: >> >>>> 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''_. >>>> >>>> Can somebody please help me out! >> >>> It helps to recall that A->B is A<->A.B and to derive the rule >>> A<->B / LA<->LB. >> >> That can be derived? >> Then (A <-> B) -> (LA <-> LB). > > Why? A <-> B |- LA -> LB implies |- (A <-> B) -> (LA -> LB) >> L(A <-> B) -> (LA <-> LB) is believable as is >> >> |- A <-> B implies |- LA <-> LB. > > Are you certain you know what he meant by the > symbol "/"? I'm not, but I _suspect_ that when > he says "A<->B / LA<->LB" that means exactly > the same thing as "|- A <-> B implies |- LA <-> LB". I alluded to both possibilities.
From: David C. Ullrich on 21 Jan 2010 08:54 On Wed, 20 Jan 2010 22:21:57 -0800, William Elliot <marsh(a)rdrop.remove.com> wrote: >On Wed, 20 Jan 2010, David C. Ullrich wrote: >> <marsh(a)rdrop.remove.com> wrote: >>> On Sun, 17 Jan 2010, Frederick Williams wrote: >>> >>>>> 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''_. >>>>> >>>>> Can somebody please help me out! >>> >>>> It helps to recall that A->B is A<->A.B and to derive the rule >>>> A<->B / LA<->LB. >>> >>> That can be derived? >>> Then (A <-> B) -> (LA <-> LB). >> >> Why? > >A <-> B |- LA -> LB > >implies > >|- (A <-> B) -> (LA -> LB) Yes. But where did that "A <-> B |- LA -> LB" come from? >>> L(A <-> B) -> (LA <-> LB) is believable as is >>> >>> |- A <-> B implies |- LA <-> LB. >> >> Are you certain you know what he meant by the >> symbol "/"? I'm not, but I _suspect_ that when >> he says "A<->B / LA<->LB" that means exactly >> the same thing as "|- A <-> B implies |- LA <-> LB". > >I alluded to both possibilities.
From: Frederick Williams on 21 Jan 2010 09:40 Max Weiss wrote: > > On Jan 17, 7:38 am, Frederick Williams <frederick.willia...(a)tesco.net> > wrote: > > It helps to recall that A->B is A<->A.B and to derive the rule > > A<->B / LA<->LB. > > Thanks! Could you please spell out the derivation? ---Max Sorry, I'm mistaken about this. I think you need LA.LB -> L(A.B) and LT as well. -- 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: Frederick Williams on 21 Jan 2010 09:43
"David C. Ullrich" wrote: > > [...] but I _suspect_ that when > he says "A<->B / LA<->LB" that means exactly > the same thing as "|- A <-> B implies |- LA <-> LB". That's what I meant (and it's true) but my hint is useless. See my second reply to Max. Sorry an' all. -- 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 |