# Help with a proof in Classical Sentence Logic

Premise: (A implies B) implies C

Conclusion: (C implies A) implies A

I had a logic exam a few hours ago and this was one of the problems, but I really didn't know where to start. Since the main connective of the conclusion is an implication, I figured I should assume (C implies A) and prove A...but this didn't lead anywhere, and I didn't have time to try out any other (more obscure, perhaps) lines of reasoning.

I think it would be a touch easier with derived rules and rules of replacement, because associativity and idempotence help to simplify the conclusion. But we were supposed to use only the "main" rules of Classical Sentence Logic.

• What is CSL? --
– user2953
Feb 12, 2015 at 18:46
• Classical sentence logic. Sorry if my question/terminology doesn't make sense. This is my first exposure to logic, so I don't know what terms are commonly used and things like that. Feb 12, 2015 at 18:48
• That's alright. As far as I know, 'the main rules of classical sentence logic' are not universally defined, so it would be helpful if you'd list those as well.
– user2953
Feb 12, 2015 at 19:03

Natural deduction is as much an art as a science --it takes some creativity. You might check my answer to How to prove a theorem using Sentential Derivation for some general advice. Keelan's method of solving is correct (and quite clever), but I suspect it might baffle a beginner. For that matter, it wouldn't have naturally occurred to me. I personally solved it in a somewhat more labor-intensive manner.

• Let's start as you did, by assuming C->A
• We know that we want to end with A, so now assume the opposite (Not A).

• Now we are apparently stuck. Is there anything that helps in the premise? If we had A->B we might get somewhere. How can we get A->B? Assume A and derive B. How to do this? If we do assume A, we have made two contradictory assumptions (A and Not A). We can subsequently get anything we want. In this case we want B, so we assume the opposite, show A and Not A and thus demonstrate B. Now we have A->B

• A->B gives us C (via the premise).

• C gives us A (via our first assumption).

• Now we have A and Not A at this level too. That means our assumption of Not A was wrong, and therefore A is correct (given C->A). That's exactly what we wanted all along.

You'll want to follow along by diagramming this (using whatever system you have been taught). You'll see it gets a little complex because of all the nested assumptions. However, as long as you are careful, they will all clear up neatly. You can't be afraid to make assumption after assumption, as long as you always know how deeply you have traveled. It's also OK to make contradictory assumptions, if they serve a purpose.

Keelan's version, which is shorter and less nested, starts from the fact that C OR Not C is a tautology (it is always true). Some systems will allow you to start with this, others would require you to prove it first.

• Thanks for this. I agree that the other answer is more elegant, but it's nice to see a proof using only some of the most basic rules. I think there was even a harder one of the exam, but I got it without trouble - proofs are fickle things. Feb 12, 2015 at 19:41

We make a case distinction over C.

Suppose C is true. Then if (C → A) we know A, so the statement holds.

Suppose C is false. Then, following the premise, (A → B) must be false (otherwise C would have been true). Now, recall the truth table of implication. (A → B) is false iff A is true(, but B not). Therefore, the statement holds for C is false as well.

Since the statement holds for both C being true and C being false, the statement holds in any case.

First we assume the premise,

• (A implies B) implies C.

Now we'll assume (C implies A), and try to prove A. (C implies A) may be rewritten as (not-C or A). So there are two cases:

Case 1: A is true. Done.

Case 2: not-C is true (that is, C is false). The contrapositive of the premise states:

• not-C implies not-(A implies B),

so we may conclude

• not-(A implies B).

This negation may be rewritten as

• A and not-B.

Thus A is true. Done.

This is an alternate proof provided since the OP had a constraint which this might fill:

But we were supposed to use only the "main" rules of Classical Sentence Logic.

Although this proof checker had a modus tollens rule it did not have a rule going from a conditional to a disjunction. Hence it might be closer to the available inference rules.

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, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf