We need to introduce four new rules. Why? Well we have two quantifiers and we need an introduction and elimination rule for each.
Two of the rules are very easy to specify. We consider only these easy ones in this tutorial. First think about a rule to eliminate the universal quantifier.
Universal Elimination: ^E
The idea here is simple. Suppose you have a derivation beginning like this:
Because line 2 says that everything is a B, it follows that anything 'd' might name is a B. So, at line 3, we can reasonably conclude that d is B. We justify this by ^E:
Make sure you see that this makes sense! Line 2 premises that everything is B, so we conclude on line 3 that d is B. Right? We call this "^E".
We could apply the same thinking and the same rule to line 1. This could result in which of the following?