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?

enter image description here


enter image description here

Edit 2

enter image description here


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

  • $\begingroup$ I think now I managed to build the proof.. Check that out, please $\endgroup$
    – lucasbbs
    Apr 19 at 2:27
  • $\begingroup$ 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 ^_^ $\endgroup$ Apr 19 at 4:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.