2
$\begingroup$

This paper on universal search mentions (on pp. 6-7) that proof checking can be done in $O(n^2)$ where $n$ is the length of the proof. Is this optimal? I don't want to specify the problem too precisely at the risk of excluding a useful interpretation, but for example if we take plain first order logic with some quickly computable set of axioms like ZFC, then checking time is dominated by substitution verification (which is linear time) for the linearly many proof steps, hence the quadratic bound, and I am fairly sure there are proof sequences that exercise this bound, where we substitute $O(n)$ many slightly different variations on an $O(n)$ sized formula.

But I don't know if I am baking in too many assumptions about how a proof system must work, and I would like a lower bound that considers arbitrary alternative proof encodings, as long as they can do something equivalent to "FOL + axioms" proof verification.

More formally, let us fix an effectively computable FOL theory $T$ (like ZFC), and a standard (effectively computable) encoding of formulas as bitstrings. Let's call the algorithm above, using a sequence of formulas and substitution, the "baseline algorithm" $B$.

The input to the algorithm $A$ is consists of two parts: $(\phi, p)$ where $\phi$ and $p$ are bit strings of lengths $k$ and $n$ respectively (where $k\in O(n)$), and $\phi$ encodes a formula in the language of $T$. We will say that $A$ is a verifier for $T$ if $\phi$ is a theorem of $T$ if and only if there exists some $p$ such that $A$ accepts $(\phi,p)$. What is the best lower bound on $A$'s time complexity?


Edit: In fact, we need more than this, because a proof verifier can get an artificial leg up by being too picky. If it rejects all proofs then it is not equivalent to $T$, but it might reject all proofs that are not of size at most $\sqrt n$ suffixed by $n-\sqrt n$ zeros; in this case it can appear to be linear time since the actual proof content is only $O(\sqrt n)$. So we add a constraint that for every $B$-proof $q$ of $\phi$ (that is, algorithm $B$ accepts $q$ as a proof in its own format), we can compute (in $o(n^2)$) an $A$-proof $f(q)$ of $\phi$ which is at most a constant factor longer than $q$.


Edit 2: For the sake of concreteness, I will specify algorithm $B$ a bit more. It is intended to be a standard proof algorithm but augmented with conservative techniques to make it not obviously suboptimal. (There are probably additional mechanisms I am missing.)

Each step either constructs a formula using a formula constructor like $\to$ or $\neg$ and formulas constructed in previous steps, or is an application of a primitive inference rule to theorems constructed in previous steps, or is an axiom. We assume that every formula is constructed at most once, and take advantage of this to make formula equality testing $O(1)$. Proofs that do not satisfy this property can be spuriously rejected, but proofs can be "deduplicated" in $O(n\log n)$ so this is not a severe restriction.

An example of a proof which takes $O(n^2)$ to check with this algorithm is (using PA as the FOL axiomatization):

  • Let $A_n:=\forall x, S^n(x)\ne 0$
  • We prove $A_{n+1}$ from $A_n$ by instantiating $x$ to $S(x)$, and $A_1$ is an axiom.

Now there are $\Theta(n)$ many subformulas involved in all the $A_n$ put together, and $A_{n+1}$ is proved from $A_n$ using $\Theta(1)$ steps, so the entire proof is $\Theta(n)$ large ($\Theta(n\log n)$ if you include the size of the numbers in the backreferences, omitted in the word-RAM model). However, each time we substitute $S(x)$ for $x$ in $S^n(x)\ne 0$ we must traverse the stack of successors, which takes $\Theta(n)$ time, so the overall proof is $\Theta(n^2)$.

$\endgroup$
8
  • 1
    $\begingroup$ I don’t understand where you got the quadratic bound from. If, as you say, substitution can be verified in linear time, this means that each step in the proof can be verified in time linear in the size of the formula involved in that step, and by summing up these, the whole proof can be verified in time linear in the size of the proof. $\endgroup$ Sep 18 at 9:36
  • $\begingroup$ @EmilJeřábek That assumes that the steps of the proof are all disjoint. Both in theory and practice, the steps are actually sharing lots of subterms from earlier parts, so it is possible to compactly represent many formulas, and $O(n)$ many steps might need to be checked against one or a few $O(n)$ formulas. (Part of what makes the analysis of this bound problematic is that less efficient proof formats get a lower asymptotic complexity, because the proofs are more sparse. A contrived version of that is mentioned in the "Edit:".) $\endgroup$ Sep 18 at 16:07
  • $\begingroup$ In practice maybe, but in theory, it is certainly standard in proof complexity that proofs are just plain old sequences of whatever objects the proof system operates with (formulas, sequents, polynomials, ...). Since you have something different, but quite specific, in mind, you should formulate in the question what exactly is the proof system you are interested in, and how exactly are the proofs represented. The answer will depend on all kinds of details. $\endgroup$ Sep 19 at 10:34
  • $\begingroup$ And let me add that this is not just a case of a "don't care" attitude towards a minor optimization to simplify the theory: it really essentially affects major open problems in the area. In particular, if you allow indiscriminate sharing of subformulas across the proof, then Frege = Extended Frege. $\endgroup$ Sep 19 at 10:52
  • $\begingroup$ @EmilJeřábek For a theorem like this, the complexity is very much dependent on the efficiency of the encoding. Ideally, I would like a theorem about the "most compact" proof encoding, but I also know that there are lots of ways for such an optimal format to degenerate, and I don't know any better way than to use "algorithm B" as a point of reference / sanity check on the encoding. ... $\endgroup$ Sep 19 at 21:37

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.