- #1

- 3

- 0

## Homework Statement

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".

## Homework 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.

## 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!