We show now how to solve equations as structured derivations, and check their correctness with an automatic checker.
The video below shows how to solve a first-degree equation and check that the solution is correct. We use the step-by-step presentation feature that is available in view mode in eMath Studio. This is a very handy tool: you show the solution to a problem one step at a time, simulating how the solution is shown on the white board while explaining the solution at the same time.
Here is the solution that we constructed in the video.
Comparison with standard method of solving an equation
Note that we use equivalence between equations when solving the equation. Equivalence guarantees that we will find all the solutions, and no false solutions.
The traditional way of solving an equation lists the equations one below the other, aligned on the equality sign. The above solution would be written, e.g., as follows:
The idea is that each equation follows logically from the previous equations.
The structured derivation shows a different way of solving an equation, by a logical calculation. An equation is a logical statement, so it can be true for some values of x and false for other values. The successive equations in the structured calculation are equivalent, i.e. two successive equations are either both true or both false for each value of x. We show this by writing the equivalence symbol between the equations. By transitivity, this means that the original equation will be equivalent to the final equation, which is the solution. Hence, the solution is satisfied by exactly the same values for x that satisfy the original equation. In other words, equivalence guarantees that we get all solutions to the equation, and no false solutions.
Equation solving is thus a special kind of logical calculations. Logical calculations are similar to algebraic and arithmetic calculations, the only difference being that we calculate with logical expressions, rather than arithmetic or algebraic expressions. The equivalence relation has the same important role in logical calculations as the equality relation has in the algebraic and arithmetic calculations. In fact, equivalence is just equality of (the truth values of) logical expressions.
The need for assumptions
Our next example shows that equation solving is not just manipulating the equations, often we can only solve an equation under certain assumptions. We show the need for assumptions in the following example video, and also show where to place the assumptions in a structured derivation.
The checker is very strict about undefined expressions. It treats each function as a total function, including division as here. This means that an expression like x/0 is assumed to have a value. However, the checker does not know what this value is (nobody does), so it can only prove trivial properties about undefined expressions, like that x/0 = x/0. Most algebraic rules require that the expressions are well-defined, and can only be applied then. The fact that an expression could be undefined for some variable values shows up as unproved steps when the checker checks the correctness of the calculation. The remedy is to restrict the values that the variable x can have with assumptions so that the equation does have a solution, as we show in the example above.
Here is the solution to the equation solved in the video.
Equation Solving as a logical calculation
As we said, solving an equation is just calculating with logical expressions. The next example illustrates the power of treating equation solving as a logical calculation. It allows us to use more complex logical expressions in the calculation, and to simplify logical expression using standard rules of logic.
As in the previous solution, the square root would be undefined for negative arguments (in real arithmetic). This is handled by adding a suitable assumption that guarantees that the equation has a solution. Moreover, we use logical conjunction here to describe an intermediate step in the derivation, and apply a logical rule for simplifying the expression (the rule is that true propositions can always be eliminated in a conjunction).
Here is the final solution to the square root example.
