Logic Proof with Natural Deduction: if I assume the antecedent, do I still have to prove the consequent?

Question

I have the unpleasent feeling that my "proof" is dead wrong. The core of my concerns is: when I have something like A -> (B -> C) and I assumed A, am I allowed to infer (B -> C) as the next step? In particular, I am struggling with the following proof: given

1. [ B -> (C v ~A) ] ^ [ ~B -> (D ^ A) ]

I am supposed to prove

A -> [ (B -> C) ^ (~B -> D) ] ^ (~A -> B)

Now, to prove (~A -> B) I wrote:

1. [ B -> (C v ~A) ] ^ [ ~B -> (D ^ A) ]
    2. ~A (assume)
        3. ~B (assume)
        4. D ^ A 
        5. A
    6. B (RAA)
7. ~A -> B

which should be ok (I hope). What I'm pretty sure is not ok is the rest:

To prove A -> (B -> C) I have:

1. [ B -> (C v ~A) ] ^ [ ~B -> (D ^ A) ]
    8. A (assume)
        9. B (assume)
       10. C v ~A
            11. ~A (assume)
            12. A
       13. C
       14. B -> C
    15. A -> (B -> C)

Questions:

1. Is it legit to infer 10 from 9 and 1?
2. Is it legit to infer 13 from 10-12?

Finally, to prove ~B -> (D ^ A) I have:

1. [ B -> (C v ~A) ] ^ [ ~B -> (D ^ A) ] 
    16. A (assume)
        17. ~B (assume)
        18. D ^ A
        19. D
    20. ~B -> D

Again, is it legit to infer 18 from 17 and 1?

Thank you.

Answer 1

About your question :

"when I have something like A→(B→C) and I assume A, am I allowed to infer (B→C)"

the answer is : Yes.

But with (A -> B) -> C , you cannot conclude anything only assuming A.

About :

"it is legit to infer 18 from 17 and 1 ?"

the answer is : Yes.

From 1. you derive (by ∧-elim) 1.b : [¬B→(D∧A)]; thus, assuming ¬B, by modus ponens (or →-elim) you can derive 18. : (D∧A).

About the proof of A -> (B -> C), the steps 10-13. are not clear.

Basically, ¬A∨C is equivalent to A→C; thus, assuming A you will get C, and the conclusion follows by two →-intro. With C∨¬A, which rule do you have applied ?

There is a rule called Disjunctive syllogism : from ϕ∨ψ and ¬ϕ, infer ψ; you have to check with your rule-set (or enlarge it adding "derived" rules).

If you do not have it, I suppose you have to use ∨-elim, i.e. : if ϕ⊢σ and ψ⊢σ, then ϕ∨ψ⊢σ.

Thus, you have to derive C from C (trivial) and C form ¬A (with the help of the assumption A), in order to conclude C, and then go on with the proof.

Answer 2

So, I guess officially the answer is almost surely "no", because you probably have made steps with rules that you haven't derived. But, interestingly enough, every step you've made actually seems valid!

"1. [ B -> (C v ~A) ] ^ [ ~B -> (D ^ A) ]
   8. A (assume)
      9. B (assume)
      10. C v ~A
         11. ~A (assume)
         12. A
      13. C
      14. B -> C
   15. A -> (B -> C)"

So, when you moved from step 9 to step 10, you basically used a rule {[$\alpha$ $\rightarrow$ $\beta$]$\land$$\gamma$], $\alpha$ $\vdash$ $\beta$]. This rule is valid, but is it in your given rule set or did you derive it first? It's derivation doesn't take many steps.

When you moved from step 12 to 13 you used a rule {($\alpha$ $\lor$ ~$\beta$), (~$\beta$ $\vdash$ $\beta$)} $\vdash$ $\alpha$. This consists of a perfectly valid rule in classical propositional calculus. For if (~$\beta$ $\vdash$ $\beta$), then by conditional introduction $\vdash$ (~$\beta$$\rightarrow$$\beta$). Since the law of clauvius ((~p$\rightarrow$p)$\rightarrow$p)) comes as provable from no premises, $\beta$ follows by conditional elimination. By double negation introduction we could infer ~~$\beta$. And then by disjunctive syllogism $\alpha$ follows. Thus, the move from step 12 to 13 does come as valid! But it's almost surely not formal because you didn't follow the a priori specified rules of the logical system you were working with, in effect you used a derivable rule without deriving it!

The move from step 13 to step 14 also works as valid. Thing is, I don't know how you did it. Did you discharge the assumption made in step 9, or do you have a rule $\alpha$ $\vdash$ ($\beta$ $\rightarrow$ $\alpha$) and thus the assumption made in step 9 still sits in place? Alright, I guess you discharged the assumption, but if you hadn't the move from step 14 to 15 would still come as valid. Since B would then come as the last hypothesis made, we could infer [B $\rightarrow$ (B $\rightarrow$ C)] discharging B, then by a rule which I would call "contraction" [$\alpha$ $\rightarrow$ ($\alpha$ $\rightarrow$ $\beta$)] $\vdash$ ($\alpha$ $\rightarrow$ $\beta$) we can infer (B $\rightarrow$ C). Then by the rule $\alpha$ $\vdash$ ($\beta$ $\rightarrow$ $\alpha$) we could infer (A $\rightarrow$ (B $\rightarrow$ C)) as a hypothesis. We might write this as...

1. [ B -> (C v ~A) ] ^ [ ~B -> (D ^ A) ]
   8. A (assume)
      9. B (assume)
      10. (C v ~A)
        11. ~A (assume)
        12. A  8 repitition
      13. C  from 10, and 11-12 by  {(α ∨ ~β), (~β ⊢ β)} ⊢ α
      14. (B -> C) from 13 by α ⊢ (β → α)
   15. (B->(B -> C)) 9-14 by conditional introduction
   16. (B -> C) 15 by [α → (α → β)] ⊢ (α → β)
17. A -> (B -> C) 8-16 by conditional introduction.

So, you almost surely didn't mean this. It helps to keep track of your assumptions a little more closely in some way.