I'm having some issues coming up with a proof for |- (Box(P) ^ Box(Q)) -> Box(P ^ Q).
Box is the unary operator for "necessary for".
Axiom 1 A -> (B -> A)
Axiom 2 (A -> (B -> C)) -> ((A->B) -> (A -> C))
Axiom 3 (~a -> B) -> ((~A -> ~B) -> A)
Axiom 4 A ^ B -> A
Axiom 5 A ^ B -> B
Axiom 6 A -> (B -> A ^ B)
Modus Ponens A and A -> B write B
Nec: A written without assumptions can write Box(A)
Note: Box means necessary for.
The Attempt at a Solution
There are no assumptions for this and I started by writing
Box(p ^ q) -> (( Box(p) ^ Box(q)) -> Box(p ^ q)) by Axiom 1
Now Nec says if I can write p ^ q then I can write Box(p^q) and then use modus ponens to arrive at what I'm looking for. The problem I'm having is coming up with a proof for p ^ q.
Axiom 6 seems useful so I can write p -> (q -> (p ^ q)) which makes sense. This would require me to write p and q which is where I'm having problems. I don't even know if this is actually possible without some kind of assumption.
I'm stuck here. Does this look like it's on the right track or can somebody help me get a good start on this??