# Help with a modal Hilbert-style proof of (□(a>b)&◊(a&c))>◊(b&c)

Can't grasp how it can be proved. To proof just propositional calculus formula (without modal operators) at first seems rather natural to me. Tried the law of importation scheme but it didn't work out.

Update:

there are a lot axiom schemata allowed (actually, any usage of theorems would work) + K + MP + Substituition no assumptions no premises

I've never done much modal logic, but I think I can outline a proof for you assuming I'm reading this correctly.

(□(a>b)&◊(a&c))>◊(b&c)

meaning

((NecessaryThat(a IMPLIES b) AND PossibleThat(a AND c))
IMPLIES
PossibleThat(b AND c)

So, proceed as follows:

1. Assume N(a IMPLIES b) AND P(a AND c)
2. P(a AND c)
3. P(a) AND P(c)
4. P(a)
5. P(c)
6. N(a IMPLIES b)
7. P(a IMPLIES b)
8. P(a) IMPLIES P(b)
9. P(b) (via 4 and 8)
10. P(b) AND P(c) (via 9 and 5)
11. P(b AND c) THEREFORE... 1 IMPLIES 11

You might have to tweak this to fit the exact axioms open to you, but I think the basic approach is sound.

EDIT: Try this kind of approach

1. a -> P(a)
2. b&c -> P(b&c)
3. ((a->b)&c) ->P(b&c)
4. (N(a->b) & c) -> P(b&c) etc...
• Thank you, Chris! Unfortunately, I am not allowed to use assumption and hypotheses. – user8354 Jul 4 '14 at 6:04