Tiny examples
Looking at a couple of very small examples shows how to structure equation-solving and proof in the Prooftoys logic. Everything is set up to work entirely with statements that are mathematically known to be true. Let’s see how to work this way.
Solving an equation
Mathematically speaking, a full solution of an equation is an equivalence between the “problem statement” and the solution, often under some assumptions — typically that we are interested in solutions of certain types; often real numbers, as we see here.
Any statement is equivalent to itself — a basic property of logic — and that is often an excellent way to start, with the equation as the chosen statement. We do that here. In the rule menu this is always available (when no term is selected) as “consider a term to transform”.
A couple of extemely useful facts about numbers are x = y == x + z = y + z and x = y == x - z = y - z. In basic algebra it is very common to
“cancel out” a term like the 2 in x - 2 to remove it from one side
of the equation.
About the steps
And so on.
Playing around
Feel free to play around with the proof editor, below. Pressing the “Solve” button enters the entire proof into the proof builder. That may take a moment, so be patient.
A minimal proof
About the proof steps
asdf asfd