This question is a continuation of a related previous question (check here).

Let $\mathcal{L}$ be a recursive first-order theory with the Hilbert-Ackerman's proof calculus, and such that the computational cost of deciding whether or not a formula $\theta$ is an axiom is in **P**.

Let $\phi$ be a formula, and let $\ell=(\psi_1, \ldots, \psi_n = \phi)$ be a *proof of number of lines* $n$; that is, each $\psi_i$ is either an axiom or is obtained by a single application of a inference rule involving only formulas that appear previously in $\ell$ (i.e., $\psi_j, j<i$).

**Question:**what is the asymptotical computational complexity of deciding whether or not $\phi$ has a proof of number of lines $n$? If we change $\mathcal{L}$ to a suitable (recursive) higher order theory and the proof calculus (e.g., Gentzen's proof calculus), how this complexity function can change?

**EDIT** as discussed in the comments, the question above is undecidable in general.

Let *lenght of* $\ell$ be the total number of symbols appearing on it, which I will denot by $|\ell|$

**Question modified:**what is the asymptotical computational complexity of deciding whether or not $\phi$ has a proof $\ell$ with a fixed lenght $|\ell|=n$? If we change $\mathcal{L}$ to a suitable (recursive) higher order theory and the proof calculus (e.g., Gentzen's proof calculus), how this complexity function can change?

**SECOND EDIT**

As seen in the coments, the modified question has a complexity function that is essentially always **NP**-complete.

lengthis usually called thenumber of lines, whereas the length of a proof is defined as the total number of symbols.) $\endgroup$number of linesby the total number of symbols? Anyway, I thank you very much for pointing this, I am editing the question for appropriate terminology $\endgroup$