In an attempt to prove the formula, I tried setting a hypothesis

C -> A

like the following

1   A <-> B             Premise
2   |C -> A         Hypothesis
3   |A -> B         1 (<->E)
4   |C -> B         1, 2, 3 (?????)

, but I don't know what rule to apply to support the forth line

|C -> B 

, even though I do know that I can reach this conclusion by combining 1, 2, 3.

What rule goes in to the ????? in the parenthesis above?

Also, I assume that I can prove

(C → A) → (C → B)

if I prove

A -> B 
C -> A

, but how do I add

C -> 

part to A and B?

I know that I can prove like if


is true, then

A V B 

is true as well (VI rule)

Also, if


is true and


is true, then

A Ʌ B 

is true as well (ɅI rule).

and in this proof I want to add

C ->

to A and B so it will be

(C -> A) -> (C -> B)

, but how can I do it? There are introduction rules like

(VI rule)
(ɅI rule)

, but it seems there is no rule like

(->I rule)

It may be easier to see the steps using the Fitch format of the natural deduction proof. Here is how the proof checker associated with the forallx text presents this:

enter image description here

Because one is trying to derive a conditional, assume the antecedent of the conditional which is what is done on line 2.

The consequent of the conditional is also a conditional. So assume the antecedent, $C$, of that conditional, $C \to B$. This was done one line 3.

Line 4 uses conditional elimination (→E) to derive $A$ referencing lines 2 and 3.

Line 5 uses biconditional elimination (↔E) to derive B referencing lines 1 and 4.

Note that $B$ is what we want to derive given the assumption of $C$ on line 3. At this point we can proceed with conditional introduction (→I) used twice to derive the desired goal.

Since there was some concern about the existence of the conditional introduction rule, see section 15.3 in the forallx text linked to below for a discussion of the conditional and the associated introduction and elimination 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, Winter 2018. http://forallx.openlogicproject.org/

  • 1
    $\begingroup$ Oh yes that's really clear and easy to understand. Thank you! $\endgroup$ – Shinichi Takagi May 13 at 13:28

An alternative proof using mainly (1) conditional proof and (2) contraposition.

It also makes use of the replacement rule : (X --> Y) :: ~ ( X & ~Y)

as definition of the material implication operator.

The strategy is as follows :

(1) since the desired conclusion is a conditional statement ( having itself conditional statements as antecedent and consequent, but that does not matter), and since a conditional statement is always equivalent to its contrapositive statement ( the contrapositive of X --> Y is ~ Y --> ~ X) , one can prove a conditional by proving its contrapositive ;

(2) the contrapositive of the desired conclusion is :

                 ~ ( C --> B)  -->  ~ ( C --> A) 

(3) in order to prove this contrapositive, we use conditional proof, by assuming the antecedent, and deriving the consequent under this assumption.

(4) finally, we use contraposition to recover the desired conclusion ( for the contrapositive of the contrapositive of X is X itself, or, in other words, the relation " being the contrapositive of " is a symmetric relation).

enter image description here


It is quite simple : you have to use the $(→ \text I)$ rule.

The first part of your proof is correct :

1) $A ↔ B$ --- premise

2) $C → A$ --- assumed [a]

3) $C$ --- assumed [b]

4) $A → B$ --- from 1) by $(↔ \text E)$

5) $A$ --- from 3) and 2) by $(→ \text E)$

6) $B$ --- from 5) and 4) by $(→ \text E)$

7) $C → B$ --- from 3) and 6) by $(→ \text I)$, discharging [b]

8) $(C → A) \to (C → B)$ --- from 2) and 7) by $(→ \text I)$, discharging [a].

  • $\begingroup$ Thank you for the explanation. Yeah it makes sense, but how does it lead to the final conclusion (C → A) → (C → B)? $\endgroup$ – Shinichi Takagi May 13 at 9:13
  • $\begingroup$ @ShinichiTakagi - Do you know the $(\to \text I)$ rule ? I've linked an explanation of it in my answer. $\endgroup$ – Mauro ALLEGRANZA May 13 at 9:34
  • $\begingroup$ Oh now I think I get it. C -> A is assumed, so if C -> B is either assumed or proven, then I can combine (C -> A) and (C -> B) by (->I) rule, which becomes (C → A) → (C → B), right? $\endgroup$ – Shinichi Takagi May 13 at 9:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.