# Natural deduction - sequent not valid (not provable)?

I'm working on a project assigned to me by my lecturer. It involves automated proofs. It is quite complex but I simplified it and narrowed it down to natural deduction. So far I have proven:

$$P(x) \rightarrow (Q(x) \rightarrow R(x)), P(y) \rightarrow P(x), P(y), R(x) \rightarrow \lnot R(y), \lnot R(y) \rightarrow R(x), Q(y)$$

and I have to show $$R(y)$$. I tried law of excluded middle ($$Q(x) \lor \lnot Q(x)$$ and $$P(x) \lor \lnot P(x)$$), proof by contradiction etc. but I just cannot prove it. I start to think that I'm lacking assumptions. Can someone confirm? Is this not provable?

Finding a counter example would maybe help me see what kind of assumption I'm missing.

There is not enough information to determine whether $$R(y)$$ is true or not. Let's see what you know. You've already proven $$P(y).$$ From that and $$P(y) \rightarrow P(x)$$ you can prove $$P(x).$$ From that and $$P(x) \rightarrow (Q(x) \rightarrow R(x))$$ you can prove $$Q(x) \rightarrow R(x).$$ And you also know that $$R(x) \leftrightarrow \lnot R(y)$$ which, combined with $$Q(x) \rightarrow R(x)$$, implies $$Q(x) \rightarrow \lnot R(y).$$ Finally, you've proven $$Q(y).$$ In summary, you know that $$P(x), P(y), Q(y)$$ are true. There are three scenarios for the rest:
• Suppose $$Q(x)$$. Then you know $$R(x)$$ and $$\lnot R(y)$$.
• Suppose $$\lnot Q(x)$$. Then either $$R(x) \land \lnot R(y)$$ or $$\lnot R(x) \land R(y)$$.
• Keep in mind though that even if you manage to show $\lnot Q(x)$ (which must hold for $R(y)$ having the possibility of being true), that won't tell you whether $R(y)$ is true or not. I.e. in order to show R(y), you either have to show that directly, or by showing $\lnot R(x)$. Jul 19, 2019 at 13:01