17.2 →Elim and ↔Elim
You know how to do modus ponens in informal proofs. Now we'll learn how to do it in a formal proof.
You know enough about how we created BOOL, our first logical system, that you might be able to figure out how to make the new rules for PROP yourself. Before reading below, imagine what sentences you need, what the conclusion looks like, and how to cite →Elim.
Okay, here's our example. You need two sentences, just like for MP: you need an arrow sentence and the antecedent. The conclusion, then, is identical to the consequent.
Now let's try a real example. We want to prove this argument:
Now something more interesting:
Try to work it out yourself before reading any of our suggestions below.
Part of gaining expertise in proofs is knowing what information is most salient. You already know that the main connectives are the most salient bits of any proof. So your eyes already should have look at the disjunction and two arrows.
But which of those should jump out at you as the thing to start with?
Last proof, you started with the arrow, because you had the antecedent. But in harder proofs you won't have the antecedent handed to you; you have to earn it.
That's why you almost never start with arrow premises. If you don't have the antecedent, there's nothing to do right away. But with a disjunction you always know what to do.
When you sketch the proof out, it looks something like this:
Modus ponens, recall, works for the conditional and biconditional. Naturally, then, ↔Elim works just like →Elim. The only difference is that you can do in either direction with ↔.
Work out this whole proof yourself before answering the questions below.