-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

Improve this question
7
  • Because Existential elimination needs a new constant.
    – Mauro ALLEGRANZA
    May 13, 2020 at 6:05
  • The solution is simple: you have to swap the initial Existential-elim with the Universal-elim.
    – Mauro ALLEGRANZA
    May 13, 2020 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, 2020 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."
    – Mauro ALLEGRANZA
    May 14, 2020 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, 2020 at 14:00

1 Answer 1

Reset to default
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

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

Not the answer you're looking for? Browse other questions tagged .