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

• chili5
In summary, the conversation discusses difficulties in coming up with a proof for the statement |- (Box(P) ^ Box(Q)) -> Box(P ^ Q), where Box is the unary operator for "necessary for". The conversation also mentions several axioms and techniques such as Modus Ponens and Nec to arrive at the desired proof. The suggestion is to split the proof into separate cases and use the given axioms to prove each case, ultimately leading to the proof of the original statement. There is also a discussion about the meaning of placing a statement before the turnstyle and using it as a hypothesis.

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

Welcome to PF, chili5!

Couldn't you split the proof in separate proofs?

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

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

Last edited by a moderator:
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.

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.

I like Serena said:
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!

## What is a K system proof?

A K system proof is a type of mathematical proof that is used to show the validity of a statement or theorem without making any assumptions. It relies solely on the principles of logic and the given definitions and axioms.

## Why is it important to write a proof for p and q without assumptions?

Writing a proof for p and q without assumptions is important because it allows for a more rigorous and accurate demonstration of the validity of a statement or theorem. It eliminates the possibility of any errors or gaps in reasoning that may occur when assumptions are made.

## What are the steps involved in writing a K system proof?

The steps involved in writing a K system proof include: clearly stating the statement or theorem to be proven, defining any relevant terms, using logical and mathematical principles to demonstrate the truth of the statement, and making sure all steps are valid and without any assumptions.

## What are some common challenges when writing a K system proof?

Some common challenges when writing a K system proof include making sure all steps are logically sound and valid, avoiding circular reasoning, and being thorough and precise in the use of definitions and axioms.

## How do you know when a K system proof is complete?

A K system proof is considered complete when all steps are valid and logically sound, and it has been shown that the statement or theorem can be derived without making any assumptions.