could someone help me check if my proof is valid?

Use direct proof to prove the following theorem: $$ A \lor (B \rightarrow A), B \vdash_R A $$

We aren't allowed to use proof by resolution, we can only use logic axioms and inference rules such as hypothetical and disjunctive syllogism, constructive and destructive dilemma, modus ponens and modus tolens. Also, we can use similar equivalencies like contraposition $(A \Rightarrow B) \Leftrightarrow (\lnot B \Rightarrow \lnot A)$

Here is my proof:

  1. $A \lor(B \rightarrow A)$, premise
  2. $B$, premise
  1. $\lnot A$, (assumption)
  2. $\lnot A \rightarrow(B \rightarrow A)$, elimination of disjunction from (1)
  3. $B\rightarrow A $, (modus ponens from (3), (4))
  4. $A$, (modus ponens from (2), (5))

The reason I'm asking is because I'm not sure if it is valid, since I made an assumption that A is incorrect and used it as a premise until I got to a contradiction at $6.$

Since I have used an incorrect assumption as a premise, should I start anew but using the assumption that A is true, albeit me getting a contradiction?


2 Answers 2


This is a valid proof (minus a potential error in notation and a little cleanup at the end) but I wouldn't call it a "direct" or constructive proof, but instead a proof by contradiction. Replacing your assumption of $\neg A$ with assuming $A$ would not be helpful because proving $A$ while assuming $A$ is not helpful, it's a circular argument. I think you can extend your logic in this proof to a direct proof without too much trouble, but there's actually a much simpler way to do it.

As a hint, try starting by rewriting the implication in your first premise as a disjunction: $X \to Y \leftrightarrow \neg X \vee Y.$ From there a direct proof will follow very easily.

  • $\begingroup$ Then it indeed turns into a simple proof using the argument of disjunctive syllogism. However, I never knew I am allowed to do that. I thought I can only do that if my premise is only consisted of a single implication (say, if I had only $B \rightarrow A$ for example, or any other implication), but since this is a disjunction involving a literal and another expression, I wasn't sure if I am allowed to do that. $\endgroup$
    – john doe
    Commented Apr 17, 2021 at 14:25
  • $\begingroup$ I believe for any case like this, if you can simplify one part of an expression using a rule to an equivalent expression, then you can substitute the simplification for the smaller expression to get an equivalent statement for the larger expression. (sorry I know that's a mouthful) $\endgroup$ Commented Apr 17, 2021 at 14:34

Under the assumption of $\lnot A$ you have derived a contradiction (since you have derived $A$). You are not finished, as the subproof is still open at this point.

So the next step is to discharge that assumption, closing this indirect proof and deriving $A$ under only the premises.

Look to you rules on negation intro/elim to see how your particular system implements this (it varies).


You must log in to answer this question.

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