# Algorithmically determining proof complexity for Frege systems?

I apologize if this falls wildly short of research level - I am just learning the very basics of proof complexity and lack any real logic background.

Let $$F$$ be a Frege proof system (a finite complete sound set of axioms and inference rules in some finite complete language of logical connectives). Let $$\mu(\pi)$$ be some reasonable complexity measure of a proof $$\pi$$ in $$F$$ - for concreteness say the number of steps in $$\pi$$ (although we could also take the height of $$\pi$$, or the width of $$\pi$$, or the size of $$\pi$$,...). For a tautology $$A$$ in the underlying language of $$F$$, let $$\mu(A)$$ denote the minimum number of steps needed to prove $$A$$.

Can we determine $$\mu(A)$$ in exponential time? A priori this seems to depend on the details of $$F$$, but since Reckhow proved all Frege systems are polynomially related, I imagine this question does not depend on the details of $$F$$.

Here is a more embarrassing question that I do not know how to answer: Is determining $$\mu(A)$$ decidable? I very much imagine it is and you can just "list all possible proofs", but since arbitrary substitutions are allowed in the deductive steps, I am not sure how to make this precise. I suppose if instead we were measuring size instead of number of steps, then this works to give an algorithm.

• I don't know any complexity results, but I don't see why $\mu(A)$ should be computable in exponential time even for a weaker proof system like resolution. There are statements which require exponentially long resolution proofs, and there are probably roughly doubly exponentially many such proofs. Apr 4 at 4:05