1. The problem statement, all variables and given/known data 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". 2. Relevant equations 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. 3. 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?? Thanks!