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
Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.Sign up to join this community
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.
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
|_ | |_ (a=b)˄(b=c) | | a=b ˄ elim | | b=c ˄ elim | | a=c = elim | ((a=b)˄(b=c))→(a=c)