Universal Introduction

How to apply ∀I Forwards

1. Select ∀I from the Intro Rules menu in the ToolBox.
   Show me
2. Select a substitution instance of the universal formula you want to derive in the Fitch. Recall that this substitution instance must not violate the restrictions on the rule.
   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 from the substitution instance. If necessary, click in the text area to give it focus, then enter the appropriate instantiating term using the keyboard.
   Show me
5. Click "OK" once the instantiating term has been entered.
   Show me
6. A dialogue box will appear prompting you to enter the desired variable of quantification. If necessary, click in the text area to give it focus, then enter the appropriate variable using the keyboard. Recall that this variable must not violate the restrictions on the rule.
   Show me
7. Click "OK" once the variable has been entered.
   Show me

• Watch a demonstration of ∀I applied forwards

How to apply ∀I Backwards

1. Select ∀I from the Intro Rules menu in the ToolBox.
   Show me
2. Select the universal formula you want to derive in the Goal Tree.
   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 from the substitution instance. If necessary, click in the text area to give it focus, then enter the appropriate instantiating term using the keyboard. Recall that this instantiating term must not violate the restrictions on the rule.
   Show me
5. Click "OK" once the instantiating term has been entered.
   Show me

• Watch a demonstration of ∀I applied backwards

Understanding the Restrictions

Troubleshooting

If you're having trouble applying ∀I, click on the statement below that best describes the problem you're having.

• I can't select ∀I from the Intro Rules menu.
• I can't select the formula I want to quantify over in the Fitch.
• I can't select the universal I want to derive in the Goal Tree.
• When I clicked the Apply Rule button, no dialogue box appears.
• When I clicked "OK" after entering the terms, I got an error message or nothing happens.
• I'm trying to apply ∀I forwards to more or than one line.
• I can apply the rule successfully, but the wrong universal is derived.

I can't select ∀I from the Intro 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 formula I want to quantify over 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 formulae no matter where you click on them, try exiting the CPL and reloading the problem. If the problem persists after reloading, please inform your instructor.

Back to troubleshooting topics

I can't select the universal I want to derive in the Goal Tree.

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.

Make sure you have selected a formula in the Fitch or a universal in the Goal Tree before attempting to apply the rule.

If a formula has been selected in the Fitch, or a universal has been selected in the Goal Tree, 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 the terms, 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 for each term in the input dialogue. Additionally, the first term must be a variable, so only the letters u, v, w, x, y, and z are acceptable.

Your attempt to apply the rule may have violated one of the restrictions. Please see the section on understanding the restrictions to ensure that this is not the case.

If you have definitely entered acceptable terms, and no restrictions are being violated, but 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 ∀I forwards to more or than one line.

∀I is applied to a single line, the line on which the substitution instance of the universal to be derived appears.

Back to troubleshooting topics

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

You probably just selected the wrong line, or entered one of the terms incorrectly. Check the justification for the new line in the Fitch and compare the new formula to the substitution instance carefully to verify whether this is the case.

Show me where to look for the justification

If the universal you wish to derive is present in the Goal Tree, you can always apply ∀I backwards to this formula in order to eliminate the possibility of making incorrect selections in the Fitch.

Back to troubleshooting topics