# Checking existence of proofs of fixed length

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).

• 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.

• In general, this is an undecidable problem, even if $n$ is a fixed constant. Jul 13 '20 at 14:33
• (Which is related to the fact that what you call length is usually called the number of lines, whereas the length of a proof is defined as the total number of symbols.) Jul 13 '20 at 14:40
• @EmilJeřábek and what if I change number of lines by the total number of symbols? Anyway, I thank you very much for pointing this, I am editing the question for appropriate terminology Jul 13 '20 at 15:17
• If $n$ is the number of symbols in the proof, and it is given as input in unary, then the problem is obviously in NP. In fact, it is NP-complete as long as the theory proves $\exists x\exists y\,(x\ne y)$. Jul 13 '20 at 15:49