Natural Deduction Proof: A ↔ B |- (C → A) → (C → B)

Question

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

A 

is true, then

A V B 

is true as well (VI rule)

Also, if

A 

is true and

B 

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)

Answer 1

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:

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/

Answer 2

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].

Answer 3

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).