Natural deduction - sequent not valid (not provable)?

Question

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.

Answer 1

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

You can verify that each of the three scenarios is compatible with your initial assertions.