# Prove reflexivity using Fitch software

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.

• I think you are going to have a hard time proving the theorem, since the empty relation satisfies all of your conditions and not your conclusion. Your attempt shows a condition 3, but your post doesn't say anything like that. Oct 27 '17 at 16:00
• I think what you are saying in your post is a little different than what you are trying to prove. Start by coming up with any proof at all of your claim. We can show you how to translate a proof into fitch like format, but trying to prove a theorem in fitch when you can't prove it in anything is pointless. Oct 27 '17 at 16:06
• @DanielV Totally concur .. yes, it's always a good idea to state the proof informally before trying to formalize it! Oct 27 '17 at 16:13

First of all, to prove a universal you need to unievrsal proof structure, i.e. set up a $\forall$ Intro by starting a subproof with $a$ as an arbitrary object. Here is the basic set-up you therefore need:
Then inside this subproof you can get the all important existential, and do another subproof of the kind you already have to eliminate this existential, but make sure to introduce a $b$ as the witness for that existential:
• @DanielV Yes, in most systems that's how it works ... but in Fitch this is what it looks like .. you have a whole line basically saying 'Let $a$ be some arbitrary object ...' Without the subproof $a$ would not be considered an arbitrary object, but a specific object, and hence Fitch would complain at the $\forall$ Intro on line 10 Oct 27 '17 at 16:09
• That sounds exactly backwards from the version I'm used to. The rule of going from 9 to 10 would only have a restriction that $a$ doesn't exist in any assumptions. But I can see how this way would work too, I guess it is up to the software which way $\forall-I$ is done. Oct 27 '17 at 16:29