• Support PF! Buy your school textbooks, materials and every day products Here!

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

  • Thread starter chili5
  • Start date
  • #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!
 

Answers and Replies

  • #2
I like Serena
Homework Helper
6,577
176
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.
 
  • #3
3
0
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:
  • #4
I like Serena
Homework Helper
6,577
176
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.
 
  • #5
I like Serena
Homework Helper
6,577
176
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.
 
  • #6
3
0
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!
 

Related Threads on K system proof - writing proof for p and q without assumptions

  • Last Post
Replies
1
Views
1K
  • Last Post
Replies
2
Views
572
  • Last Post
Replies
1
Views
603
  • Last Post
Replies
2
Views
821
  • Last Post
Replies
1
Views
897
Replies
2
Views
1K
Replies
3
Views
1K
Replies
2
Views
14K
Replies
1
Views
966
Top