K system proof - writing proof for p and q without assumptions

[chili5]

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!

 

[I like Serena]

Welcome to PF, chili5!

Couldn't you split the proof in separate proofs?

So you'd start with:
P, Q \vdash ... (Box(P) \wedge Box(Q)) \to Box(P \wedge Q)
then proof
\neg P, Q \vdash ... (Box(P) \wedge Box(Q)) \to Box(P \wedge Q)
and so forth, finally combining them to:
\vdash (Box(P) \wedge Box(Q)) \to Box(P \wedge Q)

I think you need to do something like this, because otherwise you can never get for instance Box(P).
The only way to get Box(P) is with Nec, and the only way to apply Nec is if you have P given.

 

[chili5]

Thanks! :)

The problem is though I'm not actually given p or q. Or is there some other reason you can write P before the turnstyle?

This is the question:

\vdash ((Box(P) ^ Box(Q)) -> Box(P ^ Q))

This is what I thought use Ax1 to write:

Box(P ^ Q) -> ((Box(P) ^ Box(Q)) -> Box(P ^ Q))

Then if we can write P ^ Q we can use Nec to write Box(P ^ Q). Then use MP on Box(P ^ Q) and line 1 from axiom 1. To write P ^ Q we need to write P and Q. We can write a proof for P -> P pretty easily. Is there someway to go from P -> P to just P?

So we have this axiom: P -> (Q -> (P ^ Q)).

so I don't think I can do this:

P, Q \vdash ... (Box(P) ^ Box(Q)) -> Box(P ^ Q)

 

[I like Serena]

Putting P before the turnstyle means that you use P as a hypothesis.
That is: Assuming P is true, then ...

You can't get P otherwise, since the statement P means: "P is true".
Same for P^Q, it means: "P and Q are both true".
You can state P->P, since that only means: "if P is true, then P is true", which is self-evident.

The crux of my suggestion is to split the proof in separate cases, as you would in a truth table.
Since all results are the same, the proof must be valid regardless of the hypotheses.

 

[I like Serena]

Or is there some special meaning to

Box is the unary operator for "necessary for".

?

I don't understand what you mean by this sentence.

 

[chili5]

Putting P before the turnstyle means that you use P as a hypothesis.
That is: Assuming P is true, then ...

You can't get P otherwise, since the statement P means: "P is true".
Same for P^Q, it means: "P and Q are both true".
You can state P->P, since that only means: "if P is true, then P is true", which is self-evident.

The crux of my suggestion is to split the proof in separate cases, as you would in a truth table.
Since all results are the same, the proof must be valid regardless of the hypotheses.

Thanks this helps a lot!