Universal Elimination

How to apply ∀E

1. Select ∀E from the Elim Rules menu in the ToolBox.
   Show me
2. Select the universally quantified formula you want to instantiate in the Fitch.
   Show me
3. Click the Apply Rule button in the ToolBox.
   Show me
4. A dialogue box will appear prompting you to enter the instantiating term. If necessary, click in the text area to give it focus, then enter the desired instantiating term using the keyboard.
   Show me
5. Click "OK" once the instantiating term has been entered.
   Show me

• Watch a demonstration of ∀E being applied

Troubleshooting

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.
• I can't select the universal I want to eliminate in the Fitch.
• When I clicked the Apply Rule button, I got an error message that said the formula I had selected was not universally quantified.
• When I clicked the Apply Rule button, I got another error message or nothing happened.
• I'm trying to apply ∀E backwards.
• I'm trying to apply ∀E to more or fewer than two lines.
• I can apply the rule successfully, but the wrong formula is derived.

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 universal I want to eliminate 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, no dialogue box appears.

Universal elimination can only be applied to a universally quantified formula. If you try to apply the rule when anything other than a universally quantified formula has been selected, no dialogue box will appear, and you may also see an error message. Check carefully to make certain that the formula you are selecting really has a universal quantifier as its main operator (and isn't, for example, a conjunction with a universally quantified formula as its left-hand conjunct). Any universally quantified formula will appear in the Fitch in the form (∀x)φ.

If the formula is definitely a universal but the dialogue box fails to appear 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 "OK" after entering a term, I got an error message or nothing happens.

You may have entered an expression that was not an acceptable term. Try re-applying the rule, being careful to enter only a single lower case letter in the input dialogue.

If you have definitely entered only a single lower case letter, and are still unable to apply the rule successfully, try exiting the CPL and reloading the problem. If the problem persists 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 than one line.

∀E is applied to a single line, the line on which the universal to be instantiated appears.

Back to troubleshooting topics

I can apply the rule successfully, but the wrong formula is derived.

The only formulae that can be derived using universal elimination are substitution instances of the selected universal. If the formula you are attempting to derive is not a substitution instance of the universal you select, you will have to derive it another way.

Back to troubleshooting topics