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.
