Derivations involving predicate logic (using variables such as F and G) are somewhat more complicated than those which involve only propositional logic (using variables such as P and Q). This is because often we have to drop down into an imagined vsw (very small world) to show that something would be true hypothetically.
For instance, supposing we have the case "Anyone who is rich is famous, and there is somebody rich, so there has to be somebody famous." Let's use the variable F for the idea of being rich and the variable G for the idea of being famous. Symbolized the pattern is FGD, FW |- GW.
We clearly need some additional rules:
FV |- Fa (this could be anyone's name) -- V elim
FW |- Fa (this must be a new name and it is used hypothetically)
FGD |- FaGaC (this could be anyone's name) -- D elim
FGE |- FaGaA (this must be a new name) -- E elim
Fa |- FW -- W int
Fa |- FV (provided that the name is "free" in the sense it could refer to anybody at all in our vsw; in practice this usually means that it did not appear as a result of W elim or E elim) -- V int
FGD |- GNFND and GNFND |- FGD -- D subs
FGE |- GFE and GFE |- FGE -- E subs
FGDN |- FGNE and FGNE |- FGDN -- DN subs
FGEN |- FGND and FGND |- FGEN -- EN subs
FVN |- FNW and FNW |- FVN -- VW subs
...note that the following patterns also are instances of VW subs:
---FWN |- FNV, FNVN |- FW, FNWN |- FV
Let's do the derivation for the original problem.
1. FGD
2. FW \ show GW
3. Fa.............2 W elim (note we do this first to avoid problems with any new name)
4. FaGaC.......1 D elim
5. Ga.............3,4 C elim
6. GW............5 E int
Sometimes, though, we do not need to instantiate expressions with quantifiers, as in the following example.
FVGNWO, FNW |- GVN
1. FVGNWO
2. FNW \ show GVN
3. FVN........2 VW subs
4. GNW.......1,3 O elim
5. GVN........4 VW subs
Go on to more about derivations with quantifiers.
Go back to the starting page.