There are two kinds of definition for formal proof in the logic books I read.
One is: Let be an ℒ-formula and be an ℒ-theory. A formal proof of in is a finite sequence of ℒ-formulas (0, ... , ) with equal to such that, for every ≤ , either ∈ , or is a logical axiom, or it can be deduced by (MP) from some and with , < , or it can be obtained by generalization from a formula with <
The other is like this: A formal proof is a sequence of $\sum_1\vdash A_1$,...,$\sum_n\vdash A_n$ where $\sum_i\vdash A_i$ is a rule itself or generated by previous ones using some rule(you can find the rules in this post).
I did not see a proof like the second definition in other math books except some logic books. Why does the second kind of definition exist? Is there a systematic way (algorithm) to convert one kind of formal proof to the other?(I can convert simple proofs manually, but it seems hard to do so for complex proofs.)