Is this a valid proof of $ A \lor (B \rightarrow A), B \vdash_R A $

Question

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

3. $\lnot A$, (assumption)
4. $\lnot A \rightarrow(B \rightarrow A)$, elimination of disjunction from (1)
5. $B\rightarrow A $, (modus ponens from (3), (4))
6. $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?

Answer 1

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.

Answer 2

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