How to prove transitivity in Fitch. Is it Ok?

| 1. a = b
| 2. b = c
| 3. c = c  =Intro
| 4. a = c  =Elim: 3, 2
| 5. b = c  =Elim: 4, 1
  • I made an edit adding some formatting. You may roll this back or continue editing. You can see the versions by clicking on the "edited" link. Welcome to this SE! – Frank Hubeny Sep 15 '18 at 14:05
  • Line 3 is unneeded, and line 4 is where you should stop (and its by =Elim: 1,2). – Graham Kemp Sep 20 '18 at 5:21

I was not able to get the proof as you presented it to work in the fitch-style proof checker I am using.

However, the following did work using equality elimination (=E).

enter image description here

The proof checker you are using may be different and the result could require other steps.


Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

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/ Wikipedia, "Fitch notation" https://en.wikipedia.org/wiki/Fitch_notation

| improve this answer | |

The = introduction rule is that: an entity will equal itself.

|  c=c    = intro

This is a distraction. You do not need it for your proof.

The = elimination rule is that: you may substitute an entity for an entity that it equals.

|  a=b
|_ F(b)
|  F(a)   = elim

Now this is just what you need. Transitivity (of equality) is that: if a=b and b=c then a=c . Which is clearly substituting a for b in b=c.

|  a=b
|_ b=c
|  a=c    = elim

In full

|  |_ (a=b)˄(b=c)
|  |  a=b             ˄ elim
|  |  b=c             ˄ elim
|  |  a=c             = elim
|  ((a=b)˄(b=c))→(a=c)
| improve this answer | |

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.