As 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 faster than relationship is transitive.
Our goal is to show that Harry is faster than Ralph. In other words, starting with the
preceding sentences, we want to derive the sentence f(harry,ralph).
The derivation of this conclusion goes as shown below. The first six lines correspond to the premises just formalized.
∀x.∀y.(h(x) ∧ d(y) ⇒ f(x,y))
∃y.(g(y) ∧ ∀z.(r(z) ⇒ f(y,z)))
∀y.(g(y) ⇒ d(y))
∀x.∀y.∀z.(f(x,y) ∧ f(y,z) ⇒ f(x,z))
On line 7, we use existential elimination to derive an instance of the second premise, here using the Skolem term [c] to refer to the greyhound that is faster than every rabbit. Lines 8 and 9 come from And Elimination applied to line 7. Line 10 is the result of applying Universal Elimination to the sentence on line 9. On line 11, we use Implication Elimination to infer that [c] is faster than Ralph.
g([c]) ∧ ∀z.(r(z) ⇒ f([c],z))
∀z.(r(z) ⇒ f([c],z))
r(ralph) ⇒ f([c],ralph)
IE: 10, 6
Next, we instantiate the sentence about greyhounds and dogs and infer that [c] is a dog. Then, we instantiate the sentence about horses and dogs; we use And Introduction to form a conjunction matching the antecedent of this instantiated sentence; and we infer that Harry is faster than [c].
g([c]) ⇒ d([c])
IE: 12, 8
∀y.(h(harry) ∧ d(y) ⇒ f(harry,y))
h(harry) ∧ d([c]) ⇒ f(harry,[c])
h(harry) ∧ d([c])
AI: 5, 13
IE: 15, 16
We then instantiate the transitivity sentence, again form the necessary conjunction, and infer the desired conclusion.
∀y.∀z.(f(harry,y) ∧ f(y,z) ⇒ f(harry,z))
∀z.(f(harry,[c]) ∧ f([c],z) ⇒ f(harry,z))
f(harry,[c]) ∧ f([c],ralph) ⇒ f(harry,ralph)
f(harry,[c]) ∧ f([c],ralph)
AI: 17, 11
IE: 20, 21
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.