One of the most natural ways to record derivations formally is called, well, Natural Deduction. Each inference rule is written as a line with assumptions written above and one conclusion below the line. Also, there are scoping rules: some assumptions are available up to some point, after which the are closed. E.g., in proving A -> B, we assume A and may use it to derive B. Then A is closed and we obtain A -> B. After that, A can no longer be used.

Existential elimination rule (using an assumption of the form $\displaystyle \exists x\,P(x))$ has the following form.

$\displaystyle \frac{\exists x\,P(x)\qquad\begin{aligned}[b]

&P(x)\\

&\;\;\vdots\\

&\;R

\end{aligned}}{R}$

Here the assumption $\displaystyle P(x)$ is closed by the last line. It corresponds to regular mathematical practice: if we know $\displaystyle \exists x\,P(x)$, but don't know what exactly $\displaystyle x$ is, we could prove that $\displaystyle P(x)$ implies $\displaystyle R$ *for any* $\displaystyle x$. Then we would know $\displaystyle R$.

In text form, it is convenient to write derivations showing scoping explicitly. The existential elimination rule is written as follows.

Code:

$\displaystyle \exists x\,P(x)$
$\displaystyle P(x)$
$\displaystyle \;\;\vdots$
$\displaystyle R$
$\displaystyle R$

This means that, having $\displaystyle \exists x\,P(x)$, we temporarily introduce an assumption $\displaystyle P(x)$, deduce $\displaystyle R$ from it, and then close $\displaystyle P(x)$. The result is a derivation of $\displaystyle R$ from $\displaystyle \exists x\,P(x)$.

Using this, the proof about < can be written as follows.

Code:

$\displaystyle \exists x\,a+x=b$ (1) assumption
$\displaystyle a+x=b$ (2) introducing a temporary assumption from (1)
$\displaystyle \exists y\,b+y=c$ (3) assumption
$\displaystyle b+y=c$ (4) introducing a temporary assumption from (3)
$\displaystyle a+x=b\land b+y=c$ (5) from (2), (4)
$\displaystyle \exists y\,a+x=b\land b+y=c$ (6) from (5)
$\displaystyle \exists x\,\exists y\,a+x=b\land b+y=c$ (7) from (6)
$\displaystyle \exists x\,\exists y\,a+x=b\land b+y=c$ (8) close (4)
$\displaystyle \exists x\,\exists y\,a+x=b\land b+y=c$ (9) close (2)