Logical Symbols and Equations

We show some examples to illustrate how logical symbols are useful when solving equations.

Logical symbols are nice for expressing more or less than one root.

Solve the following equations.

x² − 3x = 0. equation x = 0 \/ x = 3 ends ok_text Correct! f_nodes 7 x^2 -3x = 0 <=>

x − 1 = 1 + x. equation x FF ends ok_text Correct! f_nodes 1 x-1 = 1+x <=>

Reasoning operators are nice for expressing stepwise solutions. A stepwise solution to x² − 3x = 0 is shown below. Try it first as it is, and then make errors to it, to see what happens. equation x = 0 \/ x = 3 ends ok_text Correct! f_nodes 7 x^2 -3x = 0 <=>
(x-3)x = 0 <=> x-3 = 0 \/ x = 0 <=> x = 3 \/ x = 0

Solve

4x + 7

x2 + 2

= 1. You may write a step, then try it, then add <=> and the next step and so on, until the roots are shown explicitly. If you introduce a fake root, it may be that the tool does not detect it immediately (please remember that the tool is only a prototype!), but it will detect it at the end at the latest. equation x = -1 \/ x = 5 ends ok_text Correct! f_nodes 8 (4x+7)/(x^2+2) = 1 <=>

The operator ⇒ is nice for expressing that there may be fake roots that will be eventually filtered out. We use 2√x + 3 = x as an example. From now on we show the first ⇔ in the answer box, so that you can change it to ⇒ if wou wish. equation x = 9 ends ok_text Correct! f_nodes 3 2 sqrt(x) + 3 = x
<=> 2 sqrt(x) = x - 3 /**//* Squaring both sides introduces fake root 1 */ ==> 4x = x^2 - 6x + 9 <=> x = 1 \/ x = 9 /**//* Assignmment reveals that 9 is and 1 is not a root */ original <=> x = 9

Please notice how /* and */ were used to add comments to the output, and /**/ to introduce line breaks.

Alternatively, one can add a constrait that rules out the fake roots. equation x = 9 ends ok_text Correct! f_nodes 3 2 sqrt(x) + 3 = x
<=> 2 sqrt(x) = x - 3 /**//* `2 sqrt(x)` is non-negative, so also `x-3` must be */ <=> x-3 >= 0 /\ 4x = x^2 - 6x + 9 /**/ <=> x >= 3 /\ (x = 1 \/ x = 9) /**/ <=> x = 9

Solve

x2 − x − 20

x − 5

= 11. equation x = 7 ends ok_text Correct! f_nodes 3 (x^2-x-20)/(x-5) = 11
<=>

Logical symbols can also express splitting to cases. To illustrate it, we solve 3|x − 3| = x + 1. equation x=2 \/ x=5 ends ok_text Correct! f_nodes 7 3|x−3| = x+1
/**/<=> x < 3 /\ 3(3-x) = x+1 \/ x >= 3 /\ 3(x-3) = x+1 /**/<=> x < 3 /\ 9-3x = x+1 \/ x >= 3 /\ 3x-9 = x+1 /**/<=> x < 3 /\ x = 2 \/ x >= 3 /\ x = 5 /**/<=> x = 2 \/ x = 5

Solve 2|x| = x + 2. equation x = -2/3 \/ x = 2 ends ok_text Correct! f_nodes 10 2|x| = x+2
/**/<=>

This kind of splitting to cases is, however, not good for difficult problems, because it forces both cases solved in parallel, or at least one case being carried along while the other is solved. Perhaps sometime in the future the tool makes it possible to solve them separately.