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.


1 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.

  • $\begingroup$ Thank you very much. That did indeed help me a lot. I kinda was at that point as well, but i couldn't state it as clear as you did. Now I know that I have to investigate my Q a bit more. $\endgroup$
    – Rolle
    Jul 19, 2019 at 11:21
  • $\begingroup$ Oh, that was so simple to solve with your help. I was sitting over that prove almost a week. Thanks again $\endgroup$
    – Rolle
    Jul 19, 2019 at 11:58
  • $\begingroup$ 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)$. $\endgroup$
    – posilon
    Jul 19, 2019 at 13:01

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .