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

Question

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.

Answer 1

Below are proofs for each problem.

Answer 2

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

Answer 3

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/