# How to prove that $P_b \leftrightarrow (P_a \land P_b), P_a \leftrightarrow \neg P_b \vdash P_a$ with natural deduction

I need to build a proof for $$P_b \leftrightarrow (P_a \land P_b), P_a \leftrightarrow \neg P_b \vdash P_a$$ with natural deduction... I have built the following proof, however I am stuck in the middle of the problem. How can I finish it?

# Edit 2

Welcome to MSE!

First, I would review the introduction/elimination rules for the sequent calculus. Your last step is

$$\frac{\lnot P_b \quad P_a \to \lnot P_b}{P_a}$$

but this is not a valid inference rule. You call it $$\to_e$$, but $$\to_e$$ actually says

$$\frac{P \quad P \to Q}{Q}$$

knowing the conclusion doesn't let us infer anything about the assumption!

As for solving the problem, here's an informal proof. It will be a good exercise for you to convert it into a formal proof tree:

Since $$P_b \leftrightarrow P_a \land P_b$$, and $$P_a \leftrightarrow \lnot P_b$$, we see that $$P_b \leftrightarrow \lnot P_b \land P_b$$. That is, $$P_b \leftrightarrow \bot$$. But then $$P_a \leftrightarrow \lnot \bot$$, so $$P_a = \top$$, as desired.

As a hint for turning this into a proof tree, we will end with

$$\frac{\lnot P_b \to P_a \quad \lnot P_b}{P_a}$$

the proper direction for $$\to_e$$. Building $$\lnot P_b \to P_a$$ is easy -- it's basically one of your axioms. Building a $$\lnot P_b$$ is trickier. You'll want to build a proof that $$P_b \to \bot$$. So assume you have a $$P_b$$, and then chase through the informal proof that I outlined above. Can you finish it from here?

I hope this helps ^_^

• I think now I managed to build the proof.. Check that out, please Apr 19 at 2:27
• Provided I'm reading your proof tree correctly (your exact notation is different from the one that I'm familiar with) it looks good to me ^_^ Apr 19 at 4:58