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