Biconditional Elimination

↔ EL
↔ ER

How to apply ↔EL

  1. Select ↔EL from the Elim Rules menu in the ToolBox.
    Show me
  2. Select the line on which the left-hand equivalent appears in the Fitch.
    Show me
  3. Click the Apply Rule button in the ToolBox.
    Show me

How to apply ↔ER

  1. Select ↔ER from the Elim Rules menu in the ToolBox.
    Show me
  2. Select the line on which the right-hand equivalent appears in the Fitch.
    Show me
  3. Click the Apply Rule button in the ToolBox.
    Show me

Troubleshooting

If you're having trouble applying either ↔EL or ↔ER, click on the statement below that best describes the problem you're having.

I can't select ↔EL/↔ER 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 biconditional I want to eliminate/the equivalent 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 were not of the correct form.

You may have selected the biconditional and an equivalent in the wrong order. The biconditional ( φ ↔ ψ ) to be eliminated must be the first line selected for the application of ↔EL/↔ER, while the appropriate equivalent (φ for ↔EL and ψ for ↔ER) must be selected second. Try re-applying the rule, being careful to select the lines in this order.

Also be sure that you select the appropriate equivalent for the rule variant. Remember to select the left equivalent in order to apply ↔EL and the right equivalent in order to apply ↔ER.

If you have selected a biconditional and the correct equivalent for the rule variant, 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 a biconditional and the appropriate equivalent 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 ↔EL/↔ER backwards.

Elimination rules can't be applied backwards in the CPL.

Back to troubleshooting topics

I'm trying to apply ↔EL/↔ER to more or fewer than two lines.

Biconditional elimination is applied to two lines. The formula on the first of those lines must be a biconditional, and the formula on the second must be on of the equivalents of that biconditional.

Back to troubleshooting topics

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

The only formula that can be derived by biconditional elimination is one of the equivalents of the biconditional in question (which one depends on the variant of the rule selected). If you are trying to derive a different formula, you'll need to do it another way.

Back to troubleshooting topics