Let $\mathcal{L}$ be a recursive first-order theory, with a deductive system $\Xi$ (for instance, Hilbert-Ackerman proof system). Let $\phi$ be a formula and let $l=(\psi_1, \ldots, \psi_n=\phi)$ be a sequence of formulas.

Question 1: Suppose we what want to discuss the (asymptotical) computational complexity cost of checking wether $l$ constitutes a proof for the pair $(\mathcal{L}, \Xi)$. What are the relevant numerical parameters, depending on $L$, involved in such a complexity function, and to which complexity class it belongs (

**P**,**NP**, etc)?Question 2: How much the complexity of verifying $l$ is a proof changes if we change the deductive system (Gentzen's style, for instance), or consider a suitable higer-order theory, or etc?

I apologize in advance about question 2, I hope it makes sense (albeit it is a somewhat non-rigorous question).

The motivation of these questions are the very famous work of Gödel, *On the lenght of proofs*, and naturally, **P=NP?** problem.