Biconditional Introduction

How to apply ↔I Forwards

1. Select ↔I from the Intro Rules menu in the ToolBox.
   Show me
2. Select the last line of the subderivation opened by the assumption of the desired left-hand equivalent in the Fitch. The formula on this line should be the right-hand equivalent of the biconditional you want to derive.
   Show me
3. Select the last line of the subderivation opened by the assumption of the desired right-hand equivalent in the Fitch. The formula on this line should be the left-hand equivalent of the biconditional you want to derive.
   Show me
4. Click the Apply Rule button in the ToolBox.
   Show me

• Watch a demonstration of ↔I being applied forwards

How to apply ↔I Backwards

1. Select ↔I from the Intro Rules menu in the ToolBox.
   Show me
2. Select the biconditional you want to derive in the Goal Tree.
   Show me
3. Click the Apply Rule button in the ToolBox.
   Show me

• Watch a demonstration of ↔I being applied backwards

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 last formulae in the two subderivations in the Fitch.
• I can't select the biconditional I want to derive in the Goal Tree.
• When I clicked the Apply Rule button when attempting to apply ↔I backwards, I got an error message saying that the goal formula was not a biconditional.
• When I clicked the Apply Rule button, I got another error message or nothing happened.
• I'm trying to apply ↔I forwards to more or fewer than two lines.
• I can apply the rule successfully, but the wrong biconditional 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 last formulae in the two subderivations 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

I can't select the biconditional 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 when attempting to apply ↔I backwards, I got an error message saying that the goal formula was not a biconditional.

Biconditional introduction can only be used to derive biconditionals. Check carefully to make certain that the formula you are selecting in the Goal Tree really is a biconditional. Any biconditional will appear in the Goal Tree in the form ( φ ↔ ψ ).

If the formula is definitely a biconditional 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 either the final lines of the two subderivations in the Fitch or a biconditional in the Goal Tree. If your selections are correct, the instantiation pane of the ToolBox will be auto-filled with the left equivalent, right equivalent, and the biconditional, respectively.

If the rule instantiation 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 ↔I forwards to more or fewer than two lines.

Biconditional elimination is applied to two lines. These two lines must be the final lines of two subderivations, each subderivation being opened with the assumption of one equivalent from the biconditional to be derived, and ended with the other equivalent.

Back to troubleshooting topics

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

You probably just selected the lines in the wrong order. Check the justification for the new line in the Fitch to verify whether this is the case.

Show me where to look for the justification

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

Back to troubleshooting topics