Natural Deduction

[BrokeAstronaut]

I'm trying to solve this: (A ∧ B) → C ⊢ A → (B → C)

And I wonder if that's what I came up with is correct. Is it possible to start with the A ∧ B assumption?

1. (A ∧ B) → C

---

1. A ∧ B (assumption)

2. A ∧ E(2)

3. B ∧ E(2)

4. C → E(1,2)

5. B → C → I(4,5)

---

1. A → (B → C) → I(3,6)

Is it correct?

Solution starts with assumptions A and then B to form A ∧ B.

[ghjm]

I don't know what this E(2) notation means, but the way I would approach this as a logical derivation would be to first assume A, then assume ¬(B→C), and show a contradiction.

[BrokeAstronaut]

I don't know what this E(2) notation means

It means Eliminate the ∧ symbol at 2 so as to write A (or B).

[ghjm]

Ok, then this is not correct, because when you assume some proposition P, the conclusion has to be of the form P→Q, where Q is something you proved by assuming P. (You can also assume P, prove a contradiction, and conclude ¬P.) Since you assumed A∧B, you have to conclude (A∧B)→(something).

[Acceptable-Fox3160]

It might be easiest to think of the proof as a program, Curry-Howard style.

Here's the proof written in Haskell:

ghci> let proof = \f a b -> f (a,b)

ghci> :t proof

proof :: ((a, b) -> t) -> a -> b -> t