1. Limited time only! Sign up for a free 30min personal tutor trial with Chegg Tutors
    Dismiss Notice
Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Homework Help: K system proof - writing proof for p and q without assumptions

  1. Oct 31, 2011 #1
    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??

  2. jcsd
  3. Nov 1, 2011 #2

    I like Serena

    User Avatar
    Homework Helper

    Welcome to PF, chili5! :smile:

    Couldn't you split the proof in separate proofs?

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

    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.
  4. Nov 1, 2011 #3
    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:

    [tex] \vdash ((Box(P) ^ Box(Q)) -> Box(P ^ Q))[/tex]

    This is what I thought use Ax1 to write:

    [tex] Box(P ^ Q) -> ((Box(P) ^ Box(Q)) -> Box(P ^ Q))[/tex]

    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:

    [tex]P, Q \vdash ... (Box(P) ^ Box(Q)) -> Box(P ^ Q)[/tex]
    Last edited by a moderator: Nov 1, 2011
  5. Nov 1, 2011 #4

    I like Serena

    User Avatar
    Homework Helper

    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.
  6. Nov 1, 2011 #5

    I like Serena

    User Avatar
    Homework Helper

    Or is there some special meaning to

    I don't understand what you mean by this sentence.
  7. Nov 1, 2011 #6
    Thanks this helps a lot!
Share this great discussion with others via Reddit, Google+, Twitter, or Facebook