Can we extend that idea to proving a universal sentence? One witness is certainly not enough. We'd need to work with lots of witnesses, in fact, every single member of our domain. That's not very practical, especially with infinitely large domains. We need to show that no matter what domain element you choose, the formula holds.
Consider the statements "If n is prime, then we know that ..." and "A person X who runs a business should always ...". Which n is being talked about, and which person? Well, any number or person, respectively. After learning about quantifiers, you may want to preface these sentences with "For all n" or "For all [any] persons X". But a linguist might point out that while yes "for all" is related to the speaker's thought, they are actually using a subtly different mode that of referring to a single person or number, albeit an anonymous, arbitrary one. If "an arbitrary element" really is a natural mode of thought, should our proof system reflect that?
If we choose an arbitrary member of the domain, and show that the sentence holds for it, that is sufficient. But, what do we mean by "arbitrary"? In short, it means that we have no control over what element is picked, or equivalently, that the proof must hold regardless of what element is picked. More precisely, a variable is arbitraryunless:
- A variable is not arbitrary if it is free in (an enclosing) premise.
- A variable is not arbitrary if it is free after applying ∃Elim either as the introduced witness c, or free anywhere else in the formula.
The usual way to introduce arbitrary variables is during ∀Elim (wjo later using it in ∃Elim). The formal inference rule for introduction of universal quantifcation will use these cases as restrictions.
- 1442 reads
