I am trying to learn how to use the Fitch software from Barwise and Etchemendy to develop proofs. I am trying to prove that $R$ is reflexive from the following premises.
If $R$ is symmetric, transitive, and if $R$ relates $x$ to some element in the domain, then it relates $x$ to itself. Which I have formalised (perhaps incorrectly) as:
In the proof above, I have used First Order consequence (FO Con) which does not help me understand the proof itself. I would like to represent the proof in Fitch without using FO Con. Here is my best effort:
Any help in completing this proof would be appreciated.
I have migrated this question from Computer Science Stack Exchange.