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

3 Answers 3


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


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)

Here is the proof for transitivity of identity.

enter image description here

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .