10.1 Introduction

As 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 logical rules of inference we have already seen, there are a few new rules of inference (described in the next section) - rules of inference for universally quantified sentences, rules of inference for existentially quantified sentences, and a new type of rule called Domain Closure.

Note that the Fitch system described here works only for premises and conclusions that are closed sentences. This is not a significant limitation, since every open sentence is logically equivalent to a closed sentence in which the free variables have been universally quantified.

10.2 Rules for Quantifiers

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 τ.)

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 Fitch proofs, we differentiate placeholders from ordinary constants by choosing constants that (1) begin with a letter and (2) do not appear in the given premises. For example, if the only object constants in our premises are a and b, we might choose c as 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.

Suppose, for example, we have derived the conclusion hates(c,jane) ⇒ hates(jane,c) and suppose that the placeholder 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 τ.)

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.

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 σ₁, ... , σ_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.

10.3 Examples

As 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, there exists a z such that 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 and for all y and for all z, loves(y,z) implies 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.

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 jill for y. The sentence on line 4 is the result of applying Universal Elimination to the sentence on line 2, substituting jack for x. The sentence on line 5 is the result of applying Universal Elimination to the sentence on line 4, substituting jill for y. Finally, we apply Implication Elimination to produce our conclusion on line 6.

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 and for all y, x loves 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 placeholder. 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 use of placeholders. 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.

10.4 More Examples

In this section, we use our proof system to prove some general results about the interaction between quantifiers and logical sentences.

Given ∀x.∀y.(p(x,y) ⇒ q(x)), we know that ∀x.(∃y.p(x,y) ⇒ q(x)). In general, given a universally quantified implication, it is okay to drop a universal quantifier of a variable outside the implication and apply an existential quantifier of that variable to the antecedent of the implication, provided that the variable does not occur in the consequent of the implication.

Our proof is shown below. As usual, we start with our premise. We use Universal Elimination ti instantiate that sentence using a new placeholder. We then start a subproof with an existential sentence as assumption. We then make another assumption by instantiating the target of the existential sentence and a new placeholder. We use Universal Elimination to strip away the quantifier from our conclusion in line 2. We use Implication Introduction to produce an implication and Universal Introduction to produce a universally quantified version of the implication. We then use Existential Elimination to infer q(c). Finally, we generalize using Universal Introduction.

The relationship holds the other way around as well. Given ∀x.(∃y.p(x,y) ⇒ q(x)), we know that ∀x.∀y.(p(x,y) ⇒ q(x)). We can convert an existential quantifier in the antecedent of an implication into a universal quantifier outside the implication.

Our proof is shown below. Once again, we start with our premise. We create a new placeholder and use Universal Elimination to strip away the quantifier in the premise to expose the implication. We start a subproof by making an assumption. We make an assumption using another new placeholder. We turn the assumption into an existential sentence to match the antecedent of the premise in line 2. Then, we apply Implication Elimination to derive q(c). We use Implication Introduction to create an implication. Finally, we generalize using two applications of Universal Introduction.

Recap

A Fitch system for Relational Logic can be obtained by extending the Fitch system for Propositional Logic with five additional rules to deal with quantifiers. The Universal Elimination rule allows us to reason from a universally quantified sentence to a version of the target of that sentence in which the universally quantified variable is replaced by an appropriate term. The Universal Introduction rule allows us to reason from arbitrary sentences to universally quantified versions of those sentences. The Existential Introduction rule allows us to reason from a sentence involving a term τ to an existentially quantified sentence in which one, some, or all occurrences of τ have been replaced by the existentially quantified variable. The Existential Elimination rule allows us to derive consequences of an existentially quantified sentence. Finally, the Domain Closure rule allows us to reason from all instances of a sentence to a universally quantified version of that sentence.

Exercises

Exercise 10.1: Given ∀x.(p(x) ∧ q(x)), use the Fitch System to prove ∀x.p(x) ∧ ∀x.q(x).

Exercise 10.2: Given ∀x.(p(x) ⇒ q(x)), use the Fitch System to prove ∀x.p(x) ⇒ ∀x.q(x).

Exercise 10.3: Given the premises ∀x.(p(x) ⇒ q(x)) and ∀x.(q(x) ⇒ r(x)), use the Fitch system to prove the conclusion ∀x.(p(x) ⇒ r(x)).

Exercise 10.4: Given ∀x.∀y.p(x,y), use the Fitch System to prove ∀y.∀x.p(x,y).

Exercise 10.5: Given ∀x.∀y.p(x,y), use the Fitch System to prove ∀x.∀y.p(y,x).

Exercise 10.6: Given ∃y.∀x.p(x,y), use the Fitch system to prove ∀x.∃y.p(x,y).

Exercise 10.7: Given ∃x.¬p(x), use the Fitch System to prove ¬∀x.p(x).

Exercise 10.8: Given ∀x.¬p(x), use the Fitch System to prove ¬∃x.p(x).

Exercise 10.9: Given ¬∃x.p(x), use the Fitch System to prove ∀x.¬p(x).

Exercise 10.10: Given ¬∀x.p(x), use the Fitch System to prove ∃x.¬p(x).