Recent content by chili5

  1. C

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

    Thanks this helps a lot!
  2. C

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

    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 ^...
  3. C

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

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