# 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! Sep 15, 2018 at 14:05
• Line 3 is unneeded, and line 4 is where you should stop (and its by =Elim: 1,2). Sep 20, 2018 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)
``````