Essential structure of proofs as a measure of complexity (Q2183713)

The article is well organized and written. Mainly, it shows that introducing the notions of \textit{schema calculus, schema derivation} and \textit{description complexity of a schema formula}, they were able to recognize that two distinct derivations of two distinct theorems can be the same in the sense that both are instances of the same schema derivation, so, intuitively both must have the same description complexity in an appropriate schema calculus. Besides, using these concepts they prove general robustness results relating to description complexity of a schema formula across Hilbert and Gentzen calculus. In page 212, inside the definition of \textit{schema calculus}, subpart \textit{proviso oracle map}, it will be appropriate to explicitly mention that \(\Lambda \subseteq A\).