If you're having trouble applying ∃E, click on the statement below that best describes the problem you're having.
I can't select ∃E from the Elim Rules menu.
If a rule is not appearing in the ToolBox menus, then that rule is not available for the currently loaded problem. Rules are available only for derivation problems that follow the presentation of the rule in the text, regardless of what problems you may have completed previously.
Back to troubleshooting topics
I can't select the existential I want to eliminate or the final line of the subderivation in the Fitch.
First, make sure that there isn't a problem with your mouse by clicking to change applications or browser windows. If your mouse is working properly, try clicking on different parts of the formula. If you are still unable to select the formula no matter where you click on it, try exiting the CPL and reloading the problem. If the problem persists after reloading, please inform your instructor.
Back to troubleshooting topics
When I clicked the Apply Rule button, I got an error message that said the formulae I had selected violated the restrictions.
See the section on understanding the restrictions to make certain that you haven't accidentally violated one of them in trying to apply the rule.
If no restrictions have been violated, try exiting the CPL and reloading the problem. If the problem persists after reloading, please inform your instructor.
Back to troubleshooting topics
When I clicked the Apply Rule button, I got an error message that said the formulae I had selected were not of the correct form.
If you have selected an existentially quantified formula and the final line of a subderivation opened by the assumption of a substitution instance of that existential (where the formula on that line does not violate any of the restrictions), in that order, but you still get the same error message when applying the rule, try exiting the CPL and then reloading the problem. If the problem persists after reloading, please inform your instructor.
Back to troubleshooting topics
When I clicked the Apply Rule button, I got another error message or nothing happens.
Make sure that you have selected the correct rule in the ToolBox, and that you have selected an existentially quantified formula and the final line of a subderivation opened by the assumption of a substitution instance of that existential (where the formula on that line does not violate any of the restrictions) in the Fitch. If your selections are correct, the formula that will be derived when the rule is applied will auto-fill in the instantiation pane of the ToolBox.
If the formula is auto-filled, but you continue to experience problems when attempting to apply the rule, try exiting the CPL and reloading the problem. If the problems persist after reloading, please inform your instructor.
Back to troubleshooting topics
I'm trying to apply ∃E backwards.
Elimination rules can't be applied backwards in the CPL.
Back to troubleshooting topics
I'm trying to apply ∃E to more or fewer than two lines.
∃E is applied to two lines. The first of these is that on which the existential to be eliminated appears. The second is the final line of a subderivation opened with the assumption of a susbstitution instance of the existential. The formula on this line must not violate any of the restrictions in order for the rule application to be successful.
Back to troubleshooting topics
I can apply the rule successfully, but the wrong formula is derived.
Check the justification for the new line in the Fitch to make sure you applied the rule in the way you expected. The formula derived will be the same as that on the last line of the subderivation.
Show me where to look for the justification
Back to troubleshooting topics