Universal Elimination (UE) allows us to reason from the general to the particular. It states that, whenever we believe a universally quantified sentence, we can infer an instance of the target of that sentence in which the universally quantified variable is replaced by a ground term. (In the following rule, the notation φν⇐τ means an instance of φ in which all occurrences of ν have been replaced by τ.)
where τ is ground
For example, consider the sentence ∀y.hates(jane,y). From this premise, we can infer that Jane hates Jill, i.e. hates(jane,jill). We can even infer than Jane hates herself, i.e. hates(jane,jane).
Universal Introduction (UI) is the opposite of Universal Elimination - it allows us to reason from sentences about individuals to universally quantified versions of those sentences.
Unfortunately, it is not as easy as Universal Elimination. Just because we can prove that a sentence is true of one specific object does not mean that it is true of all objects. Of course, we could try proving a sentence about every known object. (See the Domain Closure rule described later in this section.) However, that could require a lot of work if the universe contains many objects.
Fortunately, there is a technique that allows us to derive universally quantified sentences without enumerating all individual objects. The trick is the use of a new type of constant, called a placeholder. A placeholder is effectively a stand-in for an actual object constant; we just do not know which constant it is. In writing placeholders, we use square brackets to differentiate placeholders from ordinary object constants. For example, [c] is a placeholder.
The basic idea is to introduce a new placeholder in our proof. Once we have this new placeholder, we can use it like any other placeholder to derive conclusions. Since we have not made any assumptions about this object, whatever we derive must be true of all objects. So we can derive any such conclusion by a universally quantified sentence in which we have replaced the placeholder with a variable, provided that the placeholder does not occur in any active assumptions.
where [τ] is not used in any active assumptions
Suppose, for example, we have derived the conclusion hates([c],jane) ⇒ hates(jane,[c]) and suppose that [c] does not occur in any active assumptions. Then we can use Universal Introduction to conclude the universally quantified sentence ∀x.(hates(x,jane) ⇒ hates(jane,x)).
Existential Introduction (EI) is easy. If we believe a sentence involving a ground term τ, then we can infer an existentially quantified sentence in which occurrences of τ have been replaced by the existentially quantified variable. (In the following rule, the notation φν←τ means an instance of φ in which zero or more occurrences of ν have been replaced by τ.)
where τ is ground
For example, from the sentence hates(jill,jill), we can infer that there is someone who hates himself, i.e. ∃x.hates(x,x). We can also infer that there is someone Jill hates, i.e. ∃y.hates(jill,y), and there is someone who hates Jill, i.e. ∃x.hates(x,jill). And, by two applications of Existential Introduction, we can infer that someone hates someone, i.e. ∃x.∃y.hates(x,y).
Note that Existential Introduction applies only in cases where the term being replaced is ground. This restriction is necessary to avoid incorrect conclusions. Suppose, for example, we had the sentence ∀x.hates(x,x). If we were to use EI to replace the second occurrence of x, we would get the conclusion ∃y.∀x.hates(x,y), i.e. there is someone whom everyone hates. The original sentence says that everyone hates himself whereas this incorrect conclusion states that there is a single person whom everyone hates.
Existential Elimination (EE) works in the opposite direction.Suppose we have an existentially quantified sentence with target φ; and suppose we have a universally quantified implication in which the antecedent is the same as the scope of our existentially quantified sentence and the conclusion does not contain any occurrences of the quantified variable. Then, we can use Existential Elimination to infer the consequent.
∀ν.(φ ⇒ ψ)
where ν does not occur free in ψ
For example, if we have the sentence ∀x.(hates(jane,x) ⇒ mean(jane)) and we have the sentence ∃x.hates(jane,x), then we can conclude mean(jane)).
It is interesting to note that Existential Elimination is analogous to Or Elimination. This is as it should, as an existential sentence is effectively a disjunction. Recall that, in Or Elimination, we start with a disjunction with n disjuncts and n implications, one for each of the disjuncts and produce as conclusion the consequent shared by all of the implications. An existential sentence (like the first premise in any instance of Existential Elimination) is effectively a disjunction over the set of all ground terms; and a universal implication (like the second premise in any instance of Existential Elimination) is effectively a set of implications, one for each ground term in the language. The conclusion of Existential Elimination is the common consequent of these implications, just as in Or Elimination.
Domain Closure (DC) offers an alternative way to derive universally quantified sentences. For a language with object constants σ1, ... , σn, the rule is written as shown below. If we believe a schema is true for every instance, then we can infer a universally quantified version of that schema.
For example, in a language with four object constants a and b and c and d, we can derive the conclusion ∀x.φ[x] whenever we have φ[a] and φ[b] and φ[c] and φ[d].
Note that in applying Domain Closure, we do not need to worry about placeholders. Placeholders are just surrogates for constants in our language. If we have managed to prove that a condition holds for all of our object constants, then it must be true of everything, including whatever objects our placeholders represent.
Why restrict Domain Closure to languages with finitely many ground terms? Why not use domain closure rules for languages with infinitely many ground terms as well? It would be good if we could, but this would require rules of infinite length, and we do not allow infinitely large sentences in our language. We can get the effect of such sentences through the use of induction, which is discussed in a later chapter.
Use the arrow keys to navigate. Press the escape key to toggle all / one.