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

Question

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

Edit 2

Answer 1

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 ^_^