## 8.1 IntroductionAs with Propositional Logic, we can demonstrate logical entailment in Relational Logic by writing proofs. As with Propositional Logic, it is possible to show that a set of Relational Logic premises logically entails a Relational Logic conclusion if and only if there is a finite proof of the conclusion from the premises. Moreover, it is possible to find such proofs in a finite time. The Fitch system for Relational Logic is an extension of the Fitch system for Propositional Logic. In addition to the ten logical rules of inference, there are five new rules of inference. In the next section, we introduce two rules of inference for universally quantified sentences. We then introduce two rules of inference for existentially quantified sentences. After that, we describe a new type of rule called If you are like me, the prospect of going through a discussion of so many rules of inference sounds a little repetitive and boring. However, it is not so bad. Each of the rules has its own quirks and idiosyncrasies, its own personality. In fact, a couple of the rules suffer from a distinct excess of personality. If we are to use the rules correctly, we need to understand these idiosyncrasies. ## 8.2 Rules for Universal Quantifiers
For example, consider the sentence ∀ In addition, we can use Universal Elimination to create conclusions with free variables. For example, from ∀ In using Universal Elimination, we have to be careful to avoid conflicts with other variables and quantifiers in the quantified sentence. This is the reason for the constraint on the replacement term. As an example of what can go wrong without this constraint, consider the sentence ∀ We can avoid this problem by obeying the restriction on the Universal Elimination rule. We say that a term τ is
Typically, UI is used on sentences with free variables to make their quantification explicit. For example, if we have the sentence Note that we can also apply the rule to sentences that do not contain the variable that is quantified in the conclusion. For example, from the sentence There is one important restriction on the use of Universal Introduction. If the variable being quantified appears in the sentence being quantified, it must not appear free in any If we want to quantify a sentence in this situation, we must first use Implication Introduction to discharge the assumption and then we can apply Universal Introduction. For example, in the case just described, we can first apply Implication Introduction to derive the result ( ## 8.3 Rules for Existential Quantifiers
The main problem in eliminating an existential quantifier is choosing an expression to replace the existential variable. Should we replace it with a variable? How about an object constant? Unfortunately, neither of these solutions works. We cannot use a variable since the resulting instance would be equivalent to a universally quantified sentence (given our convention that our free variables are universally quantified). For example, given the sentence ∃ And we cannot replace the quantified variable with an object constant. Although we know the sentence is true of some object, we do not know which it is. For example, given a language with just two object constants The solution to this problem is to replace the variable in an existentially quantified sentence with a new type of expression, called a Using the idea of Skolem terms, we can formulate a rule of inference for eliminating existential quantifiers. There are two cases to consider - the case where the quantified sentence is closed and the case where the quantified sentence contains one or more free variables.
For example, if we have the sentence ∃ Unfortunately, things get a little more difficult when the existentially quantified sentence contains free variables. Suppose, for example, we had the sentence ∃ Fortunately, we can solve this problem through the use of more complex Skolem terms that include not just a new constant but also include free variables in the Skolem term.
For example, if we have the sentence ∃ In what follows, we combine these two cases into a single rule, called By comparison to Existential Elimination,
For example, from the sentence Note that, in Existential Introduction, it is important to avoid variables that appear in the sentence being quantified. Without this restriction, starting from ∃ Note also that the rule applies only in cases where the term being replaced does not contain any universally quantified variables. This restriction is necessary to avoid incorrect conclusions. Suppose, for example, we had the sentence ∀ ## 8.4 Domain ClosureFinally, for languages with finite Herbrand bases, we have the
For example, in a language with four object constants Note that in applying Domain Closure, we do Why restrict DC 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 ## 8.5 ExampleAs an illustration of these concepts, consider the following problem. Suppose we believe that everybody loves somebody. And suppose we believe that everyone loves a lover. Our job is to prove that Jack loves Jill. First, we need to formalize our premises. Everybody loves somebody. For all y.∃z.loves(y,z)
Everybody loves a lover. If a person is a lover, then everyone loves him. If a person loves another person, then everyone loves him. For all x.∀y.(∃z.loves(y,z) ⇒ loves(x,y))
Our goal is to show that Jack loves Jill. In other words, starting with the preceding sentences, we want to derive the following sentence. loves(jack,jill)
A proof of this result is shown below. Our premises appear on lines 1 and 2. The sentence on line 3 is the result of applying Universal Elimination to the sentence on line 1, substituting
Now, let's consider a slightly more interesting version of this problem. We start with the same premises. However, our goal now is to prove the somewhat stronger result that everyone loves everyone. For all x.∀y.loves(x,y)
The proof shown below is analogous to the proof above. The only difference is that we have free variables in place of object constants at various points in the proof. Once again, our premises appear on lines 1 and 2. Once again, we use Universal Elimination to produce the result on line 3; but this time the result contains a free variable. We get the results on lines 4 and 5 by successive application of Universal Elimination to the sentence on line 2. We deduce the result on line 6 using Implication Elimination. Finally, we use two applications of Universal Introduction to generalize our result and produce the desired conclusion.
This second example illustrates the power of free variables. We can manipulate them as though we are talking about specific individuals (though each one could be any object); and, when we are done, we can universalize them to derive universally quantified conclusions. ## 8.6 ExampleAs another illustration of Relational Logic proofs, consider the following problem. We know that horses are faster than dogs and that there is a greyhound that is faster than every rabbit. We know that Harry is a horse and that Ralph is a rabbit. Our job is to derive the fact that Harry is faster than Ralph. First, we need to formalize our premises. The relevant sentences follow. Note that we have added two facts about the world not stated explicitly in the problem: that greyhounds are dogs and that our
Our goal is to show that Harry is faster than Ralph. In other words, starting with the preceding sentences, we want to derive the following sentence. f(harry,ralph)
The derivation of this conclusion goes as shown below. The first six lines correspond to the premises just formalized. On line 7, we use existential elimination to derive an instance of the second premise, here using the Skolem term [
This derivation is somewhat lengthy, but it is completely mechanical. Each conclusion follows from previous conclusions by a mechanical application of a rule of inference. On the other hand, in producing this derivation, we rejected numerous alternative inferences. Making these choices intelligently is one of the key problems in the process of inference. ## 8.7 ExampleIn this section, we use our proof system to prove some basic results involving quantifiers. Given ∀ Our proof is shown below. As usual, we start with our premise. We start a subproof with an existential sentence as assumption. We use Existential Elimination to eliminate the existential quantifier. We then use two applications of Universal Elimination to strip away the quantifiers from the premise. And we use Implication Elimination to derive
The relationship holds the other way around as well. Given ∀ Our proof is shown below. As usual, we start with our premise.
We start a subproof by making an assumption. Then we turn the assumption into an existential sentence to match the antecedent of the premise. We use Universal Implication to strip away the quantifier in the premise to expose the implication. Then, we apply Implication Elimination to derive
## RecapA Fitch system for Relational Logic can be obtained by extending the Fitch system for Propositional Logic with four additional rules to deal with quantifiers. The ## ExercisesExercise 8.1: Given ∀ Exercise 8.2: Given ∀ Exercise 8.3: Given the premises ∀ Exercise 8.4: Given ∀ Exercise 8.5: Given ∀ Exercise 8.6: Given ∃ Exercise 8.7: Given ∃ Exercise 8.8: Given ∀ |