From CS2800 wiki
- If your goal is to prove "for all , P", you can proceed by choosing an arbitrary value and then proving that P holds for that .
The fact that arbitrary does not mean you get to pick ; on the contrary, your proof should work no matter what you choose. This means you can't use any property of other than that .is
- If you know for all , then you can conclude holds for any specific . For example, if you know for all , , then you can conclude (since ). holds
- To disprove that a predicate holds for all , you only need to choose a specific (called a counterexample) and show that is false. Put another way, the logical negation of "for all , " is "there exists an such that is false".For all and there exists are quantifiers: they describe how to interpret a variable in a predicate.