# 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: The rest is pretty much as you had it.

• I think 4 shouldn't be a subproof. 5 is just a consequence of 3. Oct 27 '17 at 16:08
• @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
• @DanielV Yeah, it's insane how many different formal systems there are ... which is exactly why your suggestion to always first produce an informal proof (or: proof as one would typically give as a mathematician, rather than formal logician) is very good! Doing formal proofs and getting stuck might make one think that one is not good at proofs, but often it's just due to the technical particulars of the system you have to work with. Here, the OP clearly had the right idea, but just needs some assistance to get it into the Fitch 'straightjacket'! Oct 27 '17 at 16:31
• Thanks, I appreciate that you agree with that sentiment, it is one of my mantras. I wish more instructors treated logics as just languages for conveying reasoning, rather than merely complicated rule games. Oct 27 '17 at 16:35