# Computational complexity of proof verification

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.