<p><a href="https://arxiv.org/abs/cs/0206022" rel="nofollow noreferrer">This paper</a> on universal search mentions (on pp. 6-7) that proof checking can be done in <span class="math-container">$O(n^2)$</span> where <span class="math-container">$n$</span> 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 <span class="math-container">$O(n)$</span> many slightly different variations on an <span class="math-container">$O(n)$</span> sized formula.</p>
<p>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 &quot;FOL + axioms&quot; proof verification.</p>
<p>More formally, let us fix an effectively computable FOL theory <span class="math-container">$T$</span> (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 &quot;baseline algorithm&quot; <span class="math-container">$B$</span>.</p>
<p>The input to the algorithm <span class="math-container">$A$</span> is consists of two parts: <span class="math-container">$(\phi, p)$</span> where <span class="math-container">$\phi$</span> and <span class="math-container">$p$</span> are bit strings of lengths <span class="math-container">$k$</span> and <span class="math-container">$n$</span> respectively (where <span class="math-container">$k\in O(n)$</span>), and <span class="math-container">$\phi$</span> encodes a formula in the language of <span class="math-container">$T$</span>. We will say that <span class="math-container">$A$</span> is a verifier for <span class="math-container">$T$</span> if <span class="math-container">$\phi$</span> is a theorem of <span class="math-container">$T$</span> if and only if there exists some <span class="math-container">$p$</span> such that <span class="math-container">$A$</span> accepts <span class="math-container">$(\phi,p)$</span>. What is the best lower bound on <span class="math-container">$A$</span>'s time complexity?</p>
<hr />
<p>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 <span class="math-container">$T$</span>, but it might reject all proofs that  are not of size at most <span class="math-container">$\sqrt n$</span> suffixed by <span class="math-container">$n-\sqrt n$</span> zeros; in this case it can appear to be linear time since the actual proof content is only <span class="math-container">$O(\sqrt n)$</span>. So we add a constraint that for every <span class="math-container">$B$</span>-proof <span class="math-container">$q$</span> of <span class="math-container">$\phi$</span> (that is, algorithm <span class="math-container">$B$</span> accepts <span class="math-container">$q$</span> as a proof in its own format), we can compute (in <span class="math-container">$o(n^2)$</span>) an <span class="math-container">$A$</span>-proof <span class="math-container">$f(q)$</span> of <span class="math-container">$\phi$</span> which is at most a constant factor longer than <span class="math-container">$q$</span>.</p>
<hr />
<p>Edit 2: For the sake of concreteness, I will specify algorithm <span class="math-container">$B$</span> 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.)</p>
<p>Each step either constructs a formula using a formula constructor like <span class="math-container">$\to$</span> or <span class="math-container">$\neg$</span> 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 <span class="math-container">$O(1)$</span>. Proofs that do not satisfy this property can be spuriously rejected, but proofs can be &quot;deduplicated&quot; in <span class="math-container">$O(n\log n)$</span> so this is not a severe restriction.</p>
<p>An example of a proof which takes <span class="math-container">$O(n^2)$</span> to check with this algorithm is (using PA as the FOL axiomatization):</p>
<ul>
<li>Let <span class="math-container">$A_n:=\forall x, S^n(x)\ne 0$</span></li>
<li>We prove <span class="math-container">$A_{n+1}$</span> from <span class="math-container">$A_n$</span> by instantiating <span class="math-container">$x$</span> to <span class="math-container">$S(x)$</span>, and <span class="math-container">$A_1$</span> is an axiom.</li>
</ul>
<p>Now there are <span class="math-container">$\Theta(n)$</span> many subformulas involved in all the <span class="math-container">$A_n$</span> put together, and <span class="math-container">$A_{n+1}$</span> is proved from <span class="math-container">$A_n$</span> using <span class="math-container">$\Theta(1)$</span> steps, so the entire proof is <span class="math-container">$\Theta(n)$</span> large (<span class="math-container">$\Theta(n\log n)$</span> if you include the size of the numbers in the backreferences, omitted in the word-RAM model). However, each time we substitute <span class="math-container">$S(x)$</span> for <span class="math-container">$x$</span> in <span class="math-container">$S^n(x)\ne 0$</span> we must traverse the stack of successors, which takes <span class="math-container">$\Theta(n)$</span> time, so the overall proof is <span class="math-container">$\Theta(n^2)$</span>.</p>

CC BY-SA 4.0
2021-09-18T09:36:24.770Z
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.
Emil Jeřábek
CC BY-SA 4.0
2021-09-18T16:07:31.563Z
@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:".)
Mario Carneiro
CC BY-SA 4.0
2021-09-19T10:34:33.180Z
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.
Emil Jeřábek
CC BY-SA 4.0
2021-09-19T10:52:44.647Z
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.
Emil Jeřábek
CC BY-SA 4.0
2021-09-19T21:37:33.827Z
@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. ...
Mario Carneiro
CC BY-SA 4.0
2021-09-19T21:43:04.933Z
... If you have a small set of distinguishing features you are looking for in the proof encoding or algorithm, please let me know, because I am interested in knowing not just the efficiency of my chosen format but whether there are more efficient alternative formats or algorithms. That is, I really would prefer not to use "algorithm B" at all and instead try to classify algorithms / proof formats that have short check time even after controlling for the differing proof lengths of different formats.
Mario Carneiro
CC BY-SA 4.0
2021-09-19T22:19:50.183Z
@EmilJeřábek I added a section that defines algorithm B some more. Regarding Extended Frege, assume that the baseline system is extended in this way, if it is beneficial to total check time. (I'm even contemplating throwing in ACA0 style second order variables since those also give a speedup, but I don't want to bog down the question with too much detail on such systems.) Hopefully this is enough to get a sense of where I'm going with this.
Mario Carneiro
CC BY-SA 4.0
2021-09-20T08:40:11.353Z
All right, now it is more clear.
Emil Jeřábek
<cc.complexity-theory><time-complexity><proof-complexity><proof-theory>
Asymptotic complexity lower bounds of proof checking
Mario Carneiro
# Asymptotic complexity lower bounds of proof checking

(Asked by: username_0 on 2021-09-18)

[This paper](https://arxiv.org/abs/cs/0206022) 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)$.

**Tags:** cc.complexity-theory, time-complexity, proof-complexity, proof-theory

> **Comments:**
> **username_1**: 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.  
> **username_0**: @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:".)  
> **username_1**: 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.  
> **username_1**: 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.  
> **username_0**: @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. ...  
> **username_0**: ... If you have a small set of distinguishing features you are looking for in the proof encoding or algorithm, please let me know, because I am interested in knowing not just the efficiency of my chosen format but whether there are more efficient alternative formats or algorithms. That is, I really would prefer not to use "algorithm B" at all and instead try to classify algorithms / proof formats that have short check time even after controlling for the differing proof lengths of different formats.  
> **username_0**: @EmilJeřábek I added a section that defines algorithm B some more. Regarding Extended Frege, assume that the baseline system is extended in this way, if it is beneficial to total check time. (I'm even contemplating throwing in ACA0 style second order variables since those also give a speedup, but I don't want to bog down the question with too much detail on such systems.) Hopefully this is enough to get a sense of where I'm going with this.  
> **username_1**: All right, now it is more clear.  

---

## 0 answers

