# Prove transitivity in Fitch

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). The proof checker you are using may be different and the result could require other steps.

References

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

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)
``````