Is there a formal notation for implication in a chain of equations?

Question

In arithmetic, I'm sure we've all used the informal notation where we write a list of numbers above each other with an operator, find the answer, then use that number and chain another operation, etc. For example:

$$\begin{array} {rr} & 123 \\ & 157 \\ + & 34 \\ \hline & 314 \\ \times & 2 \\ \hline & 628 \end{array}$$

Currently I'm in a logic-oriented calculus series, and the professor says anything that isn't pedantically correct, no matter how minor, is wrong, and points will be deducted. I know I can use $\Rightarrow$ and re-write the 314 in this example, but then the beneficial terseness of the equation chaining is lost. Is there a pedantically accurate way of chaining equations like this, especially for "sidebars"/scratch-work and substitutions?

Answer 1

It's a universal convention that whenever we write "$a = b = c$" we mean "$a = b \land b = c$". Note that this applies for binary relations in general such as "$x \in S \subseteq T$" or "$p \le q < r$" or "$C_n \cong H \unlhd G$".

So it is perfectly valid (no sane professor should reject) to write:

$(123+157+34) \times 2 = 314 \times 2 = 628$.

Note that for equality or inequality chains we essentially never explicitly write down the easily deducible conclusion about the relation between the first and last in the chain, which in this case is:

$(123+157+34) \times 2 = 628$.

Either way, note that presentation of the computation as an equality chain can be easily made totally rigorous in a formal system, even though most programming languages do not have such constructs (because they are designed to capture not reasoning but processes).

Finally, note that it is actually logically incorrect to use the "$\Rightarrow$" symbol in-between statements each of which follows from the previous one. "$A \Rightarrow B$" has a very precise meaning.

Answer 2

A chain of identities of equations such as $E1=E2=E3=E4$ translates to the following sequence of implications in logic:

1. $E1=E2$

2. $E2=E3$

3. $E1=E3$ from 1 and 2 (as a formal inference, this is typically called $= Elim$)

4. $E3=E4$

5. $E1=E4$ ( $= Elim$ on 3 and 4)

So, for your example, we would get:

1. $123+157+34=314$

2. $2*314 = 628$

3. $\therefore 2*(123+157+34)=628$ ($= Elim 1,2$)

Is that the kind of thing you are looking for?