# How should I use the propositional logic rules for → and ↔?

My question is how should I use the propositional logic rules for → and ↔ (although other rules may be required) to prove the following:

1. A → B, B → C ⊢ (AvB) → C

2. A ↔ B ⊢ ¬A ↔ ¬B

Please use the language of propositional logic.

Below are proofs for each problem. Here's an answer to your first question using conditional proof. If you're unfamiliar with it, conditional proof is a proof method in PL that allows you to assume the antecedent of a conclusion (assuming, of course, that the main operator of your conclusion is a conditional), and allows you to derive a conditional whose consequent is whatever you can deduce within the scope of your assumption. This is what's going on on lines 4-6. Notice the indentation - by convention, we indent whatever follows from our assumption, only returning to the non-indented position when we discharge our assumption by deriving the conditional (again, a conditional whose antecedent == whatever you've assumed). The question is how to use propositional logic rules for → and ↔ to prove the following:

1. A → B, B → C ⊢ (AvB) → C

2. A ↔ B ⊢ ¬A ↔ ¬B

The first proof illustrates the use of the conditional (→). On the first two lines of a natural deduction proof list the two premises, A → B and B → C. To show the conditional, (AvB) → C, assume the antecedent of the conditional, (AvB), and derive the consequent, C.

Can one derive the consequent from the two premises and that assumption? Since the antecedent is a disjunction we consider two cases, A and B.

For the A case, we use the first premise, A → B, to derive B using conditional elimination. We can use B and the second premise to derive C.

For the B case, we can use the second premise, B → C, to derive C using conditional elimination.

Since we were able to derive C from both of those cases we can use disjunction elimination and derive C. But then we can use conditional introduction to derive what we want: (AvB) → C.

For the second proof we have a biconditional as a premise, A ↔ B. We want to derive ¬A ↔ ¬B. We will create two subproofs to show this. First, we will show that ¬A implies ¬B. That will allow us to derive ¬A → ¬B. Then we will assume ¬B and derive ¬A. That will allow us to derive ¬B → ¬A. With those two subproofs we can derive what we want, the biconditional, ¬A ↔ ¬B. Here are the details for that using the proof checker associated with forallx, both linked below: 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/