# Logic Text Chapter 10 Solutions

## Chapter 10: Trees for Predicate Logic

### Basic

Question {10.1}

1. A tautology. Here is my tree for it:

 ~((∃ x)Fx ≡ ~(∀ x)~ Fx) / \ (∃ x)Fx /a ~(∃ x)Fx \a ~~(∀ x)~ Fx ~(∀ x)~ Fx /a | | (∀ x)~ Fx \a ~~ Fa | | Fa ~ Fa | X ~ Fa X

2. A tautology.

 ~((∃ x) Fx ∨ (∃ x)~ Fx) | ~(∃ x)Fx \a ~(∃ x)~ Fx \a | ~ Fa | ~~ Fa X

3. Not a tautology.

 ~((∀ x)(Fx ∨ Gx) ⊃ ((∀ x)Fx ∨ (Ax)Gx)) | (∀ x)(Fx ∨ Gx) \ a, b ~((∀ x)Fx ∨ (∀ x)Gx) | ~(∀ x)Fx / a ~(∀ x)Gx / b | ~ Fa | ~ Gb | Fa ∨ Ga / \ Fa Ga X | Fb ∨ Gb / \ Fb Gb ^ X

This branch stays open. We have resolved every single-use formula, and the reusable formula (∀ x)(FxGx) has had every name substituted into it. So, we read off the open branch the following interpretation.

D = {a,b}

 I(F) I(G) a 0 1 b 1 0

And this indeed makes our original formula false. We have everything in the domain either F or G, yet it’s not the case that everything is F and it’s not the case that everything is G.

4. Is a tautology.

 ~((∃ x)(Fx ⊃ p) ⊃ ((∀ x)Fx ⊃ p)) | (∃ x)(Fx ⊃ p) \ a ~((∀ x)Fx ⊃ p) | (∀ x)Fx / a ~ p | Fa ⊃ p / \ ~ Fa p | X Fa X

You need to keep an eye on the brackets in the original formula. On the left of the conditional, the (∃ x) binds the whole (Fxp). On the right, the (∀ x) binds just the Fx, and (∀ x)Fx is the antecedent of the whole conditional (∀ x)Fxp.

The question in the text book contains an error. The question should have been to test the formula (∃ x)(Fxp) ≡ ((∀ x)Fxp). This is also a tautology. The tree is:

 ~((∃ x)(Fx ⊃ p) ≡ ((∀ x)Fx ⊃ p)) / \ / \ (∃ x)(Fx ⊃ p) \ a ~(∃ x)(Fx ⊃ p) \ a,b ~((∀ x)Fx ⊃ p) (∀ x)Fx ⊃ p | | (∀ x)Fx / a ~(Fa ⊃ p) ~ p | | Fa Fa ⊃ p ~ p / \ / \ ~ Fa p ~(∀ x)Fx / b p | X | X Fa ~ Fb X | ~(Fb ⊃ p) | Fb ~ p X

This one was quite difficult. You need to keep an eye on the brackets in the original formula. On the left of the biconditional, the (∃ x) binds the whole (Fxp). On the right, the (∀ x) binds just the Fx, and (∀ x)Fx is the antecedent of the whole conditional (∀ x)Fxp.

Then on the right branch we needed to substitute into the negated existential twice to get it to close.

We could have done it after processing (∀ x)Fxp, and this would have resulted in a tree with fewer substitutions. The right branch would have been:

 ~(∃ x)(Fx ⊃ p) \ a (∀ x)Fx ⊃ p / \ ~(∀ x)Fx / a p | | ~ Fa ~(Fa ⊃ p) | | ~(Fa ⊃ p) Fa | ~ p Fa X ~ p X

There’s something tricky going on here. The name `a’ gets introduced in the right branch with the ~(∀ x)Fx. Then we substitute the name into the negated existential at the top of the tree here. The result, ~(Fap), gets placed in both branches below it. In one, `a’ is already there, and in the other, `a’ is new. This is permissible, according to our rules.

5. Is a tautology.

 ~((∀ x)(Fx ⊃ Gx) ⊃ ((∀ x)Fx ⊃ (∀ x)Gx)) | (∀ x)(Fx ⊃ Gx) \ a ~((∀ x)Fx ⊃ (∀ x)Gx) | (∀ x)Fx \ a ~(∀ x)Gx / a | ~ Ga | Fa ⊃ Ga / \ ~ Fa Ga | X Fa X

6. Is a tautology.

 ~((∀ x)(Fx ∨ Gx) ⊃ ((∀ x) Fx ∨ (∃ x) Gx )) | (∀ x)(Fx ∨ Gx) \ a ~((∀ x)Fx ∨ (∃ x)Gx) | ~(∀ x)Fx / a ~(∃ x)Gx \ a | ~ Fa | ~ Ga | Fa ∨ Ga / \ Fa Ga X X

7. Is a tautology. The `p’ here is just a basic proposition.

 ~((∀ x)(Fx & p) ⊃ ((∀ x)Fx & p)) | (∀ x)(Fx & p) \ a ~((∀ x)Fx & p) / \ ~(∀ x)Fx / a ~ p | | ~ Fa Fa & p | | Fa & p Fa | p Fa X p X

8. Is a tautology.

 ~(∃ x)(Fx ⊃ (∀ y)Fy) \ a,b | ~(Fa ⊃ (∀ y)Fy) | Fa ~(∀ y)Fy / b | ~ Fb | ~(Fb ⊃ (∀ y)Fy) | Fb ~(∀ y)Fy X

9. Is a tautology.

 ~(∃ x)((∃ y)Fy ⊃ Fx) \ a,b | ~((∃ y)Fy ⊃ Fa) | (∃ y)Fy / b ~ Fa | Fb | ~((∃ y)Fy ⊃ Fb) | (∃ y)Fy ~ Fb X

10. Is a tautology.

 ~(∃ x)(∀ y)(Fy ⊃ Fx) \ a,b | ~(∀ y)(Fy ⊃ Fa) / b | ~(Fb ⊃ Fa) | Fb ~ Fa | ~(∀ y)(Fy ⊃ Fb) / c | ~(Fc ⊃ Fb) | Fc ~ Fb X

Question {10.2}

The arguments 1, 4 and 5 are valid. The rest are not.

1. Valid:

 (∀ x)((Fx & Gx) ⊃ Hx) \ a ~(∀ x)(Fx ⊃ (~ Gx ∨ Hx)) / a | ~(Fa ⊃ (~ Ga ∨ Ha)) | Fa ~(~ Ga ∨ Ha) | ~~ Ga ~ Ha | (Fa & Ga) ⊃ Ha / \ ~(Fa & Ga) Ha / \ X ~ Fa ~ Ga X X

2. Invalid.

 (∀ x)(∀ y)(Lxy ⊃ Mxy) \ a,b (∀ x)(∀ y)(Lxy ⊃ Lyx) \ a,b ~(∀ x)(∀ y)(Mxy ⊃ Myx) / a | ~(∀ y)(May ⊃ Mya) / b | ~(Mab ⊃ Mba) | Mab ~ Mba | (∀ y)(Lay ⊃ May) \ a,b | (∀ y)(Lby ⊃ Mby) \ a,b | (∀ y)(Lay ⊃ Lya) \ a,b | (∀ y)(Lby ⊃ Lyb) \ a,b | Laa ⊃ Maa | Lab ⊃ Mab | Lba ⊃ Mba | Lbb ⊃ Mbb | Laa ⊃ Laa | Lab ⊃ Lba | Lbb ⊃ Lbb | Lba ⊃ Lab | Lbb ⊃ Lbb | . .

We’ve substituted every name into each universal quantifier, and the only formulae left to process have the form Lcd ⊃ .., where c and d are each replaced by either a and b. Note that there is nothing in this branch which compels us to take any formula of the form Lcd as true. The only results we have are that Mab is true and Mba false. Each of the conditionals Lcd ⊃ … will be true if the antecedent is false. Therefore we can construct the following interpretation:

D = {a,b}

 I(L) a b a 0 0 b 0 0
 I(M) a b a 0 1 b 0 0

The values for Maa and Mbb are arbitrary. Any will do. This makes the premises true and the conclusion false, as you can see.

3. Invalid.

This tree is like the first infinite tree example we’ve seen. The premise (∀ x)(∃ y)Lxy on its own will generate the infinite branch. We will therefore use the names a1, a2, a3 … to keep track of the pattern.

 (∀ x)(∃ y)Lxy / a1,a2,a3,a4 ~(∃ x)(∀ y)Lxy / a1,a2,a3,a4 | (∃ y)La1y \ a2 | ~(∀ y)La1y \ a3 | La1a2 | ~ La1a3 | (∃ y)La2y \ a4 | ~(∀ y)La2y \ a5 | La2a4 | ~ La2a5 | (∃ y)La3y \ a6 | ~(∃ y)La3y \ a7 | La3a6 | ~ La3a7 | (∃ y)La4y \ a8 | ~(∀ y)La4y \ a9 | La4a8 | ~ La4a9 | . . .

You can see the pattern.

If we take each name to name one object only, we get the following domain D = {a1, a2, a3, a4, a5, a6, a7, a8 …}

And L works like this. L relates object number n to object (2 x n), and it doesn't relate object n to object (2 x n) + 1. So, a4 gets related to a8, and not to a9. a5 gets related to a10 and not to a11. And so on.

This will obviously make (∀ x)(∃ y)Lxy true (object n is related to object (2 x n). And (∃ x)(∀ y)Lxy is false. There is no object which is related to everything. Object n is not related to object (2 x n) + 1. Here’s the table, for those who like thinking in pictures:

 I(L) a1 a2 a3 a4 a5 a6 a7 a8 a9 … a1 1 0 … a2 1 0 … a3 1 0 … a4 1 0 … : : : : : : : : : :

Now: Let’s see what we know about these objects, to see whether we can make a smaller interpretation.

a2 can’t be the same as a3, and a4 can’t be the same as a5, and a6 can’t be the same as a7, because of the 1s and 0s in each row. However, that is all that we can’t do. a1 can be the same as anything, as there’s nothing in the a1 column, and the a1 row doesn’t clash with any row.

Now: a2 can be the same as a4, which can be the same as a6, etc… Similarly, a3 can be the same as a5, which can be the same as a7, etc… So, let the odd-numbered names all name one object, and the even-numbered names name another.

Compressing the table, you get:

 I(L) b c b 0 1 c 1 0

As b is named by a1, a3, a5, etc… b can’t be related to itself (as a1 isn’t related to a3), but b is related to c, as a1 is to a2. Similarly, c isn’t related to b (a2 isn’t related to a5) but c is related to itself (a2 is related to a4).

This makes the premise true: (∀ x)(∃ y)Lxy — Everything is related to something (everything is related to c). However, there isn’t something related to everything (nothing is related to b).

4. Is valid.

 (∀ x)(∀ y)(Lxy ⊃ Lyx) \ a (∀ x)(∀ y)(∀ z)((Lxy & Lyz) ⊃ Lxz) \ a ~(∀ x)((∃ y)Lxy ⊃ Lxx) / a | ~((∃ y)Lay ⊃ Laa) | (∃ y)Lay / b ~ Laa | (*) Lab | (∀ y)(Lay ⊃ Lya) \ b | Lab ⊃ Lba / \ ~ Lab Lba X | (∀ y)(∀ z)((Lay & Lyz) ⊃ Laz) \ b | (∀ z)((Lab & Lbz) ⊃ Laz) \ a | (Lab & Lba) ⊃ Laa / \ ~(Lab & Lba) Laa / \ X ~ Lab ~ Lba X X

The tree is very much longer if you don’t do the substitutions I did here (or ones very much like them). To do this, you need to think about how the reasoning goes. Down to the line I marked (*), it is completely automatic, using the edict “do particular rules before general ones”. Then you must make the first substitution into a universal quantifier. I picked the formula (∀ x)(∀ y)(LxyLyx) because I saw that I could substitute a for x and b for y to get LabLba. I knew I had Lab, and this would give me new and interesting information: Lba. Then our facts are Lab, Lba and ~ Laa. This then is inconsistent with the other premise: (∀ x)(∀ y)(∀ z)((Lxy & Lyz) ⊃ Lxz) when you substitute a, b and a for x, y, and z, respectively. So, they were the substitutions I made, and that closed the tree.

If you just did any substitutions you liked, in any order, the tree would still close (if you applied the rules correctly.) It would just have been much longer.

5. Is valid too.

 (∀ x)(∀ y)(Lxy ∨ Lyx) / a,b (∀ x)(∀ y)(∀ z)((Lxy & Lyz) ⊃ Lxz) ~(∀ x)(∀ y)(∃ z)(Lxz & Lyz) / a | ~(∀ y)(∃ z)(Laz & Lyz) / b | ~(∃ z)(Laz & Lbz) / a,b | ~(Laa & Lba) | ~(Lab & Lbb) | (∀ y)(Lay ∨ Lya) / a,b | Laa ∨ Laa | Lab ∨ Lba | (∀ y)(Lby ∨ Lyb) / b | Lbb ∨ Lbb / \ / \ / \ ~ Laa ~ Lba / \ / \ Laa Laa Lab Lba X X / \ X ~ Lab ~ Lbb X / \ Lbb Lbb X X

Notice that the premise (∀ x)(∀ y)(∀ z)((Lxy & Lyz) ⊃ Lxz) is completely irrelevant to the proof. We got the tree to close without it. I didn’t substitute a into (∀ y)(LbyLyb) in this proof as it would just have given us LbaLab, and we already had LabLba on an earlier line. Similarly, I didn’t branch the disjunctions until I knew I could use them to close one disjunct. That way the tree remained reasonably manageable.

Question {10.3}

Arguments 1, 6, 7, 8, 9 and 10 are valid, in the way that I formalised them in the solutions to {8.4}. The rest are not. I will present trees for the valid ones and just small interpretations for those which are not.

1. Lb, Rb, therefore Lb & Rb. That’s obviously valid.

 Lb Rb ~(Lb & Rb) / \ ~ Lb ~ Rb X X

2. (∃ x)Lx, (∃ x)Rx, therefore (∃ x)(Lx & Rx) . Invalid.

D = {a, b}

 I(L) I(R) a 1 0 b 0 1

3. (∀ x)(Sx ⊃ (∃ y)(Ly & Oxy)) therefore (∃ y)(Ly & (∀ x)(SxOxy))

Invalid.

D = {a, b, c, d}

 I(S) I(L) a 1 0 b 1 0 c 0 1 d 0 1
 I(O) a b c d a 0 0 1 0 b 0 0 0 1 c 0 0 0 0 d 0 0 0 0

a and b are solids, c and d are liquids, a dissolves in c, and b in d. So each solid dissolves in some liquid. However, there’s no liquid such that each solid dissolves in it.

4. (∀ x)(Ex ⊃ (SxAx)), Ea therefore Sa & Aa

Invalid.

D = {a}

 I(E) I(S) I(A) a 1 1 0

Ian is a secretary but not and administrator. He’s eligible for the clean desk prize.

5. (∀ x)Mx, therefore (~(∃ x)Mx ∨ ((∃ x)(Mx & Tx) & (∀ x)(TxMx))) & ~(~(∃ x)Mx & ((∃ x)(Mx & Tx) & (∀ x)(TxMx)))

D = {a}

Invalid.

 I(M) I(T) a 1 0

(∀ x)Mx is obviously true. However, the conclusion is false as ~(∃ x)Mx is false, and so is (∃ x)(Mx & Tx).

6. (∃ x)(Mx & (∀ y)((My & ~ Syy) ⊃ Sxy)) therefore (∃ x)(Mx & Sxx)

This is valid:

 (∃ x)(Mx & (∀ y)((My & ~ Syy) ⊃ Sxy)) / a ~(∃ x)(Mx & Sxx) / a | Ma & (∀ y)((My & ~ Syy) ⊃ Say) | Ma (∀ y)((My & ~ Syy) ⊃ Say) / a | (Ma & ~ Saa) ⊃ Saa | ~(Ma & Saa) / \ ~ Ma ~ Saa X / \ ~(Ma & ~ Saa) Saa / \ X ~ Ma ~~ Saa X X

7. (∀ x)(HxAx), therefore (∀ x)((∃ y)(Hy & Oxy) ⊃ (∃ y)(Ay & Oxy))

This is valid:

 (∀ x)(Hx ⊃ Ax) \ b ~(∀ x)((∃ y)(Hy & Oxy) ⊃ (∃ y)(Ay & Oxy)) / a | ~((∃ y)(Hy & Oay) ⊃ (∃ y)(Ay & Oay)) | (∃ y)(Hy & Oay) / b ~(∃ y)(Ay & Oay) \ b | Hb & Oab | Hb Oab | ~(Ab & Oab) / \ ~ Ab ~ Oab | X Hb ⊃ Ab / \ ~ Hb Ab X X

8. (∀ x)(∀ y)((Rxy & Py) ⊃ Nx), ~(∃ x)(Nx & Fx), (∀ x)(∀ y)((Rxy & (Ny & ~ Py)) ⊃ ~ Fx), therefore (∀ x)(∀ y)((Rxy & Ny) ⊃ ~ Fx)

This is valid:

 (∀ x)(∀ y)((Rxy & Py) ⊃ Nx) \ a ~(∃ x)(Nx & Fx) \ a (∀ x)(∀ y)((Rxy & (Ny & ~ Py)) ⊃ ~ Fx) \ a ~(∀ x)(∀ y)((Rxy & Ny) ⊃ ~ Fx) / a | ~(∀ y)((Ray & Ny) ⊃ ~ Fa) / b | ~((Rab & Nb) ⊃ ~ Fa) | Rab & Nb ~~ Fa | Rab Nb | (∀ y)((Ray & (Ny & ~ Py)) ⊃ ~ Fa) \ b | (Rab & (Nb & ~ Pb)) ⊃ ~ Fa) / \ ~( Rab & (Nb & ~ Pb)) ~ Fa / \ X ~ Rab ~(Nb & ~ Pb) X / \ ~ Nb ~~ Pb X | (∀ y)((Ray & Py) ⊃ Na) \ b | (Rab & Pb) ⊃ Na / \ ~(Rab & Pb) Na / \ | ~ Rab ~ Pb ~(Na & Fa) X X / \ ~ Na ~ Fa X X

9. ~(∃ x)(Px & Cx) ⊃ (∃ x)(Px & Dx), therefore (∃ x)(Px & (~ CxDx))

This is valid, surprisingly!

 ~(∃ x)(Px & Cx) ⊃ (∃ x)(Px & Dx) ~(∃ x)(Px & (~ Cx ⊃ Dx)) \a / \ / \ ~~(∃ x)(Px & Cx) (∃ x)(Px & Dx) / a | | (∃ x)(Px & Cx) / a Pa & Da | | Pa & Ca Pa | | Pa Da | | Ca ~(Pa & (~ Ca ⊃ Da)) | / \ ~(Pa & (~ Ca ⊃ Da)) ~ Pa ~(~ Ca ⊃ Da) / \ X | ~ Pa ~(~ Ca ⊃ Da) ~ Ca X | ~ Da ~ Ca X ~ Da X

Why is it valid? Well, if ~(∃ x)(Px & Cx) ⊃ (∃ x)(Px & Dx) is true, then either someone contributes to Oxfam or someone dies. If someone contributes to Oxfam then that person is someone who will die if she doesn’t. (Why is this true? Because of the material conditional! It is true if the antecedent is false.) On the other hand, if someone dies, then that person is someone who will die if she doesn’t contribute to Oxfam. (Why is this true? Because of the material conditional! It is true if the consequent is true.)

10. ~(∃ x)(Ax & ~ Kx), (∀ x)(GxIx), ~(∃ x)(Ix & Kx) therefore (∀ x)(Gx ⊃ ~ Ax).

{I have treated “no-one” as “nothing” here.}

This is valid.

 ~(∃ x)(Ax & ~ Kx) \a (∀ x)(Gx ⊃ Ix) \a ~(∃ x)(Ix & Kx) \a ~(∀ x)(Gx ⊃ ~ Ax) / a | ~(Ga ⊃ ~ Aa) | Ga ~~ Aa | Ga ⊃ Ia / \ ~ Ga Ia X | ~(Ia & Ka) / \ ~ Ia ~ Ka X | ~(Aa & ~ Ka) / \ ~ Aa ~~ Ka X X

Questions {10.4}

1.

a = PS

Sx = x is an axiomatic system.

Txy = x is a theorem of y.

Ox = x is a tautology.

Vx = x is a variable.

Cx = x is post-consistent.

Sa, (∀ x)(TxaOx), ~(∃ x)(Vx & Ox), (∀ x)((Sx & ~(∃ y)(Vy & Tyx)) ⊃ Cx), therefore Ca

This is valid.

 Sa (∀ x)(Txa ⊃ Ox) \b ~(∃ x)(Vx & Ox) \b (∀ x)((Sx & ~(∃ y)(Vy & Tyx)) ⊃ Cx) ~ Ca | (Sa & ~(∃ y)(Vy & Tya)) ⊃ Ca / \ ~(Sa & ~(∃ y)(Vy & Tya)) Ca / \ X ~ Sa ~~(∃ y)(Vy & Tya) X | (∃ y)(Vy & Tya) / b | Vb & Tba | Vb Tba | Tba ⊃ Ob / \ ~ Tba Ob X | ~(Vb & Ob) / \ ~ Vb ~ Ob X X

With this argument, (as with the others) it is helpful to keep in mind what each name stands for. The name ’a’ names PS. It’s a system. The name ’b’ names a propositional variable which is a theorem of PS. So that is the sensible thing to substitute into the second and third premises, not a.

2.

p = Every decision is to be referred to the central authority.

Px = x is a program.

Dx = x is delayed.

p ⊃ (∃ x)(Px & Dx), (∀ x)(PxAx), ~(∃ x)(Dx & Ax), therefore ~ p.

It is possible to expand p as follows:

Cx = x is a decision

Rx = x is to be referred to the central authority,

and p is then (∀ x)(CxRx).

But this plays no role in the argument.

It is valid either way. Here is the tree for when we use ’p’.

 p ⊃ (∃ x)(Px & Dx) (∀ x)(Px ⊃ Ax) \a ~(∃ x)(Dx & Ax) \a ~~ p / \ ~ p (∃ x)(Px & Dx) / a X | Pa & Da | Pa Da | Pa ⊃ Aa / \ ~ Pa Aa X | ~(Da & Aa) / \ ~ Da ~ Aa X X

3.

Tx = x is true.

Fx = x is false.

Kxy = x knows y.

Px = x is a person.

j = John.

(∀ x)(Tx ⊃ ~ Fx) & (∀ x)(~ FxTx), (∀ x)(Fx ⊃ ~(∃ y)(Py & Kyx)), (∃ x)(Kjx) & Pj Therefore (∃ x)Tx.

This is valid. Consider the following tree:

 (∀ x)(Tx ⊃ ~ Fx) (∀ x)(~ Fx ⊃ Tx) \a (∀ x)(Fx ⊃ ~(∃ y)(Py & Kyx)) \a (∃ x)Kjx & Pj ~(∃ x)Tx \a | (∃ x)Kjx / a Pj | Kja | ~ Ta | ~ Fa ⊃ Ta / \ ~~ Fa Ta | X Fa | Fa ⊃ ~(∃ y)(Py & Kya) / \ ~ Fa ~(∃ y)(Py & Kya) \j X | ~(Pj & Kja) / \ ~ Pj ~ Kja X X

The tree is quite short, when you know what substitutions to make, to make things close.

Question {10.5}

For each of these we need to find a counterexample to the arguments. One way to do this is to do a tree for each and read off the counterexample

Here are some suggestions:

(1) To show that reflexivity and symmetry does not produce transitivity:

Let the domain be {a,b,c}

and R is interpreted as:

 I(R) a b c a 1 1 0 b 1 1 1 c 0 1 1

In this interpretation the premises are true and the conclusion is false.

See if you can think of a way of determining whether a relation is reflexive, symmetry or transitive at a mere glance of its table.

(2) To show that reflexivity and transitivity does not produce symmetry:

Let the domain be {a,b}

and R is interpreted as:

 I(R) a b a 1 1 b 0 1

In this interpretation the premises are true and the conclusion is false.

(3) To show that symmetry and transitivity does not produce reflexivity:

Let the domain be {a}

and R is interpreted as:

 I(R) a a 0

In this interpretation the premises are true and the conclusion is false.

Question {10.6}

This is the tree for the argument (∀ x)(∀ y)(RxyRyx), (∀ x)(∀ y)(∀ z)((Rxy & Ryz) ⊃ Rxz), (∀ x)(∃ y)Rxy therefore (∀ x)Rxx.

 (∀ x)(∀ y)(Rxy ⊃ Ryx) \a (∀ x)(∀ y)(∀ z)((Rxy & Ryz) ⊃ Rxz) \a (∀ x)(∃ y)Rxy \a ~(∀ x)Rxx / a | ~ Raa | (∃ y)Ray / b | Rab | (∀ y)(Ray ⊃ Rya) \b | Rab ⊃ Rba / \ ~ Rab Rba X | (∀ y)(∀ z)((Ray & Ryz) ⊃ Raz) \b | (∀ z)((Rab & bz) ⊃ Raz) \a | (Rab & Rba) ⊃ Raa / \ ~(Rab & Rba) Raa / \ X ~ Rab ~ Rba X X