2

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.

enter image description here

1

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
0

I agree with Graham Kemp's answer. I am adding a proof using a Fitch-style natural deduction proof editor and checker.

enter image description here

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:

enter image description here

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:

enter image description here

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.