# How does one go about proving (A&B)⊃C |- A⊃(B⊃C)?

I am relatively new to logic and deductive reasoning, so this problem has been giving me some trouble.

I want to start with an assumption of (A&B) and try to isolate a subproof where I can then get B⊃C through a conditional introduction, but I keep getting stuck in my subproofs and unable to reason out of them.

Any hints and demonstrations will be greatly appreciated!

• There is scope for many such demonstrations depending on the framework you're using! Do you have a set text that you're working from? – Paul Ross Oct 21 '18 at 18:53
• Damn, these symbols are implications and not subsets. Damn. – rus9384 Oct 22 '18 at 9:31

Assuming A&B will get you something of the form (A&B)⊃... which is not what you want. Instead, to derive A⊃... you want to start with assuming A.

It should go something like this.

``````1. (A&B)⊃C        premise
2. | A            assumption
3. | | B          assumption
4. | | A&B        2,3
5. | | C          1,4
6. | B⊃C          3,5
7. A⊃(B⊃C)        2,6
``````
• Indeed. In a Conditional Proof, one assumes the antecedant of the conclusion, and aims to derive the desired consequent. Basically, @MoIsStillHere : start from the finish and work your way backwards. – Graham Kemp Oct 24 '18 at 3:11

I want to start with an assumption of (A&B) and try to isolate a subproof where I can then get B⊃C through a conditional introduction, but I keep getting stuck in my subproofs and unable to reason out of them.

Indeed, you will not get far with assuming the antecedant of the premise.

Given (A&B)⊃C and assuming (A&B), will allow you to derive C, and from that B⊃C may be derived (assume B, restate C, discharge). However discharging the assumption of (A&B) therfore allows you to deduce,.. (A&B)⊃(B⊃C) from the premise. So close, but no good.

But looking at that should have shown you where you went wrong and indicate what to do.

In a Conditional Proof, one assumes the antecedant of the conclusion, and aims to derive the consequent. Basically: start from the finish and work your way backwards.

Okay. So you seek to derive A⊃(B⊃C) from (A&B)⊃C . Thus you should assume A aiming to derive B⊃C. To do that, you should assume B aiming to derive C.

`````` |_ (A & B) ⊃ C        by premise.
|  |_ A                 by assumption.
|  |  |_ B                by assumption.
|  |  :
|  |  :
|  |  |  C                we hope .
|  |  B ⊃ C             by discharging assumed B with conditional introduction.
|  A ⊃ (B ⊃ C)        by discharging assumed A with conditional introduction.
``````

Now how might you derive C ?

Well, it is time to use the premise. To derive C from (A&B)⊃C you will also need (A&B). We're okay. This can be derived from the assumptions.

Thus:

`````` |_ (A & B) ⊃ C        by premise.
|  |_ A                 by assumption.
|  |  |_ B                by assumption.
|  |  |  A & B            by conjunction introduction.
|  |  |  (A & B) ⊃ C      by restating the premise
|  |  |  C                by conditional elimination (modus ponens) .
|  |  B ⊃ C             by discharging assumed B with conditional introduction.
|  A ⊃ (B ⊃ C)        by discharging assumed A with conditional introduction.
``````

Now, can you do the converse? Prove A ⊃ (B ⊃ C) entails (A & B) ⊃ C.

The following proof agrees with the lines in Eliran H's answer, but it provides the justification.

The OP has the following concern which I would like to address by explaining how not to get stuck in the subproofs:

I want to start with an assumption of (A&B) and try to isolate a subproof where I can then get B⊃C through a conditional introduction, but I keep getting stuck in my subproofs and unable to reason out of them.

Here is the result using Klement's proof checker. Note that I am using "∧" rather than "&" and "→" rather than "⊃" so that I have well-formed formulas recognizable by the proof checker I am using. Also the inference rules are those the proof checker accepts. You may be required to use some different terminology: On line 1 is the premise: "(A ∧ B) → C"

Because I will have two conditionals, rather than assuming "(A&B)", I will break this up into two subproofs, one assuming "A" and the other assuming "B". This will allow me to get two conditionals.

I start the first subproof on line 2. Note how the subproof is indented in this style of presentation. I immediately start the second subproof on line 3. At this point I have both "A" (line 2) and "B" (line 3) and so I can combine them with conjunction introduction (∧I) on line 4.

This is the first line of the proof that was not a premise nor an assumption. I need to provide a justification for it. That justification is given by "∧I 2, 3". Those symbols mean I am using conjunction introduction on lines 2 and 3.

Since line 4 is the premise needed to get "C" on line 1, I can use modus ponens or conditional elimination (→E) as the proof checker I am using requires me to call it and reference lines 1 and 4 for the justification.

At this point I can close the subproof starting on line 3. This discharges the assumption on line 3. I assumed "B" and reached a line that has "C" on it so I can write on line 6 "B→C" which, if you think about it is just another way of writing that subproof--if I assume "B" then I can derive "C".

Note that I can now do the same thing for the subproof starting at line 2 and ending at line 6 again using conditional introduction. When I do that I get the desired result. The proof checker notes this with an acknowledgement that the proof is correct.

For more information about these particular rules see forall x. The link to the proof checker provides directions for how you may use it to check your other proofs.

Reference

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/