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.

  • $\begingroup$ 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. $\endgroup$ Apr 4 at 4:05


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.