# I am stuck on how to prove the contradiction of R(b,a) can anybody help me?

Here are some well-known properties of dyadic (2-place) relations:

∀xR(x, x) (Reflexivity)

∀x¬R(x, x) (Irreflexivity)

∀x∀y(R(x, y) → R(y, x)) (Symmetry)

∀x∀y(R(x, y) → ¬R(y, x)) (Asymmetry)

∀x∀y∀z((R(x, y) ∧ R(y, z)) → R(x, z)) (Transitivity)

∀x∀y∀z((R(x, y) ∧ R(y, z)) → ¬R(x, z)) (Intransitivity)

Use Fitch proofs to demonstrate that asymmetry is a consequence of transitivity and irreflexivity together. Use Fitch proofs to demonstrate that asymmetry is a consequence of transitivity and irreflexivity together .

You are assuming symmetry and seem to be trying to derive a contradiction. Do not do that.

You are not trying to disprove symmetry: ¬∀x.∀y.(R(x,y)→R(y,x)).

Your target is to prove asymmetry: ∀x.∀y.(R(x,y)→¬R(y,x)). That is not the same thing at all.

Just assume Rab for any [a b], eliminate the universals so that transitivity and irreflexivity allow you to introduce a negation (specifically ¬Rba).

• │ _1) Ɐx.Ɐy.Ɐz.((Rxy ˄ Ryz) → Rxz)
• │ _2) Ɐx.¬Rxx
• ├────────
• ││ _3) [a b] Rab
• │├──────────
• ││ _4) ¬Raa : ⱯE, 2
• ││ _5) Ɐy.Ɐz.((Ray ˄ Ryz) → Raz) : ⱯE,1
• ││ _6) Ɐz.((Rab ˄ Rbz) → Raz) : ⱯE,5
• ││ _7) (Rab ˄ Rba) → Raa : ⱯE,6
• │││ _8) Rba
• ││├─────────
• │││ _9) Rab ˄ Rba : ˄I,3,8
• │││ 10) Raa : →, 7,9
• │││ 11) ┴ : ¬E,4,10
• ││ 12) ¬Rba : ¬I,8-11
• │ 13) Ɐx.Ɐy.(Rxy → ¬Ryx) : ⱯI,3-12
• +1 I checked this in a proof checker. – Frank Hubeny Jul 25 '18 at 20:16

I agree with Graham Kemp's answer. I am adding a proof using a Fitch-style natural deduction proof editor and checker. Two lines can be removed from the proof if I use a recommendation in the comments from Graham Kemp:

Just use the core rules of inference: assume Rba, to derive Rab ˄ Rba and thus Raa, which contradicts ¬Raa so therefore deducing ¬Rba.

Here is the alternate proof: Graham Kemp offered another suggestion which shortened the length of the proof and perhaps made it more understandable to a reader:

That checker explicitly lists ~E and ~I rules in the Basic Rules column. You can surely use them.

I rearranged the universal eliminations to get this new version: The premises are in the first two lines.

In lines 3 to 6 I use universal elimination (∀E) to replace the quantified variables, x, y and z, with the names, a and b. See Chapter 32, "Basic Rules for FOL" in forall x: Calgary Remix for a discussion. In particular I select names that will make the goal easy to reach: x becomes a, y becomes b, and z becomes also a.

Since the goal is a conditional I will need to start a subproof with an assumption that is the antecedent of the conditional I want to derive. If I can derive the desired consequent then I can close the subproof discharging the assumption and introduce the desired conditional. This is done in line 7 to 13.

To complete the proof I use universal introduction (∀I) in lines 14 and 15 to reach the final goal completing the proof.

References

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/

• Eh. Don't mess with Modus Tollens and deMorgan's. Just use the core rules of inference: assume Rba, to derive Rab ˄ Rba and thus Raa, which contradicts ¬Raa so therefore deducing ¬Rba. – Graham Kemp Jul 26 '18 at 0:26
• @GrahamKemp I'll see if I can get a simpler proof with your suggestion. – Frank Hubeny Jul 26 '18 at 0:31
• @GrahamKemp Your suggestion worked. – Frank Hubeny Jul 26 '18 at 2:26
• A proof by negation is all you need. Assume Rba , derive the contradition, then use negation introduction to deduce ¬Rba . – Graham Kemp Jul 26 '18 at 3:03
• @GrahamKemp Since I am using a specific proof checker I have to follow those built in rules of that software. I can't start with Rba and deduce ~Rba. I have to start with the negation of what I want which would be ~~Rba. Regardless, it is still an indirect proof. – Frank Hubeny Jul 26 '18 at 3:36