1
$\begingroup$

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: !!Coarse grain proof of  reflexivity

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: !!My Attempt at a fine grain proof

Any help in completing this proof would be appreciated.

I have migrated this question from Computer Science Stack Exchange.

$\endgroup$
3
  • $\begingroup$ 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. $\endgroup$
    – DanielV
    Oct 27 '17 at 16:00
  • 1
    $\begingroup$ 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. $\endgroup$
    – DanielV
    Oct 27 '17 at 16:06
  • 1
    $\begingroup$ @DanielV Totally concur .. yes, it's always a good idea to state the proof informally before trying to formalize it! $\endgroup$
    – Bram28
    Oct 27 '17 at 16:13
2
$\begingroup$

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:

enter image description here

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:

enter image description here

The rest is pretty much as you had it.

$\endgroup$
10
  • $\begingroup$ I think 4 shouldn't be a subproof. 5 is just a consequence of 3. $\endgroup$
    – DanielV
    Oct 27 '17 at 16:08
  • $\begingroup$ @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 $\endgroup$
    – Bram28
    Oct 27 '17 at 16:09
  • $\begingroup$ 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. $\endgroup$
    – DanielV
    Oct 27 '17 at 16:29
  • $\begingroup$ @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'! $\endgroup$
    – Bram28
    Oct 27 '17 at 16:31
  • $\begingroup$ 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. $\endgroup$
    – DanielV
    Oct 27 '17 at 16:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.