Is it possible to rewrite the solution of an equation as a sequence of logical inferences in a logic system (e.g. FOL, SOL, etc.)?

Question

If I solve an equation, for instance, if I assume the premise 5 * x = 10, I can logically conclude that x = 10 / 5 = 2. This is a trivial example, but even for more complex equations, a correct solution would still be a sequence of steps, each being a logical conclusion from the previous steps. This makes me wonder: is it possible to formalize the solution of an equation as a sequence of logical inferences by applying inference rules in a logic system, e.g. first-order logic (FOL), second-order logic (SOL), etc.?

Answer 1

Sure it is possible. If you couldn't do that, those formal system would basically be failing at the very purpose they were create to meet, namely expressing arguments of ordinary mathematical arguments.

Actually doing it is not terribly enlightening in most cases -- the only cases (outside coursework) where you'd want to do it would be if you're trying to construct a machine-checkable proof, and in that case you will generally have plenty of software support for doing the most low-level nitty-gritty manipulations for you. And probably you would be working in a logical formalism that is explicitly designed to make the process less painful than it would be in the theoretically "neat" systems that introductory logic textbooks present.

A major part of learning formal logic consists of getting familiar enough with the systems that it is clear to you that you could do this encoding of an ordinary mathematical argument if you ever wanted to. (And then never actually doing it).

Answer 2

To illustrate how it would be possible to formalize an argument, let me trace through a proof script using the Coq proof assistant.

Require Import Reals.

Open Scope R_scope.

Goal forall x:R, 5 * x = 10 -> x = 2.
Proof.
intros x H. apply f_equal with (f := fun a => 1/5 * a) in H.
rewrite <- Rmult_assoc in H. unfold Rdiv in H.
rewrite (Rmult_assoc 1 (/ 5) 5) in H. rewrite Rinv_l in H.
+ repeat rewrite Rmult_1_l in H. rewrite H. field.
+ intro H0. assert (0 < 5).
  - apply Rplus_lt_0_compat.
    * exact Rlt_0_1.
    * apply Rmult_lt_0_compat.
      { exact Rlt_0_2. }
      { exact Rlt_0_2. }
  - rewrite H0 in H1. contradict H1. apply Rlt_irrefl.
Qed.

The first couple lines import Coq's real analysis library and sets up the parser so that equations are assumed to use operations on R by default.

Require Import Reals.

Open Scope R_scope.

Then, we open a proof goal:

Goal forall x:R, 5 * x = 10 -> x = 2.
Proof.

The proof context display of CoqIde or Proof General will show the initial proof context as:

1 subgoal
______________________________________(1/1)
forall x : R, 5 * x = 10 -> x = 2

The first step is to move the variable x and the hypothesis into the assumptions section.

intros x H.

The proof context is now:

1 subgoal
x : R
H : 5 * x = 10
______________________________________(1/1)
x = 2

This corresponds to uses of the logical rules of $\forall$-introduction and $\rightarrow$-introduction (for example from natural deduction).

The next step is to multiply both sides of H by $\frac{1}{5}$. We do this by applying a pre-defined result that if $x=y$, then $f(x) = f(y)$:

apply f_equal with (f := fun a => 1/5 * a) in H.

This turns the proof context into:

1 subgoal
x : R
H : 1 / 5 * (5 * x) = 1 / 5 * 10
______________________________________(1/1)
x = 2

We now apply some rewriting operations on H to simplify the left hand side:

rewrite <- Rmult_assoc in H. unfold Rdiv in H.
rewrite (Rmult_assoc 1 (/ 5) 5) in H.

Which brings us to:

1 subgoal
x : R
H : 1 * (/ 5 * 5) * x = 1 * / 5 * 10
______________________________________(1/1)
x = 2

(Here, / 5 represents application of the multiplicative inverse operation to 5.) Now, we apply another rewrite to simplify / 5 * 5 to 1:

rewrite Rinv_l in H.

New proof context:

2 subgoals
x : R
H : 1 * 1 * x = 1 * / 5 * 10
______________________________________(1/2)
x = 2
______________________________________(2/2)
5 <> 0

Here Rinv_l had an extra precondition that to conclude / x * x = 1 you are required to show that x <> 0. Therefore, Coq split the proof into two parts: one for proceeding after the rewrite, and the other for showing that the precondition 5 <> 0 is satisfied.

The first part is now straightforward, rewriting to eliminate the 1 * parts, substituting H in the goal to reduce to proving / 5 * 10 = 2, then using a builtin tactic to prove this equality.

+ repeat rewrite Rmult_1_l in H. rewrite H. field.

The other part is a bit trickier. To prove $5 \ne 0$ we start off by applying a reductio absurdum: we want to show $5 = 0$ results in a contradiction, by way of an intermediate goal to show that $0 < 5$.

+ intro H0. assert (0 < 5).

The assert tactic splits the proof into two parts, one in which you want to prove the assertion, and the other in which the assertion is inserted as a hypothesis and you continue on to prove what you originally wanted.

2 subgoals
x : R
H : 1 * (/ 5 * 5) * x = 1 * / 5 * 10
H0 : 5 = 0
______________________________________(1/2)
0 < 5
______________________________________(2/2)
False

Now, the tricky part here is that 5 is actually pretty-printing for the expression $1 + ((1 + 1) \cdot (1 + 1))$. (If you want to see this, you can disable notation displays from the CoqIde "View" menu, or presumably also from Proof General - though I'm not as familiar with Proof General.) Now, for example, to prove that $0 < 5$, we apply a preproved result that if $0 < x$ and $0 < y$ then $0 < x = y$:

- apply Rplus_lt_0_compat.

Proof context:

2 subgoals
x : R
H : 1 * (/ 5 * 5) * x = 1 * / 5 * 10
H0 : 5 = 0
______________________________________(1/2)
0 < 1
______________________________________(2/2)
0 < 4

The rest of the proof of the assertion proceeds similarly, eventually reducing to known results.

Then, for the other part, to get a contradiction from 5 = 0 and 0 < 5 proceeds by substituting the first into the second, and then applying a known result that $x \not < x$.

---

So, as you can see, the formal proof needs to go into every small detail, way past the level of detail that a human would require to be convinced. (That said, there are also tactics built in to Coq that would be able to automate more portions of the proof, similar to the way I already used the field tactic to automate the portion of the proof showing that $\frac{1}{5} \cdot 10 = 2$. I just wanted to expand one part of the proof to illustrate what proof such a tactic might generate behind the scenes.)

In general, the structure of a formal proof in Coq is built "from the top down", though with some exceptions when manipulating hypotheses or with some tactics such as assert which allow a more "bottom up" style. It is not at all unusual to mix the two directions as appropriate, as this proof script did.

To tie some of these tactics to formal logic rules: the apply tactic typically corresponds to a use of modus ponens, sometimes along with an application of $\forall$-specialization. Similarly, the assert tactic corresponds to a use of the cut rule: building a proof of $\Gamma \vdash P$, using an intermediate result $Q$, by splitting it into a proof of $\Gamma \vdash Q$ and a proof of $\Gamma, Q \vdash P$. The rewrite tactic is a bit more involved, but at its heart it uses $=$-elimination (or the substitution rule, if you prefer).

Answer 3

If you are given only set theory, the rules of logical inference and Peano's Axioms, you would have to (1) formally construct (i.e. prove the existence of) the addition and multiplication functions on $N$, (2) define subtraction in terms of addition and division in terms of multiplication, (3) establish the required algebraic properties of these functions/relations (i.e. associativity, commutativity and cancelability), (4) define the numbers 1 through 10 in terms of zero, and (5) prove that $2\times 5 =10$. I would estimate maybe 2000 lines of non-trivial formal proof would be required thus far (based on my experience with my own formal proof checker). Then solving your equation would be a fairly trivial exercise, maybe an additional 100 lines of formal proof.