# Help with natural deduction by introduction and elimination rules

This is where I’ve gotten so far. I’ve proven it from left to right but I’m getting some trouble proving it from right to left. I’m trying to reach the conclusion by double negation.

• Oct 9, 2019 at 18:38
• My professor only wants us to use the introduction and elimination rules Oct 9, 2019 at 20:04
• You might be able to show this directly by assuming A on line 2 and then considering the two cases in line 1. In both you will need to derive B. Here is a proof checker you can use to guide your work: proofs.openlogicproject.org Oct 9, 2019 at 20:20
• Well you can use conditional proof with assuming \$A\$, and then double negation of \$A\$, and then destructive syllogism on ~AvB and ~~A, to deduce B. Oct 9, 2019 at 20:31
• Have you completed this yet? Nov 9, 2019 at 8:10

Right to left? But that's the easy one. The harder one is left to right, because it's not a valid rule in Intuitionistic logic and so it requires extra rules, specific to Classical logic, such as double-negation elimination. You split the disjunction. Working backwards, it looks like this:

``````            ¬A ∨ B ⊢ A ⊃ B
⇐       ¬A ⊢ A ⊃ B      │       B ⊢ A ⊃ B
⇐       ¬A, A ⊢ B       │       B, A ⊢ B
``````

You haven't laid out what the specifics of your natural deduction system is (and there are many variants), but you should be able to take it from there.

I’m trying to reach the conclusion by double negation.

Well, you might do that, but it is not indicated. You have a premise that is a disjunction and a conclusion that is a conditional.

You will want to use a Conditional Proof to introduce the conditional, so assume A attempting to derive B.

You will want to use a Proof by Cases to eliminate the disjunction in the premise. So do that .

``````   1 (1) ~A v B  Premise
2 (2) A       Assumption
3 (3) ~A      Assumption
... (4) ...     ...
2,3 (5) B       ...
4 (6) B       Assumption
1,2 (7) B       Disjunction Elimination 1,2-5,6-6
1 (8) A -> B  Conditional Introduction 2-7
``````

I took symbolic logic a while ago, but I believe this should be correct. Apologies for my sometimes messy handwriting.

The truth table definition of `A -> B` says that:

• `~A` implies `A -> B` is true
• `B` implies `A -> B` is true

PROOF OF `(~A v B) --> (A --> B)`

``````0 ....    (~A v B)         ..... assumption
1 ....    ~A --> (A --> B) ..... by truth-table definition of logical implication
2 ....    B  --> (A --> B) ..... by truth-table definition of logical  implication
3 ....    A --> B          ..... 0, 1, 2  proof by cases
``````
• This is not a natural deduction proof. Apr 4, 2020 at 17:04