-1

I am wondering why fitch is not allowing me to use existential elimination for this final step

I am wondering why fitch is not allowing me to use existential elimination for this final step

7
  • Because Existential elimination needs a new constant. May 13 '20 at 6:05
  • The solution is simple: you have to swap the initial Existential-elim with the Universal-elim. May 13 '20 at 13:21
  • @Mauro ALLEGRANZA, the name used to instantiate Existential-elim should not appear in any undischarged assumptions but line 3 is not. Why do you think a new constant is necessary in this case ? Perhaps, this proof system has a slight different requirement.
    – F. Zer
    May 13 '20 at 18:04
  • @F.Zer - please, re-read the ND quantifier rules: "In case of (forall I) and (exists E) a parameter a is required to be “fresh” in the sense of having no other occurrences in Gamma , Delta, phi, psi." May 14 '20 at 6:09
  • 1
    Thanks, @Mauro Allegranza. I am now seeing p.357 of the book Language, Proof and Logic (this software is based on it), and for the rule of Existential Elimination the requirement is, as you say, "Where c does not occur outside the subproof where it is introduced." This book doesn't mention the word undischarged (as the link you posted).
    – F. Zer
    May 14 '20 at 14:00
1

Taking into account Mauro suggestion in the comments, you will need a fresh constant (does not appear previously in the proof), for using Existential Elimination. So, I think this would be correct.

enter image description here

2
  • 1
    Yes, that is valid. Local term c is properly isolated to its context. May 15 '20 at 4:49
  • Thanks for taking a look at my answer, @Graham Kemp !
    – F. Zer
    May 15 '20 at 11:48

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